Interp: Prettier code

colibri2/core/interp.ml

@@ -158,14 +158,14 @@ let print_value_smt d fmt v =
         let pr = Data.PrintValue.get Data.print_value k in
         pr d fmt v
 
-let spy_sequence msg s i =
-  if false then
+let spy_sequence msg s =
+  if false then fun i ->
     Sequence.mapi
       ~f:(fun i x ->
         Fmt.epr "@.%s %i: %a@." msg i Value.pp x;
         x)
       (s i)
-  else s i
+  else s
 
 let get_registered (type a) exn db call d x =
   let exception Found of a in
@@ -288,13 +288,13 @@ let check_args d g =
         raise (ArgOfGroundTermWithoutValueAfterModelFixing (g, n)))
 
 let check_ground_terms d =
-  Datastructure.Push.fold Data.reg_ground d ~init:false ~f:(fun acc g ->
+  Datastructure.Push.fold Data.reg_ground d ~init:`Right ~f:(fun acc g ->
       if Option.is_none (Egraph.get_value d (Ground.node g)) then
         raise (GroundTermWithoutValueAfterModelFixing (`Ground g));
       check_args d g;
       match check Data.check d g with
       | Right -> acc
-      | Unknown -> true
+      | Unknown -> `Unknown
       | NA -> raise (CantCheckGround (`Ground g))
       | Wrong ->
           Debug.dprintf2 Egraph.print_contradiction
@@ -302,13 +302,13 @@ let check_ground_terms d =
           Egraph.contradiction d)
 
 let check_closed_quantifier d =
-  Datastructure.Push.fold Data.reg_closed_quantifiers d ~init:false
+  Datastructure.Push.fold Data.reg_closed_quantifiers d ~init:`Right
     ~f:(fun acc g ->
       if Option.is_none (Egraph.get_value d (Ground.ClosedQuantifier.node g))
       then raise (GroundTermWithoutValueAfterModelFixing (`ClosedQuantifier g));
       match check Data.check_closed_quantifier d g with
       | Right -> acc
-      | Unknown -> true
+      | Unknown -> `Unknown
       | NA -> raise (CantCheckGround (`ClosedQuantifier g))
       | Wrong ->
           Debug.dprintf2 Egraph.print_contradiction
@@ -316,13 +316,13 @@ let check_closed_quantifier d =
           Egraph.contradiction d)
 
 let check_not_totally_applied d =
-  Datastructure.Push.fold Data.reg_not_totally_applied d ~init:false
+  Datastructure.Push.fold Data.reg_not_totally_applied d ~init:`Right
     ~f:(fun acc g ->
       if Option.is_none (Egraph.get_value d (Ground.NotTotallyApplied.node g))
       then raise (GroundTermWithoutValueAfterModelFixing (`NotTotallyApplied g));
       match check Data.check_not_totally_applied d g with
       | Right -> acc
-      | Unknown -> true
+      | Unknown -> `Unknown
       | NA -> raise (CantCheckGround (`NotTotallyApplied g))
       | Wrong ->
           Debug.dprintf2 Egraph.print_contradiction
@@ -453,7 +453,12 @@ module Fix_model = struct
               let unknown1 = check_ground_terms (Egraph.ro d) in
               let unknown2 = check_closed_quantifier (Egraph.ro d) in
               let unknown3 = check_not_totally_applied (Egraph.ro d) in
-              let unknown = unknown1 || unknown2 || unknown3 in
+              let unknown =
+                match (unknown1, unknown2, unknown3) with
+                | `Right, `Right, `Right -> false
+                | _ -> true
+              in
+              Debug.dprintf1 debug "unknown:%b" unknown;
               Egraph.set_unknown d unknown;
               Egraph.set_env d Data.env Before;
               Sequence.empty