(******************************************************************** minimetaml.ml A M Pitts 2004-04-27 A semantics-based interpreter for a miniature, untyped MetaML. The main function is den_0. *********************************************************************) (******** Syntax *********) type t;; type var = (* value identifiers *) t name;; type exp = (* expressions *) Vid of var (* x *) | Fn of <>exp (* \x. e *) | Fun of <>(<>exp)(* fun f x = e *) | App of exp * exp (* e1 e2 *) | Run of exp (* run e *) | Bra of exp (* *) | Esc of exp (* ~e *) | Let of exp * (<>exp) (* let x = e1 in e2 *) | Num of int (* m *) | Ope of exp * string * exp (* e1 op e2 *) | Ifz of exp * exp * exp;; (* if e1 = 0 then e2 else e3 *) type stage (* stages *) = int;; exception Error of string;; (********** Semantics ***********) type sem0 = (* stage-0 denotations --- note how simple they are!! *) Fn0 of (sem0 -> sem0) (* extensional function *) | Bra0 of sem (* bracketed code *) | Num0 of int (* numeral *) and sem = (* stage-s denotations, for s>0 *) VidS of var (* variable *) | FnS of <>sem (* function abstraction *) | FunS of <>(<>sem) (* recursive function abstraction *) | AppS of sem * sem (* application *) | RunS of sem (* run *) | BraS of sem (* bracketed code *) | EscS of sem (* escaped code *) | LetS of sem * (<>sem) (* let code *) | NumS of int (* numeral *) | OpeS of sem * string * sem (* arithmetic operation on code *) | IfzS of sem * sem * sem (* conditional code *) | Reify of sem0;; (* reified stage-0 denotation *) type valu = (* valuations *) (var * sem0)list;; (************* Interpreter **************) (* The following "apply" functions are used in the reflection functions when it comes to reflecting values of the foem "Reify d" down a stage *) let rec apply_0(r : valu)(d : sem0) : sem0 = (* apply a valuation to a stage-0 denotation *) match d with Fn0 phi -> Fn0(function d -> apply_0 r (phi d)) | Bra0 u -> Bra0(apply 1 r u) | Num0 _ -> d and apply(s : stage)(r : valu)(v : sem) : sem = (* apply a valuation to a stage-s denotation, for s>0 *) match v with VidS x -> (try Reify(List.assoc x r) with Not_found -> v) | FnS(<>v1) -> FnS(<>(apply s r v1)) | FunS(<>(<>v1)) -> FunS(<>(<>(apply s r v1))) | AppS(v1, v2) -> AppS(apply s r v1, apply s r v2) | RunS v1 -> RunS(apply s r v1) | BraS v1 -> BraS(apply(s+1) r v1) | EscS v1 -> if s = 1 then raise (Error "apply") else EscS(apply(s-1) r v1) | LetS(v1, <>v2) -> LetS(apply s r v1, <>(apply s r v2)) | NumS _ -> v | OpeS(v1, op, v2) -> OpeS(apply s r v1, op, apply s r v2) | IfzS(v1, v2, v3) -> IfzS(apply s r v1, apply s r v2, apply s r v3) | Reify d -> Reify(apply_0 r d);; (* Now for the reflection functions... *) let rec reflect_0(r : valu)(v : sem) : sem0 = (* given a valuation, reflect a stage-1 denotation to stage-0 *) match v with VidS x -> (try List.assoc x r with Not_found -> raise(Error "reflect_0:0")) | FnS(<>v1) -> Fn0(function d -> reflect_0 ((x, d) :: r) v1) | FunS(<>(<>v1)) -> let rec phi(d : sem0) : sem0 = reflect_0 ((f, Fn0 phi) :: (x, d) :: r) v1 in Fn0 phi | AppS(v1, v2) -> (match reflect_0 r v1 with Fn0 phi -> phi(reflect_0 r v2) | Bra0 _ | Num0 _ -> raise (Error "reflect_0:1")) | RunS v1 -> (match reflect_0 r v1 with Fn0 _ | Num0 _ -> raise (Error "reflect_0:2") | Bra0 v1' -> reflect_0 [] v1') | BraS v1 -> Bra0(reflect 1 r v1) | EscS _ -> raise(Error "reflect_0:3") | LetS(v1, <>v2) -> let d = reflect_0 r v1 in reflect_0 ((x, d) :: r) v2 | NumS n -> Num0 n | OpeS(v1, op, v2) -> (match reflect_0 r v1 with Fn0 _ -> raise (Error "reflect_0:4") | Bra0 _ -> raise (Error "reflect_0:5") | Num0 m1 -> (match reflect_0 r v2 with Fn0 _ -> raise (Error "reflect_0:6") | Bra0 _ -> raise (Error "reflect_0:7") | Num0 m2 -> (match op with "+" -> Num0(m1 + m2) | "-" -> Num0(m1 - m2) | "*" -> Num0(m1 * m2) | _ -> raise(Error( "reflect_0: "^op^" not implemented"))))) | IfzS(v1, v2, v3) -> (match reflect_0 r v1 with Fn0 _ -> raise (Error "reflect_0:8") | Bra0 _ -> raise (Error "reflect_0:9") | Num0 m -> if m = 0 then reflect_0 r v2 else reflect_0 r v3) | Reify d -> apply_0 r d and reflect(s : stage)(r : valu)(v : sem) : sem = (* given a valuation, reflect a stage-(s+1) denotation to stage-s, for s>0 *) match v with VidS x -> (try Reify(List.assoc x r) with Not_found -> v) | FnS(<>v1) -> FnS(<>(reflect s r v1)) | FunS(<>(<>v1)) -> FunS(<>(<>(reflect s r v1))) | AppS(v1, v2) -> AppS(reflect s r v1, reflect s r v2) | RunS v1 -> RunS(reflect s r v1) | BraS v1 -> BraS(reflect(s+1) r v1) | EscS v1 -> if s = 1 then (match reflect_0 r v1 with Fn0 _ | Num0 _ -> raise (Error "reflect") | Bra0 v1' -> v1') else EscS(reflect(s - 1) r v1) | LetS(v1, <>v2) -> LetS(reflect s r v1, <>(reflect s r v2)) | NumS _ -> v | OpeS(v1, op, v2) -> OpeS(reflect s r v1, op, reflect s r v2) | IfzS(v1, v2, v3) -> IfzS(reflect s r v1, reflect s r v2, reflect s r v3) | Reify d -> Reify(apply_0 r d);; let rec trans(e : exp) : sem = (* translate a stage-s expression into a stage-(s+1) denotation *) match e with Vid x -> VidS x | Fn(<>e1) -> FnS(<>(trans e1)) | Fun(<>(<>e1)) -> FunS(<>(<>(trans e1))) | App(e1, e2) -> AppS(trans e1, trans e2) | Run e1 -> RunS(trans e1) | Bra e1 -> BraS(trans e1) | Esc e1 -> EscS(trans e1) | Let(e1, <>e2) -> LetS(trans e1, <>(trans e2)) | Num m -> NumS m | Ope(e1, op, e2) -> OpeS(trans e1, op, trans e2) | Ifz(e1, e2, e3) -> IfzS(trans e1, trans e2, trans e3);; let den_0(e : exp) : sem0 = (* the interpreter takes a (closed) stage-0 expression and computes its value in sem0 (if any) by first translating it to a stage-1 code and then reflecting that code to stage-0, using the empty valuation *) reflect_0 [] (trans e);; (********** Examples ***********) let (a: var), (f : var), (n : var), (p: var), (x : var), (y : var), (z : var) = fresh, fresh, fresh, fresh, fresh, fresh, fresh;; let e0 : exp = (* run((\x. )(\y. y + 4)) *) Run(App(Fn(<>(Bra(App(Vid x, Num 3)))), Fn(<>(Ope(Vid y, "+", Num 4)))));; let d0 : sem0 = (* should have value Num0 7 *) den_0 e0;; let e1 : exp = (* run(let z = <\a. ~((\x. )(\y. )) 0> in (run z) 42) *) Run(Let(Bra(Fn(<>(App(Esc(App(Fn(<>(Bra(Vid x))), Fn(<>(Bra(Vid a))))), Num 0)))), <>(App(Run(Vid z), Num 42))));; let d1 : sem0 = (* should have value Num0 42 *) den_0 e1;; let e2 : exp = (* let f = \x. <1 + ~x> in let a = <\y. ~(f )> in (run a) 9 *) Let(Fn(<>(Bra(Ope(Num 1, "+", Esc(Vid x))))), <>(Let(Bra(Fn(<>(Esc(App(Vid f, Bra(Vid y)))))), <>(App(Run(Vid a), Num 9)))));; let d2 : sem0 = (* should have value Num0 10 *) den_0 e2;; let e3 : exp = (* let f = (fun f x = \y. if x = 0 then <1> else <~y * ~(f(x -1)y)>) in let p = \a. <\z. ~(f a )> in (run(p 3)) 5 *) Let(Fun(<>(<>(Fn(<>(Ifz(Vid x, Bra(Num 1), Bra(Ope(Esc(Vid y), "*", Esc(App(App(Vid f, Ope(Vid x, "-", Num 1)), Vid y)))))))))), <>(Let(Fn(<>(Bra(Fn(<>(Esc(App(App(Vid f, Vid a), Bra(Vid z)))))))), <

>(App(Run(App(Vid p, Num 3)), Num 5)))));; let d3 : sem0 = (* should have value Num0 125 *) den_0 e3;; let e4 : exp = (* (run <\x. ~(run )>) 1 *) App(Run(Bra(Fn(<>(Esc(Run(Bra(Vid x))))))), Num 1);; (* evaluating this should raise an exception: den_0 e4;; *) let e5 : exp = (* (run <\a. ~((\x. ) a)>) 0 *) App(Run(Bra(Fn(<>(Esc(App(Fn(<>(Bra(Vid x))), Vid a)))))), Num 0);; (* evaluating this should raise an exception: den_0 e5;; *) let e6 : exp = (* fun f n = \x. if n = 0 then x else )> *) Fun(<>(<>(Fn(<>(Ifz(Vid n, Vid x, Bra(Let(Vid n, <>(Esc(App(App(Vid f, Ope(Vid n, "-", Num 1)), Bra(Ope(Vid y, "+", Esc(Vid x))))))))))))));; let d6 : sem0 = (* should have value Num0 6 *) den_0 (Run(App(App(e6, Num 3), Bra(Num 0))));; let diverge : exp = (* (\x. xx)(\x. xx) *) App(Fn(<>(App(Vid x, Vid x))), Fn(<>(App(Vid x, Vid x))));; let e7 : exp = (* (\a.)(\x.diverge) *) App(Fn(<>(Bra(Vid a))), Fn(<>diverge));; (* evaluation of this should not diverge... *) den_0 e7;; (* evaluation of this should not terminate... den_0 (App(Run e7, Num 0));; *) (* end of minimetaml.ml *)