X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fgsv.ml;h=6f4c4166fde833f701b28dbb7dfaf06f569456d3;hp=abd305f69573dbd4c7e0485734d06147b662a0ce;hb=a0eb18e702862266fdc8a7d935d6cc33821fdf4a;hpb=9ef8c8a5c822f05b63ff23c92980a103efc85967

diff --git a/code/gsv.ml b/code/gsv.ml
index abd305f6..6f4c4166 100644
--- a/code/gsv.ml
+++ b/code/gsv.ml
@@ -1,1001 +1,94 @@
-(* GSV monadically 13 April 2015 *)
-
-type identifier = char
-let any_truths (xs : 'a list) : bool = List.exists ident xs
-let all_truths (xs : 'a list) : bool = List.for_all ident xs
-
-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 | Other | Another
-let modal_domain = [Actual; Other; Another]
-
-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)
-
-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.
-*)
-
-  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
-
-
-
-
-
-
-module R = Monad.Reader(struct type env = identifier -> entity end)
-module S = Monad.State(struct type store = identifier -> entity end)
-module S' = Monad.State(struct type store = identifier -> int end)
-module R' = Monad.Reader(struct type env = identifier -> int end)
-
-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
-
-module Y = Monad.Reader(struct type env = world end)
-
-module L = Monad.List
-
-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
-
-
-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 Sem2a = 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 the dynamic version. 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. Sem2c, 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 (* Sem2a *)
-
-(* Sem2b would convert Sem2a into having sentence meanings be Kleisli arrows, as Sem1b did.
-   Not here implemented. *)
-
-(* Variant of Sem2a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
-module Sem2c = 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 (* Sem2c *)
-
-(* Sem2d would convert Sem2c into having sentence meanings be Kleisli arrows, as Sem1b did.
-   Not here implemented. *)
-
-(* Add intensionality to 2a *)
-module Sem3a = 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 = Other 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 = Other 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 (* Sem3a *)
-
-(* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
-   Not here implemented. *)
-
-(* Add intensionality to 2c *)
-module Sem3c = 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 = Other 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 = Other 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 (* Sem3c *)
-
-(* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
-   Not here implemented. *)
-
-
-(* Dynamic version of Sem2c *)
-module Sem5c = 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 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 -> (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 (* Sem5c *)
-
-
-(* Dynamic version of Sem3c / Add intensionality to Sem5c *)
-module Sem6c = 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 = Other 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 = Other 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 (* Sem6c *)
-
-(* Sem6c seems adequate for the phenomena GSV are examining, and is substantially simpler than their own semantics. Sem6c 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 Sem5c using in part the strategies from Sem1b. *)
-module Sem5e = 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.
-  *)
-  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))
-(*
-  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)
-*)
-
-  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) (* TODO how about (k >>> j) >>> 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))
-
-(* TODO
-  let some c body = X.(mids domain >>= fun x -> modify (insert c x) body >>= guard >> mid x)
-  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)
-*)
-
-  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 (* Sem5e *)
-
-(* Add intensionality to Sem5e *)
-module Sem6e = 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 = Other 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 = Other 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 *)
-
-  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
-end (* Sem6e *)
-
-module TestAll = struct
-  print_endline "\nTesting Sem1a";;
-  module T1a = Test(Sem1a);;
-  print_endline "\nTesting Sem1b";;
-  module T1b = Test(Sem1b);;
-  print_endline "\nTesting Sem2a";;
-  module T2a = Test(Sem2a);;
-  print_endline "\nTesting Sem2c";;
-  module T2c = Test(Sem2c);;
-  print_endline "\nTesting Sem3a";;
-  module T3a = Test(Sem3a);;
-  print_endline "\nTesting Sem3c";;
-  module T3c = Test(Sem3c);;
-  print_endline "\nTesting Sem5c";;
-  module T5c = Test(Sem5c);;
-  print_endline "\nTesting Sem5e";;
-  module T5e = Test(Sem5e);;
-  print_endline "\nTesting Sem6c";;
-  module T6c = Test(Sem6c);;
-  print_endline "\nTesting Sem6e";;
-  module T6e = Test(Sem6e);;
-  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.
-*)
+open List
+
+type predicate = string
+type ent = Alice | Bob | Carl
+type world = W1 | W2 | Hungry | Full
+type variable = string
+type term = Constant of ent | Var of variable
+type clause =   Pred of predicate * term
+              | Eq of term * term
+              | Conj of clause * clause
+              | Neg of clause
+              | Poss of clause
+              | Ex of string * clause
+type assignment = (variable * ent) list
+type poss = world * assignment
+type infostate = poss list
+
+let rec referent (i:poss) (t:term):ent = match (i,t) with
+    (i, Constant e) -> e
+  | ((w,(v',a)::g), Var v) -> if 0 == compare v v' then a else referent (w,g) t
+  (* warning: no error checking *)
+
+let extension (w:world) (p:predicate) (e:ent) = match (w,p,e) with
+    _, "woman", Alice -> true
+  | _, "man", Bob -> true
+  | _, "man", Carl -> true
+  | Hungry, "hungry", Alice -> true
+  | _, "enter", Bob -> true
+  | _, "enter", Carl -> true
+  | _, "sit", Alice -> true
+  | _, "sit", Bob -> true
+  | W1, "closet", Alice -> true
+  | W1, "guilty", Bob -> true
+  | W2, "closet", Carl -> true
+  | W2, "guilty", Carl -> true
+  | _,_,_ -> false
+
+let domain = [Alice; Bob; Carl]
+
+let rec update (s:infostate) (c:clause) = match c with
+    Pred (p,t) -> filter (fun (w,g) -> extension w p (referent (w,g) t)) s
+  | Eq (t1, t2) -> filter (fun i -> (referent i t1) == (referent i t2)) s
+  | Conj (c1, c2) -> update (update s c1) c2
+  | Neg c -> filter (fun i -> update [i] c == []) s
+  | Poss c -> filter (fun i -> update s c != []) s
+  | Ex (v,c) -> concat (map (fun (a:ent) -> 
+                               update (map (fun (w,g) -> (w,(v,a)::g)) s) c)
+                            domain)
+
+(* Basic examples *)
+let test1 = update [(W1,[])] (Ex ("x", (Pred ("man", Var "x"))))
+
+let test2 = update [(W1,[])] (Ex ("x", (Pred ("woman", Var "x"))))
+
+let test3 = update [(W1,[])] 
+                   (Ex ("x", (Ex ("y", (Conj (Pred ("man", (Var "x")),
+                                              Pred ("man", (Var "y"))))))))
+let test4 = update [(W1,[])] (Ex ("x", (Ex ("y", (Eq (Var "x", Var "y"))))))
+
+
+(* Alice isn't hungry. *)
+let test5 = update [(Hungry,[]);(Full,[])] 
+                   (Neg (Pred ("hungry", Constant Alice)))
+
+(* Alice isn't hungry.  Alice might be hungry. *)  
+let test6 = update [(Hungry,[]);(Full,[])] 
+                   (Conj (Neg (Pred ("hungry", Constant Alice)),
+                          Poss (Pred ("hungry", Constant Alice))))
+
+(* Alice might be hungry.  Alice isn't hungry. *)
+let test7 = update [(Hungry,[]);(Full,[])] 
+                   (Conj (Poss (Pred ("hungry", Constant Alice)),
+                          Neg (Pred ("hungry", Constant Alice))))
+ 
+(* Someone^x entered.  He_x sat. *)
+let test8 = update [(W1,[("x",Bob)])] 
+                   (Conj (Ex ("x", Pred ("enter", Var "x")),
+                          Pred ("sit", Var "x")))
+
+(* He_x sat.  Someone^x entered. *)
+let test9 = update [(W1,[("x",Bob)])] 
+                   (Conj (Pred ("sit", Var "x"),
+                          Ex ("x", Pred ("enter", Var "x"))))
+
+(* Someone^x is in the closet.  He_x might be guilty. *)
+let test10 = update [(W1,[]);(W2,[])]
+                    (Conj (Ex ("x", Pred ("closet", Var "x")),
+                           Poss (Pred ("guilty", Var "x"))))
+
+(* Someone^x is in the closet who_x might be guilty. *)
+let test11 = update [(W1,[]);(W2,[])]
+                    (Ex ("x", Conj (Pred ("closet", Var "x"),
+                                    Poss (Pred ("guilty", Var "x")))))