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

@@ -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

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)
 

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]