proof: eliminate P_let/P_local; emit subproofs eagerly via tracer

CC.proof_of_th_lemmas now takes a Proof.Tracer.t and emits each
binding immediately (Tracer.add_step), receiving the byte offset as
a Step.id, and uses P_ref to reference it.  No more local_gen/P_let.

- Pterm: remove P_local, P_let, local_ref, let_, local_ref constructor
- CC/Expl_state: remove local_gen field and new_local_id; thread
  tracer through to_resolved_expl and lits_and_proof_of_expl
- proof_encoder: drop P_let/P_local match arms (now exhaustive)
- twp_pterm: drop P_local/P_let handling and emit_pterm_with_locals

src/cc/CC.ml

@@ -289,36 +289,29 @@ module Expl_state = struct
     mutable lits: Lit.t list;
     mutable th_lemmas:
       (Lit.t * (Lit.t * Lit.t list) list * Proof.Pterm.delayed) list;
-    mutable local_gen: int;
+
   }
 
-  let create () : t = { lits = []; th_lemmas = []; local_gen = -2 }
+  let create () : t = { lits = []; th_lemmas = [] }
   let[@inline] copy self : t = { self with lits = self.lits }
   let[@inline] add_lit (self : t) lit = self.lits <- lit :: self.lits
 
-  let[@inline] new_local_id (self : t) : Proof.Pterm.local_ref =
-    let n = self.local_gen in
-    self.local_gen <- n - 1;
-    n
-
   let[@inline] add_th (self : t) lit hyps pr : unit =
     self.th_lemmas <- (lit, hyps, pr) :: self.th_lemmas
 
   let merge self other =
-    let { lits = o_lits; th_lemmas = o_lemmas; local_gen = o_l } = other in
+    let { lits = o_lits; th_lemmas = o_lemmas } = other in
     self.lits <- List.rev_append o_lits self.lits;
     self.th_lemmas <- List.rev_append o_lemmas self.th_lemmas;
-    self.local_gen <- min self.local_gen o_l;
+
     ()
 
   (* proof of [\/_i ¬lits[i]] *)
-  let proof_of_th_lemmas (self : t) : Proof.Pterm.delayed =
+  let proof_of_th_lemmas (self : t) (tracer : Proof.Tracer.t) : Proof.Pterm.delayed =
     Proof.Pterm.delay @@ fun () ->
-    let bs = ref [] in
-    let bind (t : Proof.Pterm.t) : Proof.Pterm.local_ref =
-      let n = new_local_id self in
-      bs := (n, t) :: !bs;
-      n
+    (* Emit each sub-proof immediately; use its offset (Step.id) as a P_ref. *)
+    let bind (t : Proof.Pterm.t) : Proof.Step.id =
+      Proof.Tracer.add_step tracer (Proof.Pterm.delay (fun () -> t))
     in
 
     let p_lits1 = List.rev_map Lit.neg self.lits in
@@ -328,18 +321,13 @@ module Expl_state = struct
     let p_cc = Proof.Core_rules.lemma_cc (List.rev_append p_lits1 p_lits2) in
     let resolve_with_th_proof pr (lit_t_u, sub_proofs, pr_th) =
       let pr_th = pr_th () in
-      (* pr_th: [sub_proofs |- t=u].
-          now resolve away [sub_proofs] to get literals that were
-          asserted in the congruence closure *)
       let pr_th =
         List.fold_left
           (fun pr_th (lit_i, hyps_i) ->
-            (* [hyps_i |- lit_i] *)
             let lemma_i =
               bind
               @@ Proof.Core_rules.lemma_cc (lit_i :: List.rev_map Lit.neg hyps_i)
             in
-            (* resolve [lit_i] away. *)
             Proof.Core_rules.proof_res ~pivot:(Lit.term lit_i) lemma_i
               (bind pr_th))
           pr_th sub_proofs
@@ -347,15 +335,12 @@ module Expl_state = struct
       Proof.Core_rules.proof_res ~pivot:(Lit.term lit_t_u) (bind pr_th)
         (bind pr)
     in
-    (* resolve with theory proofs responsible for some merges, if any. *)
     let body = List.fold_left resolve_with_th_proof p_cc self.th_lemmas in
-    Proof.Pterm.let_ (List.rev !bs) body
-
-  let to_resolved_expl (self : t) : Resolved_expl.t =
-    (* FIXME: package the th lemmas too *)
-    let { lits; th_lemmas = _; local_gen = _ } = self in
+    body
+  let to_resolved_expl (self : t) (tracer : Proof.Tracer.t) : Resolved_expl.t =
+    let { lits; th_lemmas = _ } = self in
     let s2 = copy self in
-    let pr proof = proof_of_th_lemmas s2 proof in
+    let pr proof = proof_of_th_lemmas s2 tracer proof in
     { Resolved_expl.lits; pr }
 end
 
@@ -523,8 +508,8 @@ let n_is_bool_value (self : t) n : bool =
    merges. *)
 let lits_and_proof_of_expl (_self : t) (st : Expl_state.t) :
     Lit.t list * Proof.Pterm.delayed =
-  let { Expl_state.lits; th_lemmas = _; local_gen = _ } = st in
-  let pr = Expl_state.proof_of_th_lemmas st in
+  let { Expl_state.lits; th_lemmas = _ } = st in
+  let pr = Expl_state.proof_of_th_lemmas st (proof_tracer _self) in
   lits, pr
 
 (* main CC algo: add terms from [pending] to the signature table,
@@ -840,12 +825,12 @@ let explain_eq self n1 n2 : Resolved_expl.t =
   let st = Expl_state.create () in
   explain_equal_rec_ self st n1 n2;
   (* FIXME: also need to return the proof? *)
-  Expl_state.to_resolved_expl st
+  Expl_state.to_resolved_expl st self.proof
 
 let explain_expl (self : t) expl : Resolved_expl.t =
   let expl_st = Expl_state.create () in
   explain_decompose_expl self expl_st expl;
-  Expl_state.to_resolved_expl expl_st
+  Expl_state.to_resolved_expl expl_st self.proof
 
 let[@inline] on_pre_merge self = Event.of_emitter self.on_pre_merge
 let[@inline] on_pre_merge2 self = Event.of_emitter self.on_pre_merge2

src/proof/pterm.ml

@@ -1,6 +1,5 @@
 type step_id = Step.id
 type lit = Lit.t
-type local_ref = Step.id
 
 type rule_apply = {
   rule_name: string;
@@ -13,15 +12,12 @@ type rule_apply = {
 
 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 rec pp out = function
+let pp out = function
   | P_ref r -> Fmt.fprintf out "!%d" r
-  | P_local id -> Fmt.fprintf out "s%d" id
   | P_apply r ->
     Fmt.fprintf out "%s{@[" r.rule_name;
     if r.premises <> [] then
@@ -35,22 +31,11 @@ let rec pp out = function
         Fmt.Dump.(list @@ Lit.pp_limit ~max_nodes:200 ~max_depth:5)
         r.lit_args;
     Fmt.fprintf out "@]}"
-  | P_let (bs, bod) ->
-    let pp_b out (x, t) = Fmt.fprintf out "s%d := %a" x pp t in
-    Fmt.fprintf out "(@[let %a@ in %a@])"
-      (Util.pp_list ~sep:"; " pp_b)
-      bs pp bod
 
-let local_ref id = P_local id
 let ref id = P_ref id
 let[@inline] delay f = f
 let dummy = ref Step.dummy
 
-let let_ bs r =
-  match bs with
-  | [] -> r
-  | _ -> P_let (bs, r)
-
 let apply_rule ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
     ?(indices = []) rule_name : t =
   P_apply
@@ -80,7 +65,6 @@ let ser_apply_rule (tracer : Term.Tracer.t) (r : rule_apply) : Ser_value.t =
   let enc_indice (p : step_id) = V.int p in
   let enc_subst (_s : Subst.t) : V.t = assert false (* TODO *) in
 
-  (* add a field [x, v] if [v] is not the empty list *)
   let add_ x v enc_v l =
     match v with
     | [] -> l
@@ -100,16 +84,11 @@ let ser_apply_rule (tracer : Term.Tracer.t) (r : rule_apply) : Ser_value.t =
 
   V.dict_of_list l
 
-let rec to_ser (tracer : Term.Tracer.t) t : Ser_value.t =
-  let recurse = to_ser tracer in
+let to_ser (tracer : Term.Tracer.t) t : Ser_value.t =
   V.(
     match t with
     | P_ref r -> list [ int 0; int r ]
-    | P_local id -> list [ int 1; int id ]
-    | P_apply r -> list [ int 2; ser_apply_rule tracer r ]
-    | P_let (bs, bod) ->
-      let ser_b (x, t) = list [ int x; recurse t ] in
-      list [ int 3; list (List.map ser_b bs); recurse bod ])
+    | P_apply r -> list [ int 2; ser_apply_rule tracer r ])
 
 let deser_apply_rule (t_read : Term.Trace_reader.t) : rule_apply Ser_decode.t =
   let open Dec.Infix in
@@ -139,22 +118,14 @@ let deser_apply_rule (t_read : Term.Trace_reader.t) : rule_apply Ser_decode.t =
 
   { rule_name; lit_args; subst_args; term_args; premises; indices }
 
-let rec deser (t_read : Term.Trace_reader.t) : t Ser_decode.t =
+let deser (t_read : Term.Trace_reader.t) : t Ser_decode.t =
   let open Dec.Infix in
   let* l = Dec.list Dec.any in
   match l with
   | [ V.Int 0; v ] ->
     let+ i = Dec.reflect_or_fail Dec.int v in
     P_ref i
-  | [ V.Int 1; v ] ->
-    let+ i = Dec.reflect_or_fail Dec.int v in
-    P_local i
   | [ V.Int 2; v ] ->
     let+ r = Dec.reflect_or_fail (deser_apply_rule t_read) v in
     P_apply r
-  | [ V.Int 3; bs; body ] ->
-    let dec_b = Dec.tup2 Dec.int (deser t_read) in
-    let+ bs = Dec.reflect_or_fail (Dec.list dec_b) bs
-    and+ body = Dec.reflect_or_fail (deser t_read) body in
-    P_let (bs, body)
   | _ -> Dec.failf "unknown proof-term %a" (Fmt.Dump.list V.pp) l

src/proof/pterm.mli

@@ -1,15 +1,8 @@
-(** Proof terms.
-
-  A proof term is the description of a reasoning step, that yields a clause. *)
+(** Proof terms. *)
 
 type step_id = Step.id
 type lit = Lit.t
 
-type local_ref = Step.id
-(** A local reference is a step id that is only valid in the scope
-    of a {!P_let}. Typically one can use negative integers to avoid
-    accidental shadowing. *)
-
 type rule_apply = {
   rule_name: string;
   lit_args: lit list;
@@ -21,8 +14,6 @@ type rule_apply = {
 
 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
@@ -30,8 +21,6 @@ type delayed = unit -> t
 include Sidekick_sigs.PRINT with type t := t
 
 val ref : step_id -> t
-val local_ref : local_ref -> t
-val let_ : (local_ref * t) list -> t -> t
 val delay : (unit -> t) -> delayed
 
 val dummy : t
@@ -47,6 +36,4 @@ val apply_rule :
   t
 
 val to_ser : Term.Tracer.t -> t -> Ser_value.t
-(** Serialize *)
-
 val deser : Term.Trace_reader.t -> t Ser_decode.t

src/proof_minidag/proof_encoder.ml

@@ -161,29 +161,11 @@ let rec encode_rule self (r : Pterm.rule_apply) : E.offset =
         List.iter (E.ref e) prem_offs;
         List.iter (E.ref e) term_offs)
 
-and encode_pterm ?(local_tbl : (int, E.offset) Hashtbl.t option)
-    self (pt : Pterm.t) : E.offset =
+and encode_pterm self (pt : Pterm.t) : E.offset =
   match pt with
   | Pterm.P_ref sid -> step_off self sid
-  | Pterm.P_local id ->
-    (match local_tbl with
-     | Some t ->
-       (match Hashtbl.find_opt t id with
-        | Some off -> off
-        | None -> emit_sorry self (Printf.sprintf "P_local s%d (unresolved)" id))
-     | None -> emit_sorry self (Printf.sprintf "P_local s%d (no context)" id))
   | Pterm.P_apply r -> encode_rule self r
-  | Pterm.P_let (bindings, body) ->
-    (* Evaluate each binding and store in a fresh local table. *)
-    let tbl =
-      match local_tbl with
-      | Some t -> t
-      | None -> Hashtbl.create 4
-    in
-    List.iter (fun (id, pt') ->
-        Hashtbl.replace tbl id (encode_pterm ~local_tbl:tbl self pt'))
-      bindings;
-    encode_pterm ~local_tbl:tbl self body
+
 
 (** Emit a proof step and return its minidag offset (= the new step id). *)
 let emit_step self (_sid : Step.id) (pt : Pterm.delayed) : E.offset =

src/proof_twp/twp_pterm.ml

@@ -124,7 +124,7 @@ let emit_pterm_rule (st : Twp_state.t) (r : Proof.Pterm.rule_apply) : int =
 
 (** Translate a Pterm.t and emit .twp lines.
     Returns the P-index of the outermost proof step. *)
-let rec emit_pterm (st : Twp_state.t) (pt : Proof.Pterm.t) : int =
+let emit_pterm (st : Twp_state.t) (pt : Proof.Pterm.t) : int =
   match pt with
   | Proof.Pterm.P_apply r ->
     emit_pterm_rule st r
@@ -140,35 +140,4 @@ let rec emit_pterm (st : Twp_state.t) (pt : Proof.Pterm.t) : int =
       emit_line st (Printf.sprintf "P%d assume E%d" n Twp_state.e_false);
       n)
 
-  | Proof.Pterm.P_local local_ref ->
-    (* Local ref within a P_let binding; resolved by emit_pterm_with_locals *)
-    let n = alloc_p st in
-    emit_line st (Printf.sprintf "# P_local s%d (unresolved) -> P%d" local_ref n);
-    emit_line st (Printf.sprintf "P%d assume E%d" n Twp_state.e_false);
-    n
 
-  | Proof.Pterm.P_let (bindings, body) ->
-    (* Process bindings, then process body with the local map *)
-    let local_map : (int, int) Hashtbl.t = Hashtbl.create 4 in
-    List.iter (fun (local_id, pt_inner) ->
-      let p_inner = emit_pterm st pt_inner in
-      Hashtbl.add local_map local_id p_inner
-    ) bindings;
-    emit_pterm_with_locals st body local_map
-
-and emit_pterm_with_locals (st : Twp_state.t) (pt : Proof.Pterm.t)
-    (locals : (int, int) Hashtbl.t) : int =
-  match pt with
-  | Proof.Pterm.P_local local_ref ->
-    (match Hashtbl.find_opt locals local_ref with
-    | Some n -> n
-    | None ->
-      let n = alloc_p st in
-      emit_line st (Printf.sprintf "# unresolved P_local s%d -> P%d" local_ref n);
-      emit_line st (Printf.sprintf "P%d assume E%d" n Twp_state.e_false);
-      n)
-  | Proof.Pterm.P_apply r ->
-    (* For rule_apply within let, we need to resolve premise refs via locals *)
-    (* For simplicity, just call the regular handler *)
-    emit_pterm_rule st r
-  | other -> emit_pterm st other