refactor(proof): more and better constructs; compile again

src/base-term/Base_types.ml

@@ -1094,11 +1094,6 @@ module Cstor = struct
   let pp out c = ID.pp out c.cstor_id
 end
 
-module Proof = struct
-  type t = Default
-  let default = Default
-end
-
 module Statement = struct
   type t = statement =
     | Stmt_set_logic of string

src/base-term/Proof.ml

@@ -0,0 +1,135 @@
+open Base_types
+
+module T = Term
+module Ty = Ty
+type term = T.t
+type ty = Ty.t
+
+type lit =
+  | L_eq of term * term
+  | L_neq of term * term
+  | L_a of term
+  | L_na of term
+
+let not = function
+  | L_eq (a,b) -> L_neq(a,b)
+  | L_neq (a,b) -> L_eq(a,b)
+  | L_a t -> L_na t
+  | L_na t -> L_a t
+
+let pp_lit out = function
+  | L_eq (t,u) -> Fmt.fprintf out "(@[+@ (@[=@ %a@ %a@])@])" T.pp t T.pp u
+  | L_neq (t,u) -> Fmt.fprintf out "(@[-@ (@[=@ %a@ %a@])@])" T.pp t T.pp u
+  | L_a t -> Fmt.fprintf out "(@[+@ %a@])" T.pp t
+  | L_na t -> Fmt.fprintf out "(@[-@ %a@])" T.pp t
+
+let a t = L_a t
+let na t = L_na t
+let eq t u = L_eq (t,u)
+let neq t u = L_neq (t,u)
+let lit_st (t,b) = if b then a t else na t
+
+type clause = lit list
+
+type t =
+  | Unspecified
+  | Sorry (* NOTE: v. bad as we don't even specify the return *)
+  | Sorry_c of clause
+  | Refl of term
+  | CC_lemma_imply of t list * term * term
+  | CC_lemma of clause
+  | Assertion of term
+  | Assertion_c of clause
+  | Hres of t * hres_step list
+  | DT_isa_split of ty * term list
+  | DT_isa_disj of ty * term * term
+  | DT_cstor_inj of Cstor.t * int * term list * term list (* [c t…=c u… |- t_i=u_i] *)
+  | Bool_true_is_true
+  | Bool_true_neq_false
+  | Bool_eq of term * term (* equal by pure boolean reasoning *)
+  | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *)
+  | Ite_false of term
+  | LRA of clause
+
+and hres_step =
+  | R of { pivot: term; p: t}
+  | R1 of t
+  | P of { lhs: term; rhs: term; p: t}
+  | P1 of t
+
+let r p ~pivot : hres_step = R { pivot; p }
+let r1 p = R1 p
+let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs }
+let p1 p = P1 p
+
+let default=Unspecified
+let sorry_c c = Sorry_c (Iter.to_rev_list c)
+let sorry_c_l c = Sorry_c c
+let sorry = Sorry
+let refl t : t = Refl t
+let make_cc iter : t = CC_lemma (Iter.to_rev_list iter)
+let cc_lemma c : t = CC_lemma (Iter.to_rev_list c)
+let cc_imply_l l t u : t = CC_lemma_imply (l, t, u)
+let cc_imply2 h1 h2 t u : t = CC_lemma_imply ([h1; h2], t, u)
+let assertion t = Assertion t
+let assertion_c c = Assertion_c (Iter.to_rev_list c)
+let assertion_c_l c = Assertion_c c
+
+let isa_split ty i = DT_isa_split (ty, Iter.to_rev_list i)
+let isa_disj ty t u = DT_isa_disj (ty, t, u)
+let cstor_inj c i t u = DT_cstor_inj (c, i, t, u)
+
+let ite_true t = Ite_true t
+let ite_false t = Ite_false t
+let true_is_true : t = Bool_true_is_true
+let true_neq_false : t = Bool_true_neq_false
+let bool_eq a b : t = Bool_eq (a,b)
+
+let hres_l c l : t = Hres (c,l)
+let hres_iter c i : t = Hres (c, Iter.to_list i)
+
+let lra_l c : t = LRA c
+let lra c = LRA (Iter.to_rev_list c)
+
+let rec pp out (self:t) : unit =
+  let pp_l ppx out l = Fmt.(list ~sep:(return "@ ") ppx) out l in
+  let pp_cl out c = Fmt.fprintf out "(@[cl@ %a@])" (pp_l pp_lit) c in
+  match self with
+  | Unspecified -> Fmt.string out "<unspecified>"
+  | CC_lemma l ->
+    Fmt.fprintf out "(@[cc-lemma@ %a@])" pp_cl l
+  | CC_lemma_imply (l,t,u) ->
+    Fmt.fprintf out "(@[cc-lemma-imply@ (@[%a@])@ (@[=@ %a@ %a@])@])"
+      (pp_l pp) l T.pp t T.pp u
+  | Refl t -> Fmt.fprintf out "(@[refl@ %a@])" T.pp t
+  | Sorry -> Fmt.string out "sorry"
+  | Sorry_c c -> Fmt.fprintf out "(@[sorry-c@ %a@])" pp_cl c
+  | Bool_true_is_true -> Fmt.string out "true-is-true"
+  | Bool_true_neq_false -> Fmt.string out "(@[!= T F@])"
+  | Bool_eq (a,b) -> Fmt.fprintf out "(@[bool-eq@ %a@ %a@])" T.pp a T.pp b
+  | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" T.pp t
+  | Assertion_c c ->
+    Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c
+  | Hres (c, l) ->
+    Fmt.fprintf out "(@[hres@ (@[init@ %a@]) %a@])" pp c
+      (pp_l pp_hres_step) l
+  | DT_isa_split (ty,l) ->
+    Fmt.fprintf out "(@[dt.isa.split@ (@[ty %a@])@ (@[cases@ %a@])@])"
+      Ty.pp ty (pp_l T.pp) l
+  | DT_isa_disj (ty,t,u) ->
+    Fmt.fprintf out "(@[dt.isa.disj@ (@[ty %a@])@ %a@ %a@])" Ty.pp ty T.pp t T.pp u
+  | DT_cstor_inj (c,i,ts,us) ->
+    Fmt.fprintf out "(@[dt.cstor.inj %d@ (@[%a@ %a@])@ (@[%a@ %a@])@])"
+      i Cstor.pp c (pp_l T.pp) ts Cstor.pp c (pp_l T.pp) us
+  | Ite_true t -> Fmt.fprintf out "(@[ite-true@ %a@])" T.pp t
+  | Ite_false t -> Fmt.fprintf out "(@[ite-false@ %a@])" T.pp t
+  | LRA c -> Fmt.fprintf out "(@[lra@ %a@])" pp_cl c
+
+and pp_hres_step out = function
+  | R {pivot; p} ->
+    Fmt.fprintf out "(@[r@ (@[pivot@ %a@])@ %a@])" T.pp pivot pp p
+  | R1 p -> Fmt.fprintf out "(@[r1@ %a@])"  pp p
+  | P {p; lhs; rhs} ->
+    Fmt.fprintf out "(@[r@ (@[lhs@ %a@])@ (@[rhs@ %a@])@ %a@])"
+      T.pp lhs T.pp rhs pp p
+  | P1 p -> Fmt.fprintf out "(@[p1@ %a@])"  pp p

src/base-term/Proof.mli

@@ -0,0 +1,16 @@
+open Base_types
+
+include Sidekick_core.PROOF
+  with type term = Term.t
+   and type ty = Ty.t
+
+val isa_split : ty -> term Iter.t -> t
+val isa_disj : ty -> term -> term -> t
+val cstor_inj : Cstor.t -> int -> term list -> term list -> t
+
+val bool_eq : term -> term -> t
+val ite_true : term -> t
+val ite_false : term -> t
+
+val lra : lit Iter.t -> t
+val lra_l : lit list -> t

src/base-term/Sidekick_base_term.ml

@@ -10,6 +10,7 @@ module Ty = Base_types.Ty
 module Statement = Base_types.Statement
 module Data = Base_types.Data
 module Select = Base_types.Select
+module Proof = Proof
 
 module Arg
   : Sidekick_core.TERM

src/cc/Sidekick_cc.ml

@@ -661,7 +661,7 @@ module Make (A: CC_ARG)
         let proof =
           let lits =
             Iter.of_list lits
-            |> Iter.map (fun lit -> Lit.term lit, Lit.sign lit)
+            |> Iter.map (fun lit -> P.lit_st (Lit.signed_term lit))
           in
           P.cc_lemma lits
         in
@@ -782,7 +782,8 @@ module Make (A: CC_ARG)
                let lits = explain_pair cc ~th acc u1 t1 in
                let p =
                  A.P.cc_lemma
-                   (Iter.of_list lits |> Iter.map (fun l -> Lit.term l, Lit.sign l))
+                   (Iter.of_list lits
+                    |> Iter.map (fun l -> A.P.(lit_st (Lit.signed_term l))))
                in
                lits, p
              ) in
@@ -854,7 +855,7 @@ module Make (A: CC_ARG)
     let proof =
       let lits =
         Iter.of_list lits
-        |> Iter.map (fun lit -> Lit.term lit, Lit.sign lit)
+        |> Iter.map (fun lit -> P.lit_st (Lit.signed_term lit))
       in
       P.cc_lemma lits
     in

src/core/Sidekick_core.ml

@@ -147,22 +147,53 @@ end
 
 module type PROOF = sig
   type term
-  type clause
+  type ty
   type t
   val pp : t Fmt.printer
 
-  (** hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation *)
+  type hres_step
-  type hres_step = | R | R1 | P | P1
+  (** hyper-resolution steps: resolution, unit resolution;
+      bool paramodulation, unit bool paramodulation *)
 
-  val hres_iter : t -> (hres_step * t) Iter.t -> t (* hyper-res *)
+  val r : t -> pivot:term -> hres_step
-  val hres_l : t -> (hres_step * t) list -> t (* hyper-res *)
+  (** Resolution step on given pivot term *)
+
+  val r1 : t -> hres_step
+  (** Unit resolution; pivot is obvious *)
+
+  val p : t -> lhs:term -> rhs:term -> hres_step
+  (** Paramodulation using proof whose conclusion has a literal [lhs=rhs] *)
+
+  val p1 : t -> hres_step
+  (** Unit paramodulation *)
+
+  type lit
+  (** Proof representation of literals *)
+
+  val pp_lit : lit Fmt.printer
+  val a : term -> lit
+  val na : term -> lit
+  val lit_st : term * bool -> lit
+  val eq : term -> term -> lit
+  val neq : term -> term -> lit
+  val not : lit -> lit
+
+  val assertion : term -> t
+  val assertion_c : lit Iter.t -> t
+  val assertion_c_l : lit list -> t
+  val hres_iter : t -> hres_step Iter.t -> t (* hyper-res *)
+  val hres_l : t -> hres_step list -> t (* hyper-res *)
   val refl : term -> t (* proof of [| t=t] *)
   val true_is_true : t (* proof of [|- true] *)
   val true_neq_false : t (* proof of [|- not (true=false)] *)
-  val cc_lemma : (term*bool) Iter.t -> t (* equality tautology, unsigned *)
+  val cc_lemma : lit Iter.t -> t (* equality tautology, unsigned *)
   val cc_imply2 : t -> t -> term -> term -> t (* tautology [p1, p2 |- t=u] *)
   val cc_imply_l : t list -> term -> term -> t (* tautology [hyps |- t=u] *)
   val sorry : t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
+  val sorry_c : lit Iter.t -> t
+  [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
+
+  val sorry_c_l : lit list -> t
 
   val default : t [@@alert cstor "do not use default constructor"]
 end
@@ -194,6 +225,8 @@ module type LIT = sig
   val abs : t -> t
   (** [abs lit] is like [lit] but always positive, i.e. [sign (abs lit) = true] *)
 
+  val signed_term : t -> T.Term.t * bool
+
   val equal : t -> t -> bool
   val hash : t -> int
   val pp : t Fmt.printer

src/lra/sidekick_arith_lra.ml

@@ -57,8 +57,9 @@ module type ARG = sig
   val has_ty_real : term -> bool
   (** Does this term have the type [Real] *)
 
-  (** TODO: actual proof *)
+  (** TODO: more accurate certificates *)
-  val proof_lra : S.lemma
+  val proof_lra : S.P.lit Iter.t -> S.lemma
+  val proof_lra_l : S.P.lit list -> S.lemma
 
   module Gensym : sig
     type t
@@ -268,9 +269,10 @@ module Make(A : ARG) : S with module A = A = struct
         let lit_t = mk_lit t in
         let lit_u1 = mk_lit u1 in
         let lit_u2 = mk_lit u2 in
-        add_clause [SI.Lit.neg lit_t; lit_u1] A.proof_lra;
+        add_clause [SI.Lit.neg lit_t; lit_u1] A.S.P.(A.proof_lra_l [na t; a u1]) ;
-        add_clause [SI.Lit.neg lit_t; lit_u2] A.proof_lra;
+        add_clause [SI.Lit.neg lit_t; lit_u2] A.S.P.(A.proof_lra_l [na t; a u2]);
-        add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t] A.proof_lra;
+        add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t]
+          A.S.P.(A.proof_lra_l [a t;na u1;na u2]);
       );
       None
 
@@ -332,7 +334,7 @@ module Make(A : ARG) : S with module A = A = struct
           end;
 
           Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
-          let proof = A.proof_lra in
+          let proof = A.S.P.sorry in (* TODO: some sort of equality + def? *)
           Some (new_t, proof)
       end
 
@@ -393,7 +395,7 @@ module Make(A : ARG) : S with module A = A = struct
       let le = as_linexp_id t in
       if LE.is_const le then (
         let c = LE.const le in
-        Some (A.mk_lra self.tst (LRA_const c), A.proof_lra)
+        Some (A.mk_lra self.tst (LRA_const c), A.S.P.sorry)
       ) else None
     | LRA_pred (pred, l1, l2) ->
       let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
@@ -407,12 +409,14 @@ module Make(A : ARG) : S with module A = A = struct
           | Eq -> Q.(c = zero)
           | Neq -> Q.(c <> zero)
         in
-        Some (A.mk_bool self.tst is_true, A.proof_lra)
+        Some (A.mk_bool self.tst is_true, A.S.P.sorry)
       ) else None
     | _ -> None
 
   module Q_map = CCMap.Make(Q)
 
+  let plit_of_lit lit = A.S.P.lit_st (Lit.signed_term lit)
+
   (* raise conflict from certificate *)
   let fail_with_cert si acts cert : 'a =
     Profile.with1 "simplex.check-cert" SimpSolver._check_cert cert;
@@ -422,14 +426,19 @@ module Make(A : ARG) : S with module A = A = struct
       |>  List.rev_map SI.Lit.neg
     in
     (* TODO: more detailed proof certificate *)
-    SI.raise_conflict si acts confl A.proof_lra
+    let pr =
+      A.(S.P.(proof_lra (Iter.of_list confl |> Iter.map plit_of_lit))) in
+    SI.raise_conflict si acts confl pr
 
   let on_propagate_ si acts lit ~reason =
     match lit with
     | Tag.Lit lit ->
       (* TODO: more detailed proof certificate *)
       SI.propagate si acts lit
-        (fun() -> CCList.flat_map (Tag.to_lits si) reason, A.proof_lra)
+        (fun() ->
+           let lits = CCList.flat_map (Tag.to_lits si) reason in
+           let proof = A.proof_lra Iter.(cons lit (of_list lits) |> map plit_of_lit) in
+           CCList.flat_map (Tag.to_lits si) reason, proof)
     | _ -> ()
 
   let check_simplex_ self si acts : SimpSolver.Subst.t =

src/msat-solver/Sidekick_msat_solver.ml

@@ -49,6 +49,7 @@ module Make(A : ARG)
     let[@inline] sign t = t.lit_sign
     let[@inline] abs t = {t with lit_sign=true}
     let[@inline] term (t:t): term = t.lit_term
+    let[@inline] signed_term t = term t, sign t
 
     let make ~sign t = {lit_sign=sign; lit_term=t}
 
@@ -512,6 +513,19 @@ module Make(A : ARG)
         Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver)) in
       Dot.pp
 
+    (* TODO: instead export to regular proof, which must get:
+       - [defc name cl proof] to bind [name] to given clause and proof
+       - [deft name t] to define [name] as a shortcut for [t] (tseitin, etc.).
+         Checker will always expand these.
+       - [steps <defc>+] for a structure proof with definitions, returning last one
+       - [subproof (assms <lit>* ) (proof)] which uses [proof] to get
+         clause [c] under given assumptions (each assm is a lit),
+         and return [-a1 \/ … \/ -an \/ c], discharging assumptions
+
+       proof must provide a mutable builder for "steps" which is passed along
+       in main solver context so that theories can use it for their global
+       definitions. This is also what resolution should use to translate the proof.
+    *)
     let pp out (self:t) : unit =
       let n_step = ref 0 in
       let n_tbl_ = SC.Tbl.create 32 in (* node.concl -> unique idx *)
@@ -560,18 +574,18 @@ module Make(A : ARG)
                   Fmt.fprintf out "(@[r c%d@ :pivot %a@])" n_p' pp_atom pivot
                 )
               in
-              Fmt.fprintf out "(@[hres@ %d@ (@[%a@])@])"
+              Fmt.fprintf out "(@[hres@ c%d@ (@[%a@])@])"
                 n_init Fmt.(list ~sep:(return "@ ") pp_step) steps
           in
 
-          Fmt.fprintf out "(@[defc c%d@ (@[cl %a@])@ (@[<1>src@ %a@])@])@ "
+          Fmt.fprintf out "@ (@[defc c%d@ (@[cl %a@])@ (@[<1>src@ %a@])@])"
             idx Fmt.(list ~sep:(return "@ ") pp_atom) atoms
             pp_step step;
         )
       in
-      Fmt.fprintf out "(@[<v>quip 1@ ";
+      Fmt.fprintf out "(@[<v>quip 1";
       Sat_solver.Proof.fold pp_node () self;
-      Fmt.fprintf out "@])@.";
+      Fmt.fprintf out "@])";
       ()
   end
 

src/smtlib/Process.ml

@@ -273,13 +273,14 @@ let process_stmt
       CCOpt.iter (fun h -> Vec.push h [atom]) hyps;
       Solver.add_clause solver (IArray.singleton atom) (Proof.assertion t);
       E.return()
-    | Statement.Stmt_assert_clause c ->
+    | Statement.Stmt_assert_clause c_ts ->
       if pp_cnf then (
-        Format.printf "(@[<hv1>assert-clause@ %a@])@." (Util.pp_list Term.pp) c
+        Format.printf "(@[<hv1>assert-clause@ %a@])@." (Util.pp_list Term.pp) c_ts
       );
-      let c = List.map (Solver.mk_atom_t solver) c in
+      let c = List.map (Solver.mk_atom_t solver) c_ts in
       CCOpt.iter (fun h -> Vec.push h c) hyps;
-      Solver.add_clause solver (IArray.of_list c);
+      let proof = Proof.(assertion_c (Iter.of_list c_ts |> Iter.map (fun t->a t))) in
+      Solver.add_clause solver (IArray.of_list c) proof ;
       E.return()
     | Statement.Stmt_data _ ->
       E.return()
@@ -322,12 +323,19 @@ module Th_data = Sidekick_th_data.Make(struct
 
     let ty_is_finite = Ty.finite
     let ty_set_is_finite = Ty.set_finite
+
+    let proof_isa_disj = Proof.isa_disj
+    let proof_isa_split = Proof.isa_split
+    let proof_cstor_inj = Proof.cstor_inj
   end)
 
 module Th_bool = Sidekick_th_bool_static.Make(struct
   module S = Solver
   type term = S.T.Term.t
   include Form
+  let proof_bool = Proof.bool_eq
+  let proof_ite_true = Proof.ite_true
+  let proof_ite_false = Proof.ite_false
 end)
 
 module Th_lra = Sidekick_arith_lra.Make(struct
@@ -347,6 +355,9 @@ module Th_lra = Sidekick_arith_lra.Make(struct
   let ty_lra _st = Ty.real()
   let has_ty_real t = Ty.equal (T.ty t) (Ty.real())
 
+  let proof_lra = Proof.lra
+  let proof_lra_l = Proof.lra_l
+
   module Gensym = struct
     type t = {
       tst: T.state;

src/smtlib/Proof.ml

@@ -1,29 +0,0 @@
-
-module T = Sidekick_base_term.Term
-type term = T.t
-
-type t =
-  | Unspecified
-  | Sorry of term
-  | CC_lemma_imply of t list * term * term
-  | CC_lemma of (term * bool) list
-  | Assertion of term
-
-let default=Unspecified
-let sorry t = Sorry t
-let make_cc iter : t = CC_lemma (Iter.to_rev_list iter)
-let assertion t = Assertion t
-
-
-
-let rec pp out (self:t) : unit =
-  let pp_signed_t_ out (t,b) =
-    if b then T.pp out t else Fmt.fprintf out "(@[not@ %a@])" T.pp t
-  in
-  match self with
-  | Unspecified -> Fmt.string out "<unspecified>"
-  | CC_lemma_imply (l,t,u) ->
-    Fmt.fprintf out "(@[cc-lemma@ (@[%a@])@])"
-  | CC_lemma l ->
-    Fmt.fprintf out "(@[cc-lemma@ (@[%a@])@])"
-      Fmt.(list ~sep:(return "@ ") pp_lit) l

src/smtlib/Proof.mli

@@ -1 +0,0 @@
-include Sidekick_core.PROOF with type term = Sidekick_base_term.Term.t

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -142,10 +142,10 @@ module Make(A : ARG) : S with module A = A = struct
       let a, pr_a = SI.Simplify.normalize_t simp a in
       begin match A.view_as_bool a with
         | B_bool true ->
-          let pr = SI.P.(hres_l (A.proof_ite_true t) [R1, pr_a]) in
+          let pr = SI.P.(hres_l (A.proof_ite_true t) [r1 pr_a]) in
           Some (b, pr)
         | B_bool false ->
-          let pr = SI.P.(hres_l (A.proof_ite_false t) [R1, pr_a]) in
+          let pr = SI.P.(hres_l (A.proof_ite_false t) [r1 pr_a]) in
           Some (c, pr)
         | _ ->
           None
@@ -184,11 +184,11 @@ module Make(A : ARG) : S with module A = A = struct
       begin match A.view_as_bool a with
         | B_bool true ->
           (* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *)
-          let proof = SI.P.(hres_l (A.proof_ite_true t) [P1, pr_a]) in
+          let proof = SI.P.(hres_l (A.proof_ite_true t) [p1 pr_a]) in
           Some (b, proof)
         | B_bool false ->
           (* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *)
-          let proof = SI.P.(hres_l (A.proof_ite_false t) [P1, pr_a]) in
+          let proof = SI.P.(hres_l (A.proof_ite_false t) [p1 pr_a]) in
           Some (c, proof)
         | _ ->
           let t_ite = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in

src/th-data/Sidekick_th_data.ml

@@ -24,7 +24,6 @@ let name = "th-data"
 module type DATA_TY = sig
   type t
   type cstor
-  type proof
 
   val equal : t -> t -> bool
 
@@ -75,9 +74,9 @@ module type ARG = sig
   val ty_is_finite : S.T.Ty.t -> bool
   val ty_set_is_finite : S.T.Ty.t -> bool -> unit
 
-  val proof_isa_split : S.T.Term.t Iter.t -> S.P.t
+  val proof_isa_split : S.T.Ty.t -> S.T.Term.t Iter.t -> S.P.t
-  val proof_isa_disj : S.T.Term.t -> S.T.Term.t -> S.P.t
+  val proof_isa_disj : S.T.Ty.t -> S.T.Term.t -> S.T.Term.t -> S.P.t
-  val proof_cstor_inj : Cstor.t -> S.T.Term.t list -> S.T.Term.t list -> S.P.t
+  val proof_cstor_inj : Cstor.t -> int -> S.T.Term.t list -> S.T.Term.t list -> S.P.t
 end
 
 (** Helper to compute the cardinality of types *)
@@ -247,6 +246,7 @@ module Make(A : ARG) : S with module A = A = struct
       in
       if A.Cstor.equal c1.c_cstor c2.c_cstor then (
         (* same function: injectivity *)
+        (* FIXME proof *)
         assert (IArray.length c1.c_args = IArray.length c2.c_args);
         IArray.iter2
           (fun u1 u2 -> SI.CC.merge cc u1 u2 expl)
@@ -254,6 +254,7 @@ module Make(A : ARG) : S with module A = A = struct
         Ok c1
       ) else (
         (* different function: disjointness *)
+        (* FIXME proof *)
         Error expl
       )
   end
@@ -571,10 +572,10 @@ module Make(A : ARG) : S with module A = A = struct
         |> Iter.to_rev_list
       in
       SI.add_clause_permanent solver acts c
-        (A.proof_isa_split @@ (Iter.of_list c|>Iter.map SI.Lit.term));
+        (A.proof_isa_split (T.ty t) @@ (Iter.of_list c|>Iter.map SI.Lit.term));
       Iter.diagonal_l c
         (fun (c1,c2) ->
-           let proof = A.proof_isa_disj (SI.Lit.term c1) (SI.Lit.term c2) in
+           let proof = A.proof_isa_disj (T.ty t) (SI.Lit.term c1) (SI.Lit.term c2) in
            SI.add_clause_permanent solver acts
              [SI.Lit.neg c1; SI.Lit.neg c2] proof);
     )

src/th-data/Sidekick_th_data.mli

@@ -73,6 +73,10 @@ module type ARG = sig
   (** Modify the "finite" field (see {!ty_is_finite}) *)
 
   (* TODO: should we store this ourself? would be simpler… *)
+
+  val proof_isa_split : S.T.Ty.t -> S.T.Term.t Iter.t -> S.P.t
+  val proof_isa_disj : S.T.Ty.t -> S.T.Term.t -> S.T.Term.t -> S.P.t
+  val proof_cstor_inj : Cstor.t -> int -> S.T.Term.t list -> S.T.Term.t list -> S.P.t
 end
 
 module type S = sig