Re: Errors&Wishes

[td@babar.inria.fr (Thierry Despeyroux)]

In article <16343@sophia.inria.fr>, kuehne@pi.informatik.th-darmstadt.de (Thomas Kuehne) writes:
|> First a hint for all who use annotations and did not find a way
|> to get rid of the error:
|> 
|> ** toplevel : undefined escape : (not_found ...)
|> 
|> without loading some file by hand into the Lisp environment.
|> 
|> In my LANGUAGE.env file i use loadfile to load the file 
|> containing the new_decor function:
|> 
|> (de {SLOTOS}:new_decor (name)
|>     (lock (lambda (tag val)
|>               (cond
|>                   ((eq tag 'not_found)
|>                       ({tree}:new_decor
|>                           name 'tree ({name}:formalism 'SLOTOS)))
|>                   (tag (exit tag val))
|>                   (t val)))
|>         ({name}:decor name 'tree ({name}:formalism 'SLOTOS)))
|> )
|> 
|> If one places the call to that function simply in the LANGUAGE.env
|> files one will get the error message.
|> I put it into the {LANGUAGE}:set-environment function which is called
|> when loading a LANGUAGE file into a ctedit, that contained something
|> different before.

Annotations are not part of the formalisms. In particular it is impossible 
to declare annotations in a METAL file. This is because annotations are 
designed as dynamic extensions to abstract syntaxes. The problem is then 
that you mau declare annotations only when the annotated formalism exists.
This is always the case with your function {SLOTOS}:new_decor, because
{name}:formalism loads the formalism. So I do not understand why you have to
call your function in the set-environment function. The only problem I can
imagine is that you did redefine your formalism after loading then .env file.
In thos case the annotaions must also be redefined.

|> Errors and wishes for:
|> 
|> METAL
|> 
|> It would be nice if it were possible to 'USE' other languages
|> like in TYPOL. This would allow more precise mixing of languages
|> than is possible with 'implemented as TREE'.
|> 
|> It is too bad that the METAL ctedit does not offer a pop-up menu
|> to select one of its functions.

Where are persuaded that a modular definition od abstract syntaxes is
necessary. While we have looked into this topic, we can't promise you that
we will have the man power to implement modular abstract syntaxes definitions
soon.

|> TYPOL
|> 
|> Choosing 'Write Code' results in writing an empty .pg file
|> if one did not 'Type-Check'ed and 'Compile'ed before.
|> Instead of this it should initiate 'Type Check' and 'Compile'
|> (maybe in the last mode (Normal, Concurrent, Debug) used) one
|> after another. This would allow 'one button' recompilation.

In the next version of Centaur there wil be two new buttons: "Reload Code"
and "Restore". I hope this will be useful. If you want  a one button
recompilation, you may use the function {TYPOL}:compile-file
(and {TYPOL}:compile-file-and-reload in the next version). A more automatic
mode would be useful  but must include some coherence check (an internal
"make" inside Centaur).

|> TYPOL DEBBUGER
|> 
|> Very often it does not suffices to 'Delete' a module with the
|> TYPOL DEBUGGER menu. Without an additional prolog:restore the
|> old version will be used.

This is true. Delete  only deletes the module in the semantics window,
and not in the prolog state. The new reload button will do both.

|> My Breakpoints do not work. TYPOL execution becomes inacceptably
|> slow but will not stop at the specified points!?

Yes a patch as been distributed to cure this problem.

|> Sometimes it is confusing the way proofing subgoals is presented.
|> For example the rule:
|> 
|> A &
|> B
|> ---
|> C
|> 
|> When A has been proofed the DEBUGGER !jumps! to 'TRY' proofing B.
|> If one has several subgoals to proof and did not name all the rules
|> one easily loose the context of the current rule.
|> A (probably not realizable) solution might be to step back to the
|> 'parent rule' when a subgoal has been prooven and highlight the
|> next subgoal to be proofed. After a 'STEP' or 'PROOVE' execution
|> continues at the next subgoal. This also would allow to skip
|> some subgoals and some others not.

It should be possible to show the parent as well as the current rule. 
Do you think this must be done? I think this is not a lot of work.
But are you sure that after that you will not ask for the grand-father,
and then ask for the complete proof tree ? (:-))

|> In order to 'send' and 'get' annotations to treenodes i used the
|> subject as the path for the annotation. I had to use the
|> withsubject construct to avoid loosing the subject for this purpose.
|> I could get rid of it it were possible to identify 'this_rule' or
|> 'this_abstract_syntax_tree_node'. This would serve as a path to
|> 'getannot' or 'sendannot' and one would not have to bother with
|> keeping the subject.

Could you explain a bit more what you would like, the context in which you
hope to use it. Do you want to annotate rewritten tree?

I think that one must be careful with the use of annotations in Typol.
"getannot" may be seen as a way of using an extended abstract syntax of 
a formalism. "sendannot" is a way of saving some results of the proof tree
when the proof tree is isomorphic to the subject tree. But using both
"sendannot" and "getannot" (on the same annoatation) within the same execution
of a Typol program is completely non logical.

|> CTEDIT
|> 
|> The scrolling of a ctedit in entities of pixel is not very useful.
|> The scroll bar should adapt in size corresponing to the percentage of
|> text shown in the window relative to the whole text.
|> 
|> One very convienent feature will be a 'ReRead' Button to allow loading
|> the same file again into the ctedit. (I use xemacs as a editor and
|> changes made in xemacs must be forwarded to the ctedit. For often
|> used file pathes i cut them first and paste them into the 'Read file' box
|> but ReReading would be easier)
|> 
|> With a certain PPML definition i was presented the message:
|> 
|> *** funcall undefined function #:box:normal

|> CENTAUR
|> 
|> It should be possible to specify whether a #:prolog:send
|> or a #:prolog:quietsend is generated in the LANGUAGE.ll 
|> file by the export clause in a TYPOL program.
|> 
|> Sometimes i wish the files i produced were seperated from
|> the files generated by centaur. In other words centaur
|> should use a directory located at the position of my files
|> to put in all the files it needs.

This will be possible using resources in the next version of Centaur (1.2)
for PPML. However, it has not yet been implemented for Typol.

|> It would be nicer to have several semantics directories located
|> at the position of the syntax definition for the specific 
|> language. Currently one has to use one large semantics
|> directory for all languages that relate to eachother
|> in order to use the import mechanism.

I know this problem, but what you said is not completely true.
You can import rules from a Typol program that is in another semantics
directory. So only Typl programs that relate to one language must be in the same
directory. (In fact they may be in the semantics directory of any
declared langage...)

I would like to hear the users point of view. Would you prefer a path
to search for semantics definitions, or a resource that tells you
what file is used for a given program ?

|> DREAMS:
|> 
|> TYPOL Project Manager, recompiles files that changed and all
|>                        files that depend on changed files.

Laurent Thery suggested a Centaur Project manager. But I am not sure
that we are ready for this.

|> Electronic Retrieval System for Centaur, like man for UNIX.
|> Will allow faster (interactive) access than the conventional (big) manual.
|> 
|> Faster Garbarge Collection, everything but collecting the garbarge runs
|> at acceptable speed.
|> 
|> 
|> 	- Thomas -

-- 
Send contributions to centaur@sophia.inria.fr. Registration and
administrative matters should be sent to centaur-request@sophia.inria.fr.
+---------------------------------------------------------------------------+
|     Thierry Despeyroux      | email: Thierry.Despeyroux@sophia.inria.fr   |
| I.N.R.I.A. Sophia-Antipolis | phone: +33 93 65 77 07 fax: +33 93 65 77 66 |
+---------------------------------------------------------------------------+