Re: Typol facilities

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

In article <16602@sophia.inria.fr>, kuehne@pi.informatik.th-darmstadt.de (Thomas Kuehne) writes:
|> 
|> First i would like to suggest a useful extension of the TYPOL typechecker.
|> There should be (maybe on&off switchable) WARNINGS for TYPOL variables
|> used only once in a TYPOL rule. If the single occurence was intentional
|> use of the anonymous variable is appropiate. In the case of a misspelled
|> variable name (that is the single ocurrence happened by accident) it would
|> be most helpful to get a hint from the typechecker. Currently one wonders
|> why things go wrong during execution, simply because some unification did not
|> take place that should have (If the variable name were spelled correctly).

This feature was implemented in an old version of Typol. I disconnected it
because I was tired of seeing a lot of irrelevant messages. I don't like
to use anonymous variables for this purpose: you can't examine these variables
and the are not very readable (I never saw a paper with inference rules
using anonymous variables).

I propose a mode that will highlight singleton variables and
constrained variables after type-checking.

|> Am i right to assume that, using TYPOL, there is no way walking up some tree,
|> without walking down before ?
|> Say i want to start at some leaf in a tree, working way up to the root, while
|> modifying the path from root to leaf.
|> The possibility i can think of is to start at the root, walking to all leafs
|> and returning new subtrees for each subtree in the tree.
|> The result of the calculation, which will be the old tree in most of the
|> subtrees, will replace the old tree.
|> Is there another more fitting solution for my aim?
|> If you want to reply on this matter please consider that if i have to
|> start at the root i do not want to use additional information to navigate
|> to the goal-leaf.

No, there is no way to go up in the tree. I think that you want to 
translate a tree. The translated tree is closed to the original one,
but sone leaves are modified. What is the problem with this point
of view ?

Thierry.

-- 
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 |
+---------------------------------------------------------------------------+