
(* definition of syntax *)
(* there is no concrete syntax for closures, environments, or continuations *)

type variable = string

type valu =
    C of variable * exp * env (* closures *)
  | B of bool                 (* boolean constants *)
  | P of valu * valu          (* pairs of values *)
  | Continuation of context  (* something you can throw to *)

and exp = 
    S of variable         (* variables *)
  | L of variable * exp   (* lambdas -- which are not values! *)
  | V of valu             (* values -- see above *)
  | A of exp * exp        (* applications *)
  | MP of exp * exp       (* make-pair -- which is not a value *)
  | Fst of exp            (* get first field *)
  | Snd of exp            (* get second field *)
  | If of exp * exp * exp (* conditional *)
  | Letcc of variable * exp (* get current continuation *)
  | Throw of exp * exp      (* invoke a continuation *)

and env = (variable * valu) list

and context_elt = 

    (* work on left side of application, 
       exp is right side, to be evaluated later under env *)
    LeftApp  of exp * env 

    (* work on right side of application,
       valu is left side, which will be applied to result of right side *)
  | RightApp of valu 

    (* work on left side of pair-creation,
       exp is right side, to be evaluated later under env *)
  | LeftPr   of exp * env

    (* work on right side of pair-creation,
       valu is left side, which will also be part of the resulting pair value *)
  | RightPr  of valu

    (* work on subexpression of e.1, after which we project the first field *)
  | SFst

    (* work on subexpression of e.2, after which we project the first field *)
  | SSnd

    (* work on test of a conditional, after which we evaluate one of the
       two branches under env *)
  | SIf      of exp * exp * env

    (* work on left side of throw,,
       exp is right side, to be evaluated later under env *)
  | LeftThrow of exp * env

    (* work on right side of throw,
       valu is left side, which is the continuation that will be invoked *)
  | RightThrow of valu

and context = context_elt list (* shallow end of stack at beginning of list *)

(* not well-tested -- buyer beware
   also notice continuation contents are not printed  *)
let rec valu2string v =
  match v with
    C(s,e,env) -> 
     "<" ^ "(fun " ^ s ^ " . " ^ (exp2string e) ^ "), " ^ (env2string env) ^ ">"
  | B b -> if b then "true" else "false"
  | P(v1,v2) -> "(" ^ valu2string(v1) ^ " , " ^ valu2string(v2) ^ ")"
  | Continuation ctxt -> "<<Continutation>>"
and exp2string e =
  match e with
    S s -> s
  | L(s,e) -> "(fn " ^ s ^ " . " ^ (exp2string e) ^ ")"
  | V v -> valu2string v
  | A(e1,e2) -> (exp2string e1) ^ " " ^ (exp2string e2)
  | MP(e1,e2) -> "(" ^ (exp2string e1) ^ " , " ^ (exp2string e2) ^ ")"
  | Fst(e1) -> "((" ^ (exp2string e1) ^ ").1)"
  | Snd(e1) -> "((" ^ (exp2string e1) ^ ").2)"
  | If(e1,e2,e3) -> "(if "   ^ (exp2string e1) ^ 
                    " then " ^ (exp2string e2) ^ 
                    " else " ^ (exp2string e3) ^ ")"
  | Letcc(s,e) -> "(letcc " ^ s ^ " ." ^ (exp2string e) ^ ")"
  | Throw(e1,e2) -> "(throw " ^ (exp2string e1) ^ " , " ^ (exp2string e2) ^ ")"
and env2string env =
  let dopair (s,v) = "(" ^ s ^ "," ^ (valu2string v) ^ ")" in
  let rec loop env =
    match env with
      []  -> ""
    | hd::[] -> dopair hd
    | hd::tl -> (dopair hd) ^ " ; " ^ (loop tl) in
  "[" ^ (loop env) ^ "]"

