The top portion of the file contains datatype definitions for
representing MinML programs. For reference I am also providing:
- an executable version of the static semantics in form of function typeOf, and
- an executable version of the substitution-based bigstep semantics, and
- an outline of a datatype definition for representing the frames of the C machine. Each kind of frame is represented by one of the variants of that datatype. The stack of the C machine is a frame list.
structure MinML = struct
(* 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
(* 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
(* recursive "lambda" terms: "fun f(x:argt):rest is body" *)
withtype function = { f: var, x: var, argt: typ, rest: typ, body: exp }
(* typing environments *)
type tyenv = typ env
(* determine the type of a closed expression
* (unlike last time where the type checker returned a type option,
* this time we use exceptions to indicate type errors) *)
fun typeOf e =
let fun typeError m = raise Fail ("type error: " ^ m)
fun tv (BVAL (NUM _), _) = INTt
| tv (BVAL (TRUE | FALSE), _) = BOOLt
| tv (FUN { f, x, argt, rest, body }, gamma) =
let val ft = FUNt (argt, rest)
val gamma' = bind (ft, f, bind (argt, x, gamma))
val rest' = te (body, gamma')
in if rest = rest' then ft
else typeError "body of function does not match its type"
end
and te (VAR x, gamma) = gamma x
| te (VAL v, gamma) = tv (v, gamma)
| te (PRIM (opr, e1, e2), gamma) =
(case (te (e1, gamma), te (e2, gamma)) of
(INTt, INTt) =>
(case opr of
(PLUS | TIMES | MINUS) => INTt
| (EQUAL | LESS) => BOOLt)
| _ => typeError "argument to prim op not int")
| te (IF (c, t, e), gamma) =
(case (te (c, gamma), te (t, gamma), te (e, gamma)) of
(BOOLt, tt, te) =>
if tt = te then tt
else typeError "branches of IF do not match"
| _ => typeError "condition in IF not bool")
| te (APPLY (e1, e2), gamma) =
(case (te (e1, gamma), te (e2, gamma)) of
(FUNt (t2', t), t2) =>
if t2 = t2' then t
else typeError "argument does not match \
\formal parameter type"
| _ => typeError "call of non-function")
in te (e, empty)
end
(* substitution: {v/y}e, v must be closed value *)
fun subst (v, y: var, e) =
let fun sv (v as BVAL _) = v
| sv (v as FUN { f, x, argt, rest, body }) =
if y = f orelse y = x then v
else FUN { f = f, x = x, argt = argt, rest = rest,
body = se body }
and se (e as VAR x) = if x = y then VAL v else e
| se (VAL v) = VAL (sv v)
| se (PRIM (opr, e1, e2)) = PRIM (opr, se e1, se e2)
| se (IF (e1, e2, e3)) = IF (se e1, se e2, se e3)
| se (APPLY (e1, e2)) = APPLY (se e1, se e2)
in se e
end
(* lift primop function so it works on values (as opposed to base values) *)
fun v'primop (opr, BVAL a, BVAL b) = BVAL (b'primop (opr, a, b))
| v'primop _ = raise Fail "primop: numeric argument expected"
(* substitution-based big-step semantics *)
fun bigstep'subst e =
let fun ev (VAR x) = raise Fail ("unbound variable: " ^ x)
| ev (VAL v) = v
| ev (PRIM (opr, e1, e2)) = v'primop (opr, ev e1, ev e2)
| ev (IF (e1, e2, e3)) =
(case ev e1 of
BVAL TRUE => ev e2
| BVAL FALSE => ev e3
| _ => raise Fail "if: boolean expected")
| ev (APPLY (e1, e2)) =
(case (ev e1, ev e2) of
(v1 as FUN { f, x, body, ... }, v2) =>
ev (subst (v1, f, subst (v2, x, body)))
| _ => raise Fail "function expected")
in ev e
end
Your task is to
- Fill in the remaining cases of the datatype for frames.
- Fill in the definition of function C'machine.
The C machine maps (closed) expressions to their corresponding values by looping through the appropriate sequence of C machine states. The states themselves are represented by calls of the functions "estate" and "vstate".
- A call of "estate(k,e)" represents the situation where
the current expression to be evaluated is e and the work to
be done later after e is finished is represented by k.
This corresponds to the state (k,e) as discussed in class
and in the Harper text book.
Hint: estate should dispatch on the possible shapes of e.
In each case it should make a "transition" in form of
a tail-call to either another instance of estate or
to an instance of vstate.
- A call of "vstate(v,k)" represents the situation where the current expression has been reduced to a value v which is about to be "passed up" to the next pending action represented by the topmost frame of k. This corresponds to the state (v,k) as discussed in class. Hints: What should happen if k is the empty stack? If k is not empty, vstate should dispatch on the possible shapes of the topmost frame of k and make a transition either to an estate (effectively resuming some pending work) or to another vstate.
A correct solution should not have redundant or non-exhaustive matches (i.e., it should precisely handle all the situations that can be expressed using the datatypes for expressions, values, and frames). First, fill your solution of the datatype for frames:
datatype frame =