Messages in Exp

Since the Exp interpreter is so small, there are not many places in the program where errors may occur. However, we would like to issue a warning message whenever a variable is added to the environment. Variables are added to the environment in the GETVALUE and UPDATE sets.

The message module file contrib/Exp/messages/interpreter.rdb was created when we generated the Exp hierarchy. The first thing we do is add a message specification to this file:

Centaur.Exp.MessageModules.interpreter.variable-added.Text: \resbs
The variable \{var\} has been added to the environment.

This line specifies that for the Exp formalism, the message module interpreter contains the message variable-added. The message text contains one argument (indicated by {var}) which will be instantiated to the name of the variable added to the environment.

We modify the first axiom of the GETVALUE set to post a message when the variable is added to the environment:

env[] |- variable V : 
         integer 0, env[pair(variable V, integer 0)] ;
   do message("Exp", "interpreter", "variable-added", 
              "Warning", nil(), "",
             messarg(tree(variable V), ref(subject), 
                     info "private")) ;

The value provided for the argument is the subtree variable V. The location of this Exp variable in the source is given by the subject of the axiom. We specify that the argument is private so that the location is not selected in the source until we click in the message display.

We use Typol's do construct to post the message. Any time the Typol motor proves a rule or axiom followed by a do clause, the do clause is executed.

We must similarly modify the first axiom of the UPDATE set:

env[] |- variable V, integer N : 
         env[pair(variable V, integer N)] ;           
    do message("Exp", "interpreter", "variable-added", 
               "Warning", nil(), "",
              messarg(tree(variable V), ref(subject), 
                      info "private")) ;

N.B. The PSP formalism defines a phylum named VAR, as does Exp. Using this formalism introduces an ambiguity into the GETVALUE and SETVALUE judgements, which refer to VAR. We must indicate that the VAR that interests us is the one from Exp, otherwise the Typol type checker will signal the error. The judgments thus become:

   judgement ENV |- Exp::VAR : INTEGER, ENV;