Re: [Texmacs-dev] Syntax translation

[Henri Lesourd]

address@hidden wrote:

> Hi,
>
> I wanted to make a framework for syntax translation between texmacs  
> and PVS. Currently I have been able to successfully send commands to  
> PVS and receive the corresponding outputs from the same. These 
> outputs  are then received by texmacs via an input pipe and displayed  
> correspondingly. However due to difference in the syntax of these  
> commands I would first need to convert the texmacs commands to PVS  
> -compatible form before executing them in PVS and then the  
> correspoding ouputs will have to be converted back to texmacs. Please  
> tell me how I should go ahead making such a translation, as in a  
> translation table or some other type of translator. Also how I should  
> call and use such a translation table or module from a plug-in scheme  
> file.
If I were you, I would write the macro where I input my PVS
code in Scheme, this way you are completely free to write your
translation code, and build a filter as complex as you want.

The attached TeXmacs file shows how to do something like that.
Once you  understood and reused it for your purpose, you should
create a new TeXmacs plugin (as explained in, e.g.:
http://www.ags.uni-sb.de/~henri/texmacs/aTeXmacsTutorial.pdf)

, and cut & paste the code of (test-input) inside your plugin.


-------
Another possible source of inspiration for you is to look at
the webpage for the Mizar plugin, at:
http://www.ags.uni-sb.de/~cebrown/mizar-texmacs/mizar-texmacs-tutorial.html

, the source code is available at:
http://www.ags.uni-sb.de/~cebrown/mizar-texmacs/mizar-texmacs-plugin.tar.gz

This plugin is fully functionnal, and it is probably the closest to
what you want to do.


> I saw one such TeXmacs file 
> /TeXmacs/progs/utils/plugins/plugin-convert.scm
> which seemed to carry out some kind of translation. The commands will  
> be in math mode when sent to PVS for building a theory or doing  
> proofs. My \spec command in texmacs is used to write these  
> specifications.
The problem with this way of writing plugins is that it is
very low-level (you need to stick to a pipe which exchanges
characters), and it is difficult to control what kind of translation
it does (i.e. : a certain number of predefined things are available,
but if what you need is different, you are stuck).

On the other hand, most of the TeXmacs plugins are
currently written this way.  The documentation about
that can be found under the menu:
Help->Interfacing


Best, Henri