Add basic tracing

bin/dowsindex/CmdUnify.ml

@@ -1,14 +1,16 @@
 open CommonOpts
+module Trace = Trace_core
 
 type opts = { copts : copts; all_unifs : Bool.t; ty1 : Type.t; ty2 : Type.t }
 
 let main opts =
   Logs.info (fun m -> m "@[<2>type1:@ %a@]" Type.pp opts.ty1);
   Logs.info (fun m -> m "@[<2>type2:@ %a@]" Type.pp opts.ty2);
   let unifs =
-    Acic.unifiers env_query opts.ty1 opts.ty2
-    |> Iter.sort ~cmp:Subst.compare
-    |> Iter.to_list
+    Trace.with_span ~__FILE__ ~__LINE__ "Unification" (fun _ ->
+      Acic.unifiers env_query opts.ty1 opts.ty2
+      |> Iter.sort ~cmp:Subst.compare
+      |> Iter.to_list)
   in
   let unifs = if opts.all_unifs then unifs else CCList.take 1 unifs in
   if unifs = [] then Fmt.pr "no unifier@."

bin/dowsindex/dune

@@ -1,5 +1,5 @@
 (executable
   (name dowsindex)
   (public_name dowsindex)
-  (libraries cmdliner logs bos utils common package acic index trace-tef)
+  (libraries cmdliner logs bos utils common package acic index trace trace.core trace-tef)
   (flags (:standard -open Utils -open Common)))

lib/unification/ArrowTerm.ml

@@ -9,11 +9,13 @@ type problem = {
 }
 
 let make args ret : t = {args; ret}
+
+let pp ppf self =
+  Fmt.pf ppf "%a -> %a"
+    Fmt.(array ~sep:(any " * ") Pure.pp) self.args
+    Type.pp self.ret
+
 let make_problem left right = {left; right}
 
 let pp_problem ppf self =
-  Fmt.pf ppf "%a -> %a = %a -> %a"
-    Fmt.(array ~sep:(any " * ") Pure.pp) self.left.args
-    Type.pp self.left.ret
-    Fmt.(array ~sep:(any " * ") Pure.pp) self.right.args
-    Type.pp self.right.ret
+  Fmt.pf ppf "%a = %a" pp self.left pp self.right

lib/unification/ArrowTerm.mli

@@ -11,5 +11,6 @@ type problem = {
 }
 
 val make : Pure.t array -> Type.t -> t
+val pp : t Fmt.t [@@ocaml.toplevel_printer]
 val make_problem : t -> t -> problem
 val pp_problem : problem Fmt.t [@@ocaml.toplevel_printer]

lib/unification/Diophantine.ml

@@ -24,6 +24,8 @@ module Make() = struct
      Systems of Linear Diophantine Equations", Contejean and Devie, 1994.
   *)
   module Homogeneous_system = struct
+    module Trace = Trace_core
+
     type t = {
       eqns: Z.t array array;
       n_vars: int; (* length of each sub-array *)
@@ -180,6 +182,7 @@ module Make() = struct
 
     (* main solving algorithm *)
     let solve_main (st:state) (yield : solution -> unit) : unit =
+      Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__"solve_main" (fun _sp ->
       let n = st_n st in
       while st.len > 0 do
         st.len <- st.len - 1;
@@ -196,7 +199,8 @@ module Make() = struct
           let sol = Array.copy vec in
           st.solutions <- sol :: st.solutions;
           log_ (fun k->k "! solution %a" pp_vec sol);
-          yield sol;
+          Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__"solve_yield" (fun _sp ->
+          yield sol;)
         ) else (
           (* explore next states *)
           for j=0 to n - 1 do
@@ -233,6 +237,7 @@ module Make() = struct
         st_recycle st sums;
         st_recycle st vec;
       done
+      )
 
     let default_cut _ = false
 

lib/unification/Unification.ml

@@ -4,6 +4,8 @@
     Competing for the AC-unification Race by Boudet (1993)
 *)
 
+module Trace = Trace_core
+
 module Logs = (val Logs.(src_log @@ Src.create __MODULE__))
 
 let _info = Logs.info
@@ -241,10 +243,15 @@ and attach env v t : return =
   occur_check env
 
 let insert env t u : return =
-  Logs.debug (fun m -> m "@[<v2>Insert@ %a = %a@ in@ %a@]"
-                 Type.pp t Type.pp u
-                 Env.pp env);
-  insert_rec env Stack.empty t u
+    Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__ "Insert"
+      ~data:(fun () -> [("t", `String (CCFormat.sprintf "%a" Type.pp t));
+                                 ("u", `String (CCFormat.sprintf "%a" Type.pp u))])
+      (fun _sp ->
+    Logs.debug (fun m -> m "@[<v2>Insert@ %a = %a@ in@ %a@]"
+                   Type.pp t Type.pp u
+                   Env.pp env);
+    insert_rec env Stack.empty t u
+  )
 
 let insert_var env x ty : return = insert_var env Stack.empty x ty
 
@@ -274,6 +281,10 @@ let rec solve_tuple_problems env0 =
 (* Elementary Arrow theory *)
 and solve_arrow_problem env0 { ArrowTerm.left; right } =
   (* AL -> BL ≡? AR -> BR *)
+  Trace.message ~data:(fun () ->
+      [("Left", `String (CCFormat.sprintf "%a" ArrowTerm.pp left));
+       ("Right", `String (CCFormat.sprintf "%a" ArrowTerm.pp right));
+      ]) "Solve_arrow";
   let potentials =
     [
       (fun env () ->

lib/unification/dune

@@ -1,5 +1,5 @@
 (library
  (name acic)
- (libraries logs zarith common diet)
+ (libraries logs zarith common diet trace trace.core)
  (flags
   (:standard -open Common)))