(* 
  Embedding a higher-order domain-specific language (simply-typed
  lambda-calculus with constants) with a selectable evaluation order:
  Call-by-value, call-by-name, call-by-need.
  This is an OCaml version of CBAny.hs
*)

(* The (higher-order abstract) syntax of our DSL *)

module type EDSL = sig
  type 'a exp				(* representation of terms *)
  type ('a,'b) arrow			(* The arrow type *)
  
  val int : int -> int exp
  val (+:) : int exp -> int exp -> int exp
  val (-:) : int exp -> int exp -> int exp

  val lam : ('a exp -> 'b exp) -> ('a,'b) arrow exp
  val (%:) : ('a,'b) arrow exp -> ('a exp -> 'b exp) (* application *)

					(* A convenient abbreviation 
					   (could've been called `bind') *)
  val let_ : 'a exp -> ('a exp -> 'b exp) -> 'b exp
end;;


(* A sample EDSL term *)
module EX0(S:EDSL) = struct
  open S
  let t =
    (lam (fun x -> let_ (x +: x) (fun y -> y +: y))) %: int 10
end;;


(* We now embed our EDSL into OCaml: we write several interpreters
   of EDSL, or several implementations of the signature EDSL
   Our principle is to write a term once and evaluate many times,
   in different evaluation orders.
*)

(* * // *)

(* An EDSL expression of the type 'a is interpreted as a OCaml value
   unit -> 'a
   (imagine it to be a reader monad with () as the environment).
*)

(* * // *)
(* Call-by-name interpretation *)

module CBName = struct
  type 'a exp = unit -> 'a		(* representation of terms *)
  type ('a,'b) arrow = (unit -> 'a) -> (unit ->'b) (* The arrow type *)
  
  let int x = fun () -> x
  let (+:) x y = fun () -> 
    let xv = x () in let yv = y () in 
    Printf.printf "Adding %d and %d\n" xv yv;
    xv + yv
  let (-:) x y = fun () ->
    let xv = x () in let yv = y () in
    Printf.printf "Subtracting %d and %d\n" xv yv;
    xv - yv

  let lam f = fun () -> f
  let (%:) x y = fun () -> x () y ()

  let let_ x y = (lam y) %: x
end;;

let run_cbn m = m ();;

(* The addition (x +: x) is performed twice because y is bound
   to a computation, and y is evaluated twice
*)
let t0SN = let module M = EX0(CBName) in run_cbn M.t;;
(*
Adding 10 and 10
Adding 10 and 10
Adding 20 and 20
val t0SN : int = 40
*)

(* A more elaborate example *)
module EX1(S:EDSL) = struct
  open S
  let t = (lam (fun x -> 
             let_ (x +: x) (fun y ->
               lam (fun z -> z +: (z +: (y +: y)))))) 
           %: (int 10 -: int 5) 
           %: (int 20 -: int 10)
end;;

(* Duplication of computations is more pronounced *)
let t1SN = let module M = EX1(CBName) in run_cbn M.t;;
(*
Subtracting 20 and 10
Subtracting 20 and 10
Subtracting 10 and 5
Subtracting 10 and 5
Adding 5 and 5
Subtracting 10 and 5
Subtracting 10 and 5
Adding 5 and 5
Adding 10 and 10
Adding 10 and 20
Adding 10 and 30
val t1SN : int = 40
*)


(* An even better example *)
module EX2(S:EDSL) = struct
  open S
  let t = (lam (fun z -> lam (fun x -> 
            let_ (x +: x) (fun y -> y +: y))))
          %: (int 100 -: int 10)
          %: (int 5 +: int 5)
end;;

(* The result of subtraction was not needed, and so it was not performed
   OTH, (int 5 `add` int 5) was computed four times.
*)
let t2SN = let module M = EX2(CBName) in run_cbn M.t;;
(*
Adding 5 and 5
Adding 5 and 5
Adding 10 and 10
Adding 5 and 5
Adding 5 and 5
Adding 10 and 10
Adding 20 and 20
val t2SN : int = 40
*)

(* * // *)
(* Call-by-value interpretation *)
(*
  The only difference is the interpretation of lam:
  before evaluating the body, _always_ evaluate the argument
*)

module CBValue = struct
  include CBName

  (* The only difference from CBName: a new interpretation of lam *)
  (* Now lam first evaluates its argument, no matter what. *)
  (* This is the definition of CBV after all *)
  let lam f = fun () -> 
                fun y -> let yv = y () in f (fun () -> yv)

  let let_ x y = (lam y) %: x
end;;

let run_cbv m = m ();;

(* We now re-evaluate the previously written tests EX0, Ex1, EX2
   under the new interpretation
*)


let t0SV = let module M = EX0(CBValue) in run_cbv M.t;;
(*
Adding 10 and 10
Adding 20 and 20
val t0SV : int = 40
*)

let t1SV = let module M = EX1(CBValue) in run_cbv M.t;;
(*
Subtracting 10 and 5
Adding 5 and 5
Subtracting 20 and 10
Adding 10 and 10
Adding 10 and 20
Adding 10 and 30
val t1SV : int = 40
*)

(* Although the result of subtraction was not needed, it was still performed
   OTH, (int 5 `add` int 5) was computed only once
*)
let t2SV = let module M = EX2(CBValue) in run_cbv M.t;;
(*
Subtracting 100 and 10
Adding 5 and 5
Adding 10 and 10
Adding 20 and 20
val t2SV : int = 40
*)

(* * // *)
(* Call-by-need interpretation *)
(* The only difference is the interpretation of lam:
   before evaluating the body, share the argument
   The argument is evaluated _at most_ once
*)

module CBLazy = struct
  include CBName

  (* The only difference from CBName: a new interpretation of lam *)
  (* Now lam shares its argument, no matter what. *)
  (* This is the definition of CBNeed after all *)
  let lam f = fun () -> 
                fun y -> 
		let rec yr = 
		  ref (fun () -> 
		    let v = y () in yr := (fun () -> v); v) in
		f (fun () -> !yr ())

  let let_ x y = (lam y) %: x
end;;

let run_cbl m = m ();;

(* We now re-evaluate the previously written tests EX0, Ex1, EX2
   under the new interpretation
*)

(* Here, Lazy is just as efficient as CBV *)
let t0SL = let module M = EX0(CBLazy) in run_cbl M.t;;
(*
Adding 10 and 10
Adding 20 and 20
val t0SL : int = 40
*)

(* Ditto *)
let t1SL = let module M = EX1(CBLazy) in run_cbl M.t;;
(*
Subtracting 20 and 10
Subtracting 10 and 5
Adding 5 and 5
Adding 10 and 10
Adding 10 and 20
Adding 10 and 30
val t1SL : int = 40
*)

(* Now, Lazy is better than both CBN and CBV: subtraction was not needed,
   and it was not performed.
   All other expressions were needed, and evaluated once.
*)

let t2SL = let module M = EX2(CBLazy) in run_cbl M.t;;
(*
Adding 5 and 5
Adding 10 and 10
Adding 20 and 20
val t2SL : int = 40
*)