To underline the fact that the semantics concerning the environment differ from those of pure arithmetic, we will describe them in distinct Typol sets. A set is a named collection of declarations and inference rules. A program such as eval_exp is just a special kind of set. Sequents used within a set refer to other rules within the set unless preceded by the name of a different set. Rules in one set may be used in another, which allows you to define the semantics of a language in a modular fashion.
A set may have declarations, including judgements. Since unnamed sequents refer to other rules in a set, they observe local judgements, allowing you to overload judgement forms in different sets.
For environment semantics, we create two sets, one to retrieve the value of a variable in the environment and one to update the value of a variable. Following the semantic specifications for variables enumerated above, we have the following set definitions:
set GETVALUE is
judgement ENV |- VAR : INTEGER, ENV ;
env[] |- variable V :
integer 0, env[pair(variable V, integer 0)] ;
env[pair(variable V, I) . env]
|- variable V : I, env[pair(variable V, I) . env] ;
env |- variable V : n, env'
----------------------------
env[pair(variable V', I) . env]
|- variable V :
n, env[pair(variable V', I) . env'] ;
provided diff(V, V') ;
end GETVALUE ;
The first rule indicates that if we search for a variable in an empty environment, we create the variable with an initial value of 0. The value 0 and new environment are returned.
When the variable in the subject of the second rules matches the first variable in the context (the head of the list), the variable's value is returned along with the unchanged environment.
Otherwise, if the current variable is not at the head of the environment, the third rule recursively examines the rest of the environment and returns the recursively calculated value and environment. The premise (recursive call) is evaluated with only the tail end of the initial environment, named env.
Note the use of the Typol provided clause in the third rule. The provided part of a rule contains a list of conditions that must be met before a rule can be applied. In general, the expression: provided premises
premises stands for a list of sequents separated by ampersands (&). The provided part of the third rule ensures that it will only be applied when the variable name of the subject differs from that at the head of the environment.
N.B. We must add the function diff to our prolog file expfunc.sp. This function is defined as expfunc$diff(A, B) :- A ~= B. We must also import it in the Typol program.
In order to modify a variable's value in the environment, we define the UPDATE set.
set UPDATE is
judgement ENV |- VAR, INTEGER : ENV ;
env[] |- variable V, integer N :
env[pair(variable V, integer N)] ;
env[pair(variable V, _) . env]
|- variable V, I : env[pair(variable V, I) . env] ;
env |- variable V, n : env'
-------------
env[pair(variable V', I) . env]
|- variable V, n : env[pair(variable V', I) . env'] ;
provided diff(V, V') ;
end UPDATE ;
The first rule adds a variable and the assigned value to an empty environment. The second rule means that if the first variable in the environment is the current variable, then the value of this variable is updated, whatever the old value (note use of underscore). In this case, the environment is otherwise unmodified. The last rule recursively searches the rest of the environment to find the current variable.
Having defined these two sets, we may complete the initial definition of eval_exp by adding the following rules for the variable and assign operators. Note the use of named sequents to explicitly refer to imported judgements.
env |- EXP : v, env' & UPDATE(env' |- variable V, v : env'') ---------------- env |- assign(variable V, EXP) : v, env'' ; GETVALUE(env |- variable V : v, env') ---------------- env |- variable V : v, env' ;
The first rule may be read:
To evaluate the operator assign, evaluate the expression in the current environment, update the variable with this value, and return the value and modified environment.
while the second means:
To evaluate the variable V, find and return its value in the current environment and return the (possibly) modified environment.