wip: reconstruct quip proof from binary proof-trace

src/base/Proof.ml

@@ -128,7 +128,6 @@ let emit_fun_ (self:t) (f:Fun.t) : term_id =
     let id = alloc_id self in
     Fun.Tbl.add self.map_fun f id;
     let f_name = ID.to_string (Fun.id f) in
-    Format.printf "encode fun with name %S@." f_name;
     emit_step_ self
       Proof_ser.({ Step.id; view=Fun_decl {Fun_decl.f=f_name}});
     id
@@ -222,18 +221,19 @@ let lemma_rw_clause c ~using (self:t) =
   let using = Iter.to_array using in
   PS.(Step_view.Step_clause_rw {Step_clause_rw.c; using})
 
+(* TODO *)
 let with_defs _ _ (_pr:t) = dummy_step
 
+(* not useful *)
 let del_clause _ _ (_pr:t) = ()
 
-let emit_unsat_core _ (_pr:t) = dummy_step (* TODO *)
+(* TODO *)
+let emit_unsat_core _ (_pr:t) = dummy_step
 
 let emit_unsat c (self:t) : unit =
   emit_no_return_ self @@ fun() ->
   PS.(Step_view.Step_unsat {Step_unsat.c})
 
-let lemma_lra _ _ = dummy_step
-
 let lemma_bool_tauto lits (self:t) =
   emit_ self @@ fun() ->
   let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
@@ -244,6 +244,10 @@ let lemma_bool_c rule (ts:Term.t list) (self:t) =
   let exprs = ts |> Util.array_of_list_map (emit_term_ self) in
   PS.(Step_view.Step_bool_c {Step_bool_c.exprs; rule})
 
+(* TODO *)
+
+let lemma_lra _ _ = dummy_step
+
 let lemma_bool_equiv _ _ _ = dummy_step
 
 let lemma_ite_true ~ite:_ _ = dummy_step
@@ -257,3 +261,7 @@ let lemma_isa_disj _ _ (_pr:t) = dummy_step
 let lemma_cstor_inj _ _ _ (_pr:t) = dummy_step
 let lemma_cstor_distinct _ _ (_pr:t) = dummy_step
 let lemma_acyclicity _ (_pr:t) = dummy_step
+
+module Unsafe_ = struct
+  let[@inline] id_of_proof_step_ (p:proof_step) : proof_step = p
+end

src/base/Proof.mli

@@ -78,3 +78,7 @@ val iter_steps_backward : t -> Proof_ser.Step.t Iter.t
     This will yield nothing if the proof was disabled or used
     a dummy backend. *)
 
+
+module Unsafe_ : sig
+  val id_of_proof_step_ : proof_step -> Proof_ser.ID.t
+end

src/base/Proof_quip.ml

@@ -1,538 +1,141 @@
 
-open Base_types
+(* output proof *)
+module P = Sidekick_quip.Proof
 
-module T = Term
+(* serialized proof trace *)
-module Ty = Ty
+module PS = Sidekick_base_proof_trace.Proof_ser
-type term = T.t
-type ty = Ty.t
 
-type lit =
+type t = P.t
-  | L_eq of bool * term * term
-  | L_a of bool * term
 
-let lit_not = function
+module type CONV_ARG = sig
-  | L_eq (sign,a,b) -> L_eq(not sign,a,b)
+  val proof : Proof.t
-  | L_a (sign,t) -> L_a (not sign,t)
+  val unsat : Proof.proof_step
+end
 
-let pp_lit_with ~pp_t out =
+module Make_lazy_tbl(T:sig type t end)() = struct
-  let strsign = function true -> "+" | false -> "-" in
+  let lazy_tbl_ : T.t lazy_t Util.Int_tbl.t = Util.Int_tbl.create 32
-  function
-  | L_eq (b,t,u) -> Fmt.fprintf out "(@[%s@ (@[=@ %a@ %a@])@])" (strsign b) pp_t t pp_t u
-  | L_a (b,t) -> Fmt.fprintf out "(@[%s@ %a@])" (strsign b) pp_t t
-let pp_lit = pp_lit_with ~pp_t:Term.pp
 
-let lit_a t = L_a (true,t)
+  (** FInd step by its ID *)
-let lit_na t = L_a (false,t)
+  let find (id:PS.ID.t) : T.t =
-let lit_eq t u = L_eq (true,t,u)
+    match Util.Int_tbl.get lazy_tbl_ (Int32.to_int id) with
-let lit_neq t u = L_eq (false,t,u)
+    | Some (lazy p) -> p
-let lit_mk b t = L_a (b,t)
+    | None ->
-let lit_sign = function L_a (b,_) | L_eq (b,_,_) -> b
+      Error.errorf "proof-quip: step `%a` was not reconstructed" PS.ID.pp id
 
-type clause = lit list
+  (** Add entry *)
+  let add id (e:T.t lazy_t) =
+    assert (not (Util.Int_tbl.mem lazy_tbl_ (Int32.to_int id)));
+    Util.Int_tbl.add lazy_tbl_ (Int32.to_int id) e
+end
 
-type t =
+module Conv(X : CONV_ARG) : sig
-  | Unspecified
+  val reconstruct : unit -> t
-  | Sorry (* NOTE: v. bad as we don't even specify the return *)
+end = struct
-  | Sorry_c of clause
-  | Named of string (* refers to previously defined clause *)
-  | Refl of term
-  | CC_lemma_imply of t list * term * term
-  | CC_lemma of clause
-  | Assertion of term
-  | Assertion_c of clause
-  | Drup_res of clause
-  | Hres of t * hres_step list
-  | Res of term * t * t
-  | Res1 of t * t
-  | 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 *)
-  | Bool_c of bool_c_name * term list (* boolean tautology *)
-  | Nn of t (* negation normalization *)
-  | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *)
-  | Ite_false of term
-  | LRA of clause
-  | Composite of {
-      (* some named (atomic) assumptions *)
-      assumptions: (string * lit) list;
-      steps: composite_step array; (* last proof_rule is the proof *)
-    }
 
-and bool_c_name = string
+  (* Steps we need to decode.
+     Invariant: the IDs of these steps must be lower than the current processed
+     ID (we start from the end) *)
+  let needed_steps_ = Util.Int_tbl.create 128
 
-and composite_step =
+  let add_needed_step (id:PS.ID.t) : unit =
-  | S_step_c of {
+    Util.Int_tbl.replace needed_steps_ (Int32.to_int id) ()
-      name: string; (* name *)
-      res: clause; (* result of [proof] *)
-      proof: t; (* sub-proof *)
-    }
-  | S_define_t of term * term (* [const := t] *)
-  | S_define_t_name of string * term (* [const := t] *)
 
-  (* TODO: be able to name clauses, to be expanded at parsing.
+  let unsat_id = Proof.Unsafe_.id_of_proof_step_ X.unsat
-     note that this is not the same as [S_step_c] which defines an
-     explicit proof_rule with a conclusion and proofs that can be exploited
-     separately.
 
-     We could introduce that in Compress.rename…
+  (* start with the unsat step *)
+  let () = add_needed_step unsat_id
 
-  | S_define_c of string * clause (* [name := c] *)
+  (* store reconstructed proofs, but lazily because their dependencies
-   *)
+     (sub-steps, terms, etc.) might not have come up in the reverse stream yet. *)
+  module L_proofs = Make_lazy_tbl(struct type t = P.t end)()
 
-and hres_step =
+  (* store reconstructed terms *)
-  | R of { pivot: term; p: t}
+  module L_terms = Make_lazy_tbl(struct type t = P.term end)()
-  | R1 of t
-  | P of { lhs: term; rhs: term; p: t}
-  | P1 of t
 
-let r p ~pivot : hres_step = R { pivot; p }
+  (* list of toplevel steps, in the final proof order *)
-let r1 p = R1 p
+  let top_steps_ : P.composite_step lazy_t list ref = ref []
-let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs }
+  let add_top_step s = top_steps_ := s :: !top_steps_
-let p1 p = P1 p
 
-let stepc ~name res proof : composite_step = S_step_c {proof;name;res}
+  let conv_lit (lit:PS.Lit.t) : P.Lit.t lazy_t =
-let deft c rhs : composite_step = S_define_t (c,rhs)
+    let v = Int32.abs lit in
-let deft_name c rhs : composite_step = S_define_t_name (c,rhs)
+    add_needed_step v;
+    lazy (
+      let t = L_terms.find v in
+      let sign = lit > Int32.zero in
+      (* reconstruct literal *)
+      P.Lit.mk sign t
+    )
 
-let is_trivial_refl = function
+  let conv_clause (c:PS.Clause.t) : P.clause lazy_t =
-  | Refl _ -> true
+    let lits =
-  | _ -> false
+      c.lits
-
+      |> Util.array_to_list_map conv_lit
-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 ref_by_name name : t = Named name
-let cc_lemma c : t = CC_lemma c
-let cc_imply_l l t u : t =
-  let l = List.filter (fun p -> not (is_trivial_refl p)) l in
-  match l with
-  | [] -> refl t (* only possible way [t=u] *)
-  | l -> 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 composite_a ?(assms=[]) steps : t =
-  Composite {assumptions=assms; steps}
-let composite_l ?(assms=[]) steps : t =
-  Composite {assumptions=assms; steps=Array.of_list steps}
-let composite_iter ?(assms=[]) steps : t =
-  let steps = Iter.to_array steps in
-  Composite {assumptions=assms; steps}
-
-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 bool_c name c : t = Bool_c (name, c)
-let nn c : t = Nn c
-
-let drup_res c : t = Drup_res c
-let hres_l p l : t =
-  let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in
-  if l=[] then p else Hres (p,l)
-let hres_iter c i : t = hres_l c (Iter.to_list i)
-let res ~pivot p1 p2 : t = Res (pivot,p1,p2)
-let res1 p1 p2 : t = Res1 (p1,p2)
-
-let lra_l c : t = LRA c
-let lra c = LRA (Iter.to_rev_list c)
-
-let iter_lit ~f_t = function
-  | L_eq (_,a,b) -> f_t a; f_t b
-  | L_a (_,t) -> f_t t
-
-let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit =
-  match p with
-  | Unspecified | Sorry -> ()
-  | Sorry_c c -> f_clause c
-  | Named _ -> ()
-  | Refl t -> f_t t
-  | CC_lemma_imply (ps, t, u) -> List.iter f_p ps; f_t t; f_t u
-  | CC_lemma c | Assertion_c c -> f_clause c
-  | Assertion t -> f_t t
-  | Drup_res c -> f_clause c
-  | Hres (i, l) ->
-    f_p i;
-    List.iter
-      (function
-        | R1 p -> f_p p
-        | P1 p -> f_p p
-        | R {pivot;p} -> f_p p; f_t pivot
-        | P {lhs;rhs;p} -> f_p p; f_t lhs; f_t rhs)
-      l
-  | Res (t,p1,p2) -> f_t t; f_p p1; f_p p2
-  | Res1 (p1,p2) -> f_p p1; f_p p2
-  | DT_isa_split (_, l) -> List.iter f_t l
-  | DT_isa_disj (_, t, u) -> f_t t; f_t u
-  | DT_cstor_inj (_, _c, ts, us) -> List.iter f_t ts; List.iter f_t us
-  | Bool_true_is_true | Bool_true_neq_false -> ()
-  | Bool_eq (t, u) -> f_t t; f_t u
-  | Bool_c (_, ts) -> List.iter f_t ts
-  | Nn p -> f_p p
-  | Ite_true t | Ite_false t -> f_t t
-  | LRA c -> f_clause c
-  | Composite { assumptions; steps } ->
-    List.iter (fun (_,lit) -> iter_lit ~f_t lit) assumptions;
-    Array.iter f_step steps;
-
-(** {2 Compress by making more sharing explicit} *)
-module Compress = struct
-  type 'a shared_status =
-    | First (* first occurrence of t *)
-    | Shared (* multiple occurrences observed *)
-    | Pre_named of 'a (* another proof_rule names it *)
-    | Named of 'a (* already named it *)
-
-  (* is [t] too small to be shared? *)
-  let rec is_small_ t =
-    match T.view t with
-    | T.Bool _ -> true
-    | T.App_fun (_, a) -> IArray.is_empty a (* only constants are small *)
-    | T.Not u -> is_small_ u
-    | T.Eq (_, _) | T.Ite (_, _, _) -> false
-    | T.LRA _ -> false
-
-  type name = N_s of string | N_t of T.t
-  type sharing_info = {
-    terms: name shared_status T.Tbl.t; (* sharing for non-small terms *)
-  }
-
-  let no_sharing : sharing_info =
-    { terms = T.Tbl.create 8 }
-
-  (* traverse [p] and apply [f_t] to subterms (except to [c] in [c := rhs]) *)
-  let rec traverse_proof_ ?on_step ~f_t (p:t) : unit =
-    let recurse = traverse_proof_ ?on_step ~f_t in
-    let f_step s =
-      CCOpt.iter (fun f->f s) on_step;
-      traverse_step_ ~f_t s
     in
-    iter_p p
+    lazy (List.map Lazy.force lits)
-      ~f_t
-      ~f_clause:(traverse_clause_ ~f_t)
-      ~f_step
-      ~f_p:recurse
-  and traverse_step_ ~f_t = function
-    | S_define_t_name (_, rhs)
-    | S_define_t (_, rhs) -> f_t rhs
-    | S_step_c {name=_; res; proof} ->
-      traverse_clause_ ~f_t res; traverse_proof_ ~f_t proof
-  and traverse_clause_ ~f_t c : unit =
-    List.iter (iter_lit ~f_t) c
 
-  (** [find_sharing p] returns a {!sharing_info} which contains sharing information.
+  (* process a step of the trace *)
-      This information can be used during printing to reduce the
+  let process_step_ (step: PS.Step.t) : unit =
-      number of duplicated sub-terms that are printed. *)
+    let lid = step.id in
-  let find_sharing p : sharing_info =
+    let id = Int32.to_int lid in
-    let self = {terms=T.Tbl.create 32} in
+    if Util.Int_tbl.mem needed_steps_ id then (
+      Log.debugf 1 (fun k->k"(@[proof-quip.process-needed-step@ %a@])" PS.Step.pp step);
+      Util.Int_tbl.remove needed_steps_ id;
 
-    let traverse_t t =
+      (* now process the step *)
-      T.iter_dag t
+      begin match step.view with
-        (fun u ->
+        | PS.Step_view.Step_input i ->
-           if not (is_small_ u) then (
+          let c = conv_clause i.PS.Step_input.c in
-             match T.Tbl.get self.terms u with
+          let name = Printf.sprintf "c%d" id in
-             | None -> T.Tbl.add self.terms u First
+          let step = lazy (
-             | Some First -> T.Tbl.replace self.terms u Shared
+            let lazy c = c in
-             | Some (Shared | Named _ | Pre_named _) -> ()
+            P.S_step_c {name; res=c; proof=P.assertion_c_l c}
-           ))
+          ) in
-    in
+          add_top_step step;
+          (* refer to the step by name now *)
+          L_proofs.add lid (lazy (P.ref_by_name name));
 
-    (* if a term is already name, remember that, do not rename it *)
+        | PS.Step_view.Step_unsat us -> () (* TODO *)
-    let on_step = function
+        | PS.Step_view.Step_rup rup -> () (* TODO *)
-      | S_define_t_name (n,rhs) ->
+        | PS.Step_view.Step_bridge_lit_expr _ -> assert false
-        T.Tbl.replace self.terms rhs (Pre_named (N_s n));
+        | PS.Step_view.Step_cc cc -> () (* TODO *)
-      | S_define_t (c,rhs) ->
+        | PS.Step_view.Step_preprocess _ -> () (* TODO *)
-        T.Tbl.replace self.terms rhs (Pre_named (N_t c));
+        | PS.Step_view.Step_clause_rw _ -> () (* TODO *)
-      | S_step_c _ -> ()
+        | PS.Step_view.Step_bool_tauto _ -> () (* TODO *)
-    in
+        | PS.Step_view.Step_bool_c _ -> () (* TODO *)
+        | PS.Step_view.Step_proof_p1 _ -> () (* TODO *)
+        | PS.Step_view.Step_true _ -> () (* TODO *)
+        | PS.Step_view.Fun_decl _ -> () (* TODO *)
+        | PS.Step_view.Expr_def _ -> () (* TODO *)
+        | PS.Step_view.Expr_bool _ -> () (* TODO *)
+        | PS.Step_view.Expr_if _ -> () (* TODO *)
+        | PS.Step_view.Expr_not _ -> () (* TODO *)
+        | PS.Step_view.Expr_eq _ -> () (* TODO *)
+        | PS.Step_view.Expr_app _ -> () (* TODO *)
 
-    traverse_proof_ p ~on_step ~f_t:traverse_t;
-    self
-
-  (** [renaming sharing p] returns a new proof [p'] with more definitions.
-      It also modifies [sharing] so that the newly defined objects are
-      mapped to {!Named}, which we can use during printing. *)
-  let rename sharing (p:t) : t =
-    let n = ref 0 in
-    let new_name () = incr n; Printf.sprintf "$t%d" !n in
-
-    match p with
-    | Composite {assumptions; steps} ->
-      (* now traverse again, renaming some things on the fly *)
-      let new_steps = Vec.create() in
-
-      (* definitions we can skip *)
-      let skip_name_s = Hashtbl.create 8 in
-      let skip_name_t = T.Tbl.create 8 in
-
-      (* traverse [t], and if there's a subterm that is shared but
-         not named yet, name it now.
-      *)
-      let traverse_t t : unit =
-        T.iter_dag_with ~order:T.Iter_dag.Post t
-          (fun u ->
-              match T.Tbl.get sharing.terms u with
-              | Some Shared ->
-                (* shared, but not named yet *)
-                let name = new_name() in
-                Vec.push new_steps (deft_name name u);
-                T.Tbl.replace sharing.terms u (Named (N_s name))
-              | Some (Pre_named name) ->
-                (* named later in the file, declare it earlier to preserve
-                   a well ordering on definitions since we need it right now *)
-                Vec.push new_steps
-                  (match name with
-                   | N_s n -> Hashtbl.add skip_name_s n (); deft_name n u
-                   | N_t t -> T.Tbl.add skip_name_t t (); deft t u);
-                T.Tbl.replace sharing.terms u (Named name)
-              | _ -> ())
-      in
-
-      (* introduce naming in [proof_rule], then push it into {!new_steps} *)
-      let process_step_ proof_rule =
-        traverse_step_ proof_rule ~f_t:traverse_t;
-        (* see if we print the proof_rule or skip it *)
-        begin match proof_rule with
-          | S_define_t (t,_) when T.Tbl.mem skip_name_t t -> ()
-          | S_define_t_name (s,_) when Hashtbl.mem skip_name_s s -> ()
-          | _ ->
-            Vec.push new_steps proof_rule;
       end
-      in
+    )
 
-      Array.iter process_step_ steps;
+  let reconstruct_once_ = lazy (
-      composite_a ~assms:assumptions (Vec.to_array new_steps)
+    Profile.with_ "proof-quip.reconstruct" @@ fun () ->
+    Proof.iter_steps_backward X.proof process_step_;
+    ()
+  )
 
-    | p -> p (* TODO: warning? *)
+  let reconstruct () : t =
+    Lazy.force reconstruct_once_;
+    let steps = Util.array_of_list_map Lazy.force !top_steps_ in
+    P.composite_a steps
 end
 
-(** {2 Print to Quip}
+let of_proof (self:Proof.t) ~(unsat:Proof.proof_step) : P.t =
+  let module C = Conv(struct
+      let proof = self
+      let unsat = unsat
+    end) in
+  C.reconstruct()
 
-    Print to a format for checking by an external tool *)
+type out_format = Sidekick_quip.out_format =
-module Quip = struct
+  | Sexp
-  module type OUT = sig
+  | CSexp
-    type out
-    type printer = out -> unit
-    val l : printer list -> printer
-    val iter_toplist : ('a -> printer) -> 'a Iter.t -> printer
-    (* list of steps, should be printed vertically if possible *)
-    val a : string -> printer
-  end
 
-  (*
+let output = Sidekick_quip.output
-  TODO: make sure we print terms properly
-  *)
-
-  module Make(Out : OUT) = struct
-    open Out
-
-    let rec pp_t sharing (t:Term.t) : printer =
-      match T.Tbl.get sharing.Compress.terms t with
-      | Some (Named (N_s s)) -> a s(* use the newly introduced name *)
-      | Some (Named (N_t t)) -> pp_t sharing t (* use name *)
-      | _ -> pp_t_nonshare_root sharing t
-
-    and pp_t_nonshare_root sharing t =
-      let pp_t = pp_t sharing in
-      match Term.view t with
-      | Bool true -> a"true"
-      | Bool false -> a"false"
-      | App_fun (c, args) when IArray.is_empty args -> a (ID.to_string (id_of_fun c))
-      | App_fun (c, args) ->
-        l(a (ID.to_string (id_of_fun c)) :: IArray.to_list_map pp_t args)
-      | Eq (t,u) -> l[a"=";pp_t t;pp_t u]
-      | Not u -> l[a"not";pp_t u]
-      | Ite (t1,t2,t3) -> l[a"ite";pp_t t1;pp_t t2;pp_t t3]
-      | LRA lra ->
-        begin match lra with
-          | LRA_pred (p, t1, t2) -> l[a (string_of_lra_pred p); pp_t t1; pp_t t2]
-          | LRA_op (p, t1, t2) -> l[a (string_of_lra_op p); pp_t t1; pp_t t2]
-          | LRA_mult (n, x) -> l[a"lra.*"; a(Q.to_string n);pp_t x]
-          | LRA_const q -> a(Q.to_string q)
-          | LRA_simplex_var v -> pp_t v
-          | LRA_simplex_pred (v, op, q) ->
-            l[a(Sidekick_arith_lra.S_op.to_string op); pp_t v; a(Q.to_string q)]
-          | LRA_other x -> pp_t x
-        end
-
-    let rec pp_ty ty : printer =
-      match Ty.view ty with
-      | Ty_bool -> a"Bool"
-      | Ty_real -> a"Real"
-      | Ty_atomic {def;args=[];finite=_} ->
-        let id = Ty.id_of_def def in
-        a(ID.to_string id)
-      | Ty_atomic {def;args;finite=_} ->
-        let id = Ty.id_of_def def in
-        l(a(ID.to_string id)::List.map pp_ty args)
-
-    let pp_l ppx xs = l (List.map ppx xs)
-    let pp_lit ~pp_t lit = match lit with
-      | L_a(b,t) -> l[a(if b then"+" else"-");pp_t t]
-      | L_eq(b,t,u) -> l[a(if b then"+" else"-");l[a"=";pp_t t;pp_t u]]
-    let pp_cl ~pp_t c =
-      l (a "cl" :: List.map (pp_lit ~pp_t) c)
-
-    let rec pp_rec (sharing:Compress.sharing_info) (self:t) : printer =
-      let pp_rec = pp_rec sharing in
-      let pp_t = pp_t sharing in
-      let pp_cl = pp_cl ~pp_t in
-      match self with
-      | Unspecified -> a "<unspecified>"
-      | Named s -> l[a "@"; a s]
-      | CC_lemma c -> l[a"ccl"; pp_cl c]
-      | CC_lemma_imply (hyps,t,u) ->
-        l[a"ccli"; pp_l pp_rec hyps; pp_t t; pp_t u]
-      | Refl t -> l[a"refl"; pp_t t]
-      | Sorry -> a"sorry"
-      | Sorry_c c -> l[a"sorry-c"; pp_cl c]
-      | Bool_true_is_true -> a"t-is-t"
-      | Bool_true_neq_false -> a"t-ne-f"
-      | Bool_eq (t1,t2) -> l[a"bool-eq";pp_t t1;pp_t t2]
-      | Bool_c (name,ts) -> l(a"bool-c" :: a name :: List.map pp_t ts)
-      | Nn p -> l[a"nn";pp_rec p]
-      | Assertion t -> l[a"assert";pp_t t]
-      | Assertion_c c -> l[a"assert-c";pp_cl c]
-      | Drup_res c -> l[a"drup";pp_cl c]
-      | Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map (pp_hres_step sharing) steps)]
-      | Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2]
-      | Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2]
-      | DT_isa_split (ty,cs) ->
-        l[a"dt.isa.split";pp_ty ty;l(a"cases"::List.map pp_t cs)]
-      | DT_isa_disj (ty,t,u) ->
-        l[a"dt.isa.disj";pp_ty ty;pp_t t;pp_t u]
-      | DT_cstor_inj (c,i,ts,us) ->
-        l[a"dt.cstor.inj";a(ID.to_string(Cstor.id c));
-          a(string_of_int i); l(List.map pp_t ts); l(List.map pp_t us)]
-      | Ite_true t -> l[a"ite-true"; pp_t t]
-      | Ite_false t -> l[a"ite-false"; pp_t t]
-      | LRA c -> l[a"lra";pp_cl c]
-      | Composite {steps; assumptions} ->
-        let pp_ass (n,ass) : printer =
-          l[a"assuming";a n;pp_lit ~pp_t ass] in
-        l[a"steps";l(List.map pp_ass assumptions);
-          iter_toplist (pp_composite_step sharing) (Iter.of_array steps)]
-
-    and pp_composite_step sharing proof_rule : printer =
-      let pp_t = pp_t sharing in
-      let pp_cl = pp_cl ~pp_t in
-      match proof_rule with
-      | S_step_c {name;res;proof} ->
-        l[a"stepc";a name;pp_cl res;pp_rec sharing proof]
-      | S_define_t (c,rhs) ->
-        (* disable sharing for [rhs], otherwise it'd print [c] *)
-        l[a"deft";pp_t c; pp_t_nonshare_root sharing rhs]
-      | S_define_t_name (c,rhs) ->
-        l[a"deft";a c; pp_t_nonshare_root sharing rhs]
-
-    (*
-      | S_define_t (name, t) ->
-        Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t
-    *)
-
-    and pp_hres_step sharing = function
-      | R {pivot; p} -> l[a"r";pp_t sharing pivot; pp_rec sharing p]
-      | R1 p -> l[a"r1";pp_rec sharing p]
-      | P {p; lhs; rhs} ->
-        l[a"r"; pp_t sharing lhs; pp_t sharing rhs; pp_rec sharing p]
-      | P1 p -> l[a"p1"; pp_rec sharing p]
-
-    (* toplevel wrapper *)
-    let pp self : printer =
-      (* find sharing *)
-      let sharing = Profile.with1 "proof.find-sharing" Compress.find_sharing self in
-      (* introduce names *)
-      let self = Profile.with2 "proof.rename" Compress.rename sharing self in
-      (* now print *)
-      l[a"quip"; a"1"; pp_rec sharing self]
-
-    let pp_debug ~sharing self : printer =
-      if sharing then pp self
-      else pp_rec Compress.no_sharing self
-  end
-
-  module Out_csexp = struct
-    type out = out_channel
-    type printer = out -> unit
-    let l prs out =
-      output_char out '(';
-      List.iter (fun x->x out) prs;
-      output_char out ')'
-    let a s out = Printf.fprintf out "%d:%s" (String.length s) s
-    let iter_toplist f it out =
-      output_char out '(';
-      it (fun x -> f x out);
-      output_char out ')'
-  end
-
-  module Out_sexp = struct
-    type out = out_channel
-    type printer = out -> unit
-    let l prs out =
-      output_char out '(';
-      List.iteri (fun i x->if i>0 then output_char out ' ';x out) prs;
-      output_char out ')'
-    let a =
-      let buf = Buffer.create 128 in
-      fun s out ->
-        Buffer.clear buf;
-        CCSexp.to_buf buf (`Atom s);
-        Buffer.output_buffer out buf
-    let iter_toplist f it out =
-      output_char out '(';
-      let first=ref true in
-      it (fun x -> if !first then first := false else output_char out '\n'; f x out);
-      output_char out ')'
-  end
-
-  type out_format = Sexp | CSexp
-  let default_out_format = Sexp
-
-  let out_format_ = match Sys.getenv "PROOF_FMT" with
-    | "csexp" -> CSexp
-    | "sexp" -> Sexp
-    | s -> failwith (Printf.sprintf "unknown proof format %S" s)
-    | exception _ -> default_out_format
-
-  let output oc (self:t) : unit =
-    match out_format_ with
-    | Sexp -> let module M = Make(Out_sexp) in M.pp self oc
-    | CSexp ->
-      (* canonical sexp *)
-      let module M = Make(Out_csexp) in M.pp self oc
-end
-
-let pp_debug ~sharing out p =
-  let module Out = struct
-    type out = Format.formatter
-    type printer = out -> unit
-    let l prs out =
-      Fmt.fprintf out "(@[";
-      List.iteri(fun i x -> if i>0 then Fmt.fprintf out "@ "; x out) prs;
-      Fmt.fprintf out "@])"
-    let a s out = Fmt.string out s
-    let iter_toplist f it out =
-      Fmt.fprintf out "(@[<v>";
-      let first=ref true in
-      it (fun x -> if !first then first := false else Fmt.fprintf out "@ "; f x out);
-      Fmt.fprintf out "@])"
-  end
-  in
-  let module M = Quip.Make(Out) in
-  M.pp_debug ~sharing p out
-
-
-let of_proof _ _ : t = Sorry
-
-let output = Quip.output

src/base/Proof_quip.mli

@@ -1,22 +1,13 @@
+(** Export to Quip from {!module:Proof}.
 
-(** Proofs of unsatisfiability exported in Quip
+    We use {!Sidekick_quip} but do not export anything from it. *)
-
-    Proofs are used in sidekick when the problem is found {b unsatisfiable}.
-    A proof collects inferences made by the solver into a list of steps,
-    each with its own kind of justification (e.g. "by congruence"),
-    and outputs it in some kind of format.
-
-    Currently we target {{: https://c-cube.github.io/quip-book/ } Quip}
-    as an {b experimental} proof backend.
-*)
-
-open Base_types
 
 type t
-(** The state holding the whole proof. *)
 
-val pp_debug : sharing:bool -> t Fmt.printer
+val of_proof : Proof.t -> unsat:Proof.proof_step -> t
 
-val of_proof : Proof.t -> Proof.proof_step -> t
+type out_format = Sidekick_quip.out_format =
+  | Sexp
+  | CSexp
 
-val output : out_channel -> t -> unit
+val output : ?fmt:out_format -> out_channel -> t -> unit

src/base/dune

@@ -3,7 +3,7 @@
  (public_name sidekick-base)
  (synopsis "Base term definitions for the standalone SMT solver and library")
  (libraries containers iter sidekick.core sidekick.util sidekick.lit
-            sidekick-base.proof-trace
+            sidekick-base.proof-trace sidekick.quip
             sidekick.arith-lra sidekick.th-bool-static sidekick.th-data
             sidekick.zarith
             zarith)

src/quip/Sidekick_quip.ml

@@ -1,249 +1,13 @@
 
-(** A reference to a previously defined object in the proof *)
+module Proof = Proof
-type id = int
+open Proof
 
-module Ty = struct
+type t = Proof.t
-  type t =
-    | Bool
-    | Arrow of t array * t
-    | App of string * t array
-    | Ref of id
-
-  let equal : t -> t -> bool = (=)
-  let hash : t -> int = CCHash.poly
-  let[@inline] view (self:t) : t = self
-
-  let rec pp out (self:t) =
-    match self with
-    | Bool -> Fmt.string out "Bool"
-    | Arrow (args, ret) ->
-      Fmt.fprintf out "(@[->@ %a@ %a@])" (Util.pp_array pp) args pp ret
-    | App (c, [||]) -> Fmt.string out c
-    | App (c, args) ->
-      Fmt.fprintf out "(@[%s@ %a@])" c (Util.pp_array pp) args
-    | Ref id -> Fmt.fprintf out "@@%d" id
-end
-
-module Fun = struct
-  type t = string
-  let pp out (self:t) = Fmt.string out self
-  let equal : t -> t -> bool = (=)
-  let hash : t -> int = CCHash.poly
-end
-
-module Cstor = Fun
-
-module T = struct
-  type t =
-    | Bool of bool
-    | App_fun of Fun.t * t array
-    | App_ho of t * t
-    | Ite of t * t * t
-    | Not of t
-    | Eq of t * t
-    | Ref of id
-  let[@inline] view (self:t) : t = self
-
-  let equal : t -> t -> bool = (=)
-  let hash : t -> int = CCHash.poly
-
-  let rec pp out = function
-    | Bool b -> Fmt.bool out b
-    | Ite (a,b,c) -> Fmt.fprintf out "(@[if@ %a@ %a@ %a@])" pp a pp b pp c
-    | App_fun (f,[||]) -> Fmt.string out f
-    | App_fun (f,args) ->
-      Fmt.fprintf out "(@[%a@ %a@])" Fun.pp f (Util.pp_array pp) args
-    | App_ho (f,a) -> Fmt.fprintf out "(@[%a@ %a@])" pp f pp a
-    | Not a -> Fmt.fprintf out "(@[not@ %a@])" pp a
-    | Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp a pp b
-    | Ref id -> Fmt.fprintf out "@@%d" id
-
-  module As_key = struct
-    type nonrec t = t
-    let hash = hash
-    let equal = equal
-  end
-  module Tbl = CCHashtbl.Make(As_key)
-end
-
-type term = T.t
-type ty = Ty.t
-
-type lit =
-  | L_eq of bool * term * term
-  | L_a of bool * term
-
-let lit_not = function
-  | L_eq (sign,a,b) -> L_eq(not sign,a,b)
-  | L_a (sign,t) -> L_a (not sign,t)
-
-let pp_lit_with ~pp_t out =
-  let strsign = function true -> "+" | false -> "-" in
-  function
-  | L_eq (b,t,u) -> Fmt.fprintf out "(@[%s@ (@[=@ %a@ %a@])@])" (strsign b) pp_t t pp_t u
-  | L_a (b,t) -> Fmt.fprintf out "(@[%s@ %a@])" (strsign b) pp_t t
-
-let pp_lit = pp_lit_with ~pp_t:T.pp
-
-let lit_a t = L_a (true,t)
-let lit_na t = L_a (false,t)
-let lit_eq t u = L_eq (true,t,u)
-let lit_neq t u = L_eq (false,t,u)
-let lit_mk b t = L_a (b,t)
-let lit_sign = function L_a (b,_) | L_eq (b,_,_) -> b
-
-type clause = lit list
-
-type t =
-  | Unspecified
-  | Sorry (* NOTE: v. bad as we don't even specify the return *)
-  | Sorry_c of clause
-  | Named of string (* refers to previously defined clause *)
-  | Refl of term
-  | CC_lemma_imply of t list * term * term
-  | CC_lemma of clause
-  | Assertion of term
-  | Assertion_c of clause
-  | Drup_res of clause
-  | Hres of t * hres_step list
-  | Res of term * t * t
-  | Res1 of t * t
-  | 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 *)
-  | Bool_c of bool_c_name * term list (* boolean tautology *)
-  | Nn of t (* negation normalization *)
-  | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *)
-  | Ite_false of term
-  | LRA of clause
-  | Composite of {
-      (* some named (atomic) assumptions *)
-      assumptions: (string * lit) list;
-      steps: composite_step array; (* last proof_rule is the proof *)
-    }
-
-and bool_c_name = string
-
-and composite_step =
-  | S_step_c of {
-      name: string; (* name *)
-      res: clause; (* result of [proof] *)
-      proof: t; (* sub-proof *)
-    }
-  | S_define_t of term * term (* [const := t] *)
-  | S_define_t_name of string * term (* [const := t] *)
-
-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 stepc ~name res proof : composite_step = S_step_c {proof;name;res}
-let deft c rhs : composite_step = S_define_t (c,rhs)
-let deft_name c rhs : composite_step = S_define_t_name (c,rhs)
-
-let is_trivial_refl = function
-  | Refl _ -> true
-  | _ -> false
-
-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 ref_by_name name : t = Named name
-let cc_lemma c : t = CC_lemma c
-let cc_imply_l l t u : t =
-  let l = List.filter (fun p -> not (is_trivial_refl p)) l in
-  match l with
-  | [] -> refl t (* only possible way [t=u] *)
-  | l -> 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 composite_a ?(assms=[]) steps : t =
-  Composite {assumptions=assms; steps}
-let composite_l ?(assms=[]) steps : t =
-  Composite {assumptions=assms; steps=Array.of_list steps}
-let composite_iter ?(assms=[]) steps : t =
-  let steps = Iter.to_array steps in
-  Composite {assumptions=assms; steps}
-
-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 bool_c name c : t = Bool_c (name, c)
-let nn c : t = Nn c
-
-let drup_res c : t = Drup_res c
-let hres_l p l : t =
-  let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in
-  if l=[] then p else Hres (p,l)
-let hres_iter c i : t = hres_l c (Iter.to_list i)
-let res ~pivot p1 p2 : t = Res (pivot,p1,p2)
-let res1 p1 p2 : t = Res1 (p1,p2)
-
-let lra_l c : t = LRA c
-let lra c = LRA (Iter.to_rev_list c)
-
-let iter_lit ~f_t = function
-  | L_eq (_,a,b) -> f_t a; f_t b
-  | L_a (_,t) -> f_t t
-
-let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit =
-  match p with
-  | Unspecified | Sorry -> ()
-  | Sorry_c c -> f_clause c
-  | Named _ -> ()
-  | Refl t -> f_t t
-  | CC_lemma_imply (ps, t, u) -> List.iter f_p ps; f_t t; f_t u
-  | CC_lemma c | Assertion_c c -> f_clause c
-  | Assertion t -> f_t t
-  | Drup_res c -> f_clause c
-  | Hres (i, l) ->
-    f_p i;
-    List.iter
-      (function
-        | R1 p -> f_p p
-        | P1 p -> f_p p
-        | R {pivot;p} -> f_p p; f_t pivot
-        | P {lhs;rhs;p} -> f_p p; f_t lhs; f_t rhs)
-      l
-  | Res (t,p1,p2) -> f_t t; f_p p1; f_p p2
-  | Res1 (p1,p2) -> f_p p1; f_p p2
-  | DT_isa_split (_, l) -> List.iter f_t l
-  | DT_isa_disj (_, t, u) -> f_t t; f_t u
-  | DT_cstor_inj (_, _c, ts, us) -> List.iter f_t ts; List.iter f_t us
-  | Bool_true_is_true | Bool_true_neq_false -> ()
-  | Bool_eq (t, u) -> f_t t; f_t u
-  | Bool_c (_, ts) -> List.iter f_t ts
-  | Nn p -> f_p p
-  | Ite_true t | Ite_false t -> f_t t
-  | LRA c -> f_clause c
-  | Composite { assumptions; steps } ->
-    List.iter (fun (_,lit) -> iter_lit ~f_t lit) assumptions;
-    Array.iter f_step steps;
 
 (** {2 Print to Quip}
 
     Print to a format for checking by an external tool *)
-module Quip = struct
+
 module type OUT = sig
   type out
   type printer = out -> unit
@@ -253,11 +17,8 @@ module Quip = struct
   val a : string -> printer
 end
 
-  (*
+(** Build a printer that uses {!Out} *)
-  TODO: make sure we print terms properly
+module Make_printer(Out : OUT) = struct
-  *)
-
-  module Make(Out : OUT) = struct
   open Out
 
   let rec pp_t t =
@@ -299,8 +60,8 @@ module Quip = struct
 
   let pp_l ppx xs = l (List.map ppx xs)
   let pp_lit ~pp_t lit = match lit with
-      | L_a(b,t) -> l[a(if b then"+" else"-");pp_t t]
+    | Lit.L_a(b,t) -> l[a(if b then"+" else"-");pp_t t]
-      | L_eq(b,t,u) -> l[a(if b then"+" else"-");l[a"=";pp_t t;pp_t u]]
+    | Lit.L_eq(b,t,u) -> l[a(if b then"+" else"-");l[a"=";pp_t t;pp_t u]]
   let pp_cl ~pp_t c =
     l (a "cl" :: List.map (pp_lit ~pp_t) c)
 
@@ -374,6 +135,7 @@ module Quip = struct
   let pp_debug self : printer = pp self
 end
 
+(** Output to canonical S-expressions *)
 module Out_csexp = struct
   type out = out_channel
   type printer = out -> unit
@@ -388,6 +150,7 @@ module Quip = struct
     output_char out ')'
 end
 
+(** Output to classic S-expressions *)
 module Out_sexp = struct
   type out = out_channel
   type printer = out -> unit
@@ -409,21 +172,21 @@ module Quip = struct
 end
 
 type out_format = Sexp | CSexp
+let string_of_out_format = function
+  | Sexp -> "sexp"
+  | CSexp -> "csexp"
+let pp_out_format out f = Fmt.string out (string_of_out_format f)
+
 let default_out_format = Sexp
 
-  let out_format_ = match Sys.getenv "PROOF_FMT" with
+let output ?(fmt=Sexp) oc (self:t) : unit =
-    | "csexp" -> CSexp
+  match fmt with
-    | "sexp" -> Sexp
+  | Sexp ->
-    | s -> failwith (Printf.sprintf "unknown proof format %S" s)
+    let module M = Make_printer(Out_sexp) in
-    | exception _ -> default_out_format
+    M.pp self oc
-
-  let output oc (self:t) : unit =
-    match out_format_ with
-    | Sexp -> let module M = Make(Out_sexp) in M.pp self oc
   | CSexp ->
-      (* canonical sexp *)
+    let module M = Make_printer(Out_csexp) in
-      let module M = Make(Out_csexp) in M.pp self oc
+    M.pp self oc
-end
 
 let pp_debug out p =
   let module Out = struct
@@ -441,10 +204,6 @@ let pp_debug out p =
       Fmt.fprintf out "@])"
   end
   in
-  let module M = Quip.Make(Out) in
+  let module M = Make_printer(Out) in
   M.pp_debug p out
 
-
-let of_proof _ _ : t = Sorry
-
-let output = Quip.output

src/quip/Sidekick_quip.mli

@@ -5,9 +5,21 @@
     as an {b experimental} proof backend.
 *)
 
-type t
+module Proof = Proof
+
+type t = Proof.t
 (** The state holding the whole proof. *)
 
-val pp_debug : t Fmt.printer
+(** What format to use to serialize the proof? *)
+type out_format =
+  | Sexp
+    (** S-expressions *)
 
-val output : out_channel -> t -> unit
+  | CSexp
+    (** Canonical S-expressions *)
+
+val pp_out_format : out_format Fmt.printer
+
+val output : ?fmt:out_format -> out_channel -> t -> unit
+
+val pp_debug : t Fmt.printer

src/smtlib/Process.ml

@@ -180,11 +180,11 @@ let solve
         | Some file ->
           begin match unsat_proof_step() with
             | None -> ()
-            | Some step ->
+            | Some unsat_step ->
               let proof = Solver.proof s in
               let proof_quip =
                 Profile.with_ "proof.to-quip" @@ fun () ->
-                Proof_quip.of_proof proof step
+                Proof_quip.of_proof proof ~unsat:unsat_step
               in
               Profile.with_ "proof.write-file"
                 (fun () ->

src/util/Util.ml

@@ -37,6 +37,9 @@ let array_of_list_map f l =
 let array_to_list_map f arr =
   CCList.init (Array.length arr) (fun i -> f arr.(i))
 
+let lazy_map f x = lazy (let (lazy x) = x in f x)
+let lazy_map2 f x y = lazy (let (lazy x) = x and (lazy y) = y in f x y)
+
 let setup_gc () =
   let g = Gc.get () in
   Gc.set {

src/util/Util.mli

@@ -21,6 +21,9 @@ val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array
 
 val array_to_list_map : ('a -> 'b) -> 'a array -> 'b list
 
+val lazy_map : ('a -> 'b) -> 'a lazy_t -> 'b lazy_t
+val lazy_map2 : ('a -> 'b -> 'c) -> 'a lazy_t -> 'b lazy_t -> 'c lazy_t
+
 val setup_gc : unit -> unit
 (** Change parameters of the GC *)