PoC unification tracer

config/discover.ml

@@ -133,6 +133,9 @@ let discover_stats () =
       (match Unix.getenv "OCANREN_STATS" with
       | exception Not_found -> []
       | _ -> [ "-D"; "STATS" ]);
+      (match Unix.getenv "OCANREN_TRACE" with
+      | exception Not_found -> []
+      | _ -> [ "-D"; "TRACE" ]);
       (match Unix.getenv "OCANREN_NON_ABSTRACT_GOAL" with
       | exception Not_found -> []
       | _ -> [ "-D"; "NON_ABSTRACT_GOAL" ]);

samples/add.ml

@@ -1,7 +1,6 @@
 module L = List
 
 open GT
-open Printf
 open OCanren
 open OCanren.Std
 
@@ -13,12 +12,15 @@ let addo x y z =
       x == S x' & z == S z' & addo x' y z'
   }
 
-let _ =
-  L.iter (fun (q, r) -> printf "q=%s, r=%s\n" q r) @@
-  Stream.take ~n:(-1) @@
-  ocanrun (q, r : ^Nat.nat) {addo q r 2} -> (show(Nat.logic) q, show(Nat.logic) r)
+let () =
+  (ocanrun (q, r : ^Nat.nat) {addo q r 2} -> (Trace.extract_last (), show(Nat.logic) q, show(Nat.logic) r))
+    |> Stream.take ~n:(-1)
+    |> L.iter begin fun (trace, q, r) ->
+      Format.printf "q=%s, r=%s\n" q r ;
+      Format.printf "TRACE: %a\n" Trace.pp trace
+    end
 
 let _ =
-  L.iter (fun q -> printf "q=%s\n" q) @@
+  L.iter (fun q -> Format.printf "q=%s\n" q) @@
   Stream.take ~n:(-1) @@
   ocanrun (q : ^Nat.nat) {addo q 1 0} -> (show(Nat.logic) q)

samples/dune

@@ -43,7 +43,7 @@
   (file %{project_root}/camlp5/pp5+ocanren+dump.exe)
   (file %{project_root}/camlp5/pp5+gt+plugins+ocanren+logger+dump.exe)
   (file %{project_root}/camlp5/pp5+ocanren+o.exe))
- (libraries GT OCanren))
+ (libraries GT OCanren benchmark))
 
 (executable
  (name bench_reverso)
@@ -123,6 +123,6 @@
    OCanren-ppx.ppx_distrib
    OCanren-ppx.ppx_deriving_reify
    GT.ppx_all
-   ppx_expect))
+   ppx_expect_nobase))
  (preprocessor_deps
   (file %{project_root}/ppx/pp_ocanren_all.exe)))

src/core/Core.ml

@@ -260,6 +260,7 @@ module State =
       ; ctrs  : Disequality.t
       ; prunes: Prunes.t
       ; scope : Term.Var.scope
+      ; trace : (Term.t * Term.t * t) option
       }
 
     type reified = Env.t * Term.t
@@ -270,6 +271,7 @@ module State =
       ; ctrs  = Disequality.empty
       ; prunes = Prunes.empty
       ; scope = Term.Var.new_scope ()
+      ; trace = None
       }
 
     let env   {env} = env
@@ -290,7 +292,8 @@ module State =
         match Disequality.recheck env subst ctrs prefix with
         | None      -> None
         | Some ctrs ->
-          let next_state = { st with subst ; ctrs } in
+          let trace = IFDEF TRACE THEN Some (Term.repr x, Term.repr y, st) ELSE st.trace END in
+          let next_state = { st with subst ; ctrs ; trace } in
           if PrunesControl.is_exceeded ()
           then begin
             let () = PrunesControl.reset_cur_counter () in
@@ -311,33 +314,80 @@ module State =
         | Prunes.Violated -> None
         | NonViolated -> Some { st with ctrs }
 
+    IFDEF TRACE THEN
+
+    (* assigned in Trace module *)
+    let save_trace = ref @@ Obj.magic 0
+
+    END
+
     (* always returns non-empty list *)
-    let reify x { env ; subst ; ctrs } =
+    let reify x ({ env ; subst ; ctrs } as st) =
       let answ = Subst.reify env subst x in
       match Disequality.reify env subst ctrs x with
       | [] -> (* [Answer.make env answ] *) assert false
-      | diseqs -> ListLabels.map diseqs ~f:begin fun diseq ->
-        let rec helper forbidden t = Term.map t ~fval:Term.repr
-          ~fvar:begin fun v -> Term.repr @@
-            if Term.VarSet.mem v forbidden then v
-            else { v with Term.Var.constraints = Disequality.Answer.extract diseq v
-                |> List.filter begin fun dt ->
-                  match Env.var env dt with
-                  | Some u -> not @@ Term.VarSet.mem u forbidden
-                  | None   -> true
-                end
-                |> List.map (fun x -> helper (Term.VarSet.add v forbidden) x)
-                (* TODO: represent [Var.constraints] as [Set];
-                 * TODO: hide all manipulations on [Var.t] inside [Var] module;
-                 *)
-                |> List.sort Term.compare
-              }
-          end
-        in
-        Answer.make env @@ helper Term.VarSet.empty answ
-      end
+      | diseqs ->
+        IFDEF TRACE THEN !save_trace st ELSE let _ = st in () END ;
+        ListLabels.map diseqs ~f:begin fun diseq ->
+          let rec helper forbidden t = Term.map t ~fval:Term.repr
+            ~fvar:begin fun v -> Term.repr @@
+              if Term.VarSet.mem v forbidden then v
+              else { v with Term.Var.constraints = Disequality.Answer.extract diseq v
+                  |> List.filter begin fun dt ->
+                    match Env.var env dt with
+                    | Some u -> not @@ Term.VarSet.mem u forbidden
+                    | None   -> true
+                  end
+                  |> List.map (fun x -> helper (Term.VarSet.add v forbidden) x)
+                  (* TODO: represent [Var.constraints] as [Set];
+                   * TODO: hide all manipulations on [Var.t] inside [Var] module;
+                   *)
+                  |> List.sort Term.compare
+                }
+            end
+          in
+          Answer.make env @@ helper Term.VarSet.empty answ
+        end
+  end
+
+IFDEF TRACE THEN
+
+module Trace :
+  sig
+
+    type t
+
+    val pp : Format.formatter -> t -> unit
+
+    val extract_last : unit -> t
+  end = struct
+
+    type t = (Term.t * Term.t) list
+
+    let saved_state = ref None
+
+    let () = State.save_trace := fun st -> saved_state := Some st
+
+    let pp =
+        let hlp ppf (l, r) = Format.fprintf ppf "%a = %a" Term.pp l Term.pp r in
+        let pp_sep ppf () = Format.fprintf ppf "; " in
+        Format.pp_print_list ~pp_sep hlp
+
+    let extract =
+      let rec extract acc = function
+      | Some (l, r, st) -> extract ((l, r)::acc) st.State.trace
+      | None -> acc
+      in
+
+      extract []
+
+    let extract_last () = match !saved_state with
+    | Some st -> extract st.State.trace
+    | None -> raise Not_found
   end
 
+END
+
 let (!!!) = Obj.magic
 
 type 'a goal' = State.t -> 'a
@@ -816,4 +866,4 @@ let is_ground_bool
     let ans = Subst.reify (State.env st) (State.subst st) (Obj.magic v) in
     if (Term.is_var ans) then onvar()
     else on_ground (Obj.magic ans : bool)
-END
+END

src/core/Core.mli

@@ -304,6 +304,16 @@ val disj_counter        : unit -> int
 val delay_counter       : unit -> int
 END
 
+IFDEF TRACE THEN
+
+module Trace : sig
+  type t
+  val pp : Format.formatter -> t -> unit
+  val extract_last : unit -> t
+end
+
+END
+
 (** The call [debug_var var reifier callback] performs reification of variable [var] in a current state using [reifier] and passes list of answer to [callback] (multiple answers can arise in presence of disequality constraints). The [callback] can investigate reified value and construct required goal to continue search.
 
 See also: {!structural}.
@@ -338,4 +348,4 @@ val is_ground : 'a ilogic -> State.t -> (bool -> unit) -> unit
 
 val is_ground_bool : bool ilogic -> State.t -> onvar:(unit->unit) -> on_ground:(bool -> unit) -> unit
 
-END
+END