From 1edf0541043e451ebb0a39615278956c0bb38ad1 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 31 Jul 2022 15:00:27 -0400
Subject: [PATCH] refactor(proof): use a suspension but keep uniform
 `Proof_term.data` type

this makes proof terms uniformly printable or (de)serializable.
---
 src/cc/CC.ml                                  | 28 ++++-----
 src/core/proof_core.ml                        | 27 +++------
 src/core/proof_core.mli                       | 54 ++++++++---------
 src/core/proof_sat.ml                         | 10 ++--
 src/core/proof_sat.mli                        |  6 +-
 src/core/proof_term.ml                        | 16 ++---
 src/core/proof_term.mli                       | 24 ++++----
 src/sat/solver.ml                             | 55 +++++++++--------
 src/simplify/sidekick_simplify.ml             |  9 +--
 src/smt/solver.ml                             |  6 +-
 src/smt/solver_internal.ml                    | 26 ++++----
 src/th-bool-static/Sidekick_th_bool_static.ml |  9 +--
 src/th-cstor/Sidekick_th_cstor.ml             |  2 +-
 src/th-cstor/Sidekick_th_cstor.mli            |  2 +-
 src/th-data/Sidekick_th_data.ml               | 59 ++++++++++---------
 src/th-data/th_intf.ml                        | 16 ++---
 src/th-lra/intf.ml                            |  2 +-
 src/th-lra/sidekick_th_lra.ml                 | 20 +++----
 src/util/Bag.ml                               |  2 +
 src/util/Bag.mli                              |  1 +
 20 files changed, 182 insertions(+), 192 deletions(-)

diff --git a/src/cc/CC.ml b/src/cc/CC.ml
index a9192ccf..c8722d3f 100644
--- a/src/cc/CC.ml
+++ b/src/cc/CC.ml
@@ -2,12 +2,6 @@ open Types_
 
 type view_as_cc = Term.t -> (Const.t, Term.t, Term.t Iter.t) View.t
 
-open struct
-  (* proof rules *)
-  module Rules_ = Proof_core
-  module P = Proof_trace
-end
-
 type e_node = E_node.t
 (** A node of the congruence closure *)
 
@@ -305,13 +299,13 @@ module Expl_state = struct
   (* proof of [\/_i ¬lits[i]] *)
   let proof_of_th_lemmas (self : t) (proof : Proof_trace.t) : Proof_term.step_id
       =
-    let p_lits1 = Iter.of_list self.lits |> Iter.map Lit.neg in
+    let p_lits1 = List.rev_map Lit.neg self.lits in
     let p_lits2 =
-      Iter.of_list self.th_lemmas
-      |> Iter.map (fun (lit_t_u, _, _) -> Lit.neg lit_t_u)
+      self.th_lemmas |> List.rev_map (fun (lit_t_u, _, _) -> Lit.neg lit_t_u)
     in
     let p_cc =
-      P.add_step proof @@ Rules_.lemma_cc (Iter.append p_lits1 p_lits2)
+      Proof_trace.add_step proof @@ fun () ->
+      Proof_core.lemma_cc (List.rev_append p_lits1 p_lits2)
     in
     let resolve_with_th_proof pr (lit_t_u, sub_proofs, pr_th) =
       (* pr_th: [sub_proofs |- t=u].
@@ -322,16 +316,16 @@ module Expl_state = struct
           (fun pr_th (lit_i, hyps_i) ->
             (* [hyps_i |- lit_i] *)
             let lemma_i =
-              P.add_step proof
-              @@ Rules_.lemma_cc
-                   Iter.(cons lit_i (of_list hyps_i |> map Lit.neg))
+              Proof_trace.add_step proof @@ fun () ->
+              Proof_core.lemma_cc (lit_i :: List.rev_map Lit.neg hyps_i)
             in
             (* resolve [lit_i] away. *)
-            P.add_step proof
-            @@ Rules_.proof_res ~pivot:(Lit.term lit_i) lemma_i pr_th)
+            Proof_trace.add_step proof @@ fun () ->
+            Proof_core.proof_res ~pivot:(Lit.term lit_i) lemma_i pr_th)
           pr_th sub_proofs
       in
-      P.add_step proof @@ Rules_.proof_res ~pivot:(Lit.term lit_t_u) pr_th pr
+      Proof_trace.add_step proof @@ fun () ->
+      Proof_core.proof_res ~pivot:(Lit.term lit_t_u) pr_th pr
     in
     (* resolve with theory proofs responsible for some merges, if any. *)
     List.fold_left resolve_with_th_proof p_cc self.th_lemmas
@@ -590,7 +584,7 @@ and task_merge_ self a b e_ab : unit =
             E_node.pp ra E_node.pp a E_node.pp rb E_node.pp b Expl.pp e_ab);
       let th = ref false in
       (* TODO:
-         C1: P.true_neq_false
+         C1: Proof_trace.true_neq_false
          C2: lemma [lits |- true=false]  (and resolve on theory proofs)
          C3: r1 C1 C2
       *)
diff --git a/src/core/proof_core.ml b/src/core/proof_core.ml
index c6b65106..b24d17e7 100644
--- a/src/core/proof_core.ml
+++ b/src/core/proof_core.ml
@@ -6,33 +6,24 @@
 
 type lit = Lit.t
 
-let lemma_cc lits : Proof_term.t = Proof_term.make ~lits "core.lemma-cc"
+let lemma_cc lits : Proof_term.data = Proof_term.make_data ~lits "core.lemma-cc"
 
 let define_term t1 t2 =
-  Proof_term.make ~terms:(Iter.of_list [ t1; t2 ]) "core.define-term"
+  Proof_term.make_data ~terms:[ t1; t2 ] "core.define-term"
 
-let proof_r1 p1 p2 =
-  Proof_term.make ~premises:(Iter.of_list [ p1; p2 ]) "core.r1"
-
-let proof_p1 p1 p2 =
-  Proof_term.make ~premises:(Iter.of_list [ p1; p2 ]) "core.p1"
+let proof_r1 p1 p2 = Proof_term.make_data ~premises:[ p1; p2 ] "core.r1"
+let proof_p1 p1 p2 = Proof_term.make_data ~premises:[ p1; p2 ] "core.p1"
 
 let proof_res ~pivot p1 p2 =
-  Proof_term.make ~terms:(Iter.return pivot)
-    ~premises:(Iter.of_list [ p1; p2 ])
-    "core.res"
+  Proof_term.make_data ~terms:[ pivot ] ~premises:[ p1; p2 ] "core.res"
 
 let with_defs pr defs =
-  Proof_term.make ~premises:(Iter.append (Iter.return pr) defs) "core.with-defs"
+  Proof_term.make_data ~premises:(pr :: defs) "core.with-defs"
 
-let lemma_true t = Proof_term.make ~terms:(Iter.return t) "core.true"
+let lemma_true t = Proof_term.make_data ~terms:[ t ] "core.true"
 
 let lemma_preprocess t1 t2 ~using =
-  Proof_term.make
-    ~terms:(Iter.of_list [ t1; t2 ])
-    ~premises:using "core.preprocess"
+  Proof_term.make_data ~terms:[ t1; t2 ] ~premises:using "core.preprocess"
 
 let lemma_rw_clause pr ~res ~using =
-  Proof_term.make
-    ~premises:(Iter.append (Iter.return pr) using)
-    ~lits:res "core.rw-clause"
+  Proof_term.make_data ~premises:(pr :: using) ~lits:res "core.rw-clause"
diff --git a/src/core/proof_core.mli b/src/core/proof_core.mli
index 3641c14d..6e71e413 100644
--- a/src/core/proof_core.mli
+++ b/src/core/proof_core.mli
@@ -4,56 +4,56 @@ open Sidekick_core_logic
 
 type lit = Lit.t
 
-val lemma_cc : lit Iter.t -> Proof_term.t
+val lemma_cc : lit list -> Proof_term.data
 (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
-       of uninterpreted functions. *)
+     of uninterpreted functions. *)
 
-val define_term : Term.t -> Term.t -> Proof_term.t
+val define_term : Term.t -> Term.t -> Proof_term.data
 (** [define_term cst u proof] defines the new constant [cst] as being equal
-       to [u].
-       The result is a proof of the clause [cst = u] *)
+     to [u].
+     The result is a proof of the clause [cst = u] *)
 
-val proof_p1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
+val proof_p1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.data
 (** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool)
-       and [p2] proves [C \/ t], is the Proof_term.t that produces [C \/ u],
-       i.e unit paramodulation. *)
+     and [p2] proves [C \/ t], is the Proof_term.t that produces [C \/ u],
+     i.e unit paramodulation. *)
 
-val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
+val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.data
 (** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool)
        and [p2] proves [C \/ ¬t], is the Proof_term.t that produces [C \/ u],
        i.e unit resolution. *)
 
 val proof_res :
-  pivot:Term.t -> Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
+  pivot:Term.t -> Proof_term.step_id -> Proof_term.step_id -> Proof_term.data
 (** [proof_res ~pivot p1 p2], where [p1] proves the clause [|- C \/ l]
-       and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot],
-       is the Proof_term.t that produces [C \/ D], i.e boolean resolution. *)
+     and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot],
+     is the Proof_term.t that produces [C \/ D], i.e boolean resolution. *)
 
-val with_defs : Proof_term.step_id -> Proof_term.step_id Iter.t -> Proof_term.t
+val with_defs : Proof_term.step_id -> Proof_term.step_id list -> Proof_term.data
 (** [with_defs pr defs] specifies that [pr] is valid only in
        a context where the definitions [defs] are present. *)
 
-val lemma_true : Term.t -> Proof_term.t
+val lemma_true : Term.t -> Proof_term.data
 (** [lemma_true (true) p] asserts the clause [(true)] *)
 
 val lemma_preprocess :
-  Term.t -> Term.t -> using:Proof_term.step_id Iter.t -> Proof_term.t
+  Term.t -> Term.t -> using:Proof_term.step_id list -> Proof_term.data
 (** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology
-       and that [t] has been preprocessed into [u].
+     and that [t] has been preprocessed into [u].
 
-       The theorem [/\_{eqn in using} eqn |- t=u] is proved using congruence
-       closure, and then resolved against the clauses [using] to obtain
-       a unit equality.
+     The theorem [/\_{eqn in using} eqn |- t=u] is proved using congruence
+     closure, and then resolved against the clauses [using] to obtain
+     a unit equality.
 
-       From now on, [t] and [u] will be used interchangeably.
-       @return a Proof_term.t ID for the clause [(t=u)]. *)
+     From now on, [t] and [u] will be used interchangeably.
+     @return a Proof_term.t ID for the clause [(t=u)]. *)
 
 val lemma_rw_clause :
   Proof_term.step_id ->
-  res:lit Iter.t ->
-  using:Proof_term.step_id Iter.t ->
-  Proof_term.t
+  res:lit list ->
+  using:Proof_term.step_id list ->
+  Proof_term.data
 (** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c],
-       uses the equations [|- p_i = q_i] from [using]
-       to rewrite some literals of [c] into [res]. This is used to preprocess
-       literals of a clause (using {!lemma_preprocess} individually). *)
+     uses the equations [|- p_i = q_i] from [using]
+     to rewrite some literals of [c] into [res]. This is used to preprocess
+     literals of a clause (using {!lemma_preprocess} individually). *)
diff --git a/src/core/proof_sat.ml b/src/core/proof_sat.ml
index 15cb809b..63707072 100644
--- a/src/core/proof_sat.ml
+++ b/src/core/proof_sat.ml
@@ -1,8 +1,10 @@
 type lit = Lit.t
 
-let sat_input_clause lits : Proof_term.t = Proof_term.make "sat.input" ~lits
+let sat_input_clause lits : Proof_term.data =
+  Proof_term.make_data "sat.input" ~lits
 
-let sat_redundant_clause lits ~hyps : Proof_term.t =
-  Proof_term.make "sat.rup" ~lits ~premises:hyps
+let sat_redundant_clause lits ~hyps : Proof_term.data =
+  Proof_term.make_data "sat.rup" ~lits ~premises:(Iter.to_rev_list hyps)
 
-let sat_unsat_core lits : Proof_term.t = Proof_term.make ~lits "sat.unsat-core"
+let sat_unsat_core lits : Proof_term.data =
+  Proof_term.make_data ~lits "sat.unsat-core"
diff --git a/src/core/proof_sat.mli b/src/core/proof_sat.mli
index c9d89a54..f26abdcf 100644
--- a/src/core/proof_sat.mli
+++ b/src/core/proof_sat.mli
@@ -4,12 +4,12 @@ open Proof_term
 
 type lit = Lit.t
 
-val sat_input_clause : lit Iter.t -> Proof_term.t
+val sat_input_clause : lit list -> Proof_term.data
 (** Emit an input clause. *)
 
-val sat_redundant_clause : lit Iter.t -> hyps:step_id Iter.t -> Proof_term.t
+val sat_redundant_clause : lit list -> hyps:step_id Iter.t -> Proof_term.data
 (** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
     The clause must be RUP wrt [hyps]. *)
 
-val sat_unsat_core : lit Iter.t -> Proof_term.t
+val sat_unsat_core : lit list -> Proof_term.data
 (** TODO: is this relevant here? *)
diff --git a/src/core/proof_term.ml b/src/core/proof_term.ml
index 0600a51a..ae0db5b3 100644
--- a/src/core/proof_term.ml
+++ b/src/core/proof_term.ml
@@ -3,18 +3,20 @@ open Sidekick_core_logic
 type step_id = Proof_step.id
 type lit = Lit.t
 
-type t = {
+type data = {
   rule_name: string;
-  lit_args: lit Iter.t;
-  term_args: Term.t Iter.t;
-  subst_args: Subst.t Iter.t;
-  premises: step_id Iter.t;
+  lit_args: lit list;
+  term_args: Term.t list;
+  subst_args: Subst.t list;
+  premises: step_id list;
 }
 
+type t = unit -> data
+
 let pp out _ = Fmt.string out "<proof term>" (* TODO *)
 
-let make ?(lits = Iter.empty) ?(terms = Iter.empty) ?(substs = Iter.empty)
-    ?(premises = Iter.empty) rule_name : t =
+let make_data ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
+    rule_name : data =
   {
     rule_name;
     lit_args = lits;
diff --git a/src/core/proof_term.mli b/src/core/proof_term.mli
index 81ef09c3..c74a2ea4 100644
--- a/src/core/proof_term.mli
+++ b/src/core/proof_term.mli
@@ -7,20 +7,22 @@ open Sidekick_core_logic
 type step_id = Proof_step.id
 type lit = Lit.t
 
-type t = {
+type data = {
   rule_name: string;
-  lit_args: lit Iter.t;
-  term_args: Term.t Iter.t;
-  subst_args: Subst.t Iter.t;
-  premises: step_id Iter.t;
+  lit_args: lit list;
+  term_args: Term.t list;
+  subst_args: Subst.t list;
+  premises: step_id list;
 }
 
+type t = unit -> data
+
 include Sidekick_sigs.PRINT with type t := t
 
-val make :
-  ?lits:lit Iter.t ->
-  ?terms:Term.t Iter.t ->
-  ?substs:Subst.t Iter.t ->
-  ?premises:step_id Iter.t ->
+val make_data :
+  ?lits:lit list ->
+  ?terms:Term.t list ->
+  ?substs:Subst.t list ->
+  ?premises:step_id list ->
   string ->
-  t
+  data
diff --git a/src/sat/solver.ml b/src/sat/solver.ml
index 61e6f43e..c4399c2e 100644
--- a/src/sat/solver.ml
+++ b/src/sat/solver.ml
@@ -467,10 +467,10 @@ let rec proof_of_atom_lvl0_ (self : t) (a : atom) : Proof_step.id =
         if !steps = [] then
           proof_c2
         else
-          Proof_trace.add_step self.proof
-          @@ Proof_sat.sat_redundant_clause
-               (Iter.return (Atom.lit self.store a))
-               ~hyps:Iter.(cons proof_c2 (of_list !steps))
+          Proof_trace.add_step self.proof @@ fun () ->
+          Proof_sat.sat_redundant_clause
+            [ Atom.lit self.store a ]
+            ~hyps:Iter.(cons proof_c2 (of_list !steps))
     in
 
     Atom.set_proof_lvl0 self.store a p;
@@ -559,11 +559,12 @@ let preprocess_clause_ (self : t) (c : Clause.t) : Clause.t =
         k "(@[sat.add-clause.resolved-lvl-0@ :into [@[%a@]]@])"
           (Atom.debug_a store) atoms);
     let proof =
-      let lits = Iter.of_array atoms |> Iter.map (Atom.lit store) in
-      Proof_trace.add_step self.proof
-      @@ Proof_sat.sat_redundant_clause lits
-           ~hyps:
-             Iter.(cons (Clause.proof_step self.store c) (of_list !res0_proofs))
+      Proof_trace.add_step self.proof @@ fun () ->
+      let lits = Util.array_to_list_map (Atom.lit store) atoms in
+      let hyps =
+        Iter.(cons (Clause.proof_step self.store c) (of_list !res0_proofs))
+      in
+      Proof_sat.sat_redundant_clause lits ~hyps
     in
     Clause.make_a store atoms proof ~removable:(Clause.removable store c)
   )
@@ -1005,10 +1006,9 @@ let record_learnt_clause (self : t) ~pool (cr : conflict_res) : unit =
     assert (cr.cr_backtrack_lvl = 0 && decision_level self = 0);
 
     let p =
-      Proof_trace.add_step self.proof
-      @@ Proof_sat.sat_redundant_clause
-           (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store))
-           ~hyps:(Step_vec.to_iter cr.cr_steps)
+      Proof_trace.add_step self.proof @@ fun () ->
+      let lits = Util.array_to_list_map (Atom.lit self.store) cr.cr_learnt in
+      Proof_sat.sat_redundant_clause lits ~hyps:(Step_vec.to_iter cr.cr_steps)
     in
     let uclause = Clause.make_a store ~removable:true cr.cr_learnt p in
     Event.emit self.on_learnt uclause;
@@ -1022,10 +1022,9 @@ let record_learnt_clause (self : t) ~pool (cr : conflict_res) : unit =
   | _ ->
     let fuip = cr.cr_learnt.(0) in
     let p =
-      Proof_trace.add_step self.proof
-      @@ Proof_sat.sat_redundant_clause
-           (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store))
-           ~hyps:(Step_vec.to_iter cr.cr_steps)
+      Proof_trace.add_step self.proof @@ fun () ->
+      let lits = Util.array_to_list_map (Atom.lit self.store) cr.cr_learnt in
+      Proof_sat.sat_redundant_clause lits ~hyps:(Step_vec.to_iter cr.cr_steps)
     in
     let lclause = Clause.make_a store ~removable:true cr.cr_learnt p in
 
@@ -1741,8 +1740,8 @@ let assume self cnf : unit =
     (fun l ->
       let atoms = Util.array_of_list_map (make_atom_ self) l in
       let proof =
-        Proof_trace.add_step self.proof
-        @@ Proof_sat.sat_input_clause (Iter.of_list l)
+        Proof_trace.add_step self.proof @@ fun () ->
+        Proof_sat.sat_input_clause l
       in
       let c = Clause.make_a self.store ~removable:false atoms proof in
       Log.debugf 10 (fun k ->
@@ -1825,10 +1824,10 @@ let resolve_with_lvl0 (self : t) (c : clause) : clause =
   (* no resolution happened *)
   else (
     let proof =
-      let lits = Iter.of_list !res |> Iter.map (Atom.lit self.store) in
+      Proof_trace.add_step self.proof @@ fun () ->
+      let lits = List.rev_map (Atom.lit self.store) !res in
       let hyps = Iter.of_list (Clause.proof_step self.store c :: !lvl0) in
-      Proof_trace.add_step self.proof
-      @@ Proof_sat.sat_redundant_clause lits ~hyps
+      Proof_sat.sat_redundant_clause lits ~hyps
     in
     Clause.make_l self.store ~removable:false !res proof
   )
@@ -1861,8 +1860,9 @@ let mk_unsat (self : t) (us : unsat_cause) : _ unsat_state =
            (* increasing trail order *)
            assert (Atom.equal first @@ List.hd core);
            let proof =
-             let lits = Iter.of_list core |> Iter.map (Atom.lit self.store) in
-             Proof_trace.add_step self.proof @@ Proof_sat.sat_unsat_core lits
+             Proof_trace.add_step self.proof @@ fun () ->
+             let lits = List.rev_map (Atom.lit self.store) core in
+             Proof_sat.sat_unsat_core lits
            in
            Clause.make_l self.store ~removable:false [] proof)
       in
@@ -1937,15 +1937,14 @@ let add_clause self (c : Lit.t list) (pr : Proof_step.id) : unit =
 
 let add_input_clause self (c : Lit.t list) =
   let pr =
-    Proof_trace.add_step self.proof
-    @@ Proof_sat.sat_input_clause (Iter.of_list c)
+    Proof_trace.add_step self.proof @@ fun () -> Proof_sat.sat_input_clause c
   in
   add_clause self c pr
 
 let add_input_clause_a self c =
   let pr =
-    Proof_trace.add_step self.proof
-    @@ Proof_sat.sat_input_clause (Iter.of_array c)
+    Proof_trace.add_step self.proof @@ fun () ->
+    Proof_sat.sat_input_clause (Array.to_list c)
   in
   add_clause_a self c pr
 
diff --git a/src/simplify/sidekick_simplify.ml b/src/simplify/sidekick_simplify.ml
index 2daa4114..3a49c947 100644
--- a/src/simplify/sidekick_simplify.ml
+++ b/src/simplify/sidekick_simplify.ml
@@ -1,10 +1,5 @@
 open Sidekick_core
 
-open struct
-  module P = Proof_trace
-  module Rule_ = Proof_core
-end
-
 type t = {
   tst: Term.store;
   proof: Proof_trace.t;
@@ -68,8 +63,8 @@ let normalize (self : t) (t : Term.t) : (Term.t * Proof_step.id) option =
   else (
     (* proof: [sub_proofs |- t=u] by CC + subproof *)
     let step =
-      P.add_step self.proof
-      @@ Rule_.lemma_preprocess t u ~using:(Bag.to_iter pr_u)
+      Proof_trace.add_step self.proof @@ fun () ->
+      Proof_core.lemma_preprocess t u ~using:(Bag.to_list pr_u)
     in
     Some (u, step)
   )
diff --git a/src/smt/solver.ml b/src/smt/solver.ml
index 670a5630..fb71706c 100644
--- a/src/smt/solver.ml
+++ b/src/smt/solver.ml
@@ -113,7 +113,7 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
    let t_true = Term.true_ tst in
    Sat_solver.add_clause self.solver
      [ Lit.atom t_true ]
-     (P.add_step self.proof @@ Rule_.lemma_true t_true));
+     (P.add_step self.proof @@ fun () -> Rule_.lemma_true t_true));
   self
 
 let[@inline] solver self = self.solver
@@ -173,9 +173,7 @@ let add_clause_l self c p = add_clause self (CCArray.of_list c) p
 
 let assert_terms self c =
   let c = CCList.map Lit.atom c in
-  let pr_c =
-    P.add_step self.proof @@ Proof_sat.sat_input_clause (Iter.of_list c)
-  in
+  let pr_c = P.add_step self.proof @@ fun () -> Proof_sat.sat_input_clause c in
   add_clause_l self c pr_c
 
 let assert_term self t = assert_terms self [ t ]
diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml
index 35d28732..e6e73bb9 100644
--- a/src/smt/solver_internal.ml
+++ b/src/smt/solver_internal.ml
@@ -1,13 +1,6 @@
 open Sigs
-module Proof_rules = Sidekick_core.Proof_sat
-module P_core_rules = Sidekick_core.Proof_core
 module Ty = Term
 
-open struct
-  module P = Proof_trace
-  module Rule_ = Proof_core
-end
-
 type th_states =
   | Ths_nil
   | Ths_cons : {
@@ -200,7 +193,7 @@ module type ARR = sig
   type 'a t
 
   val map : ('a -> 'b) -> 'a t -> 'b t
-  val to_iter : 'a t -> 'a Iter.t
+  val to_list : 'a t -> 'a list
 end
 
 module Preprocess_clause (A : ARR) = struct
@@ -222,16 +215,21 @@ module Preprocess_clause (A : ARR) = struct
         pr_c
       else (
         Stat.incr self.count_preprocess_clause;
-        P.add_step self.proof
-        @@ Rule_.lemma_rw_clause pr_c ~res:(A.to_iter c')
-             ~using:(Iter.of_list !steps)
+        Proof_trace.add_step self.proof @@ fun () ->
+        Proof_core.lemma_rw_clause pr_c ~res:(A.to_list c') ~using:!steps
       )
     in
     c', pr_c'
 end
 [@@inline]
 
-module PC_list = Preprocess_clause (CCList)
+module PC_list = Preprocess_clause (struct
+  type 'a t = 'a list
+
+  let map = CCList.map
+  let to_list l = l
+end)
+
 module PC_arr = Preprocess_clause (CCArray)
 
 let preprocess_clause = PC_list.top
@@ -518,7 +516,9 @@ let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
       in
 
       let c = List.rev_append c1 c2 in
-      let pr = P.add_step self.proof @@ Rule_.lemma_cc (Iter.of_list c) in
+      let pr =
+        Proof_trace.add_step self.proof @@ fun () -> Proof_core.lemma_cc c
+      in
 
       Log.debugf 20 (fun k ->
           k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])"
diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml
index f18edbfd..c0e61cad 100644
--- a/src/th-bool-static/Sidekick_th_bool_static.ml
+++ b/src/th-bool-static/Sidekick_th_bool_static.ml
@@ -36,8 +36,9 @@ end = struct
 
     let add_step_eq a b ~using ~c0 : unit =
       add_step_ @@ mk_step_
-      @@ Proof_core.lemma_rw_clause c0 ~using
-           ~res:(Iter.return (Lit.atom (A.mk_bool tst (B_eq (a, b)))))
+      @@ fun () ->
+      Proof_core.lemma_rw_clause c0 ~using
+        ~res:[ Lit.atom (A.mk_bool tst (B_eq (a, b))) ]
     in
 
     let[@inline] ret u = Some (u, Iter.of_list !steps) in
@@ -81,11 +82,11 @@ end = struct
       Option.iter add_step_ prf_a;
       (match A.view_as_bool a with
       | B_bool true ->
-        add_step_eq t b ~using:(Iter.of_opt prf_a)
+        add_step_eq t b ~using:(Option.to_list prf_a)
           ~c0:(mk_step_ @@ A.P.lemma_ite_true ~ite:t);
         ret b
       | B_bool false ->
-        add_step_eq t c ~using:(Iter.of_opt prf_a)
+        add_step_eq t c ~using:(Option.to_list prf_a)
           ~c0:(mk_step_ @@ A.P.lemma_ite_false ~ite:t);
         ret c
       | _ -> None)
diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml
index 67a4845a..31c8ae3c 100644
--- a/src/th-cstor/Sidekick_th_cstor.ml
+++ b/src/th-cstor/Sidekick_th_cstor.ml
@@ -9,7 +9,7 @@ let name = "th-cstor"
 
 module type ARG = sig
   val view_as_cstor : Term.t -> (Const.t, Term.t) cstor_view
-  val lemma_cstor : Lit.t Iter.t -> Proof_term.t
+  val lemma_cstor : Lit.t list -> Proof_term.data
 end
 
 module Make (A : ARG) : sig
diff --git a/src/th-cstor/Sidekick_th_cstor.mli b/src/th-cstor/Sidekick_th_cstor.mli
index 0cf658a9..024e06da 100644
--- a/src/th-cstor/Sidekick_th_cstor.mli
+++ b/src/th-cstor/Sidekick_th_cstor.mli
@@ -7,7 +7,7 @@ type ('c, 't) cstor_view = T_cstor of 'c * 't array | T_other of 't
 
 module type ARG = sig
   val view_as_cstor : Term.t -> (Const.t, Term.t) cstor_view
-  val lemma_cstor : Lit.t Iter.t -> Proof_term.t
+  val lemma_cstor : Lit.t list -> Proof_term.data
 end
 
 val make : (module ARG) -> SMT.theory
diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml
index bcaae31a..956bec1b 100644
--- a/src/th-data/Sidekick_th_data.ml
+++ b/src/th-data/Sidekick_th_data.ml
@@ -186,7 +186,7 @@ end = struct
           let t1 = E_node.term c1.c_n in
           let t2 = E_node.term c2.c_n in
           mk_expl t1 t2 @@ Proof_trace.add_step proof
-          @@ A.P.lemma_cstor_inj t1 t2 i
+          @@ fun () -> A.P.lemma_cstor_inj t1 t2 i
         in
 
         assert (CCArray.length c1.c_args = CCArray.length c2.c_args);
@@ -199,7 +199,7 @@ end = struct
         let expl =
           let t1 = E_node.term c1.c_n and t2 = E_node.term c2.c_n in
           mk_expl t1 t2 @@ Proof_trace.add_step proof
-          @@ A.P.lemma_cstor_distinct t1 t2
+          @@ fun () -> A.P.lemma_cstor_distinct t1 t2
         in
 
         Error (CC.Handler_action.Conflict expl)
@@ -332,15 +332,14 @@ end = struct
            with exhaustiveness: [|- is-c(t)] *)
         let proof =
           let pr_isa =
-            Proof_trace.add_step self.proof
-            @@ A.P.lemma_isa_split t
-                 (Iter.return @@ Act.mk_lit (A.mk_is_a self.tst cstor t))
+            Proof_trace.add_step self.proof @@ fun () ->
+            A.P.lemma_isa_split t [ Lit.atom (A.mk_is_a self.tst cstor t) ]
           and pr_eq_sel =
-            Proof_trace.add_step self.proof
-            @@ A.P.lemma_select_cstor ~cstor_t:u t
+            Proof_trace.add_step self.proof @@ fun () ->
+            A.P.lemma_select_cstor ~cstor_t:u t
           in
-          Proof_trace.add_step self.proof
-          @@ Proof_core.proof_r1 pr_isa pr_eq_sel
+          Proof_trace.add_step self.proof @@ fun () ->
+          Proof_core.proof_r1 pr_isa pr_eq_sel
         in
 
         Term.Tbl.add self.single_cstor_preproc_done t ();
@@ -394,8 +393,8 @@ end = struct
                %a@])"
               name Term.pp_debug t is_true E_node.pp n Monoid_cstor.pp cstor);
         let pr =
-          Proof_trace.add_step self.proof
-          @@ A.P.lemma_isa_cstor ~cstor_t:(E_node.term cstor.c_n) t
+          Proof_trace.add_step self.proof @@ fun () ->
+          A.P.lemma_isa_cstor ~cstor_t:(E_node.term cstor.c_n) t
         in
         let n_bool = CC.n_bool cc is_true in
         let expl =
@@ -421,8 +420,8 @@ end = struct
         assert (i < CCArray.length cstor.c_args);
         let u_i = CCArray.get cstor.c_args i in
         let pr =
-          Proof_trace.add_step self.proof
-          @@ A.P.lemma_select_cstor ~cstor_t:(E_node.term cstor.c_n) t
+          Proof_trace.add_step self.proof @@ fun () ->
+          A.P.lemma_select_cstor ~cstor_t:(E_node.term cstor.c_n) t
         in
         let expl =
           Expl.(
@@ -458,9 +457,9 @@ end = struct
             name Monoid_parents.pp_is_a is_a2 is_true E_node.pp n1 E_node.pp n2
             Monoid_cstor.pp c1);
       let pr =
-        Proof_trace.add_step self.proof
-        @@ A.P.lemma_isa_cstor ~cstor_t:(E_node.term c1.c_n)
-             (E_node.term is_a2.is_a_n)
+        Proof_trace.add_step self.proof @@ fun () ->
+        A.P.lemma_isa_cstor ~cstor_t:(E_node.term c1.c_n)
+          (E_node.term is_a2.is_a_n)
       in
       let n_bool = CC.n_bool cc is_true in
       let expl =
@@ -487,9 +486,9 @@ end = struct
               E_node.pp n2 sel2.sel_idx Monoid_cstor.pp c1);
         assert (sel2.sel_idx < CCArray.length c1.c_args);
         let pr =
-          Proof_trace.add_step self.proof
-          @@ A.P.lemma_select_cstor ~cstor_t:(E_node.term c1.c_n)
-               (E_node.term sel2.sel_n)
+          Proof_trace.add_step self.proof @@ fun () ->
+          A.P.lemma_select_cstor ~cstor_t:(E_node.term c1.c_n)
+            (E_node.term sel2.sel_n)
         in
         let u_i = CCArray.get c1.c_args sel2.sel_idx in
         let expl =
@@ -598,10 +597,13 @@ end = struct
           (* conflict: the [path] forms a cycle *)
           let path = (n, node) :: path in
           let pr =
-            Proof_trace.add_step self.proof
-            @@ A.P.lemma_acyclicity
-                 (Iter.of_list path
-                 |> Iter.map (fun (a, b) -> E_node.term a, E_node.term b.repr))
+            Proof_trace.add_step self.proof @@ fun () ->
+            let path =
+              List.rev_map
+                (fun (a, b) -> E_node.term a, E_node.term b.repr)
+                path
+            in
+            A.P.lemma_acyclicity path
           in
           let expl =
             let subs =
@@ -654,7 +656,9 @@ end = struct
         Log.debugf 50 (fun k ->
             k "(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])" name
               Term.pp_debug u Term.pp_debug rhs Lit.pp lit);
-        let pr = Proof_trace.add_step self.proof @@ A.P.lemma_isa_sel t in
+        let pr =
+          Proof_trace.add_step self.proof @@ fun () -> A.P.lemma_isa_sel t
+        in
         (* merge [u] and [rhs] *)
         CC.merge_t (SI.cc solver) u rhs
           (Expl.mk_theory u rhs
@@ -680,12 +684,11 @@ end = struct
         |> Iter.to_rev_list
       in
       SI.add_clause_permanent solver acts c
-        (Proof_trace.add_step self.proof
-        @@ A.P.lemma_isa_split t (Iter.of_list c));
+        (Proof_trace.add_step self.proof @@ fun () -> A.P.lemma_isa_split t c);
       Iter.diagonal_l c (fun (l1, l2) ->
           let pr =
-            Proof_trace.add_step self.proof
-            @@ A.P.lemma_isa_disj (Lit.neg l1) (Lit.neg l2)
+            Proof_trace.add_step self.proof @@ fun () ->
+            A.P.lemma_isa_disj (Lit.neg l1) (Lit.neg l2)
           in
           SI.add_clause_permanent solver acts [ Lit.neg l1; Lit.neg l2 ] pr)
     )
diff --git a/src/th-data/th_intf.ml b/src/th-data/th_intf.ml
index 1004e5b0..500f7b85 100644
--- a/src/th-data/th_intf.ml
+++ b/src/th-data/th_intf.ml
@@ -22,35 +22,35 @@ type ('c, 'ty) data_ty_view =
   | Ty_other
 
 module type PROOF_RULES = sig
-  val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t
+  val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.data
   (** [lemma_isa_cstor (d …) (is-c t)] returns the clause
       [(c …) = t |- is-c t] or [(d …) = t |- ¬ (is-c t)] *)
 
-  val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t
+  val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.data
   (** [lemma_select_cstor (c t1…tn) (sel-c-i t)]
       returns a proof of [t = c t1…tn |- (sel-c-i t) = ti] *)
 
-  val lemma_isa_split : Term.t -> Lit.t Iter.t -> Proof_term.t
+  val lemma_isa_split : Term.t -> Lit.t list -> Proof_term.data
   (** [lemma_isa_split t lits] is the proof of
       [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *)
 
-  val lemma_isa_sel : Term.t -> Proof_term.t
+  val lemma_isa_sel : Term.t -> Proof_term.data
   (** [lemma_isa_sel (is-c t)] is the proof of
       [is-c t |- t = c (sel-c-1 t)…(sel-c-n t)] *)
 
-  val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.t
+  val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.data
   (** [lemma_isa_disj (is-c t) (is-d t)] is the proof
       of [¬ (is-c t) \/ ¬ (is-c t)] *)
 
-  val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.t
+  val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.data
   (** [lemma_cstor_inj (c t1…tn) (c u1…un) i] is the proof of
       [c t1…tn = c u1…un |- ti = ui] *)
 
-  val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.t
+  val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.data
   (** [lemma_isa_distinct (c …) (d …)] is the proof
       of the unit clause [|- (c …) ≠ (d …)] *)
 
-  val lemma_acyclicity : (Term.t * Term.t) Iter.t -> Proof_term.t
+  val lemma_acyclicity : (Term.t * Term.t) list -> Proof_term.data
   (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false]
       by acyclicity. *)
 end
diff --git a/src/th-lra/intf.ml b/src/th-lra/intf.ml
index c9b60c30..8e2cd63f 100644
--- a/src/th-lra/intf.ml
+++ b/src/th-lra/intf.ml
@@ -44,7 +44,7 @@ module type ARG = sig
   val has_ty_real : Term.t -> bool
   (** Does this term have the type [Real] *)
 
-  val lemma_lra : Lit.t Iter.t -> Proof_term.t
+  val lemma_lra : Lit.t list -> Proof_term.data
 
   module Gensym : sig
     type t
diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml
index 80bd87cd..d1666f2d 100644
--- a/src/th-lra/sidekick_th_lra.ml
+++ b/src/th-lra/sidekick_th_lra.ml
@@ -248,13 +248,13 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         proxy)
 
   let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits =
-    let pr = Proof_trace.add_step PA.proof @@ A.lemma_lra (Iter.of_list lits) in
+    let pr = Proof_trace.add_step PA.proof @@ fun () -> A.lemma_lra lits in
     let pr =
       match using with
       | None -> pr
       | Some using ->
-        Proof_trace.add_step PA.proof
-        @@ Proof_core.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using
+        Proof_trace.add_step PA.proof @@ fun () ->
+        Proof_core.lemma_rw_clause pr ~res:lits ~using
     in
     PA.add_clause lits pr
 
@@ -396,12 +396,12 @@ module Make (A : ARG) = (* : S with module A = A *) struct
   let simplify (self : state) (_recurse : _) (t : Term.t) :
       (Term.t * Proof_step.id Iter.t) option =
     let proof_eq t u =
-      Proof_trace.add_step self.proof
-      @@ A.lemma_lra (Iter.return (Lit.atom (Term.eq self.tst t u)))
+      Proof_trace.add_step self.proof @@ fun () ->
+      A.lemma_lra [ Lit.atom (Term.eq self.tst t u) ]
     in
     let proof_bool t ~sign:b =
       let lit = Lit.atom ~sign:b t in
-      Proof_trace.add_step self.proof @@ A.lemma_lra (Iter.return lit)
+      Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ]
     in
 
     match A.view_as_lra t with
@@ -467,7 +467,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       |> List.rev_map Lit.neg
     in
     let pr =
-      Proof_trace.add_step (SI.proof si) @@ A.lemma_lra (Iter.of_list confl)
+      Proof_trace.add_step (SI.proof si) @@ fun () -> A.lemma_lra confl
     in
     SI.raise_conflict si acts confl pr
 
@@ -478,8 +478,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       SI.propagate si acts lit ~reason:(fun () ->
           let lits = CCList.flat_map (Tag.to_lits si) reason in
           let pr =
-            Proof_trace.add_step (SI.proof si)
-            @@ A.lemma_lra Iter.(cons lit (of_list lits))
+            Proof_trace.add_step (SI.proof si) @@ fun () ->
+            A.lemma_lra (lit :: lits)
           in
           CCList.flat_map (Tag.to_lits si) reason, pr)
     | _ -> ()
@@ -525,7 +525,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         (* [c=0] when [c] is not 0 *)
         let lit = Lit.atom ~sign:false @@ Term.eq self.tst t1 t2 in
         let pr =
-          Proof_trace.add_step self.proof @@ A.lemma_lra (Iter.return lit)
+          Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ]
         in
         SI.add_clause_permanent si acts [ lit ] pr
       )
diff --git a/src/util/Bag.ml b/src/util/Bag.ml
index 53e0800b..ed020939 100644
--- a/src/util/Bag.ml
+++ b/src/util/Bag.ml
@@ -44,6 +44,8 @@ let rec fold f acc = function
   | L x -> f acc x
   | N (a, b) -> fold f (fold f acc a) b
 
+let to_list self = fold (fun acc x -> x :: acc) [] self
+
 let[@unroll 2] rec to_iter t yield =
   match t with
   | E -> ()
diff --git a/src/util/Bag.mli b/src/util/Bag.mli
index 641e4dc4..2eb559eb 100644
--- a/src/util/Bag.mli
+++ b/src/util/Bag.mli
@@ -15,6 +15,7 @@ val snoc : 'a t -> 'a -> 'a t
 val append : 'a t -> 'a t -> 'a t
 val of_iter : 'a Iter.t -> 'a t
 val to_iter : 'a t -> 'a Iter.t
+val to_list : 'a t -> 'a list
 val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
 val iter : ('a -> unit) -> 'a t -> unit