Concepts and Semantics of Programming Languages 1. Therese Hardin
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 = exp OCaml type ’a defl = Let_def1 of ’a * ’a expl | Var_def1 of ’a * ’a expl
We choose to construct a value corresponding to a reference using a constructor applied to an identifier.
Python class Ref_Var1: def __init__(self,idvar): self.idvar = idvarOCaml type ’a refer = Ref_Var1 of ’a
Hence, rx will be represented by Ref_Var1(”x”). As the relation →Def1 defines a function, it can be implemented directly as follows:
Python def trans_def1(st,d): (env,mem) = st if isinstance(d,Let_def1): v = eval_exp1(env,mem,d.exp) if isinstance(v,VCste1): return (ajout_liaison_env(env,d.var,v.cste),mem) raise ValueError if isinstance(d,Var_def1): v = eval_exp1(env,mem,d.exp) if isinstance(v,VCste1): r = Ref_Var1(d.var) return (ajout_liaison_env(env,d.var,CRef1(r)), write_mem(mem,r,v.cste)) raise ValueError raise ValueErrorOCaml let trans_def1 (env, mem) d = match d with | Let_def1 (x, e) -> (match eval_exp1 env mem e with | VCste1 v -> ((ajout_liaison_env env x v), mem) | Erreur1 -> failwith “Erreur”) | Var_def1 (x, e) -> (match eval_exp1 env mem e with | VCste1 v -> ((ajout_liaison_env env x (CRef1 (Ref_Var1 x))), (write_mem mem (Ref_Var1 x) v)) | Erreur1 -> failwith “Erreur”) val trans_def1 : (’a * ’a refer const1) list * (’a refer * ’a refer const1) list -> ’a def1 -> (’a * ’a refer const1) list * (’a refer * ’a refer const1) list
By iterating this function, we obtain an implementation of
Python def trans_def1_exec(st,ld): (env,mem) = st if len(ld) == 0: return (env,mem) else: return trans_def1_exec(trans_def1((env,mem),ld[0]),ld[1:])OCaml let trans_def1_exec (env, mem) ld = (List.fold_left trans_def1 (env, mem) ld) val trans_def1_exec : (’a * ’a refer const1) list * (’a refer * ’a refer const1) list -> ’a def1 list -> (’a * ’a refer const1) list * (’a refer * ’a refer const1) list
Now, considering example 2.3, we obtain:
Python ex_ld0 = [Var_def1(“y”,Cste1(2)), Let_def1(“x”,Plus1(Bang1(“y”),Cste1(3)))] (ex_e0,ex_m0) = trans_def1_exec(([],[]),ex_ld0) >>> eval_exp1(ex_e0,ex_m0,Var1(“x”)).cste.cst_int 5 >>> eval_exp1(ex_e0,ex_m0,Bang1(“y”)).cste.cst_int 2OCaml let ex_ld0 = [ Var_def1 (“y”, Cste1 2); Let_def1 (“x”, Plus1 (Bang1 “y”, Cste1 3)) ] val ex_ld0 : string def1 list # (trans_def1_exec ([], []) ex_ld0) ;; - : (string * string refer const1) list * (string refer * string refer const1) list = ([(“x”, CInt1 5); (“y”, CRef1 (Ref_Var1 “y”))], [(Ref_Var1 “y”, CInt1 2)])
2.3.2. Assignment
The language Lang1 extends Def 1 by adding assignment.