From 19e6f80b4558271b5d4c21328e04ec2207a26ec8 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 27 Apr 2021 23:14:02 -0400
Subject: [PATCH] refactor(proof): rename `defc` to `stepc`

---
 src/base-term/Proof.ml                  | 15 ++++++++-------
 src/core/Sidekick_core.ml               |  2 +-
 src/msat-solver/Sidekick_msat_solver.ml |  4 ++--
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/base-term/Proof.ml b/src/base-term/Proof.ml
index bb2228ee..84f38a42 100644
--- a/src/base-term/Proof.ml
+++ b/src/base-term/Proof.ml
@@ -17,11 +17,12 @@ let lit_not = function
   | 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 pp_lit_with ~pp_t out = function
+  | L_eq (t,u) -> Fmt.fprintf out "(@[+@ (@[=@ %a@ %a@])@])" pp_t t pp_t u
+  | L_neq (t,u) -> Fmt.fprintf out "(@[-@ (@[=@ %a@ %a@])@])" pp_t t pp_t u
+  | L_a t -> Fmt.fprintf out "(@[+@ %a@])" pp_t t
+  | L_na t -> Fmt.fprintf out "(@[-@ %a@])" pp_t t
+let pp_lit = pp_lit_with ~pp_t:Term.pp
 
 let lit_a t = L_a t
 let lit_na t = L_na t
@@ -60,7 +61,7 @@ type t =
     }
 
 and composite_step =
-  | S_define_c of {
+  | S_step_c of {
       name: string; (* name *)
       res: clause; (* result of [proof] *)
       proof: t; (* sub-proof *)
@@ -81,7 +82,7 @@ let r1 p = R1 p
 let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs }
 let p1 p = P1 p
 
-let defc ~name res proof : composite_step = S_define_c {proof;name;res}
+let stepc ~name res proof : composite_step = S_step_c {proof;name;res}
 let deft c rhs : composite_step = S_define_t (c,rhs)
 
 let is_trivial_refl = function
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 485190b9..f5063462 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -178,7 +178,7 @@ module type PROOF = sig
   val lit_not : lit -> lit
 
   type composite_step
-  val defc : name:string -> lit list -> t -> composite_step
+  val stepc : name:string -> lit list -> t -> composite_step
   val deft : term -> term -> composite_step (** define a (new) atomic term *)
 
   val is_trivial_refl : t -> bool
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index e2cdb2d0..4df166dd 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -535,7 +535,7 @@ module Make(A : ARG)
       Some pp
 
     (* export to proof {!P.t}, translating Msat-level proof ising:
-       - [defc name cl proof] to bind [name] to given clause and proof
+       - [stepc 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. (TODO)
        - [steps <defc>+] for a structure proof with definitions, returning last one
@@ -622,7 +622,7 @@ module Make(A : ARG)
                 (Iter.of_list steps |> Iter.map tr_step)
           in
 
-          let step = P.defc ~name concl pr_step in
+          let step = P.stepc ~name concl pr_step in
           add_step step;
         )
       in