(* An interpreter for MetaML, adapted from Andrew Pitt's FreshML code. *)

(* Integers. *)

type int =
  | Zero
  | Succ of int

(* Integer addition. *)

fun addition accepts x, y produces z =
  case x of
  | Zero ->
      y
  | Succ (x) ->
      addition (x, Succ (y))
  end

(* Expressions. *)

type exp = 
  | Vid of atom                                 (* x *)
  | Fn of < atom * inner exp >                  (* \x. e *)
  | Fun of < atom * atom * inner exp >          (* fun f x = e *)
  | App of exp * exp                            (* e1 e2 *)
  | Run of exp                                  (* run e *)
  | Bra of exp                                  (* <e> *)
  | Esc of exp                                  (* ~e *)
  | Let of < atom * outer exp * inner exp >     (* let x = e1 in e2 *)
  | Num of int                                  (* m *)
  | Add of exp * exp                            (* e1 + e2 *)       
  | Ifz of exp * exp * exp                      (* if e1 = 0 then e2 else e3 *)

(* Stage-0 denotations. *)

type sem0 =
  | Fn0 of phi: sem0_to_sem0                    (* extensional function *)
  | Bra0 of s: sem                              (* bracketed code *)
  | Num0 of int                                 (* numeral *)

(* Defunctionalized functions from [sem0] into itself. These were
   obtained systematically defunctionalizing the original code.  It is
   apparent, however, that this type really describes (recursive)
   lambda abstractions with explicit substitutions. *)

type sem0_to_sem0 =
  | SSApply0 of < r: valu * inner phi: sem0_to_sem0 >
  | SSReflect0 of < r: valu * x: atom * inner v1: sem >
  | SSRecReflect0 of < r: valu * f: atom * x: atom * inner v1: sem >

(* Stage-[s] denotations, for [s > 0]. *)

type sem =
  | VidS of atom                                (* variable *)
  | FnS of < atom * inner sem >                 (* function abstraction *)
  | FunS of < atom * atom * inner 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 < atom * outer sem * inner sem >    (* let code *)
  | NumS of int                                 (* numeral *)
  | AddS of sem * sem                           (* addition on code *)
  | IfzS of sem * sem * sem                     (* conditional code *)
  | Reify of d: sem0                            (* reified stage-0 denotation *)

(* Valuations. *)

type valu binds =
  | VNil
  | VCons of valu * atom * outer d: sem0

(* Meaning of the defunctionalized functions. *)

fun meaning accepts phi (* sem0_to_sem0 *), d (* sem0 *)
produces d (* sem0 *)
=
  case phi of
  | SSApply0 (r, phi) ->
      apply_0 (r, meaning (phi, d))
  | SSReflect0 (r, x, v1) ->
      reflect_0 (VCons (r, x, d), v1)
  | SSRecReflect0 (r, f, x, v1) ->
      reflect_0 (VCons (VCons (r, f, Fn0 (phi)), x, d), v1)
  end

(* Application of a valuation to a variable, which must be in the
   domain of the valuation. *)

fun lookup
accepts r (* valu *), x (* atom *)
produces d (* sem0 *)
  where free(d) <= outer(r)
=
  case r of
  | VNil ->
      fail (* runtime error *)
  | VCons (r, y, d) ->
      if x == y then d else lookup (r, x) end
  end

(* Application of a valuation to a reified variable. If the variable
   [x] is in the domain of the valuation, the result is the
   application of [Reify] to the image of [x], otherwise the result is
   the application of [VidS] to [x]. *)

fun lookup_and_reify
accepts r (* valu *), x (* atom *)
produces v (* sem *)
  where free(v) <= if free(x) <= bound(r) then outer(r) end U (free(x) \ bound(r))
=
  case r of
  | VNil ->
      VidS (x)
  | VCons (r, y, d) ->
      if x == y then Reify (d) else lookup_and_reify (r, x) end
  end

(* Application of a valuation to a stage-0 denotation. *)

fun apply_0 accepts r (* valu *), d (* sem0 *)
produces d' (* sem0 *)
  where free(d') <= outer(r) U (free(d) \ bound(r))
=
  case d of
  | Fn0 (phi) ->
      Fn0 (SSApply0 (r, phi))
  | Bra0 (u) ->
      Bra0 (apply (Succ (Zero), r, u))
  | Num0 (_) ->
      d
  end

(* Application of a valuation to a stage-[s] denotation. *)

fun apply accepts s (* stage *), r (* valu *), v (* sem *)
produces v' (* sem *)
  where free(v') <= outer(r) U (free(v) \ bound(r))
=
  case v of
  | VidS (x) ->
      lookup_and_reify (r, x)
  | FnS (x, v1) ->
      FnS(x, apply (s, r, v1))
  | FunS (f, x, v1) ->
      FunS(f, x, 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 (Succ (s), r, v1))
  | EscS (v1) -> 
      case s of
      | Succ (s) ->
          EscS (apply (s, r, v1))
      end
  | LetS (x1, v1, v2) ->
      LetS (x1, apply (s, r, v1), apply (s, r, v2))
  | NumS (_) ->
      v
  | AddS (v1, v2) -> 
      AddS (apply (s, r, v1), 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))
  end

(* Reflection of a stage-1 denotation to stage 0. *)

fun reflect_0
accepts r (* valu *), v (* sem *)
(* TEMPORARY the precondition should be: all level-0 variables within [v] are bound in [r],
             but there can be other variables in [v]. *)
produces d (* sem0 *)
  where free(d) <= outer(r) U (free(v) \ bound(r))
=
  case v of
  | VidS (x) ->
      (* This must be a level-0 variable, hence it must be bound in [r]. *)
      (* But we cannot express this, so [lookup] can fail. *)
      lookup (r, x)
  | FnS (x, v1) ->
      Fn0 (SSReflect0 (r, x, v1))
  | FunS (f, x, v1) ->
      Fn0 (SSRecReflect0 (r, f, x, v1))
  | AppS (v1, v2) ->
      case reflect_0 (r, v1) of
      | Fn0 (phi) ->
	  meaning (phi, reflect_0 (r, v2))
      end
  | RunS (v1) ->
      case reflect_0 (r, v1) of
      | Bra0 (v1') ->
	  reflect_0 (VNil, v1')
      end
  | BraS (v1) ->
      Bra0 (reflect (Succ (Zero), r, v1))
  | LetS(x, v1, v2) ->
      let d = reflect_0 (r, v1) in
      reflect_0 (VCons (r, x, d), v2)
  | NumS (n) ->
      Num0 (n)
  | AddS (v1, v2) ->
      case reflect_0 (r, v1), reflect_0 (r, v2) of
      | Num0 (m1), Num0 (m2) ->
	  Num0 (addition (m1, m2))
      end
  | IfzS (v1, v2, v3) ->
      let w where free(w) <= free(v) =
	case reflect_0 (r, v1) of
	| Num0 (Zero) -> 
	    v2
	| Num0 (_) ->
	    v3
        end
      in
      reflect_0 (r, w)
  | Reify (d) ->
      apply_0 (r, d)
  end

(* Reflection of a stage-[s+1] denotation to stage [s], for [s > 0]. *)

fun reflect
accepts s (* stage *), r (* valu *), v (* sem *)
produces w (* sem *)
  where free(w) <= outer(r) U (free(v) \ bound(r))
=
  case v of
  | VidS (x) -> 
      lookup_and_reify (r, x)
  | FnS (x, v1) ->
      FnS (x, reflect (s, r, v1))
  | FunS (f, x, v1) ->
      FunS (f, x, 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 (Succ (s), r, v1))
  | EscS (v1) ->
      case s of
      | Succ (Zero) ->
	  case reflect_0 (r, v1) of
	  | Bra0 (v1') ->
	      v1'
	  end
      | Succ (s) ->
	  EscS (reflect (s, r, v1))
      end
  | LetS (x, v1, v2) -> 
      LetS (x, reflect (s, r, v1), reflect (s, r, v2))
  | NumS (_) ->
      v
  | AddS (v1, v2) -> 
      AddS (reflect (s, r, v1), 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))
  end

(* Translation of a stage-[s] expression into a stage-[s+1] denotation. *)

fun translate accepts e (* exp *) produces v (* sem *) =
  case e of
  | Vid (x) ->
      VidS (x)
  | Fn (x, e1) ->
      FnS(x, translate (e1))
  | Fun (f, x, e1) ->
      FunS (f, x, translate (e1))
  | App (e1, e2) ->
      AppS (translate (e1), translate (e2))
  | Run (e1) ->
      RunS (translate (e1))
  | Bra (e1) ->
      BraS (translate (e1))
  | Esc (e1) ->
      EscS (translate (e1))
  | Let (x, e1, e2) ->
      LetS (x, translate (e1), translate (e2))
  | Num (m) ->
      NumS (m)
  | Add (e1, e2) ->
      AddS (translate (e1), translate (e2))
  | Ifz (e1, e2, e3) ->
      IfzS (translate (e1), translate (e2), translate (e3))
  end

(* The interpreter accepts a closed stage-0 expression and computes
   its value in [sem0] (if any) by first translating it to a closed
   stage-1 piece of code and then reflecting that code to stage 0. *)

fun interpret accepts e (* exp *)
  where free(e) == empty
produces d (* sem0 *)
=
  reflect_0 (VNil, translate (e))