The environment

We may think of an environment as a hypothesis in a proposition: ``Given a certain environment, evaluate an expression.'' In sequents, hypotheses appear to the left of the turnstyle. Since the result of the evaluation of a premise may alter the environment, we return the modified environment as well as the result of the evaluation. Here is the modified Exp judgement:

ENV Exp : INTEGER, ENV

Note that since we have changed the judgement, we must modify the syntax of all previously defined rules, adding the initial and final environments.

The phylum ENV stands for the environment. Our environment is a list of pairs of the form variable,value. Since the environment is manipulated by a Typol program, it should be implemented as an abstract syntax tree. We may either implement the environment tree in a distinct formalism specification, dedicated to this task, or augment the Exp language to add operators for the environment. For the sake of simplicity, we prefer to modify the Exp abstract syntax as follows:


   env -> PAIR * ... ;
   pair -> VAR INTEGER ;
 
   ENV  ::= env ;
   PAIR ::= pair ;

We do not add concrete syntax rules for these operators since we don't intend to parse the environment. Where do environment trees come from?

Typol: Typol patterns will be used to build the environment during evaluation. These patterns will be coerced into Vtp trees automatically when sent to Le-Lisp.
Le-Lisp: We may either construct Vtp trees by hand, (using low level Vtp primitives) or through a graphical interface. We may use generic cut and paste operations to build an environment tree with no modifications of the Metal program. However, in order to use the guided editing mode or in-line edition, Centaur must be able to send integers and variables to an Exp parser. We must therefore add the following entry point to the Metal definition to parse integers:
```
   <axiom> ::= "[INTEGER]" <int> ;
         <int>
```
This line may accompany the previous entry point definitions in the specification.

Please add the above lines to contrib/Exp/syntax/Exp.metal, recompile it, regenerate the parser, then reset the syntax from the main Centaur menu.

Tutorial