(* ACG with a more expressive semantic lexicon that includes
   multi-prompt delimited continuations and the notion of evaluation.
   Types are considered as a mere approximation rather than
   the complete specification of grammatical composition.

   Our examples are scope ambiguity in quantified phrases with conjunction
   and verbal ellipsis.
   Sec 4.4 from
   http://www.loria.fr/equipes/calligramme/acg/publications/esslli-09/2009-esslli-acg-week-2-part-2.pdf

*)


(* The abstract form, to be interpreted in several ways. *)

(* Abstract signature, which defines base types, constants and their types *)

module type Abstract = sig
  type n				(* base types *)
  type np
  type s
  type sm				(* Complete sentence, the matrix *)

  val john  : np				(* constants *)
  val bill  : np
  val man   : n
  val woman : n
  val kid   : n

  val see   : np -> np -> s
  val love  : np -> np -> s

  val ran   : np -> s

  val every : n -> np
  val some  : n -> np
  val a     : n -> np

  val and_  : np -> np -> np
  val didnt : (np -> s) -> np -> s  (* Should've introduced the type vp,
				       to keep the signature low order.
				       But we follow the ESSLLI notes literally.
				     *)
  val that  : n -> (np -> s) -> n   (* Restrictive relative clauses *)

  val dot : s -> sm		(* Terminating dot *)
end;;

(* Sample phrases in the abstract language *)

(* Example from Sec 4.3 of the ESSLLI Advanced ACG course. *)
module Ex43(A: Abstract) = struct
 open A
 let term = dot (love (some woman) (every man))
end;;


(* Example (2) from Sec 4.4 of the ESSLLI Advanced ACG course. *)
(* The encoding is exactly t3 of Sec 4.4
*)
module Ex442(A: Abstract) = struct
 open A
 let term = dot (ran (and_ john (every kid)))
end;;

(* Example (3c) from Sec 4.4 of the ESSLLI Advanced ACG course. *)
(* The encoding is exactly t11 of Sec 4.4.3
*)
module Ex443c(A: Abstract) = struct
 open A
 let term = dot (didnt ran (every kid))
end;;

(* Example (4) from Sec 4.4.4 of the ESSLLI Advanced ACG course. *)
(* The example can't be handled with ACG at present
*)
module Ex444(A: Abstract) = struct
 open A
 let term = dot (ran (a (that man (fun np -> see np (every woman)))))
end;;


(* An interpretation of the abstract signature as the surface form: strings *)
(* This is literally L_syntax in Sec 4.4, only written in OCaml *)
module Syntax = struct
 type n  = string
 type np = string
 type s  = string
 type sm = string
   
 let john = "John"
 let bill = "Bill"
 let man   = "man"
 let woman = "woman"
 let kid   = "kid"
 let every = fun x -> "every " ^ x
 let some  = fun x -> "some " ^ x
 let a     = fun x -> "a " ^ x
 let ran   = fun x -> x ^ " ran"
 let see   = fun o s -> s ^ " saw " ^ o
 let love  = fun o s -> s ^ " loves " ^ o

 let and_  = fun np1 np2 -> np1 ^ " and " ^ np2

 let didnt = fun vp -> fun x -> x ^ " didn't" ^ (vp "")

 let that  = fun n -> fun cl -> n ^ " that " ^ (cl "")

 let dot = fun s -> s ^ "."
end;;

(* Surface forms of sample terms *)
let module Ex43S = Ex43(Syntax) in Ex43S.term;;
(*
- : Syntax.sm = "every man loves some woman."
*)

let module Ex442S = Ex442(Syntax) in Ex442S.term;;
(*
- : Syntax.sm = "John and every kid ran."
*)

let module Ex443cS = Ex443c(Syntax) in Ex443cS.term;;
(*
- : Syntax.sm = "every kid didn't ran."
*)

let module Ex444S = Ex444(Syntax) in Ex444S.term;;
(*
- : Syntax.sm = "a man that every woman saw  ran."
*)

(* ------------------------------------------------------------------------ *)
(* Semantic forms *)

(* The domain of truth values *)
module type Logic = sig
  type t
  type varname
  type var
  type quant_t = varname -> t -> t      (* Quantified formula *)

  val conj   : t -> t -> t
  val impl   : t -> t -> t
  val not    : t -> t

  val exists : quant_t
  val forall : quant_t

  val quantify : quant_t -> (var -> t) -> t
end;;

(* This is literally Sig_sem of Sec 4.3 *)
module type Meaning = sig
  include Logic
  type e

  val ind    : string -> e
  val indvar : var    -> e

  val man'   : e -> t
  val woman' : e -> t
  val kid'   : e -> t

  val run'   : e -> t

  val see'   : e -> e -> t
  val love'  : e -> e -> t

  val make_ind_quant : quant_t -> (e -> t) -> t
end;;


(* We can interpret meanings in several ways: for example, we
   can evaluate propositions in a particular world.
   For now, we are most interested in one particular interpretations:
   printing out the formulas in a nice way.
*)

(* We interpret all semantic types as strings, as text formulas *)
(* As we show formulas, we check that all variables are bound in the
   environment. The function show_closed_fml makes sure that only
   closed formulas can be shown.
   The current implementation is a bit of a hack. The scope extrusion
   can be detected well ahead of showing formulas. We need to pass the env
   to every formula, so the type of formulas in the Logic signature
   should be [varname] -> t rather than t.
*)
module ShowLogic = struct
  type prec    = int
  type varname = string
  type env     = varname list
  type var     = env -> string
  type t       = env -> prec -> string
  type quant_t = varname -> t -> t

  let paren cond text = if cond then "(" ^ text ^ ")" else text

  let conj e1 e2 = fun env p -> paren (p > 3) (e1 env 4 ^ " & "  ^ e2 env 3)
  let impl e1 e2 = fun env p -> paren (p > 2) (e1 env 3 ^ " => " ^ e2 env 2)
  let not  e1    = fun env p -> paren (p > 10) ("~" ^ e1 env 11)

  let exists v e = fun env p -> 
    paren (p > 0) ("E" ^ v ^ ". " ^ e (v::env) 0)

  let forall v e = fun env p -> 
    paren (p > 0) ("A" ^ v ^ ". " ^ e (v::env) 0)

  let app1 op arg1      = fun env p -> 
    paren (p > 10) (op env 10 ^ " " ^ arg1 env 11)
  let app2 op arg1 arg2 = fun env p -> 
    paren (p > 10) (op env 10 ^ " " ^ arg1 env 11 ^ " " ^ arg2 env 11)
  let gensym = 
   let counter = ref 0 in
   fun () -> incr counter; "x" ^ string_of_int !counter

  let quantify quant body =
    let vname = gensym () in
    let v = fun env ->
      if List.mem vname env then vname else
         (ignore (Printf.printf "%s\n" 
		    ("\n!!!Unbound var " ^ vname ^ " in the env [" ^
		     List.fold_left (fun acc vn -> 
		       if acc = "" then vn else ", " ^ vn) 
		     "" env ^ "]")); vname) in
    let body' = body v in
    quant vname body'

  let show_closed_fml e = e [] 0
end;;

let show_closed_fml = ShowLogic.show_closed_fml;; (* Useful abbreviation *)

module ShowMeaning = struct
  include ShowLogic
  type e = env -> prec -> string

  let ind name   = fun env p -> name
  let indvar var = fun env p -> var env

  let man'     = app1 (fun _ p -> "man")
  let woman'   = app1 (fun _ p -> "woman")
  let kid'     = app1 (fun _ p -> "kid")

  let run'     = app1 (fun _ p -> "run")

  let see'     = app2 (fun _ p -> "see")
  let love'    = app2 (fun _ p -> "love")

  let make_ind_quant quant body =
    quantify quant (fun var -> body (indvar var))
end;;


(* ------------------------------------------------------------------------ *)
(* Syntax-Semantics interface *)

open Delimcc;;		       	(* Load the library of multi-prompt shift *)

(* We now build the semantic signature and the lexicon -- stepwise *)

module Sem1(S: Meaning) = struct
   open S

   type np = unit -> e
   (* The following type for n describes Nbar, or ``complex common nouns''
      with complements such as prepositional phrases.
   *)
   type n  = unit -> (unit -> e) -> t
   type s  = unit -> t
   type sm = t

   let psen = new_prompt ()
   let puni = new_prompt ()
   let pexi = new_prompt ()

   let john = fun () -> ind "John'"
   let bill = fun () -> ind "Bill'"

   let man   = fun () x -> man'   (x ())
   let woman = fun () x -> woman' (x ())
   let kid   = fun () x -> kid'   (x ())
   let ran   = fun x () -> run'   (x ())
   let love  = fun o s () -> let sv = s () in 
                             let ov = o () in love' ov sv
   let see   = fun o s () -> let sv = s () in 
                             let ov = o () in see' ov sv

   let every = fun n () -> 
      let nv = n () in			(* evaluate Nbar first *)
      shift puni (fun k -> 
      make_ind_quant forall (fun x -> 
	impl (nv (fun () -> x)) (k x)))

   let some = fun n () -> 
      let nv = n () in			(* evaluate Nbar first *)
      shift pexi (fun k -> 
      make_ind_quant exists (fun x -> 
	conj (nv (fun () -> x)) (k x)))

   let a = some

   let dot s =
     push_prompt psen (fun () ->
     push_prompt puni (fun () ->
     push_prompt pexi (fun () ->
     s ())))

   let and_ = fun (np1:np) np2 () -> shift psen (fun k ->
     conj (k np1) (k np2)) ()

   let didnt = fun (vp:np->s) np () -> shift psen (fun k ->
     not (k (vp np))) ()

   let that = fun (n:n) clause () ->
     let nv = n () in
     fun (x:np) -> conj (nv x) (dot (clause x))
end;;

(* A different semantic signature, a refinement of SemBasic specifying
   a different sequence of prompts.
*)

module Sem2(S: Meaning) = struct    
  include Sem1(S)

   let dot s =
     push_prompt psen (fun () ->
     push_prompt pexi (fun () ->
     push_prompt puni (fun () ->
     s ())))
end;;

(* The result is identical to that at the end of Sec 4.3 *)
let module Ex43L1 = Ex43(Sem1(ShowMeaning)) in show_closed_fml Ex43L1.term;;
(*
- : string = "Ax3. man x3 => (Ex4. woman x4 & love x4 x3)"
*)

let module Ex43L1 = Ex43(Sem2(ShowMeaning)) in show_closed_fml Ex43L1.term;;
(*
- : string = "Ex6. woman x6 & (Ax5. man x5 => love x6 x5)"
*)

let module Ex442L = Ex442(Sem1(ShowMeaning)) in show_closed_fml Ex442L.term;;
(*
- : string = "run John' & (Ax11. kid x11 => run x11)"
*)

(* We have just reproduced the logical form L(t12) of Sec 4.4.3 *)

let module Ex443cL = Ex443c(Sem1(ShowMeaning)) in show_closed_fml Ex443cL.term;;
(*
- : string = "~(Ax12. kid x12 => run x12)"
*)

(* Quantifier scopes wider: We have just reproduced the logical form L(t13)
   of Sec 4.4.3 *)
let module Ex443cL2 = Ex443c(
  struct
    include Sem1(ShowMeaning)
    let didnt = fun (vp:np->s) np () -> ShowMeaning.not ((vp np) ())
  end) in show_closed_fml Ex443cL2.term;;
(*
- : string = "Ax13. kid x13 => ~(run x13)"
*)

let module Ex444L = Ex444(Sem1(ShowMeaning)) in show_closed_fml Ex444L.term;;
(*
- : string = "Ex14. (man x14 & (Ax15. woman x15 => see x14 x15)) & run x14"
*)

(* Here, the universal cannot scope over the existential because a 
   relative clause, like `dot', restricts the scope of all 
   embedded quantifiers.
   In our analysis, we assume that all quantifiers within a clause cannot
   take scope outside of the clause.
   Of course, this is an approximation: Some quantifiers do take scope
   wider than the scope of the containing clause; for example, `each'.
   But we can deal with them by defining a new prompt p_each and differentiating
   the clause boundary from the sentence boundary. Whereas the sentence
   boundary sets all the prompts (nothing can take the wider scope than
   that of a sentence),  the relative clause's `that' does not set the 
   p_each prompt and so does not restrict the scope for `each'.
*)