fix laziness

src/type/t_hyps.ml

@@ -20,18 +20,18 @@ let error ?at mssg =
 
 type 'a ret = 'a option Lazy.t
 
-let (||>) (f : 'a ret) (g : 'a ret) : 'a ret =
-  match Lazy.force f with
-  | Some x -> Lazy.from_val (Some x)
-  | None -> g
-
-let (&&>) (f : 'a ret) (g : 'a ret) : 'a ret =
-  match Lazy.force f with
-  | None -> Lazy.from_val None
+let (||>) (f : 'a option) (g : 'a ret) : 'a option =
+  match f with
+  | Some x -> Some x
+  | None -> Lazy.force g
+
+let (&&>) (f : 'a option) (g : 'a ret) : 'a option =
+  match f with
+  | None -> None
   | Some x -> begin
     match Lazy.force g with
-    | Some y when x = y -> Lazy.from_val (Some y)
-    | _ -> Lazy.from_val None
+    | Some y when x = y -> Some y
+    | _ -> None
   end
 
 
@@ -45,48 +45,48 @@ let search_type_hyp ~inferer ~pol scx oe =
         begin try
           begin
           match inferer scx e with
-          | TSet ty0 -> Lazy.from_val (Some ty0)
-          | _ -> Lazy.from_val None
+          | TSet ty0 -> Some ty0
+          | _ -> None
           end
-        with _ -> Lazy.from_val None
+        with _ -> None
         end
 
     | Apply ({ core = Internal (B.Eq | B.Neq as b) }, [ { core = Ix n } ; e ])
     | Apply ({ core = Internal (B.Eq | B.Neq as b) }, [ e ; { core = Ix n } ])
       when n = ix && ((pol && b = B.Neq) || (not pol && b = B.Eq)) ->
         begin try
-          Lazy.from_val (Some (inferer scx e))
-        with _ -> Lazy.from_val None
+          Some (inferer scx e)
+        with _ -> None
         end
 
     | Apply ({ core = Internal (B.Disj | B.Conj as b) }, [ e ; f ])
       when (pol && b = B.Disj) || (not pol && b = B.Conj) ->
         visit ~pol ix scx e ||>
-        visit ~pol ix scx f
+        lazy (visit ~pol ix scx f)
 
     | Apply ({ core = Internal (B.Disj | B.Conj as b) }, [ e ; f ])
       when (not pol && b = B.Disj) || (pol && b = B.Conj) ->
         visit ~pol ix scx e &&>
-        visit ~pol ix scx f
+        lazy (visit ~pol ix scx f)
 
     | List ((Or | And as b), es)
       when (pol && b = Or) || (not pol && b = And) ->
         List.fold_left begin fun r e ->
-          r ||> visit ~pol ix scx e
-        end (Lazy.from_val None) es
+          r ||> lazy (visit ~pol ix scx e)
+        end None es
 
     | List ((Or | And as b), es)
       when (not pol && b = Or) || (pol && b = And) ->
         List.fold_left begin fun r e ->
-          r &&> visit ~pol ix scx e
-        end (Lazy.from_val None) es
+          r &&> lazy (visit ~pol ix scx e)
+        end None es
 
     | Apply ({ core = Internal B.Neg }, [ e ]) ->
         visit ~pol:(not pol) ix scx e
 
     | Apply ({ core = Internal B.Implies }, [ e ; f ]) ->
         visit ~pol:(not pol) ix scx e ||>
-        visit ~pol ix scx f
+        lazy (visit ~pol ix scx f)
 
     | Quant (q, bs, e)
       when (pol && q = Forall) || (not pol && q = Exists) ->
@@ -104,24 +104,24 @@ let search_type_hyp ~inferer ~pol scx oe =
     | Sequent sq when pol ->
         visit_sq ix scx sq
 
-    | _ -> Lazy.from_val None
+    | _ -> None
 
   and visit_sq ix scx sq =
     let rec spin ix scx hs =
       match Deque.front hs with
       | Some ({ core = Fact (e, Visible, _) } as h, hs) ->
           visit ~pol:false ix scx e ||>
-          spin (ix + 1) (Deque.snoc scx h) hs
+          lazy (spin (ix + 1) (Deque.snoc scx h) hs)
       | Some (h, hs) ->
           spin (ix + 1) (Deque.snoc scx h) hs
       | None ->
-          Lazy.from_val None
+          None
     in
     spin ix scx sq.context ||>
-    visit ~pol:true (ix + Deque.size sq.context) scx sq.active
+    lazy (visit ~pol:true (ix + Deque.size sq.context) scx sq.active)
   in
 
   let dummy = Fact (Internal B.TRUE %% [], Visible, NotSet) %% [] in
   let scx = Deque.snoc scx dummy in
-  Lazy.force (visit ~pol 1 scx oe)
+  visit ~pol 1 scx oe