(* The source language. The source language is the λ-calculus, extended with
     literals (as observables).      A program is a closed term. *)

module Source = struct
    type ide = string
    type term = LIT of int
              | VAR of ide
              | LAM of ide * term
              | APP of term * term
    type program = term
end

open Source;;   (*  :-)  *)

(* The (polymorphic) environment. We make use of a structure Env
     satisfying the following signature:  *)

module type ENV = sig
    type 'a env
    val empty : 'a env
    val extend : ide * 'a * 'a env -> 'a env

    (* val lookup : ide * 'a env -> 'a option *)
    val lookup : ide * 'a env -> 'a
    val epr : 'a env * ('a -> string) -> string
    val epr1 : 'a env -> string
end ;;

let id_fail idq =
        let fws = Printf.sprintf "identifier %s not found" idq
        in failwith fws;

module EnvX = struct
    type 'a item = ide * 'a
    type 'a env = 'a item list
    let empty = []
    let extend ((id : ide), (v : 'a), (penv : 'a env))
              = ( id, v ) :: penv

    let rec epr ((penv : 'a env ), (v_mres : 'a -> string) ) =
        match penv with
          (( id, v ) :: rest)  -> " " ^ id ^ " =" ^ (v_mres v) ^ "\n        " ^ (epr (rest, v_mres))
          | []                 -> ""

    and epr1 (penv : 'a env ) =
        match penv with
          (( id, v ) :: rest)  -> " " ^ id ^ " = (unknown)\n        " ^ (epr1 rest)
          | []                 -> ""

    and lookup ((idq : ide), (penv : 'a env )) =
      begin
        (* print_string( "Lookup!  id " ^ idq ^ " in:\n" ); *)
        (* print_newline(); *)
        (* print_string( epr1 penv ); *)
        (* print_newline(); *)
        match penv with
          (( id, v ) :: rest)  ->
                     begin
                       (* print_string( "  (in Lookup:  is idq " ^ idq ^ " == " ^ id ^ "?\n" ); *)
                       if idq = id then v
                                    else  lookup (idq, rest)
                     end
        | []                   ->  id_fail idq
      end
end;;

module Env = ( EnvX : ENV ) ;;

(*
    The empty environment is denoted by Env.empty.
    The function extending an environment with a new binding
    is denoted by Env.extend. The function fetching the value
    of an identifier from an environment is denoted by Env.lookup.
*)


(****  Expressible and denotable values.  ****)

type value = INT of int
           | SUCC
           | CLOSURE of value Env.env * ide * term

let e_init = Env.extend ("succ", SUCC, Env.empty)


(* 2.1 *)
type directive = TERM of term | APPLY


(* My (DL) shortcut names *)
type stackT = value list
type envReg = value Env.env

type ctlL = directive list
type triple = (value list * value Env.env * ctlL )
type dumpReg = triple list

 (* where S = value list *)
 (* E = value Env.env *)
 (* C = directive list *)
 (* D = (S * E * C) list *)
type fourP = (stackT * envReg * ctlL * dumpReg)
type runT = fourP -> value


 (* run : S * E * C * D -> value *)
 (* where S = value list *)
 (* E = value Env.env *)
 (* C = directive list *)
 (* D = (S * E * C) list *)
 let rec run (fP: fourP) = match fP with
      (v1 :: [], ep1, [], [])                                         (* 1 *)
            -> v1
    | (v2 :: [], ep2, [], (s2, e2, c2) :: d2)                         (* 2 *)
            -> run (v2 :: s2, e2, c2, d2)
    | (s3, e3, (TERM (LIT n)) :: c3, d3)                              (* 3 *)
            -> run ((INT n) :: s3, e3, c3, d3)
    | (s4, e4, (TERM (VAR x4)) :: c4, d4)                             (* 4 *)
            -> run ((Env.lookup (x4, e4)) :: s4, e4, c4, d4)
    | (s5, e5, (TERM (LAM (x5, t))) :: c5, d5)                        (* 5 *)
            -> run ((CLOSURE (e5, x5, t)) :: s5, e5, c5, d5)
    | (s6, e6, (TERM (APP (t60, t61))) :: c6, d6)                     (* 6 *)
            -> run (s6, e6, (TERM t61) :: (TERM t60) :: APPLY :: c6, d6)
    | (SUCC :: (INT n) :: s7, e7, APPLY :: c7, d7)                    (* 7 *)
            -> run ((INT (n+1)) :: s7, e7, c7, d7)
    | ((CLOSURE (ep8, x8, t)) :: vp :: s8, e8, APPLY :: c8, d8)       (* 8 *)
            -> run ([], Env.extend (x8, vp, ep8), (TERM t) :: [], (s8, e8, c8) :: d8) ;
    | (_, _, _, _)     ->  failwith "run failed to match"           (* exception *)

 and
     (* evaluate0 : program -> value *)
     evaluate0 = function t                                       (* 9 *)
                -> run ([], e_init, (TERM t) :: [], [])
 ;;