refactor(proofs): make proof terms a recursive term

src/core/proof_core.ml

@@ -6,24 +6,24 @@
 
 type lit = Lit.t
 
-let lemma_cc lits : Proof_term.data = Proof_term.make_data ~lits "core.lemma-cc"
+let lemma_cc lits : Proof_term.t = Proof_term.apply_rule ~lits "core.lemma-cc"
 
 let define_term t1 t2 =
-  Proof_term.make_data ~terms:[ t1; t2 ] "core.define-term"
+  Proof_term.apply_rule ~terms:[ t1; t2 ] "core.define-term"
 
-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_r1 p1 p2 = Proof_term.apply_rule ~premises:[ p1; p2 ] "core.r1"
+let proof_p1 p1 p2 = Proof_term.apply_rule ~premises:[ p1; p2 ] "core.p1"
 
 let proof_res ~pivot p1 p2 =
-  Proof_term.make_data ~terms:[ pivot ] ~premises:[ p1; p2 ] "core.res"
+  Proof_term.apply_rule ~terms:[ pivot ] ~premises:[ p1; p2 ] "core.res"
 
 let with_defs pr defs =
-  Proof_term.make_data ~premises:(pr :: defs) "core.with-defs"
+  Proof_term.apply_rule ~premises:(pr :: defs) "core.with-defs"
 
-let lemma_true t = Proof_term.make_data ~terms:[ t ] "core.true"
+let lemma_true t = Proof_term.apply_rule ~terms:[ t ] "core.true"
 
 let lemma_preprocess t1 t2 ~using =
-  Proof_term.make_data ~terms:[ t1; t2 ] ~premises:using "core.preprocess"
+  Proof_term.apply_rule ~terms:[ t1; t2 ] ~premises:using "core.preprocess"
 
 let lemma_rw_clause pr ~res ~using =
-  Proof_term.make_data ~premises:(pr :: using) ~lits:res "core.rw-clause"
+  Proof_term.apply_rule ~premises:(pr :: using) ~lits:res "core.rw-clause"

src/core/proof_core.mli

@@ -4,40 +4,40 @@ open Sidekick_core_logic
 
 type lit = Lit.t
 
-val lemma_cc : lit list -> Proof_term.data
+val lemma_cc : lit list -> Proof_term.t
 (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
      of uninterpreted functions. *)
 
-val define_term : Term.t -> Term.t -> Proof_term.data
+val define_term : Term.t -> Term.t -> Proof_term.t
 (** [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] *)
 
-val proof_p1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.data
+val proof_p1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
 (** [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. *)
 
-val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.data
+val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
 (** [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.data
+  pivot:Term.t -> Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
 (** [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. *)
 
-val with_defs : Proof_term.step_id -> Proof_term.step_id list -> Proof_term.data
+val with_defs : Proof_term.step_id -> Proof_term.step_id list -> Proof_term.t
 (** [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.data
+val lemma_true : Term.t -> Proof_term.t
 (** [lemma_true (true) p] asserts the clause [(true)] *)
 
 val lemma_preprocess :
-  Term.t -> Term.t -> using:Proof_term.step_id list -> Proof_term.data
+  Term.t -> Term.t -> using:Proof_term.step_id list -> Proof_term.t
 (** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology
      and that [t] has been preprocessed into [u].
 
@@ -52,7 +52,7 @@ val lemma_rw_clause :
   Proof_term.step_id ->
   res:lit list ->
   using:Proof_term.step_id list ->
-  Proof_term.data
+  Proof_term.t
 (** [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

src/core/proof_sat.ml

@@ -1,10 +1,10 @@
 type lit = Lit.t
 
-let sat_input_clause lits : Proof_term.data =
-  Proof_term.make_data "sat.input" ~lits
+let sat_input_clause lits : Proof_term.t =
+  Proof_term.apply_rule "sat.input" ~lits
 
-let sat_redundant_clause lits ~hyps : Proof_term.data =
-  Proof_term.make_data "sat.rup" ~lits ~premises:(Iter.to_rev_list hyps)
+let sat_redundant_clause lits ~hyps : Proof_term.t =
+  Proof_term.apply_rule "sat.rup" ~lits ~premises:(Iter.to_rev_list hyps)
 
-let sat_unsat_core lits : Proof_term.data =
-  Proof_term.make_data ~lits "sat.unsat-core"
+let sat_unsat_core lits : Proof_term.t =
+  Proof_term.apply_rule ~lits "sat.unsat-core"

src/core/proof_sat.mli

@@ -4,12 +4,12 @@ open Proof_term
 
 type lit = Lit.t
 
-val sat_input_clause : lit list -> Proof_term.data
+val sat_input_clause : lit list -> Proof_term.t
 (** Emit an input clause. *)
 
-val sat_redundant_clause : lit list -> hyps:step_id Iter.t -> Proof_term.data
+val sat_redundant_clause : lit list -> hyps:step_id Iter.t -> Proof_term.t
 (** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
     The clause must be RUP wrt [hyps]. *)
 
-val sat_unsat_core : lit list -> Proof_term.data
+val sat_unsat_core : lit list -> Proof_term.t
 (** TODO: is this relevant here? *)

src/core/proof_term.ml

@@ -1,9 +1,10 @@
 open Sidekick_core_logic
 
 type step_id = Proof_step.id
+type local_ref = int
 type lit = Lit.t
 
-type data = {
+type rule_apply = {
   rule_name: string;
   lit_args: lit list;
   term_args: Term.t list;
@@ -11,12 +12,27 @@ type data = {
   premises: step_id list;
 }
 
-type t = unit -> data
+type t =
+  | P_ref of step_id
+  | P_local of local_ref
+  | P_let of (local_ref * t) list * t
+  | P_apply of rule_apply
+
+type delayed = unit -> t
 
 let pp out _ = Fmt.string out "<proof term>" (* TODO *)
 
-let make_data ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
-    rule_name : data =
+let local_ref id = P_local id
+let ref_ id = P_ref id
+
+let let_ bs r =
+  match bs with
+  | [] -> r
+  | _ -> P_let (bs, r)
+
+let apply_rule ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
+    rule_name : t =
+  P_apply
     {
       rule_name;
       lit_args = lits;

src/core/proof_term.mli

@@ -5,9 +5,10 @@
 open Sidekick_core_logic
 
 type step_id = Proof_step.id
+type local_ref = int
 type lit = Lit.t
 
-type data = {
+type rule_apply = {
   rule_name: string;
   lit_args: lit list;
   term_args: Term.t list;
@@ -15,14 +16,24 @@ type data = {
   premises: step_id list;
 }
 
-type t = unit -> data
+type t =
+  | P_ref of step_id
+  | P_local of local_ref  (** Local reference, in a let *)
+  | P_let of (local_ref * t) list * t
+  | P_apply of rule_apply
+
+type delayed = unit -> t
 
 include Sidekick_sigs.PRINT with type t := t
 
-val make_data :
+val ref_ : step_id -> t
+val local_ref : local_ref -> t
+val let_ : (local_ref * t) list -> t -> t
+
+val apply_rule :
   ?lits:lit list ->
   ?terms:Term.t list ->
   ?substs:Subst.t list ->
   ?premises:step_id list ->
   string ->
-  data
+  t

src/core/proof_trace.ml

@@ -1,6 +1,5 @@
 type lit = Lit.t
 type step_id = Proof_step.id
-type proof_term = Proof_term.t
 
 module Step_vec = struct
   type elt = step_id
@@ -26,7 +25,7 @@ end
 
 module type DYN = sig
   val enabled : unit -> bool
-  val add_step : proof_term -> step_id
+  val add_step : Proof_term.delayed -> step_id
   val add_unsat : step_id -> unit
   val delete : step_id -> unit
 end

src/core/proof_trace.mli

@@ -17,8 +17,6 @@ type step_id = Proof_step.id
 module Step_vec : Vec_sig.BASE with type elt = step_id
 (** A vector indexed by steps. *)
 
-type proof_term = Proof_term.t
-
 (** {2 Traces} *)
 
 type t
@@ -34,7 +32,7 @@ type t
 val enabled : t -> bool
 (** Is proof tracing enabled? *)
 
-val add_step : t -> proof_term -> step_id
+val add_step : t -> Proof_term.delayed -> step_id
 (** Create a new step in the trace. *)
 
 val add_unsat : t -> step_id -> unit
@@ -57,7 +55,7 @@ val dummy : t
 
 module type DYN = sig
   val enabled : unit -> bool
-  val add_step : proof_term -> step_id
+  val add_step : Proof_term.delayed -> step_id
   val add_unsat : step_id -> unit
   val delete : step_id -> unit
 end

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -44,7 +44,7 @@ end = struct
     let[@inline] ret u = Some (u, Iter.of_list !steps) in
     (* proof is [t <=> u] *)
     let ret_bequiv t1 u =
-      add_step_ @@ mk_step_ @@ A.P.lemma_bool_equiv t1 u;
+      (add_step_ @@ mk_step_ @@ fun () -> A.P.lemma_bool_equiv t1 u);
       ret u
     in
 
@@ -83,11 +83,11 @@ end = struct
       (match A.view_as_bool a with
       | B_bool true ->
         add_step_eq t b ~using:(Option.to_list prf_a)
-          ~c0:(mk_step_ @@ A.P.lemma_ite_true ~ite:t);
+          ~c0:(mk_step_ @@ fun () -> A.P.lemma_ite_true ~ite:t);
         ret b
       | B_bool false ->
         add_step_eq t c ~using:(Option.to_list prf_a)
-          ~c0:(mk_step_ @@ A.P.lemma_ite_false ~ite:t);
+          ~c0:(mk_step_ @@ fun () -> A.P.lemma_ite_false ~ite:t);
         ret c
       | _ -> None)
     | B_equiv (a, b) when is_true a -> ret_bequiv t b
@@ -140,26 +140,26 @@ end = struct
       PA.add_clause
         [ Lit.neg lit; Lit.neg a; b ]
         (if is_xor then
-          mk_step_ @@ A.P.lemma_bool_c "xor-e+" [ t ]
+          mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-e+" [ t ]
         else
-          mk_step_ @@ A.P.lemma_bool_c "eq-e" [ t; t_a ]);
+          mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-e" [ t; t_a ]);
       PA.add_clause
         [ Lit.neg lit; Lit.neg b; a ]
         (if is_xor then
-          mk_step_ @@ A.P.lemma_bool_c "xor-e-" [ t ]
+          mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-e-" [ t ]
         else
-          mk_step_ @@ A.P.lemma_bool_c "eq-e" [ t; t_b ]);
+          mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-e" [ t; t_b ]);
       PA.add_clause [ lit; a; b ]
         (if is_xor then
-          mk_step_ @@ A.P.lemma_bool_c "xor-i" [ t; t_a ]
+          mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-i" [ t; t_a ]
         else
-          mk_step_ @@ A.P.lemma_bool_c "eq-i+" [ t ]);
+          mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-i+" [ t ]);
       PA.add_clause
         [ lit; Lit.neg a; Lit.neg b ]
         (if is_xor then
-          mk_step_ @@ A.P.lemma_bool_c "xor-i" [ t; t_b ]
+          mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-i" [ t; t_b ]
         else
-          mk_step_ @@ A.P.lemma_bool_c "eq-i-" [ t ])
+          mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-i-" [ t ])
     in
 
     (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
@@ -177,11 +177,11 @@ end = struct
         (fun t_u u ->
           PA.add_clause
             [ Lit.neg lit; u ]
-            (mk_step_ @@ A.P.lemma_bool_c "and-e" [ t; t_u ]))
+            (mk_step_ @@ fun () -> A.P.lemma_bool_c "and-e" [ t; t_u ]))
         t_subs subs;
       PA.add_clause
         (lit :: List.map Lit.neg subs)
-        (mk_step_ @@ A.P.lemma_bool_c "and-i" [ t ])
+        (mk_step_ @@ fun () -> A.P.lemma_bool_c "and-i" [ t ])
     | B_or l ->
       let t_subs = Iter.to_list l in
       let subs = List.map PA.mk_lit t_subs in
@@ -192,10 +192,10 @@ end = struct
         (fun t_u u ->
           PA.add_clause
             [ Lit.neg u; lit ]
-            (mk_step_ @@ A.P.lemma_bool_c "or-i" [ t; t_u ]))
+            (mk_step_ @@ fun () -> A.P.lemma_bool_c "or-i" [ t; t_u ]))
         t_subs subs;
       PA.add_clause (Lit.neg lit :: subs)
-        (mk_step_ @@ A.P.lemma_bool_c "or-e" [ t ])
+        (mk_step_ @@ fun () -> A.P.lemma_bool_c "or-e" [ t ])
     | B_imply (t_args, t_u) ->
       (* transform into [¬args \/ u] on the fly *)
       let t_args = Iter.to_list t_args in
@@ -211,18 +211,18 @@ end = struct
         (fun t_u u ->
           PA.add_clause
             [ Lit.neg u; lit ]
-            (mk_step_ @@ A.P.lemma_bool_c "imp-i" [ t; t_u ]))
+            (mk_step_ @@ fun () -> A.P.lemma_bool_c "imp-i" [ t; t_u ]))
         (t_u :: t_args) subs;
       PA.add_clause (Lit.neg lit :: subs)
-        (mk_step_ @@ A.P.lemma_bool_c "imp-e" [ t ])
+        (mk_step_ @@ fun () -> A.P.lemma_bool_c "imp-e" [ t ])
     | B_ite (a, b, c) ->
       let lit_a = PA.mk_lit a in
       PA.add_clause
         [ Lit.neg lit_a; PA.mk_lit (eq self.tst t b) ]
-        (mk_step_ @@ A.P.lemma_ite_true ~ite:t);
+        (mk_step_ @@ fun () -> A.P.lemma_ite_true ~ite:t);
       PA.add_clause
         [ lit_a; PA.mk_lit (eq self.tst t c) ]
-        (mk_step_ @@ A.P.lemma_ite_false ~ite:t)
+        (mk_step_ @@ fun () -> A.P.lemma_ite_false ~ite:t)
     | B_eq _ | B_neq _ -> ()
     | B_equiv (a, b) -> equiv_ si ~t ~is_xor:false a b
     | B_xor (a, b) -> equiv_ si ~t ~is_xor:true a 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 list -> Proof_term.data
+  val lemma_cstor : Lit.t list -> Proof_term.t
 end
 
 module Make (A : ARG) : sig

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 list -> Proof_term.data
+  val lemma_cstor : Lit.t list -> Proof_term.t
 end
 
 val make : (module ARG) -> SMT.theory

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.data
+  val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t
   (** [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.data
+  val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t
   (** [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 list -> Proof_term.data
+  val lemma_isa_split : Term.t -> Lit.t list -> Proof_term.t
   (** [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.data
+  val lemma_isa_sel : Term.t -> Proof_term.t
   (** [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.data
+  val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.t
   (** [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.data
+  val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.t
   (** [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.data
+  val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.t
   (** [lemma_isa_distinct (c …) (d …)] is the proof
       of the unit clause [|- (c …) ≠ (d …)] *)
 
-  val lemma_acyclicity : (Term.t * Term.t) list -> Proof_term.data
+  val lemma_acyclicity : (Term.t * Term.t) list -> Proof_term.t
   (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false]
       by acyclicity. *)
 end

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 list -> Proof_term.data
+  val lemma_lra : Lit.t list -> Proof_term.t
 
   module Gensym : sig
     type t