From 6f5506d77c68c64e504078e2918aa081eab950fd Mon Sep 17 00:00:00 2001 From: Eridan Domoratskiy Date: Fri, 27 Feb 2026 00:08:37 +0300 Subject: [PATCH] WIP: PoC unification tracer --- config/discover.ml | 3 ++ samples/add.ml | 14 ++++--- samples/dune | 4 +- src/core/Core.ml | 96 +++++++++++++++++++++++++++++++++++----------- src/core/Core.mli | 12 +++++- 5 files changed, 97 insertions(+), 32 deletions(-) diff --git a/config/discover.ml b/config/discover.ml index 892359a7f..77db78ecf 100644 --- a/config/discover.ml +++ b/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" ]); diff --git a/samples/add.ml b/samples/add.ml index a31c71e63..049771652 100644 --- a/samples/add.ml +++ b/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) diff --git a/samples/dune b/samples/dune index 27fced1f8..ce69be01c 100644 --- a/samples/dune +++ b/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))) diff --git a/src/core/Core.ml b/src/core/Core.ml index aa8903cfd..94d8ab92e 100644 --- a/src/core/Core.ml +++ b/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 \ No newline at end of file +END diff --git a/src/core/Core.mli b/src/core/Core.mli index 258822df7..aea92c578 100644 --- a/src/core/Core.mli +++ b/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 \ No newline at end of file +END