From c5c5426eadbc79be72ab4c35858bde48f2358230 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 19 Nov 2021 23:25:21 -0500 Subject: [PATCH] quip: include all term definitions in proof dependency analysis will not catch these, so we include them unconditionally --- src/base/Proof_quip.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml index 38470073..58e34f1b 100644 --- a/src/base/Proof_quip.ml +++ b/src/base/Proof_quip.ml @@ -88,11 +88,16 @@ end = struct where it's typically `(stepc c5 (cl …) (ccl (cl …)))` for twice the space. *) + let is_def_ (step:PS.Step.t) = + match step.view with + | PS.Step_view.Expr_def _ -> true + | _ -> false + (* process a step of the trace *) let process_step_ (step: PS.Step.t) : unit = let lid = step.id in let id = Int32.to_int lid in - if Util.Int_tbl.mem needed_steps_ id then ( + if Util.Int_tbl.mem needed_steps_ id || is_def_ step then ( Log.debugf 20 (fun k->k"(@[proof-quip.process-needed-step@ %a@])" PS.Step.pp step); Util.Int_tbl.remove needed_steps_ id;