(* GSV monadically 15 April 2015 *)

type identifier = char

module type SEMANTICS = sig
  type noun (* this is whatever monadic type the semantics assigns to noun-sized contents *)
  type sent (* this is whatever monadic type the semantics assigns to sentence-sized contents *)
  val run : sent -> bool
  val dynamic : bool
  val extensional : bool

  val getx : noun  val gety : noun  val getz : noun
  (* OCaml will parse ~~~ as a prefix operator, but unfortunately won't let you say
     `~~~ predicate subject`; you have to say `~~~ (predicate subject)`. *)
  val ( ~~~ ) : sent -> sent
  (* OCaml will parse these three as infix operators (yay), but makes them all
     left-associative (ehh for >>>) and have the same precedence (boo). *)
  val ( &&& ) : sent -> sent -> sent
  val ( ||| ) : sent -> sent -> sent
  val ( >>> ) : sent -> sent -> sent
  (* OCaml parses this with same associativity and precedence as the preceding (boo). *)
  val (===) : noun -> noun -> sent
  val ann : noun  val bill : noun  val carol : noun  val dave : noun  val ella : noun  val frank : noun
  val male : noun -> sent  val female : noun -> sent
  val left : noun -> sent
  val single : noun -> sent
  (* Transitive verbs apply to their direct objs first, subjects second. *)
  val marriedto : noun -> noun -> sent
  val saw : noun -> noun -> sent
  val kisses : noun -> noun -> sent
  val loves : noun -> noun -> sent   (* here construed extensionally *)
  (* Quantifiers may be unimplemented. *)
  val some : identifier -> sent -> sent
  val every : identifier -> sent -> sent
  (* Intensional verbs and operators may be unimplemented. *)
  val thinks : sent -> noun -> sent
  val maybe : sent -> sent
end

type world = Actual | Second | Third
let modal_domain = [Actual; Second; Third]

type entity = Ann | Bill | Carol | Dave | Ella | Frank
let domain = [Ann; Bill; Carol; Dave; Ella; Frank]
let string_of_entity = function
  | Ann -> "Ann"
  | Bill -> "Bill"
  | Carol -> "Carol"
  | Dave -> "Dave"
  | Ella -> "Ella"
  | Frank -> "Frank"
let print_entity ent = print_string (string_of_entity ent)

let env0 = fun _ -> raise Not_found
let lookup (sought : identifier) env = env sought
let lookup_string (sought : identifier) env = try string_of_entity (env sought) with Not_found -> "*"
let print_lookup c env = print_string (lookup_string c env)
let insert (var : identifier) who env = fun sought -> if sought = var then who else env sought

let any_truths (xs : 'a list) : bool = List.exists ident xs
let all_truths (xs : 'a list) : bool = List.for_all ident xs

module Facts(X : Monad.MONAD) = struct
(* Here are the atomic facts: Ann and Bill are married, also Carol and Dave.
   Genders and marital statuses are epistemically necessary.
   In the actual world (w1), everyone left; people look leftwards (Carol sees Bill and Ann, etc.); Carol and Dave kiss; husbands love only their wives and Frank loves all the women.
   In w2, all but Carol left; no one sees anything; all spouses kiss; all men love only Carol and Ella loves the wives.
   In w3, only Ann and Bill left; no one sees anything; nobody kisses; Frank loves everyone else.
   So: everyone is either essentially married or essentially single. And Ann and Bill essentially left; others left only contingently.
*)

  let is_male = function Bill | Dave | Frank -> true | _ -> false
  let are_married = function (Ann, Bill) | (Bill, Ann) | (Carol, Dave) | (Dave, Carol) -> true | _ -> false
  let is_a_wife = function Ann | Carol -> true | _ -> false
  
  let male xx = X.(map is_male xx)
  let female xx = X.(map (not % is_male) xx)

(* Ella and Frank are single *)
  let single xx = X.(map (fun x -> x > Dave) xx)

(* Actually (in w1), everybody left. In w2, everybody but Carol left. In w3, only Ann and Bill left. *)
  let left1 xx = X.(map (fun _ -> true) xx)
  let left2 xx = X.(map (fun x -> x <> Carol) xx)
  let left3 xx = X.(map (fun x -> x = Ann || x = Bill) xx)
  
(* In the sentences, order of application is: TransitiveVerb + Object + Subject.
   But we convert to logical order for our operations. *)

(* Actually, each person saw the people alphabetically before them. In w2 and w3, no one saw anyone. *)
  let saw1 yy xx = X.(map2 (fun x y -> x < y) xx yy)
  let saw2 yy xx = X.(map2 (fun _ _ -> false) xx yy)
  let saw3 = saw2
  
(* Necessarily, Ann and Bill are married to each other; also Carol to Dave. *)
  let marriedto yy xx = X.(map2 (curry are_married) xx yy)

(* Actually, only Carol and Dave kiss. In w2, spouses kiss. In w3, there is no kissing. *)
  let kisses1 yy xx = X.(map2 (fun x y -> (x = Carol && y = Dave) || (x = Dave && y = Carol)) xx yy)
  let kisses2 yy xx = marriedto xx yy
  let kisses3 yy xx = X.(map2 (fun x y -> false) xx yy)
  
(* Actually, each husband loves only his wife and Frank also loves the women.
   In w2, all the men love Carol and Ella loves the wives.
   In w3, Frank loves everyone else. *)
  let loves1 yy xx = X.(map2 (fun x y -> (is_male x && are_married(x,y)) || (x = Frank && not (is_male y))) xx yy)
  let loves2 yy xx = X.(map2 (fun x y -> (is_male x && y = Carol) || (x = Ella && is_a_wife y)) xx yy)
  let loves3 yy xx = X.(map2 (fun x y -> x = Frank && x <> y) xx yy)
end

module Test(S : SEMANTICS) : sig end = struct
  type result = True | False | Fail
  let print_result res = match res with True -> print_string "true" | False -> print_string "false" | Fail -> print_string "failure"

  let check name expected expr =
    (match (try Some (S.run expr) with Not_found -> None) with
      | Some true -> if expected = True then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got true but expected "; print_result expected; print_newline (); false end
      | Some false -> if expected = False then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got false but expected "; print_result expected; print_newline (); false end
      | None -> if expected = Fail then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got failure but expected "; print_result expected; print_newline (); false end)
(*
    with List.Short_list -> begin print_string "Sentence \""; print_string name; print_string "\" failed: got Short_list but expected "; print_result expected; print_newline (); false end
    with Failure "Unimplemented" -> begin print_string "Sentence \""; print_string name; print_endline "\" unimplemented."; true end
*)

  let dynamic res = if S.dynamic then res else Fail

  let truth = S.(male bill)
  let falsehood = S.(female bill)
  let bool_results =
  [ check "true" True truth
  ; check "false" False falsehood
  ; check "true and true" True S.(truth &&& truth)
  ; check "true and false" False S.(truth &&& falsehood)
  ; check "false and true" False S.(falsehood &&& truth)
  ; check "false and false" False S.(falsehood &&& falsehood)
  ; check "true or true" True S.(truth ||| truth)
  ; check "true or false" True S.(truth ||| falsehood)
  ; check "false or true" True S.(falsehood ||| truth)
  ; check "false or false" False S.(falsehood ||| falsehood)
  ; check "true >>> true" True S.(truth >>> truth)
  ; check "true >>> false" False S.(truth >>> falsehood)
  ; check "false >>> true" True S.(falsehood >>> truth)
  ; check "false >>> false" True S.(falsehood >>> falsehood)
  ]
  let () = print_newline(); print_int (List.count not bool_results); print_endline " boolean test(s) failed."

  let results =
  [ check "1. Bill is male" True S.(male bill)
  ; check "2. Bill is female" False S.(female bill)
  ; check "3. Bill isn't female" True S.(~~~ (female bill))
  ; check "4. Carol didn't leave" False S.(~~~ (left carol))
  ; S.extensional || check "5. Maybe Carol didn't leave" True S.(maybe (~~~ (left carol)))
  ; S.extensional || check "6. Maybe Ann didn't leave" False S.(maybe (~~~ (left ann)))

  ; check "7. Some x. x is male" True S.(some 'x' (male getx))
  ; check "8. Some x. x isn't female" True S.(some 'x' (~~~ (female getx)))
  ; check "9. Some x. x left" True S.(some 'x' (left getx))
  ; check "10. Some x. x didn't leave" False S.(some 'x' (~~~ (left getx)))
  ; check "11. Every x. x left" True S.(every 'x' (left getx))
  ; check "12. Every x. x is female" False S.(every 'x' (female getx))
  ; check "13. Every x. x isn't male" False S.(every 'x' (~~~ (male getx)))
  ; check "14. (Some x. x is male) and Ann is female" True S.(some 'x' (male getx) &&& female ann)
  ; check "15. Some x. (x is male and Ann is female)" True S.(some 'x' (male getx &&& female ann))

  ; check "16. Some x. (x is male and x is female)" False S.(some 'x' (male getx &&& female getx))
  ; check "17. Some x. (x is male) and Some x. x is female" True S.(some 'x' (male getx) &&& some 'x' (female getx))

  ; check "18. Some x. (x is male and Some y. y is male)" True S.(some 'x' (male getx &&& some 'y' (male gety)))
  ; check "19. Some x. (x is male and Some y. y is female)" True S.(some 'x' (male getx &&& some 'y' (female gety)))
  ; check "20. Some x. (x is male and Some y. x is male)" True S.(some 'x' (male getx &&& some 'y' (male getx)))
  ; check "21. Some x. (x is male and Some y. x is female)" False S.(some 'x' (male getx &&& some 'y' (female getx)))
  ; check "22. Some x. (x is male and Some y. x isn't female)" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx))))
  ; check "23. Some x. (x is male and Some x. x is female)" True S.(some 'x' (male getx &&& some 'x' (female getx)))

  ; check "24. Some x. (x is male) and Some y. (y is female and Bill is male)" True S.(some 'x' (male getx) &&& some 'y' (male gety &&& male bill))
  ; check "25. Some x. (x is male and Some y. (y is female and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& male bill)))
  ; check "26. Some x. (x is male and Some y. (y is male and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& male bill)))
  ; check "27. Some x. (x is male and Some y. (x is female and Bill is male))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& male bill)))
  ; check "28. Some x. (x is male and Some y. (x isn't female and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx) &&& male bill)))
  ; check "29. Some x. (x is male and Some y. (x is male and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& male bill)))

  ; check "30. Some x. (x is male and Some y. (y is female and x isn't female))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& ~~~ (female getx))))
  ; check "31. Some x. (x is male and Some y. (y is female and x is single))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& single getx)))
  ; check "32. Some x. (x is male and Some y. (y is female and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& ~~~ (single getx))))
  ; check "33. Some x. (x is male and Some y. (y is male and x is single))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& single getx)))
  ; check "34. Some x. (x is male and Some y. (y is male and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& ~~~ (single getx))))

  ; check "35. Some x. (x is male and Some y. (x is female and x is single))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& single getx)))
  ; check "36. Some x. (x is male and Some y. (x is female and x isn't single))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& ~~~ (single getx))))
  ; check "37. Some x. (x is male and Some y. (x is male and x is single))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& single getx)))
  ; check "38. Some x. (x is male and Some y. (x is male and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& ~~~ (single getx))))
  
  ; check "39. (Some x. male x) and x left" (dynamic True) S.(some 'x' (male getx) &&& left getx)
  ; check "40. (Some x. male x) and female x" (dynamic False) S.(some 'x' (male getx) &&& female getx)
  ; check "41. (Some x. male x) and Some y. female x" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx))
  ; check "42. (Some x. male x) and Some y. male x" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx))
  ; check "43. (Some x. male x) and Some y. (female x and male Bill)" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx &&& male bill))
  ; check "44. (Some x. male x) and Some y. (male x and male Bill)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx &&& male bill))
  ; check "45. (Some x. male x) and Some y. (female y and x isn't single)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (female gety &&& ~~~ (single getx)))
  ; check "46. (Some x. male x) and Some y. (female x and x isn't single)" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx &&& ~~~ (single getx)))
  ; check "47. (Some x. male x) and Some y. (male x and x isn't single)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx &&& ~~~ (single getx)))

  ; check "48. Every x. (male x and (Some y. married y x) -> loves y x)" (dynamic True) S.(every 'x' (male getx &&& some 'y' (marriedto gety getx) >>> loves gety getx))
  ; check "49. Every x. (male x and (Some y. married y x) -> kisses y x)" (dynamic False) S.(every 'x' (male getx &&& some 'y' (marriedto gety getx) >>> kisses gety getx))
  ; check "50. (Some x. (male x and Some y. married y x)) -> loves y x" (dynamic True) S.(some 'x' (male getx &&& some 'y' (marriedto gety getx)) >>> loves gety getx)
  ; check "51. (Some x. (male x and Some y. married y x)) -> kisses y x" (dynamic False) S.(some 'x' (male getx &&& some 'y' (marriedto gety getx)) >>> kisses gety getx)

  ; check "52. Every x. (male x and Some y. (female y and (x = frank or married y x)) -> loves y x)" (dynamic True) S.(every 'x' (male getx &&& some 'y' (female gety &&& (getx === frank ||| marriedto gety getx)) >>> loves gety getx))
  ; check "53. Every x. (male x and (x = frank or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& (getx === frank ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
  ; check "54. Every x. (male x and (Some y. (x = frank and female y) or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& (some 'y' (getx === frank &&& female gety) ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
  ; check "55. Every x. (male x and ((x = frank and Some y. female y) or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& ((getx === frank &&& some 'y' (female gety)) ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
  ]
  let () = print_newline(); print_int (List.count not results); print_endline " test(s) failed."

end

(* create lots of monads, so that we have them if we need them *)

module L = Monad.List
module R = Monad.Reader(struct type env = identifier -> entity end)
module R' = Monad.Reader(struct type env = identifier -> int end)
module Y = Monad.Reader(struct type env = world end)
module S = Monad.State(struct type store = identifier -> entity end)
module S' = Monad.State(struct type store = identifier -> int end)

module RY = struct
  include R.T(Y)
  include Monad.Derive.Reader_dbl(Y)(R.T(Y))
end
module YR = struct
  include Y.T(R)
  include Monad.Derive.Reader_dbl(R)(Y.T(R))
end
module LR = struct
  include L.T(R)
  include Monad.Derive.Reader(R)(L.T(R))
end
module LY = struct
  include L.T(Y)
  include Monad.Derive.Reader(Y)(L.T(Y))
end
module RL = struct
  include R.M(L)
  include Monad.Derive.List(L)(R.M(L))
end
module YL = struct
  include Y.M(L)
  include Monad.Derive.List(L)(Y.M(L))
end

module SY = struct
  include S.T(Y)
  include Monad.Derive.Reader(Y)(S.T(Y))
end
module YS = struct
  include Y.T(S)
  include Monad.Derive.State(S)(Y.T(S))
end
module LS = struct
  include L.T(S)
  include Monad.Derive.State(S)(L.T(S))
end
module LY = struct
  include L.T(Y)
  include Monad.Derive.Reader(Y)(L.T(Y))
end
module SL = struct
  include S.M(L)
  include Monad.Derive.List(L)(S.M(L))
end
module YL = struct
  include Y.M(L)
  include Monad.Derive.List(L)(Y.M(L))
end

module S'Y = struct
  include S'.T(Y)
  include Monad.Derive.Reader(Y)(S'.T(Y))
end
module YS' = struct
  include Y.T(S')
  include Monad.Derive.State(S')(Y.T(S'))
end
module LS' = struct
  include L.T(S')
  include Monad.Derive.State(S')(L.T(S'))
end
module S'L = struct
  include S'.M(L)
  include Monad.Derive.List(L)(S'.M(L))
end

module LRY = struct
  include L.T(RY)
  include Monad.Derive.Reader2(RY)(L.T(RY))
end
module LYR = struct
  include L.T(YR)
  include Monad.Derive.Reader2(YR)(L.T(YR))
end
module RLY = struct
  include R.M(LY)
  include Monad.Derive.List(LY)(R.M(LY))
  include Monad.Derive.Reader_dbl(LY)(R.M(LY))
end
module RYL = struct
  include R.M(YL)
  include Monad.Derive.List(YL)(R.M(YL))
  include Monad.Derive.Reader_dbl(YL)(R.M(YL))
end
module YLR = struct
  include Y.M(LR)
  include Monad.Derive.List(LR)(Y.M(LR))
  include Monad.Derive.Reader_dbl(LR)(Y.M(LR))
end
module YRL = struct
  include Y.M(RL)
  include Monad.Derive.List(RL)(Y.M(RL))
  include Monad.Derive.Reader_dbl(RL)(Y.M(RL))
end

module LSY = struct
  include L.T(SY)
  include Monad.Derive.Reader(SY)(L.T(SY))
  include Monad.Derive.State(SY)(L.T(SY))
end
module LYS = struct
  include L.T(YS)
  include Monad.Derive.Reader(YS)(L.T(YS))
  include Monad.Derive.State(YS)(L.T(YS))
end
module SLY = struct
  include S.M(LY)
  include Monad.Derive.List(LY)(S.M(LY))
  include Monad.Derive.Reader(LY)(S.M(LY))
end
module SYL = struct
  include S.M(YL)
  include Monad.Derive.List(YL)(S.M(YL))
  include Monad.Derive.Reader(YL)(S.M(YL))
end
module YLS = struct
  include Y.M(LS)
  include Monad.Derive.List(LS)(Y.M(LS))
  include Monad.Derive.State(LS)(Y.M(LS))
end
module YSL = struct
  include Y.M(SL)
  include Monad.Derive.List(SL)(Y.M(SL))
  include Monad.Derive.State(SL)(Y.M(SL))
end

module LS'Y = struct
  include L.T(S'Y)
  include Monad.Derive.Reader(S'Y)(L.T(S'Y))
  include Monad.Derive.State(S'Y)(L.T(S'Y))
end
module LYS' = struct
  include L.T(YS')
  include Monad.Derive.Reader(YS')(L.T(YS'))
  include Monad.Derive.State(YS')(L.T(YS'))
end
module S'LY = struct
  include S'.M(LY)
  include Monad.Derive.List(LY)(S'.M(LY))
  include Monad.Derive.Reader(LY)(S'.M(LY))
end
module S'YL = struct
  include S'.M(YL)
  include Monad.Derive.List(YL)(S'.M(YL))
  include Monad.Derive.Reader(YL)(S'.M(YL))
end
module YLS' = struct
  include Y.M(LS')
  include Monad.Derive.List(LS')(Y.M(LS'))
  include Monad.Derive.State(LS')(Y.M(LS'))
end
module YS'L = struct
  include Y.M(S'L)
  include Monad.Derive.List(S'L)(Y.M(S'L))
  include Monad.Derive.State(S'L)(Y.M(S'L))
end


(*
   A variety of semantics are provided. Here is the naming scheme:
   
   Sem1* is classic semantics with support for variable binding/anaphora.
   Sem5* would be the dynamic alternative of 1*. (not here provided, but
   discussed in comments.)
   You can't implement quantification in these,
   except by bringing in some of the mechanisms of a list/set component.
   (You'll create a box([entity]) and convert it to a box([bool]),
   then convert the latter to box(bool).)
   However, Haskell already provides the needed mechanisms in the basic Monad API (as the
   function Juli8 names `seq`), so we can do quantification without _explicitly
   invoking_ a ListT in our monadic stack.

   Sem2* and Sem 6* would be the intensionalized versions of those.
   (Not here provided, but Sem6* is discussed in comments.)

   Sem3* adds a List component to the stack to do quantification.
   Sem7* is the dynamic counterpart.

   Sem4* adds an (additional) Reader monad for intensionality.
   Sem8* is the dynamic counterpart.

   Within that broad organization, here are the sub-patterns:

   SemNa uses just a bool payload, so sent types are box(bool).
   SemNb makes sent types the Klesli variant of Na, so sent types are
   bool -> box(bool).
   SemNc uses instead a unit payload, which we can do when the monadic
   stack has a List or Option component; then false will be the monad's
   mzero, whereas truth will be instances of type box(unit) that aren't
   mzero.
   SemNd would be the Kleisli variant of Nc, as Nb is the Kleisli variant
   of Na.
   SemNe (only for dynamic) would use "topics" or sequences of entities being discussed
   as payloads, so sent types are box(topic). What we really provide
   here is the Kleisli variation of this (SemNf), so sent types = topic -> box(topic).
*)
 

module Sem1a = struct
  let dynamic = false
  let extensional = true

  (* We use monad R, with env = var -> entity.
     Types of sentences are env -> bool. *)
  module X = R
  type noun = entity X.t
  type sent = bool X.t
  let run (xx : sent) : bool = X.(run xx env0 = true)
  let getx = X.(asks (lookup 'x'))
  let gety = X.(asks (lookup 'y'))
  let getz = X.(asks (lookup 'z'))
  let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)

  let (~~~) xx = X.(map not xx)
  let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
  let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
  let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)

  let some c (body : sent) =
    let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
    let (bsb : bool list X.t) = X.seq bbs in
    let (bb : bool X.t) = X.map (exists ident) bsb in
    bb
  let every c (body : sent) =
    let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
    let (bsb : bool list X.t) = X.seq bbs in
    let (bb : bool X.t) = X.map (for_all ident) bsb in
    bb

  module F = Facts(X)
  let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
  let (===) xx yy = X.(map2 (=) xx yy)
  let male = F.male let female = F.female let single = F.single let left = F.left1
  let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
  let thinks pp xx = failwith "Unimplemented"
  let maybe pp = failwith "Unimplemented"
end (* Sem1a *)

module Sem1b = struct
  let dynamic = false
  let extensional = true

  (* We again use monad R, with env = var -> entity.
     This variant defines sentence meanings as Kleisli arrows, that is:
       type sent = bool -> bool X.t
     or equivalently, bool -> (env -> bool). A true sentence takes any bool
     input to a boxed version of that input (so truth = mid), and a false
     sentence takes any input to mid false.
     This more closely parallels the dynamic semantics (though it should not,
     just on account of that structural similarity, be itself counted as dynamic).
     It also brings the boolean operations closer to monadic primitives.
  *)
  module X = R
  type noun = entity X.t
  type sent = bool -> bool X.t
  let run (k : sent) : bool = X.(run (k true) env0 = true)
  let getx = X.(asks (lookup 'x'))
  let gety = X.(asks (lookup 'y'))
  let getz = X.(asks (lookup 'z'))
  let let_ c (xx : noun) (body : sent) = fun b -> X.(xx >>= fun x -> shift (insert c x) (body b))

  let (~~~) k = fun b -> X.(if b then map not (k true) else mid false)
  let (&&&) k j = X.(k >=> j)
  let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
  let (>>>) k j = ~~~ k ||| j
(* or
  let (|||) xx yy = fun b -> X.(xx b >>= fun b' -> if b' then mid true else yy b)
  let (>>>) xx yy = fun b -> X.(xx b >>= fun b' -> if not b' then mid true else yy b)
  let (>>>) k j = ~~~ (k &&& ~~~ j)
*)

  let some c (body : sent) = fun b ->
    let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
    let (bsb : bool list X.t) = X.seq bbs in
    let (bb : bool X.t) = X.map (exists ident) bsb in
    bb
  let every c (body : sent) = fun b ->
    let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
    let (bsb : bool list X.t) = X.seq bbs in
    let (bb : bool X.t) = X.map (for_all ident) bsb in
    bb

  module F = Facts(X)
  let to_kleisli xx = fun b -> X.(xx >>= fun b' -> mid (b && b'))
  let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
  let (===) xx yy = to_kleisli X.(map2 (=) xx yy)
  let male = to_kleisli % F.male let female = to_kleisli % F.female let single = to_kleisli % F.single let left = to_kleisli % F.left1
  let marriedto yy xx = to_kleisli (F.marriedto yy xx) let saw yy xx = to_kleisli (F.saw1 yy xx) let kisses yy xx = to_kleisli (F.kisses1 yy xx) let loves yy xx = to_kleisli (F.loves1 yy xx)
  let thinks pp xx = fun b -> failwith "Unimplemented"
  let maybe pp = fun b -> failwith "Unimplemented"
end (* Sem1b *)

module Sem3a = struct
  let dynamic = false
  let extensional = true

  (* We could use either monad RL or LR, with type env = var -> entity.
     Their box type is the same: env -> ['a]
     However, the types of SL and LS differ, and the latter is more suitable for (some of) the dynamic version(s). So to keep things maximally parallel, we'll use LR here.
     We use the box type in two ways: first, we use a box(entity) to compute whether a matrix
     clause is satisfied by a bound pronoun, where entity ranges over the whole domain.
     Second, it is convenient and more consonant with later strategies
     to re-use the same monad for sentence types (rather than using a simpler monad
     that lacks a List component). Here we will let the types of sentences
     be box(bool), that is: env -> [bool]. We will understand the sentence to be true
     if there are ANY truths in the resulting list. A list of all falses is treated
     the same as an empty list. Sem3c, below, eliminates this artifact by changing
     the sentence type to box(unit). Then truths (rel to an env) are [();...] and
     falsehoods are [].
*)
  module X = LR
  type noun = entity X.t
  type sent = bool X.t
  let run (xx : sent) : bool = X.(any_truths (run xx env0))
  (* lift an 'a list to a single 'a X.t *)
  let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
  let getx = X.(asks (lookup 'x'))
  let gety = X.(asks (lookup 'y'))
  let getz = X.(asks (lookup 'z'))
  let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)

  let (~~~) xx = X.(map not xx)
  let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
  let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
  let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)

  (* On this semantics, `some c body` is a list of the boolean outcomes for body for each assignment to c.
     That matches our convention for sentence types, where any truth in the list means the sentence is true.
     However, we can't then define `every c body === ~~~ (some c (~~~ body))`, because it's only when the rhs is entirely true that the lhs should be true.
     In later semantics, the duality of `some` and `every` will be restored.
  *)
  let some c (body : sent) = X.(let_ c (mids domain) body)
  let every c body = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx) (* could alternatively return [true] instead of xs *)

  module F = Facts(X)
  let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
  let (===) xx yy = X.(map2 (=) xx yy)
  let male = F.male let female = F.female let single = F.single let left = F.left1
  let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
  let thinks pp xx = failwith "Unimplemented"
  let maybe pp = failwith "Unimplemented"
end (* Sem3a *)

(* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
   Not here implemented. *)

(* Variant of Sem3a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
module Sem3c = struct
  let dynamic = false
  let extensional = true

  (* We use monad LR as above, with same env = var -> entity and box type = env -> ['a].
     We again use box(entity) to compute whether matrix clauses are satisfied by
     bound pronouns; but now we use box(unit) for the types of sentences.
     Truths (rel to an env) are [();...] and falsehood is [].
  *)
  module X = LR
  type noun = entity X.t
  type sent = unit X.t
  let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
  (* lift an 'a list to a single 'a X.t *)
  let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
  let getx = X.(asks (lookup 'x'))
  let gety = X.(asks (lookup 'y'))
  let getz = X.(asks (lookup 'z'))
  let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
  let to_unit (x : bool) : unit X.t = X.guard x

  let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
  let (&&&) xx yy = X.(xx >> yy)
  let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
  let (>>>) xx yy = X.(~~~ xx ++ yy)
(* or
  let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
*)

  let some c (body : sent) = X.(let_ c (mids domain) body)
  let every c (body : sent) = ~~~ (some c (~~~ body))

  module F = Facts(X)
  let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
  let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
  let male xx = X.(F.male xx >>= to_unit)
  let female xx = X.(F.female xx >>= to_unit)
  let single xx = X.(F.single xx >>= to_unit)
  let left xx = X.(F.left1 xx >>= to_unit)
  let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
  let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
  let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
  let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
  let thinks pp xx = failwith "Unimplemented"
  let maybe pp = failwith "Unimplemented"
end (* Sem3c *)

(* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
   Not here implemented. *)

(* Add intensionality to 2a *)
module Sem4a = struct
  let dynamic = false
  let extensional = false

  (* Using monad LRY, with type env = var -> entity.
     Box type is env -> world -> ['a]
     Types of sentences are env -> world -> [bool]. *)
  module X = LRY
  type noun = entity X.t
  type sent = bool X.t
  let run xx = X.(any_truths (run xx env0 Actual))
  (* lift an 'a list to a single 'a X.t *)
  let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
  let getx = X.(asks (lookup 'x'))
  let gety = X.(asks (lookup 'y'))
  let getz = X.(asks (lookup 'z'))
  let getw = X.(uask) (* get world from the underlying Y monad *)
  (* select an intranstive verb based on the world *)
  let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
  (* select a transitive verb based on the world *)
  let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
  let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
  let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)

  let (~~~) xx = X.(map not xx)
  let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
  let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
  let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)

  let some c (body : sent) = X.(let_ c (mids domain) body)
  let every c (body : sent) = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx)

  module F = Facts(X)
  let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
  let (===) xx yy = X.(map2 (=) xx yy)
  let male = F.male let female = F.female let single = F.single
  let left xx = select1 F.left1 F.left2 F.left3 xx
  let saw yy xx = select2 F.saw1 F.saw2 F.saw3 yy xx
  let marriedto = F.marriedto
  let kisses yy xx = select2 F.kisses1 F.kisses2 F.kisses3 yy xx
  let loves yy xx = select2 F.loves1 F.loves2 F.loves3 yy xx
  let thinks pp xx = failwith "Unimplemented"
  let maybe (body : sent) : sent =
    let (yy : R.env -> Y.env -> bool list) = fun e w ->
      let body_int = List.map (fun w' -> any_truths (X.run (letw w' body) e w)) modal_domain in
      body_int (* can just use body's intension as the result of `maybe body` *) in
    Obj.magic yy
end (* Sem4a *)

(* Sem4b would convert Sem4a into having sentence meanings be Kleisli arrows, as Sem1b did.
   Not here implemented. *)

(* Add intensionality to 2c *)
module Sem4c = struct
  let dynamic = false
  let extensional = false

  (* Using monad LRY, with type env = var -> entity.
     Box type is env -> world -> ['a]
     Types of sentences are env -> world -> [unit]. *)
  module X = LRY
  type noun = entity X.t
  type sent = unit X.t
  let run xx = X.(not (List.is_null (run xx env0 Actual)))
  (* lift an 'a list to a single 'a X.t *)
  let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
  let getx = X.(asks (lookup 'x'))
  let gety = X.(asks (lookup 'y'))
  let getz = X.(asks (lookup 'z'))
  let getw = X.(uask) (* get world from the underlying Y monad *)
  (* select an intranstive verb based on the world *)
  let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
  (* select a transitive verb based on the world *)
  let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
  let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
  let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
  let to_unit (x : bool) : unit X.t = X.guard x

  let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
  let (&&&) xx yy = X.(xx >> yy)
  let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
  let (>>>) xx yy = X.(~~~ xx ++ yy)
(* or
  let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
*)

  let some c (body : sent) = X.(let_ c (mids domain) body)
  let every c (body : sent) = ~~~ (some c (~~~ body))

  module F = Facts(X)
  let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
  let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
  let male xx = X.(F.male xx >>= to_unit)
  let female xx = X.(F.female xx >>= to_unit)
  let single xx = X.(F.single xx >>= to_unit)
  let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
  let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
  let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
  let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
  let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
  let thinks pp xx = failwith "Unimplemented"
  let maybe (body : sent) : sent =
    let (yy : R.env -> Y.env -> unit list) = fun e w ->
      let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) e w) modal_domain in
      if any_truths body_int then [()] else [] in
    Obj.magic yy
end (* Sem4c *)

(* Sem4d would convert Sem4c into having sentence meanings be Kleisli arrows, as Sem1b did.
   Not here implemented. *)


(* Dynamic version of Sem3c *)
module Sem7c = struct
  let dynamic = true
  let extensional = true

  (* This needs to use monad SL, with store = var -> entity
     and box type = store -> ['a,store]
     Sentence meaning is box(unit).
     Later strategies with more complex sentence meanings and stores
     may be able to use monad LS, with box type store -> ['a],store
  *)
  module X = SL
  type noun = entity X.t
  type sent = unit X.t
  let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
  (* lift an 'a list to a single 'a X.t *)
  let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
  let getx = X.(gets (lookup 'x'))
  let gety = X.(gets (lookup 'y'))
  let getz = X.(gets (lookup 'z'))
  let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
  let to_unit (x : bool) : unit X.t = X.guard x

  let (~~~) (xx : sent) : sent =
    let yy : S.store -> (unit * S.store) list = fun s -> if List.is_null (X.run xx s) then [(),s] else [] in
    Obj.magic yy  (* this is an identity function that changes the type of yy to a unit X.t *)
  let (&&&) xx yy = X.(xx >> yy)
  let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
  let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))

(*
    This would propagate effects out of the disjuncts, so that for example after
      "Some y. (x = frank and female y) or Some y. married y x"
    "y" would be available for anaphor:
      let (|||) xx yy = X.(xx ++ (~~~ xx >> yy))

    This wouldn't propagate effects from antecedent to consequent, so that for example
      "(Some y. marriedto y bill) >>> female gety"
    has a failed lookup on "y":
      let (>>>) xx yy = X.(~~~ xx ++ yy)
*)

  let some c (body : sent) = X.(let_ c (mids domain) body)
  let every c (body : sent) = ~~~ (some c (~~~ body))

  module F = Facts(X)
  let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
  let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
  let male xx = X.(F.male xx >>= to_unit)
  let female xx = X.(F.female xx >>= to_unit)
  let single xx = X.(F.single xx >>= to_unit)
  let left xx = X.(F.left1 xx >>= to_unit)
  let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
  let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
  let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
  let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
  let thinks pp xx = failwith "Unimplemented"
  let maybe pp = failwith "Unimplemented"
end (* Sem7c *)


(* Dynamic version of Sem4c / Add intensionality to Sem7c *)
module Sem8c = struct
  let dynamic = true
  let extensional = false

  (* This needs to use monad SLY, with store = var -> entity
     and box type = store -> world -> ['a,store]
     Sentence meaning is box(unit).
     Later strategies with more complex sentence meanings and stores
     may be able to use monad LSY, with box type store -> world -> ['a],store
  *)
  module X = SLY
  type noun = entity X.t
  type sent = unit X.t
  let run (xx : sent) : bool = X.(not (List.is_null (run xx env0 Actual)))
  (* lift an 'a list to a single 'a X.t *)
  let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
  let getx = X.(gets (lookup 'x'))
  let gety = X.(gets (lookup 'y'))
  let getz = X.(gets (lookup 'z'))
  let getw = X.(ask) (* get world from the underlying Y monad *)
  (* select an intranstive verb based on the world *)
  let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
  (* select a transitive verb based on the world *)
  let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
  let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
  let letw world (body : sent) = X.(shift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
  let to_unit (x : bool) : unit X.t = X.guard x
(*
  let peek msg () = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s; print_string ", y="; print_lookup 'y' s; print_string ", z="; print_lookup 'z' s; print_newline (); mid () end)
*)

  let (~~~) (xx : sent) : sent =
    let yy : S.store -> Y.env -> (unit * S.store) list = fun s w -> if List.is_null (X.run xx s w) then [(),s] else [] in
    Obj.magic yy  (* this is an identity function that changes the type of yy to a unit X.t *)

  let (&&&) xx yy = X.(xx >> yy)
  let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
  let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))

  let some c (body : sent) = X.(let_ c (mids domain) body)
  let every c (body : sent) = ~~~ (some c (~~~ body))

  module F = Facts(X)
  let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
  let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
  let male xx = X.(F.male xx >>= to_unit)
  let female xx = X.(F.female xx >>= to_unit)
  let single xx = X.(F.single xx >>= to_unit)
  let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
  let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
  let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
  let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
  let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
  let thinks pp xx = failwith "Unimplemented"
  let maybe (body : sent) : sent =
    let (yy : S.store -> Y.env -> (unit * S.store) list) = fun s w ->
      let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) s w) modal_domain in
      if any_truths body_int then [(),s] else [] in
    Obj.magic yy
end (* Sem8c *)

(* Sem8c seems adequate for much of the phenomena GSV are examining, and is substantially simpler than their own semantics. Sem8c doesn't have their "pegs" and complex two-stage function from vars to referents.
   Next we develop some semantics that are closer to their actual presentation. *)

(* This develops Sem7c using in part the Kleisli strategy from Sem1b. *)
module Sem7f = struct
  let dynamic = true
  let extensional = true

  (* Let a topic be sequence of entities introduced into conversation (GSV's pegs -> entities, with pegs construed as positions in the sequence).
     Then let store = var -> int (that is, position in the topic)
     Then we can use monad LS', with box type = store -> ['a],store
     And sentence meanings are Kleisli arrows: topic -> box(topic). The list component
     in the type captures indeterminacy in what objects are being discussed (introduced
     by quantifiers). Truths (relative to a initial store and topic) result in
     non-empty topic lists; falsehoods in empty ones.
     Our stores/envs are GSV's refsys r; our topics are their g.
     Notice that GSV make their "information states" homogenous wrt r; this corresponds
     to our result type having stores _outside_ the list.
     GSV's meaning types are [store * topic * world] -> [store * topic * world], but
     as noted the homogeneity wrt store would permit also:
       store * [topic * world] -> store * [topic * world].
     Our meaning types (once we add worlds in 6e, below) will be:
       topic -> (store -> world -> ([topic] * store))
     We count a world as eliminated when it results in an empty list of topics.
     Note that our Sem8f doesn't yet properly handle Veltman's "might"; see remarks below.
  *)
  type topic = entity list
  let topic0 = []
  module X = LS'
  type noun = (topic -> entity) X.t
  type sent = topic -> topic X.t
  let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0))))
  (* lift an 'a list to a single 'a X.t *)
  let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
  let get_nth n topic = try List.nth topic n with List.Short_list -> failwith ("can't get item "^string_of_int n^" of "^List.string_of_list string_of_entity topic)
  let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
  let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
  let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
  let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))

  (* All logical operations except &&& and some are "effect islands", with the exception that effects of the antecedent
     of a conditional are visible in that conditional's consequent. *)

  let (~~~) (k : sent) : sent = fun top ->
    let yy : S'.store -> topic list * S'.store = fun s -> if List.is_null (fst (X.run (k top) s)) then ([top],s) else ([],s) in
    Obj.magic yy  (* this is an identity function that changes the type of yy to a topic X.t *)
  let (&&&) k j = X.(k >=> j)
  let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
  let (>>>) k j = X.(~~~ (k >=> ~~~ j))

  (* This properly handles `some` as GSV do, by only joining the results
     _after_ updating them on body(extended topic). See GSV pp. 28-9. *)
  let some c (body : sent) : sent = fun top ->
    let n = length top in
    let aux ent = X.(let_ c n body) (List.snoc top ent) in
    let domain' = List.map aux domain in
    X.join (mids domain')

  let every c (body : sent) = ~~~ (some c (~~~ body))

  module F = Facts(X)
  let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
  let wrap name = X.(mid (const name))
  let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
  let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
  let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
  let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
  let male (xx : noun) : sent = wrap1 F.male xx
  let female xx = wrap1 F.female xx
  let single xx = wrap1 F.single xx
  let left xx = wrap1 F.left1 xx
  let marriedto yy xx = wrap2 F.marriedto yy xx
  let saw yy xx = wrap2 F.saw1 yy xx
  let kisses yy xx = wrap2 F.kisses1 yy xx
  let loves yy xx = wrap2 F.loves1 yy xx
  let thinks pp xx = fun top -> failwith "Unimplemented"
  let maybe pp = fun top -> failwith "Unimplemented"
end (* Sem7f *)

(* Add intensionality to Sem7f. See comments there. *)
module Sem8f = struct
  let dynamic = true
  let extensional = false

  type topic = entity list
  let topic0 = []
  module X = LS'Y
  type noun = (topic -> entity) X.t
  type sent = topic -> topic X.t
  let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0 Actual))))
  (* lift an 'a list to a single 'a X.t *)
  let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
  let get_nth n topic = try List.nth topic n with List.Short_list -> failwith ("can't get item "^string_of_int n^" of "^List.string_of_list string_of_entity topic)
  let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
  let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
  let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
  let getw = X.(ask) (* get world from the underlying Y monad *)
  (* select an intranstive verb based on the world *)
  let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
  (* select a transitive verb based on the world *)
  let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
  let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
  let letw world (body : sent) : sent = fun top -> X.(shift (fun _ -> world) (body top)) (* shift the "env" of the underlying Y monad *)

  (* debugging *)
  let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#"
  let print_lookup sought env top = print_string (lookup_string sought env top)
  let peek msg top = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s top; print_string ", y="; print_lookup 'y' s top; print_string ", z="; print_lookup 'z' s top; print_newline (); mid top end)
  (* variant of run that uses a non-empty initial topic list, and displays entire result, not just whether it's true *)
  let run' (k : sent) ?(w=Actual) (tops : topic list) =
    let n = List.length (List.head tops) in
    let env = match n with
    | 1 -> insert 'x' 0 env0
    | 2 -> insert 'x' 0 (insert 'y' 1 env0)
    | 3 -> insert 'x' 0 (insert 'y' 1 (insert 'z' 2 env0))
    | _ -> failwith ("can't run' topics of length " ^ string_of_int n) in
    assert(for_all (fun top -> List.length top = n) tops);
    X.(run (mids tops >>= k) env w)

  let (~~~) (k : sent) : sent = fun top ->
    let yy : S'.store -> Y.env -> topic list * S'.store = fun s w -> if List.is_null (fst (X.run (k top) s w)) then ([top],s) else ([],s) in
    Obj.magic yy  (* this is an identity function that changes the type of yy to a topic X.t *)
  let (&&&) k j = X.(k >=> j)
  let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
  let (>>>) k j = X.(~~~ (k >=> ~~~ j))

  let some c (body : sent) : sent = fun top ->
    let n = length top in
    let aux ent = X.(let_ c n body) (List.snoc top ent) in
    let domain' = List.map aux domain in
    X.join (mids domain')

  let every c (body : sent) = ~~~ (some c (~~~ body))

  module F = Facts(X)
  let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
  let wrap name = X.(mid (const name))
  let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
  let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
  let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
  let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
  let male (xx : noun) : sent = wrap1 F.male xx
  let female xx = wrap1 F.female xx
  let single xx = wrap1 F.single xx
  let left xx = wrap1 (select1 F.left1 F.left2 F.left3) xx
  let marriedto yy xx = wrap2 F.marriedto yy xx
  let saw yy xx = wrap2 (select2 F.saw1 F.saw2 F.saw3) yy xx
  let kisses yy xx = wrap2 (select2 F.kisses1 F.kisses2 F.kisses3) yy xx
  let loves yy xx = wrap2 (select2 F.loves1 F.loves2 F.loves3) yy xx
  let thinks pp xx = failwith "Unimplemented"
  let maybe (body : sent) : sent = fun top ->
    let (yy : S'.store -> Y.env -> topic list * S'.store) = fun s w ->
      let body_int = List.map (fun w' -> not @@ List.is_null @@ fst @@ X.run (letw w' body top) s w) modal_domain in
      if any_truths body_int then [top],s else [],s in
    Obj.magic yy
  (* This implementation of `maybe` doesn't yet exactly capture Veltman's "might". It isn't a holistic filter:
     it examines topics one-by-one and will eliminate any where they (considered in isolation) make body impossible.
     Hence, if some of the possible referents for x are essentially not-body, and others are possibly-body, after
     updating on _this_ implementation of `maybe body`, we'll be left with only the latter. On Veltman's semantics,
     otoh, we'd be left with the whole original information state.
     To capture Veltman's semantics properly, we'd need to remove the List component from our monad stack, and use
     [topic] as our payloads, so that sent types would then be: [topic] -> S'Y([topic]). All of the operations except
     for `maybe` would then have to emulate the operations of the List monad by hand (manually performing catmap etc).
     But `maybe` could examine the [topic] as a whole and decide whether to return box(it) or box([]).
     This would be to go back to the Sem5/Sem6 choices of monads (without list), and to implement the handling of lists
     by hand, as we did in the Sem1/Sem2 strategies.

     Additionally, we haven't tried here to handle non-rigid noun-types. That's why we can have sent types be:
         topic (or [topic]) -> store -> world -> ([topic], store)
     the input topic doesn't depend on what the world is. GSV's types are suited to handle non-rigid noun types,
     since they are instead using an analogue of (world * topic) -> store -> ([world,topic], store). We could follow suit,
     removing the Reader monad implementing Intensionality from our stack and implementing that by hand, too. Another
     strategy would be to continue using a Reader monad but not by merging it into our main monad stack, instead using
     values of _that_ box type as _payloads for_ our main box type. This echoes a question raised by Dylan in seminar:
     why must we combine the monads only by way of "stacking them" into a single monad? As Jim said in seminar, it's not
     obvious one must do so, it just seems most natural. The strategy being evisaged now would at least in part follow
     Dylan's suggestion. We'd let our sentence types then be:
         intensionality_box([topic]) -> state_plus_intensionality_box(intensionality_box([topic]))
       = intensionality_box([topic]) -> store -> world -> (intensionality_box([topic]) * store)
     In that case, I think we could once again merge the list component into the intensionality_box type, getting:
         intens_list_box(topic) -> state_intens_box(intens_list_box(topic))
       = intens_list_box(topic) -> store -> world -> (intens_list_box(topic) * store)
       = (world -> [topic]) -> store -> world -> ((world -> [topic]) * store)
     That looks like a pretty complicated type, and might not seem an improvement over GSV's own system. But its advantage is that
     the implementation of its operations would so closely parallel the other semantic strategies illustrated above.
     Testifying to the "modularity" of monads, which we have been recommending as one of their prominent virtues.
  *)

end (* Sem8f *)

module TestAll = struct
  print_endline "\nTesting Sem1a";;
  module T1a = Test(Sem1a);;
  print_endline "\nTesting Sem1b";;
  module T1b = Test(Sem1b);;
  print_endline "\nTesting Sem3a";;
  module T3a = Test(Sem3a);;
  print_endline "\nTesting Sem3c";;
  module T3c = Test(Sem3c);;
  print_endline "\nTesting Sem4a";;
  module T4a = Test(Sem4a);;
  print_endline "\nTesting Sem4c";;
  module T4c = Test(Sem4c);;
  print_endline "\nTesting Sem7c";;
  module T7c = Test(Sem7c);;
  print_endline "\nTesting Sem7f";;
  module T7f = Test(Sem7f);;
  print_endline "\nTesting Sem8c";;
  module T8c = Test(Sem8c);;
  print_endline "\nTesting Sem8f";;
  module T8f = Test(Sem8f);;
  print_newline ()
end

(*
    One can't test the broken vase case by comparing the _truth_ of any sentences.
    The difference is in whether the sentences have meanings that are "supported by"
    the same informtation states. Compare in our model:
      (i) Someone kissed me. She might have stayed.
    and:
      (ii) Someone who might have stayed kissed me.
    Recall that in our model Ann leaves in every world, but Carol stays in some (non-actual)
    world. If my background information settles that I was kissed by either Ann or Carol,
    then I'm in a position to assert (i), since after the first clause it's left open
    that the referent be either woman. But it doesn't put me in a position to assert (ii),
    since that implies I was kissed by Carol. So far as truth-value goes,
    if Carol kissed me both sentences are true, and if Ann did then both sentences are false.
*)