Below you find our setup for MinML as we had it in homework sets 5 and 6, augmented with forms for creating and manipulating ML-style references.
structure MinML = struct
(* The following is an implementation of "memory" that you can
* (and should) use as part of your machine- and bigstep semantics.
* The part between "sig" and "end" specifies the interface.
* The data structure is pure, i.e., a memory does not have state
* in itself. A change of state must be modelled by switching from
* an old memory to a new memory. *)
structure Memory :> sig
exception NotInitialized
type location (* abstract type of locations *)
type 'a memory (* memory holding values of type 'a *)
val empty : 'a memory (* the empty memory *)
val fresh : 'a memory -> location * 'a memory
(* Each memory "knows" which locations
* are already allocated. The "fresh"
* operation produces a new location.
* It returns that location and the
* corresponding "new" memory.
* Notice that the contents of the location
* does not get initialized by this
* operation. *)
val lookup : 'a memory * location -> 'a
(* Look up a location. This can raise
* NotInitialized if the location was
* allocated (via "fresh") but never
* written to (via "update"). *)
val update : 'a memory * location * 'a -> 'a memory
(* Write to a memory location.
* There must be at least one such
* write operation before the location
* in question can be successfully read
* (via "lookup").
* The "update" operation returns the new
* memory where the modification has been
* recorded. *)
end = struct
exception NotInitialized
type location = int
type 'a memory = int * 'a IntRedBlackMap.map
val empty = (0, IntRedBlackMap.empty)
fun fresh (nextfree, m) = (nextfree, (nextfree+1, m))
fun lookup ((_, m), l) =
case IntRedBlackMap.find (m, l) of
SOME v => v
| NONE => raise NotInitialized
fun update ((nextfree, m), l, v) =
(nextfree, IntRedBlackMap.insert (m, l, v))
end
(* variables represented simply as strings *)
type var = string
(* in general, an environment is a mapping from variables to something *)
type 'a env = var -> 'a
(* extend e by binding variable x to v *)
fun bind (a, x: var, e) y = if x = y then a else e y
(* the empty environment simply complains *)
fun empty (x: var) = raise Fail ("unbound variable: " ^ x)
(* *** The MinML language *** *)
(* primitive operators: *)
datatype operator = PLUS | TIMES | MINUS | EQUAL | LESS
(* simple types *)
datatype typ =
INTt
| BOOLt
| FUNt of typ * typ
| REFt of typ
(* base values (values that are not functions) *)
datatype basevalue =
NUM of int
| TRUE
| FALSE
(* primitive operators operate on base values: *)
fun b'primop (PLUS, NUM i, NUM j) = NUM (i+j)
| b'primop (TIMES, NUM i, NUM j) = NUM (i*j)
| b'primop (MINUS, NUM i, NUM j) = NUM (i-j)
| b'primop (EQUAL, NUM i, NUM j) = if i = j then TRUE else FALSE
| b'primop (LESS, NUM i, NUM j) = if i < j then TRUE else FALSE
| b'primop _ = raise Fail "primop: numeric argument expected"
(* syntactic values: *)
datatype value =
BVAL of basevalue
| FUN of function
(* expressions: *)
and exp =
VAR of var
| VAL of value
| PRIM of operator * exp * exp
| IF of exp * exp * exp
| APPLY of exp * exp
| REF of exp (* ref e *)
| BANG of exp (* !e *)
| UPDATE of exp * exp (* e1 := e2 *)
(* recursive "lambda" terms: "fun f(x:argt):rest is body" *)
withtype function = { f: var, x: var, argt: typ, rest: typ, body: exp }
Your task is to fill in the definition of the E-machine semantics for this language.
First, add a new machine value:
datatype mvalue =
MBVAL of basevalue
| MCLOSURE of function * mvenv