simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 12:15:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

quip: include all term definitions in proof

Browse source 
dependency analysis will not catch these, so we include them
unconditionally
This commit is contained in:
Simon Cruanes 2021-11-19 23:25:21 -05:00
parent 38d90b250a
commit c5c5426ead
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/base/Proof_quip.ml
View file

@ -88,11 +88,16 @@ end = struct
where it's typically `(stepc c5 (cl …) (ccl (cl …)))` for twice the space. 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 *) (* process a step of the trace *)
let process_step_ (step: PS.Step.t) : unit = let process_step_ (step: PS.Step.t) : unit =
let lid = step.id in let lid = step.id in
let id = Int32.to_int lid 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); Log.debugf 20 (fun k->k"(@[proof-quip.process-needed-step@ %a@])" PS.Step.pp step);
Util.Int_tbl.remove needed_steps_ id; Util.Int_tbl.remove needed_steps_ id;