(* From Olivier Danvy's 2003 "A Rational Deconstruction
     of Landin's SECD Machine"

     An OCaml translation.  *)

(* 2.4 A dump-less direct-style counterpart

    The evaluator of Section 2.3 is in continuation-passing
    style and therefore it is in the image of the CPS
    transformation [11].   Its direct-style counterpart reads
    as follows, renaming run_t as eval and run_a as apply.
*)

open Ohdr;;
open Source;;

(*   eval : Source.term * S * E * C -> stack *)
(*  apply : S * E * C -> S *)
(*    where S = value list *)
(*          E = value Env.env *)
(*          C = S*E->S *)

let rec eval = function
         (LIT n, s, e, c)      -> c ((INT n) :: s, e)
  |      (VAR x, s, e, c)      -> c ((Env.lookup (x, e)) :: s, e)
  |      (LAM (x, t), s, e, c) -> c ((CLOSURE (e, x, t)) :: s, e)
  |    (APP (t0, t1), s, e, c)
             -> eval (t1, s, e,
                      fun (s1, e1) ->
                          eval (t0, s1, e1,
                                fun (s2, e2) -> apply (s2, e2, c)))
  (* |    (_, _, _, _) -> failwith "eval failed" *)

and apply = function
       (SUCC :: (INT n) :: s, e, c)
                 -> c ((INT (n+1)) :: s, e)
  |    ((CLOSURE (e', x, t)) :: v' :: s, e, c)
                 -> let (v :: []) =
                         eval (t, [], Env.extend (x, v', e'), 
                               fun (s, _) -> s)
                    in
                       c(v::s,e)

  |    (_, _, _) -> failwith "apply failed"
;;

(* evaluate3a : Source.program -> value
   Here's the nice way to write this, but ocamlc
   gives a "non-exhaustive pattern-matching" warning.
   (There's another warning in the CLOSURE branch of
   the apply function above, but I couldn't see any
   decent way of shutting ocamlc up, up there.

let evaluate3a t =
      let (v :: []) =
          eval (t, [], e_init, fun (s, _) -> s)
      in
          v
      ;;
*)

(* evaluate3 : Source.program -> value
   Here's what I did to shut ocamlc up.  *)
let evaluate3 t =
      let ev = eval (t, [], e_init, fun (s, _) -> s)
      in match ev with
        v :: [] -> v
      | _       -> failwith "evaluate3 bad return from eval"
      ;;

(* Let's see what the results look like *)
let id_to_string id : (Source.ide -> string) = id;;

let rec e_mres (e: value Env.env) = "<[" ^ (Env.epr (e, v_mres)) ^ "]>"

and t_mres = function (* term -> string *)
    | LIT ti             -> "<LIT " ^ string_of_int ti ^ ">"
    | VAR id             -> (id:string)
    | LAM (id, trm)      -> "(\\" ^ id ^ " -> " ^ (t_mres trm) ^ ")"
    | APP (tf, tp)       -> "[" ^ (t_mres tf) ^ " _ " ^ (t_mres tp) ^ "]"

and v_mres = function
    | INT vi             -> string_of_int vi
    | SUCC               -> "succ"
    | CLOSURE (e, v, t)  -> "(E:" ^ (e_mres e) ^
                            ", V:" ^ v ^
                            ", T:" ^ (t_mres t) ^ ":)"
    (* | _                -> "(no match)" *)
    ;;

let one_test f term =
    print_string( "Evaluating     " ^ t_mres term ) ;
    print_newline();
    print_string( "      result   " ) ;
    let result = f term
    in   print_string( v_mres result ) ;
         print_newline()
    ;;

let rec eval_tests f tests =
    match tests with
       [] ->            ()
     | (t1 :: z) -> one_test f t1 ;
                    eval_tests f z
    ;
    ();;

(* Some of these basic tests are from Oleg, who must have done a similar
   exercise (probably when he was three or four).  I think he has his own
   "X" function so that he can just use normal scheme S-expressions;
   I removed that part of each of these.  Later, I'd like to supply my
   own "Define".  For the source, see
       http://okmij.org/ftp/Computation/lambda-arithm-basic.scm

   Most of the other tests came from Chris Barker's Lambda tutorial at
      http://ling.ucsd.edu/~barker/Lambda/ 

   The bad_tests list, below, includes ones like
           ((LAM x (it x)) works)
   which evaluate to something
           (it works)
   that looks like an application, therefore (my translation of Danvy's
   presentation of) Landin's code tries to apply "it" to "works", and fails.
 
   The ok_tests omit those, leaving only the tests that will only ever
   apply "succ" or a LAM that's defined in that very expression.
*)
let ok_tests = [
      (LIT 7)
    ; (LIT 3)
    ; (LAM ("x", (APP ((VAR "succ"), (VAR "x")))))
    ; (APP ((LAM ("x", (APP ((VAR "succ"), (VAR "x"))))), (LIT 8)))
    ; (LAM ("x", (LAM ("y", (APP ((VAR "succ"), (VAR "x")))))))
    ; (APP ((LAM ("x", (APP ((VAR "succ"), (VAR "x"))))), (LIT 7)))

    (*

    (* Basic combinators *)
    ; (def %I (L x x))                (* identity *)

    ; (def %Y (L f ((L x (f (x x))) (L x (f (x x))))))
    ; (def %Y (L f ((L x (f (x x))) (L x (f (x x))))))

    ; (* ------------------------- *)
    ; (*  Booleans *)
    ; (def %true (L x (L y x)))
    ; (def %false (L x (L y y)))
    ; 
    ; (def %and (L p (L q (p q %false))))
    ; (def %or (L p (L q (p %true q))))
    ; (def %not (L p (p %false %true)))
    ; (def %xor (L p (L q (p (q %false %true) q))))
    ; (def %equ (L p (L q (%not (%xor p q))))) 
    ; (*  another derivation: (def %equ (L p (L q (p q (q %false %true))))) *)
    ; 
    ; (expand-shortcuts %equ)
    ; (%equ %true %false)
    ; (%equ %false %false) 
    ; (LIT 3)
    ; (LAM x (succ x))
    ; ((LAM x (succ x)) (LIT 7))
    ; ((LAM x x) (LIT 2))
    ; ((LAM x (LAM y1 (x y1))) z)
    ; ((LAM x (LAM y (x y))) y)
    ; ((LAM x (x x))(LAM x (LAM y (x y))))
    ; (LAM x (P x))
    ; ((LAM x (x x)) 2)
    ; ((LAM x (x y z)) z)
    ; ((LAM x (w y)) z)
    ; ((LAM x (P x)) j)
    ; ((LAM x (P y)) j)
    ; (((LAM x (LAM y (P y))) j) m)
    ; (((LAM x (LAM y (P x))) j) m)
    ; ((LAM P (P j)) (LAM x (Q x)))
    ; (((LAM x (LAM y (K x y))) j) m)
    ; (((LAM y (LAM x (K x y))) j) m)
    ; (P j)
    ; ((LAM x (P x)) j)
    ; ((LAM Q (Q j)) P)
    ; (((LAM Q (LAM x (Q x))) P) j)
    ; (((LAM x (LAM Q (Q x))) j) P)
    ; (((LAM Q (LAM x (Q x))) (LAM y (P y))) j)
    ; ((((LAM GQ  (LAM L (LAM x ((GQ L) x)))) (LAM Q (LAM x (Q x)))) P) j)
    ; ((LAM x (A x (K x j))) m)
    ; ((LAM x ((LAM x (K x x)) j)) m)
    ; (X sleeps)
    ; ((D man) sleeps)
    ; (((LAM x (LAM y (x y))) 2) 3)
    ; ((LAM x ((LAM y (x y)) 2)) 3)
    ; ((LAM x (x x))(LAM x (LAM y (x x))))
    ; ((LAM x (succ x)) 7)
    ; ((LAM x (it x)) works)
    ; ((LAM x (LAM y1 (x y1))) z)
    ; ((LAM x (LAM y (x y))) y)
    ; ((LAM x (x x))(LAM x (LAM y (x y))))
    ; (LAM x (P x))
    ; ((LAM x x) 2)
    ; ((LAM x (x x)) 2)
    ; ((LAM x (x y z)) z)
    ; ((LAM x (w y)) z)
    ; ((LAM x (P x)) j)
    ; ((LAM x (P y)) j)
    ; (((LAM x (LAM y (P y))) j) m)
    ; (((LAM x (LAM y (P x))) j) m)
    ; ((LAM P (P j)) (LAM x (Q x)))
    ; (((LAM x (LAM y (K x y))) j) m)
    ; (((LAM y (LAM x (K x y))) j) m)
    ; (P j)
    ; ((LAM x (P x)) j)
    ; ((LAM Q (Q j)) P)
    ; (((LAM Q (LAM x (Q x))) P) j)
    ; (((LAM x (LAM Q (Q x))) j) P)
    ; (((LAM Q (LAM x (Q x))) (LAM y (P y))) j)
    ; ((((LAM GQ  (LAM L (LAM x ((GQ L) x)))) (LAM Q (LAM x (Q x)))) P) j)
    ; ((LAM x (A x (K x j))) m)
    ; ((LAM x ((LAM x (K x x)) j)) m)
    ; (((LAM x (LAM y (x y))) 2) 3)
    ; ((LAM x ((LAM y (x y)) 2)) 3)
    ; ((LAM x (x x))(LAM x (LAM y (x x))))
    *)
]
(* The thing is, many of the "test"s that would have been
   bad_tests are now not even compilable. *)
let bad_tests = [
      (VAR "x")
    ; (APP ((LIT 7), (LIT 3)))
]

(* Not compilable ...
      (X sleeps)
    ; ((D man) sleeps)
*)

let main =
    print_string "Evaluate 0 ... " ;
    print_newline();
    eval_tests Ohdr.evaluate0 ok_tests ;
    print_string "Evaluate 3 ... " ;
    eval_tests evaluate3 ok_tests ;

    (*
    print_string "Try the bad tests, too..." ;
    print_string "Bad Evaluate 0" ;
    eval_tests Ohdr.evaluate0 bad_tests ;
    print_string "Bad Evaluate 3" ;
    eval_tests evaluate3 bad_tests
    *)
    ;;

main