[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Texmacs-dev] Syntax translation
From: |
Henri Lesourd |
Subject: |
Re: [Texmacs-dev] Syntax translation |
Date: |
Thu, 28 Jun 2007 14:47:00 +0200 |
User-agent: |
Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.4) Gecko/20030821 |
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