(*
                       Open GADTs in OCaml
         Building interpreters by composing fragments
*)

open Leibniz

(* The first primitive fragment: integers and the successor *)
type 'a exp_int =
  [ `Int of int * (int,'a) eq
  | `Inc of (int -> int,'a) eq ]

(* smart constructors, as syntactic sugar *)
let e_int x : [> 'a exp_int] = `Int (x, refl ())
(* val e_int : int -> int exp_int *)

let e_inc : [> 'a exp_int]  = `Inc (refl ())
(* val e_inc : (int -> int) exp_int *)

(* Evaluator for the fragment *)
let eval_int self : [> 'a exp_int] -> 'a =
 function
  | `Int (x,eq)  -> cast eq x
  | `Inc eq      -> cast eq succ
  |  x           -> self x


(* Another fragment: polymorphic lift *)
type 'a exp_lift = [ `Lft of 'a ]

let e_lft x = `Lft x
(* val e_lft : 'a -> 'a exp *)

let eval_lift self =
 function
  | `Lft x  -> x
  | x       -> self x


(* The third fragment: application and abstraction *)
module type LAM = sig
  type 'a exp
  type 'a exp_lam =
    [ `Lam of < m_lam : 'w. ('a,'w) lam_k -> 'w >
    | `App of < m_app : 'w. ('a,'w) app_k -> 'w > ]
  (* The standard encoding of existentials *)
  and ('a,'w) lam_k =
     {lam_k : 'u 'v. (('u -> 'v),'a) eq * ('u exp -> 'v exp) -> 'w}
  and ('a,'w) app_k =
     {app_k : 'u 'v. ('v, 'a) eq * ('u -> 'v) exp * 'u exp -> 'w}
  (* smart constructors, as syntactic sugar *)
  val e_lam : ('a exp -> 'b exp) -> [> ('a -> 'b) exp_lam ]
  val e_app : ('a -> 'b) exp -> 'a exp -> [> 'b exp_lam ]
end

module Lam(E: sig type 'a exp = private [> 'a exp_lift] end) :
  LAM with type 'a exp = 'a E.exp
= struct
  open E
  type 'a exp = 'a E.exp
  type 'a exp_lam =
    [ `Lam of < m_lam : 'w. ('a,'w) lam_k -> 'w >
    | `App of < m_app : 'w. ('a,'w) app_k -> 'w > ]
  (* The standard encoding of existentials *)
  and ('a,'w) lam_k =
     {lam_k : 'u 'v. (('u -> 'v),'a) eq * ('u exp -> 'v exp) -> 'w}
  and ('a,'w) app_k =
     {app_k : 'u 'v. ('v, 'a) eq * ('u -> 'v) exp * 'u exp -> 'w}

  (* smart constructors, as syntactic sugar *)
  (* Method signatures are, alas, required. *)
  let e_lam f : [> 'a exp_lam] =
   `Lam (object method m_lam : 'w. ('a,'w) lam_k -> 'w
    = fun k -> k.lam_k (refl (),f) end)
  (* val e_lam : ('a exp -> 'b exp) -> ('a -> 'b) exp *)

  let e_app f x : [> 'a exp_lam] =
    `App (object method m_app : 'w. ('a,'w) app_k -> 'w
     = fun k -> k.app_k (refl (),f,x) end)
  (* val e_app : ('a -> 'b) exp -> 'a exp -> 'b exp *)
end


(* The interpreter. We need polymorphic recursion -- as is
  typical with GADTs*)
module LAMEV(E: LAM with type 'a exp = private [> 'a exp_lift]) = struct
  open E
  type eval_sig = {ev: 'a. 'a exp -> 'a}
  let eval_lam self : [> 'a exp_lam] -> 'a = function
    | `Lam x ->
        x#m_lam {lam_k =
            fun (eq,f) -> cast eq (fun x -> self.ev (f (e_lft x)))}
    | `App x ->
        x#m_app {app_k =
            fun (eq,f,x) -> cast eq ((self.ev f) (self.ev x))}

    (* This case is needed to ensure that the argument type is covariantly
       extensible.

       We should have the following match here

          | x -> self.ev x

       but the types don't work out, because x has type

          [> `Lam  ...]

       and the argument type of self.ev doesn't include `Lam.  It seems we
       need to extend the type of E.exp to include `Lam and `App.  (This is a
       little trickier than it sounds, because the accompanying nominal types
       lam_k and app_k can't be constrained using 'with'.)  This needs further
       investigation.  
    *)
    | x -> failwith "unknown case"
end



(* Test expressions *)
(* Note their inferred types given in comments *)

(* Tying the knot *)
module EInt = struct
  module rec E : sig
    module LE : LAM with type 'a exp = 'a E.exp
    type 'a exp = ['a exp_int | 'a exp_lift | 'a LE.exp_lam]
  end = 
  struct
    module LE = Lam(E)
    type 'a exp = ['a exp_int | 'a exp_lift | 'a LE.exp_lam]
  end
end

module Test1 = struct
  open EInt.E.LE
  let test = e_app e_inc (e_int 1)
end
(* val test : [> int E.LE.exp_lam ] *)

module Test2 = struct
  open EInt.E.LE
  let test = e_lam (fun x -> e_app e_inc (e_app e_inc x))
end
(* val test : [> (int -> int) E.LE.exp_lam ] *)

module Test3 = struct
  open EInt.E.LE
  let test = e_lam (fun f -> e_lam (fun x -> e_app f x))
end
(* val test : [> (('_a -> '_b) -> '_a -> '_b) E.LE.exp_lam ] *)

module Test4 = struct
  open EInt.E.LE
  let test = e_app (e_app Test3.test Test2.test) (e_int 3)
end
(* module Test4 : sig val test : [> int EInt.E.LE.exp_lam ] end *)

(* Build the interpreter by composition of various pieces *)
module EInt_EVAL = struct
  module EV = LAMEV(EInt.E.LE)
  open EV
  let rec eval = {ev = fun e -> eval_lift (eval_int (eval_lam eval)) e}
end

let test1_ev = EInt_EVAL.eval.EInt_EVAL.EV.ev Test1.test
(* val test1v : int = 2  *)

let test2_ev = EInt_EVAL.eval.EInt_EVAL.EV.ev Test2.test 40
(* val test1v : int = 42  *)

let test3_ev = EInt_EVAL.eval.EInt_EVAL.EV.ev Test3.test
(* val test3v : (int -> int) -> int -> int = <fun> *)

let test4_ev = EInt_EVAL.eval.EInt_EVAL.EV.ev Test4.test
(* val test4_ev : int = 5 *)


(* ---------------------------------------------------------------------- *)
(* Extending the language: adding booleans and int comparison *)
type 'a exp_bool =
  [ `Bool of bool * (bool,'a) eq
  | `Cmp  of (int->int->bool,'a) eq ]

(* smart constructors, as syntactic sugar *)
let e_bool x : [> 'a exp_bool] = `Bool (x, refl ())
(* val e_bool : bool -> [> bool exp_bool ] = <fun> *)

let e_cmp : [> 'a exp_bool]  = `Cmp (refl ())
(* val e_bool : bool -> [> bool exp_bool ] = <fun> *)

let eval_bool self : [> 'a exp_bool] -> 'a =
 function
  | `Bool (x,eq)  -> cast eq x
  | `Cmp eq       -> cast eq (=)
  |  x            -> self x


(* Test expressions *)
(* Note their inferred types given in comments *)

(* Tying the knot *)
module EIntBool = struct
  module rec E : sig
    module LE : LAM with type 'a exp = 'a E.exp
    type 'a exp = ['a exp_int | 'a exp_bool | 'a exp_lift | 'a LE.exp_lam]
  end =
  struct
    module LE = Lam(E)
    type 'a exp = ['a exp_int | 'a exp_bool | 'a exp_lift | 'a LE.exp_lam]
  end
end


module Test5 = struct
  open EIntBool.E.LE
  let plus2 = e_lam (fun x -> e_app e_inc (e_app e_inc x))
  let test = e_app (e_app e_cmp (e_app plus2 (e_int 3))) (e_int 5)
end
(*
   val plus2 : [> (int -> int) EIntBool.E.LE.exp_lam ]
   val test : [> bool EIntBool.E.LE.exp_lam ]
*)

(* Build the interpreter by composition of various pieces *)
module EIntBool_EVAL = struct
  module EV = LAMEV(EIntBool.E.LE)
  open EV
  let rec eval = {ev = fun e ->
  eval_bool (eval_lift (eval_int (eval_lam eval))) e}
end

let test5_ev = EIntBool_EVAL.eval.EIntBool_EVAL.EV.ev Test5.test
(* val test5_ev : bool = true *)