From b6df2cd974d0b85a848a6baa994a7298fd1d8da5 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 3 Jan 2022 22:59:31 -0500
Subject: [PATCH] clause-less steps in proofs

these steps are checked only once, to accelerate checking, but the
result isn't known.
---
 src/base/Proof_quip.ml    |  9 ++++++---
 src/quip/Proof.ml         | 13 +++++++++++++
 src/quip/Sidekick_quip.ml |  2 ++
 3 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml
index 2a05bc6e..bb542800 100644
--- a/src/base/Proof_quip.ml
+++ b/src/base/Proof_quip.ml
@@ -84,6 +84,7 @@ end = struct
   let conv_clause (c:PS.Clause.t) : P.clause lazy_t = conv_lits c.lits
 
   let name_clause (id: PS.ID.t) : string = Printf.sprintf "c%ld" id
+  let name_step (id: PS.ID.t) : string = Printf.sprintf "s%ld" id
   let name_term (id: PS.ID.t) : string = Printf.sprintf "t%ld" id
 
   (* TODO: see if we can allow `(stepc c5 (cl …) (… (@ c5) …))`.
@@ -272,12 +273,14 @@ end = struct
           L_proofs.add lid p;
 
         | PS.Step_view.Step_bool_c { rule; exprs } ->
+          let name = name_step lid in
           Array.iter add_needed_step exprs;
-          let p = lazy (
+          let step = lazy (
             let exprs = Util.array_to_list_map L_terms.find exprs in
-            P.bool_c rule exprs
+            P.step_anon ~name @@ P.bool_c rule exprs
           ) in
-          L_proofs.add lid p;
+          add_top_step step;
+          L_proofs.add lid (lazy (P.ref_by_name name));
 
         | PS.Step_view.Step_preprocess { t; u; using } ->
           let name = name_clause lid in
diff --git a/src/quip/Proof.ml b/src/quip/Proof.ml
index 0a1b2322..3211adb6 100644
--- a/src/quip/Proof.ml
+++ b/src/quip/Proof.ml
@@ -141,6 +141,18 @@ and composite_step =
       res: clause; (* result of [proof] *)
       proof: t; (* sub-proof *)
     }
+  (** A named step in {!Composite}, with the expected result.
+      This decouples the checking of the sub-proof, from its use in the rest
+      of the proof, as we can use [res] even if checking [proof] failed. *)
+
+  | S_step_anon of {
+      name: string; (* name of step *)
+      proof: t; (* proof *)
+    }
+    (** A named intermediate proof, to be reused in subsequent proofs.
+        Unlike {!S_step_c} we do not specify the expected result
+        so if this fails, any proof downstream will also fail. *)
+
   | S_define_t of term * term (* [const := t] *)
   | S_define_t_name of string * term (* [const := t] *)
 
@@ -156,6 +168,7 @@ let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs }
 let p1 p = P1 p
 
 let stepc ~name res proof : composite_step = S_step_c {proof;name;res}
+let step_anon ~name proof : composite_step = S_step_anon {name;proof}
 let deft c rhs : composite_step = S_define_t (c,rhs)
 let deft_name c rhs : composite_step = S_define_t_name (c,rhs)
 
diff --git a/src/quip/Sidekick_quip.ml b/src/quip/Sidekick_quip.ml
index f996ecb5..70d8bd10 100644
--- a/src/quip/Sidekick_quip.ml
+++ b/src/quip/Sidekick_quip.ml
@@ -113,6 +113,8 @@ module Make_printer(Out : OUT) = struct
     match proof_rule with
     | S_step_c {name;res;proof} ->
       l[a"stepc";a name;pp_cl res;pp_rec proof]
+    | S_step_anon {name;proof} ->
+      l[a"step";a name;pp_rec proof]
     | S_define_t (c,rhs) ->
       (* disable sharing for [rhs], otherwise it'd print [c] *)
       l[a"deft";pp_t c; pp_t rhs]