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.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 image, the next step in evaluating let x = e; is to add the binding (x, image) to the environment, while the evaluation of var x = e; adds a binding (x, rx) to the environment and writes the value image to the reference rx. In this case, we assume that the location denoted by the reference rx is computed by an external mechanism responsible for memory allocation.

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)image

      This evaluation →Def 1 defines a relation between a state, a definition and a resulting state, or, in formal terms:

image

      Starting with a finite sequence of definitions d = [d1; . . . dn] and an initial state (Env0, Mem0), this relation produces the state (Envn, Memn):

image

      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:

image

      In the environment Env = [(x, 5), (y, ry)], we obtain = {y} and = {x}.

      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 image, is not an error result. In the case of an error, no state will be produced and the evaluation stops.

      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:

      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

      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.

Скачать книгу