Fix issue #173 (disequlaity crash)

regression_ppx/dune

@@ -148,13 +148,29 @@
  (modules test013mutual)
  (package OCanren)
  (public_names -)
- (flags
-  (:standard
-   ;-dsource
-   ;
-   ))
  (preprocess
-  (pps OCanren-ppx.ppx_distrib GT.ppx_all -- -new-typenames -pretty))
+  (pps
+   OCanren-ppx.ppx_distrib
+   GT.ppx_all
+   OCanren-ppx.ppx_fresh
+   --
+   -new-typenames
+   -pretty))
+ (libraries OCanren OCanren.tester))
+
+(executables
+ (names test014diseq)
+ (modules test014diseq)
+ (package OCanren)
+ (public_names -)
+ (preprocess
+  (pps
+   GT.ppx_all
+   OCanren-ppx.ppx_fresh
+   OCanren-ppx.ppx_tester
+   OCanren-ppx.ppx_repr
+   --
+   -pretty))
  (libraries OCanren OCanren.tester))
 
 (cram
@@ -283,3 +299,12 @@
   %{project_root}/ppx/pp_ocanren_all.exe
   test013mutual.ml
   test013mutual.exe))
+
+(cram
+ (package OCanren)
+ (applies_to test014)
+ (deps
+  (package OCanren-ppx)
+  %{project_root}/ppx/pp_ocanren_all.exe
+  test014diseq.ml
+  test014diseq.exe))

regression_ppx/test014.t

@@ -0,0 +1,35 @@
+  $ ./test014diseq.exe
+  rel, 1 answer {
+  hd1 = _.12
+  hd2 = _.14
+  tl2 = _.15
+  10: { 0: [|  10 =/= _.11 |] }
+
+  11: { 0: [|  11 =/= boxed 0 <_.12, _.13> |] }
+
+  15: { 0: [|  14 =/= _.12,  15 =/= _.13 |] }
+
+   hd2 === 1
+  15: { 0: [|  14 =/= _.12,  15 =/= _.13 |] }
+
+   tl2 === []
+  13: { 0: [|  12 =/= int<1>,  13 =/= int<0> |] }
+
+  47
+  13: { 0: [|  12 =/= int<1>,  13 =/= int<0> |] }
+
+  }
+  fun _ ->
+    fresh x
+      ((Std.list Fun.id [!< x; !< x]) =/=
+         (Std.list Fun.id [!< (!! 1); !< (!! 2)])), 1 answer {
+  q=_.10;
+  }
+  fun q ->
+    fresh (x y) (trace_index "x" x) (trace_index "y" y) ((x % y) === q)
+      ((x % y) =/= (Std.list Fun.id [!! 1; x]))
+      (y === (Std.list Fun.id [!! 2])) success, 1 answer {
+  x = _.11
+  y = _.12
+  q=[_.11; 2];
+  }

regression_ppx/test014diseq.ml

@@ -0,0 +1,87 @@
+open OCanren
+open Tester
+
+let debug_line line =
+  debug_var !!1 OCanren.reify (function _ ->
+      Format.printf "%d\n%!" line;
+      success)
+;;
+
+let trace_index msg var =
+  debug_var var OCanren.reify (function
+      | [ Var (n, _) ] ->
+          Printf.printf "%s = _.%d\n" msg n;
+          success
+      | _ -> assert false)
+;;
+
+let trace fmt =
+  Format.kasprintf
+    (fun s ->
+      debug_var !!1 OCanren.reify (function _ ->
+          Format.printf "%s\n%!" s;
+          success))
+    fmt
+;;
+
+let rel list1 =
+  let open OCanren.Std in
+  fresh
+    (list2 hd1 tl1 hd2 tl2)
+    (trace_index "hd1" hd1)
+    (trace_index "hd2" hd2)
+    (trace_index "tl2" tl2)
+    (list1 =/= list2)
+    trace_diseq
+    (list1 === hd1 % tl1)
+    trace_diseq
+    (list2 === hd2 % tl2)
+    trace_diseq
+    (trace " hd2 === 1")
+    (hd2 === !!1)
+    trace_diseq
+    (trace " tl2 === []")
+    (tl2 === nil ())
+    trace_diseq
+    (hd1 === !!1)
+    (debug_line __LINE__)
+    trace_diseq
+    (tl1 === nil ()) (* crashes here *)
+    (debug_line __LINE__)
+;;
+
+(* let () = [%tester run_r [%show GT.int GT.list] (Std.List.reify reify) 1 (fun q -> rel q)] *)
+let () = run_r (Std.List.reify reify) ([%show: GT.int logic Std.List.logic] ()) 1 q qh (REPR rel)
+
+let () =
+  let open Std in
+  run_r
+    (Std.List.reify reify)
+    ([%show: GT.int logic Std.List.logic] ())
+    1
+    q
+    qh
+    (REPR (fun _ -> fresh x (Std.list Fun.id [ !<x; !<x ] =/= Std.list Fun.id [ !<(!!1); !<(!!2) ])))
+;;
+
+let () =
+  let open OCanren.Std in
+  run_r
+    (Std.List.reify reify)
+    ([%show: GT.int logic Std.List.logic] ())
+    1
+    q
+    qh
+    (REPR
+       (fun q ->
+         fresh
+           (x y)
+           (trace_index "x" x)
+           (trace_index "y" y)
+           (x % y === q)
+           (x % y =/= Std.list Fun.id [ !!1; x ])
+           (* trace_diseq *)
+           (y === Std.list Fun.id [ !!2 ])
+           (* trace_diseq *)
+           success))
+;;

src/core/Core.ml

@@ -795,4 +795,9 @@ module Tabling =
 
 let reify_in_empty reifier x =
   let st = State.empty () in
-  reifier (State.env st) x
+  reifier (State.env st) x
+
+let trace_diseq : goal = fun st ->
+  Format.printf "%a\n%!" Disequality.pp (State.constraints st);
+  success st
+

src/core/Core.mli

@@ -320,4 +320,6 @@ module PrunesControl : sig
 end
 
 (** Runs reifier on empty state. Useful to debug execution order *)
-val reify_in_empty: ('a, 'b) Reifier.t -> 'a -> 'b
+val reify_in_empty: ('a, 'b) Reifier.t -> 'a -> 'b
+
+val trace_diseq: goal

src/core/Disequality.ml

@@ -19,6 +19,11 @@
 (* to avoid clash with Std.List (i.e. logic list) *)
 module List = Stdlib.List
 
+let log fmt =
+  if false
+  then Format.kasprintf (Format.printf "%s\n%!") fmt
+  else Format.ifprintf Format.std_formatter fmt
+
 module Answer =
   struct
     module S = Set.Make(Term)
@@ -91,6 +96,9 @@ module Disjunct :
     (* Disjunction.t is a set of single disequalities joint by disjunction *)
     type t
 
+
+    val pp : Format.formatter -> t -> unit
+
     (* [make env subst x y] creates new disjunct from the disequality [x =/= y] *)
     val make : Env.t -> Subst.t -> 'a -> 'a -> t
 
@@ -118,9 +126,19 @@ module Disjunct :
   struct
     type t = Term.t Term.VarMap.t
 
-    let update t =
-      ListLabels.fold_left ~init:t
-        ~f:(let open Subst.Binding in fun acc {var; term} ->
+    let pp ppf d =
+      if Term.VarMap.is_empty d then Format.fprintf ppf "<empty>"
+      else
+        Format.fprintf ppf "[| ";
+        Term.VarMap.iteri (fun i k v ->
+          if i<>0 then  Format.fprintf ppf ", ";
+          Format.fprintf ppf " @[%d =/= %s@]" k.Term.Var.index (Term.show v)
+          ) d;
+        Format.fprintf ppf " |]"
+
+    let update : t -> _ -> t = fun init ->
+      ListLabels.fold_left ~init
+        ~f:(fun acc {Subst.Binding.var; term} ->
           if Term.VarMap.mem var acc then
             (* in this case we have subformula of the form (x =/= t1) \/ (x =/= t2) which is always SAT *)
             raise Disequality_fulfilled
@@ -149,12 +167,32 @@ module Disjunct :
       | Fulfiled      -> raise Disequality_fulfilled
       | Violated      -> raise Disequality_violated
 
-    let rec recheck env subst t =
+    let rec recheck env subst (t: t): t  =
+      (* log "Disjunct.recheck: %a" pp t; *)
       let var, term = Term.VarMap.max_binding t in
+      (* log "       max bind index =  %d" var.Term.Var.index; *)
       let unchecked = Term.VarMap.remove var t in
+      (* log "       unchecked: %a" pp unchecked; *)
       match refine env subst (Obj.magic var) term with
-      | Fulfiled       -> raise Disequality_fulfilled
-      | Refined delta  -> update unchecked delta
+      | Fulfiled       ->
+          raise Disequality_fulfilled
+      | Refined delta  -> (
+          (* When leading terms are reified into something new, we still need to
+             do whole unification, beacuse other pairs may need walking ---
+             (we postponed walking, so som einformation may be lost.)
+             See issue #173
+          *)
+          (* log "Refined into: %a" (Format.pp_print_list Subst.Binding.pp) delta; *)
+          match Subst.unify_map env subst t with
+          | None ->
+            (* not unifiable --- always distinct *)
+            raise Disequality_fulfilled
+          | Some ([], _) -> raise Disequality_violated
+          | Some (bnds, _subst) ->
+              (* TODO(Kakadu): reconstruction of map from binding list could hurt performance  *)
+              let rez = Subst.varmap_of_bindings bnds in
+              (* log "Disjunct.recheck returns %a" pp rez; *)
+              rez)
       | Violated       ->
         if Term.VarMap.is_empty unchecked then
           raise Disequality_violated
@@ -208,6 +246,8 @@ module Conjunct :
 
     val empty : t
 
+    val pp : Format.formatter -> t -> unit
+
     val is_empty : t -> bool
 
     val make : Env.t -> Subst.t -> 'a -> 'a -> t
@@ -236,6 +276,19 @@ module Conjunct :
 
     type t = Disjunct.t M.t
 
+    let pp ppf map =
+      if M.is_empty map
+      then Format.fprintf ppf "{}"
+      else
+        let idx = ref 0 in
+        Format.fprintf ppf "{ ";
+        M.iter (fun k v ->
+          if !idx <> 0 then Format.fprintf ppf " ,";
+          Format.fprintf ppf "@[%d: %a@]" k Disjunct.pp v;
+          incr idx
+        ) map;
+        Format.fprintf ppf " }"
+
     let empty = M.empty
 
     let is_empty = M.is_empty
@@ -256,11 +309,14 @@ module Conjunct :
       ) t Term.VarMap.empty
 
     let recheck env subst t =
-      M.fold (fun id disj acc ->
+      log "Conjunct.recheck. %a" pp t;
+      let rez = M.fold (fun id disj acc ->
           try
             M.add id (Disjunct.recheck env subst disj) acc
           with Disequality_fulfilled -> acc
-      ) t M.empty
+      ) t M.empty in
+      log "rechecked =  %a" pp rez;
+      rez
 
     let merge_disjoint env subst =
       M.union (fun _ _ _ ->
@@ -351,6 +407,11 @@ type t = Conjunct.t Term.VarMap.t
 
 let empty = Term.VarMap.empty
 
+let pp ppf : t -> unit  =
+  Term.VarMap.iter (fun k v ->
+    Format.fprintf ppf "@[%d: %a@]@," k.Term.Var.index Conjunct.pp v
+    )
+
 (* merges all conjuncts (linked to different variables) into one *)
 let combine env subst cstore =
   Term.VarMap.fold (fun _ -> Conjunct.merge_disjoint env subst) cstore Conjunct.empty
@@ -370,17 +431,19 @@ let add env subst cstore x y =
     | Disequality_violated  -> None
 
 let recheck env subst cstore bs =
-  let helper var cstore =
+  let helper var cstore : t =
     try
       let conj = Term.VarMap.find var cstore in
       let cstore = Term.VarMap.remove var cstore in
       update env subst (Conjunct.recheck env subst conj) cstore
+
     with Not_found -> cstore
   in
   try
     let cstore = ListLabels.fold_left bs ~init:cstore
-      ~f:(let open Subst.Binding in fun cstore {var; term} ->
+      ~f:(fun cstore {Subst.Binding.var; term} ->
         let cstore = helper var cstore in
+        (* log "cstore = %a" pp cstore; *)
         match Env.var env term with
         | Some u -> helper u cstore
         | None   -> cstore

src/core/Disequality.mli

@@ -51,3 +51,5 @@ module Answer :
   end
 
 val reify : Env.t -> Subst.t -> t -> 'a -> Answer.t list
+
+val pp: Format.formatter -> t -> unit