let left1 (x : e) = true;; (* Everyone left *)
let saw1 (y : e) (x : e) = x < y;; (* Ann saw Bill and Cam, and Bill saw Cam *)
-left1 ann;;
-saw1 bill ann;;
-saw1 ann bill;;
+left1 ann;; (* true *)
+saw1 bill ann;; (* true *)
+saw1 ann bill;; (* false *)
(* Now we make the extension of "leave" sensitive to the world of evaluation *)
let left (x : e) (w : s) = match (x, w) with ('c', 2) -> false | _ -> true;;
let (>>=) xx k (w : s) = k (xx w) w;;
let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> f x y));;
-(mid ann >>= left) 1;;
-(mid cam >>= left) 2;;
+(mid ann >>= left) 1;; (* true *)
+(mid cam >>= left) 2;; (* false *)
-map2' saw (mid bill) (mid ann) 1;;
-map2' saw (mid bill) (mid ann) 2;;
+map2' saw (mid bill) (mid ann) 1;; (* true *)
+map2' saw (mid bill) (mid ann) 2;; (* false *)
let thinks (p : s->t) (x : e) (w : s) =
match (x, p 2) with ('a', false) -> false | _ -> p w;;
-(mid ann >>= thinks (mid bill >>= left)) 1;;
-(mid ann >>= thinks (mid cam >>= left)) 1;;
+(mid bill >>= left) 1;; (* true *)
+(mid cam >>= left) 1;; (* true *)
+(mid ann >>= thinks (mid bill >>= left)) 1;; (* true *)
+(mid ann >>= thinks (mid cam >>= left)) 1;; (* false *)