The value of an integer constant is the integer that it represents. The value of an identifier is that which is bound to it in the environment, or Err. The value of an expression constructed with an addition symbol and two expressions e1 and e2 is obtained by adding the relative integers resulting from the evaluations of e1 and e2; the result will be Err if e1 or e2 is not an integer. The value of !x is the value stored at the reference Env(x) when x is a mutable variable, and Err otherwise.
Thus, if e is evaluated as a reference, then e can only be an identifier. Furthermore, certain expressions in Exp1 are syntactically correct, but meaningless: for example, the expression !x when x is not a mutable variable, i.e. when x does not bind a reference in the environment, or x1 + x2 when x1 (or x2) is a mutable variable. On the other hand, !x + y is a meaningful expression that denotes a value when y binds an integer and x binds a reference to an integer.
EXAMPLE 2.2.– Let us evaluate the expression !x + y
in the state
The evaluation function
Python def eval_exp1(env,mem,e): if isinstance(e,Cste1): return VCste1(CInt1(e.cste)) if isinstance(e,Var1): x = valeur_de(env,e.symb) if isinstance(x,CInt1) or isinstance(x,CRef1): return VCste1(x) return Erreur1() if isinstance(e,Plus1): ev1 = eval_exp1(env,mem,e.exp1) if isinstance(ev1,Erreur1): return Erreur1() v1 = ev1.cste ev2 = eval_exp1(env,mem,e.exp2) if isinstance(ev2,Erreur1): return Erreur1() v2 = ev2.cste if isinstance(v1,CInt1) and isinstance(v2,CInt1): return VCste1(CInt1(v1.cst_int + v2.cst_int)) return Erreur1() if isinstance(e,Bang1): x = valeur_de(env,e.symb) if isinstance(x,CRef1): y = valeur_ref(mem,x.cst_adr) if y is None: return Erreur1() return VCste1(y) return Erreur1() raise ValueErrorOCaml let rec eval_exp1 env mem e = match e with | Cste1 n -> VCste1 (CInt1 n) | Var1 x -> (match valeur_de env x with Some v -> VCste1 v | _ -> Erreur1) | Plus1 (e1, e2) -> ( match ((eval_exp1 env mem e1), (eval_exp1 env mem e2)) with | (VCste1 (CInt1 n1), VCste1 (CInt1 n2)) -> VCste1 (CInt1 (n1 + n2)) | _ -> Erreur1) | Bang1 x -> (match valeur_de env x with | Some (CRef1 a) -> (match valeur_ref mem a with Some v -> VCste1 v | _ -> Erreur1) | _ -> Erreur1) val eval_exp1 : (’a * ’b const1) list -> (’b * ’b const1) list -> ’a exp1 -> ’b valeurs1
Considering example 2.2, we obtain:
Python ex_env1 = [(“x”,CRef1(“rx”)),(“y”,CInt1(2))] ex_mem1 = [(“rx”,CInt1(3))] >>> (eval_exp1(ex_env1,ex_mem1,ex_exp1)).cste.cst_int 5OCaml let ex_env1 = [ (“x”, CRefl (“rx”)); (“y”, CIntl (2)) ] val ex_env1 : (string * string constl) list let ex_mem1 = [ (“rx”, CIntl (3)) ] val ex_mem1 : (string * ‘a constl) list # (eval_exp1 ex_env1 ex_mem1 ex_exp1) ;; - : string valeursl = VCstel (CIntl 5)
2.3. Definition and assignment
2.3.1. Defining an identifier
The language Def 1 extends Exp1 by adding definitions of identifiers. There are two constructs that make it possible to introduce an identifier naming a mutable or non-mutable variable (as defined in section 2.1.3). Note that, in both cases, the initial value must be provided. This value corresponds to a constant or to the result of a computation specified by an expression e ∈ Exp1. These constructs modify the current state of the system; after computing
Table 2.3. Language Def 1 of definitions
| d ::= let x = e; | Definition of a non-mutable variable | (x ∈ X, e ∈ Exp1) |
| | var x = e; | Definition of a mutable variable | (x ∈ X, e ∈ Exp1) |
The evaluation of a definition is expressed as follows:
(2.1)
This evaluation →Def 1 defines a relation between a state, a definition and a resulting state, or, in formal terms:
Starting with a finite sequence of definitions d = [d1; . . . dn] and an initial state (Env0, Mem0), this relation produces the state (Envn, Memn):
This sequence of transitions may, more simply, be noted
EXAMPLE 2.3.– Starting with a memory with no accessible references and an “empty” environment, the sequence [var y = 2; let x = !y + 3;] builds the following state:
In the environment Env = [(x, 5), (y, ry)], we obtain
NOTE.– In the definition of the two transitions in [2.1], we presume that the result of the evaluation of the expression e, denoted as
The abstract syntax of language Def 1 may be defined as follows:
Python class Let_def1: def __init__(self,var,exp): self.var = var self.exp = exp class Var_def1: def __init__(self,var,exp): self.var = var self.exp
