fix sudoku solver

examples/sudoku/sudoku_solve.ml

@@ -1,4 +1,4 @@
-(** {1 simple sudoku solver} *)
+(** simple sudoku solver *)
 
 module Fmt = CCFormat
 module Vec = Sidekick_util.Vec
@@ -179,15 +179,14 @@ end = struct
   end
 
   module Theory = struct
+    include Sidekick_sat.Proof_dummy.Make (F)
+
     type proof = unit
     type proof_step = unit
 
     module Lit = F
 
     type lit = Lit.t
-
-    module Proof = Sidekick_sat.Proof_dummy.Make (Lit)
-
     type t = { grid: Grid.t B_ref.t }
 
     let create g : t = { grid = B_ref.create g }

src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml

@@ -1,3 +1,7 @@
+(** Dummy proof traces.
+
+    These proof traces will not record information. *)
+
 module type S = Sidekick_sigs_proof_trace.S
 
 module type ARG = sig
@@ -16,3 +20,16 @@ module Make (A : ARG) : S with type t = unit and module A = A = struct
   let add_unsat _ _ = ()
   let delete _ _ = ()
 end
+
+(** Dummy proof trace where everything is [unit]. Use this if you don't care
+   for proofs at all. *)
+module Unit :
+  S with type t = unit and type A.rule = unit and type A.step_id = unit =
+Make (struct
+  type rule = unit
+  type step_id = unit
+
+  module Step_vec = Vec_unit
+
+  let dummy_step_id = ()
+end)

src/sat/Proof_dummy.ml

@@ -1,12 +1,25 @@
-(** Dummy proof module for rule=empty *)
+(** Dummy proof module using rule=[unit].
+
+    These proof traces will not record anything. *)
 
 module Make (Lit : sig
   type t
-end) :
+end) : sig
+  module Proof_trace :
+    Sidekick_sigs_proof_trace.S
+      with type A.rule = unit
+       and type A.step_id = unit
+       and type t = unit
+
+  module Proof_rules :
     Solver_intf.PROOF_RULES
       with type lit = Lit.t
        and type rule = unit
-     and type step_id = unit = struct
+       and type step_id = unit
+end = struct
+  module Proof_trace = Sidekick_proof_trace_dummy.Unit
+
+  module Proof_rules = struct
     type lit = Lit.t
     type rule = unit
     type step_id = unit
@@ -14,4 +27,5 @@ end) :
     let sat_input_clause _ = ()
     let sat_redundant_clause _ ~hyps:_ = ()
     let sat_unsat_core _ = ()
+  end
 end

src/sat/dune

@@ -1,6 +1,7 @@
 (library
  (name sidekick_sat)
  (public_name sidekick.sat)
- (libraries iter sidekick.util sidekick.core sidekick.sigs.proof-trace)
+ (libraries iter sidekick.util sidekick.core sidekick.sigs.proof-trace
+   sidekick.proof-trace.dummy)
  (synopsis "Pure OCaml SAT solver implementation for sidekick")
  (flags :standard -open Sidekick_util))