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

feat(cc): add an invariant check before returning a model

Browse source
This commit is contained in:
Simon Cruanes 2021-12-17 15:29:28 -05:00
parent b19d80e443
commit be2d57a717
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 27 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/cc/Sidekick_cc.ml
View file

@ -935,7 +935,34 @@ module Make (A: CC_ARG)
let new_merges cc = cc.new_merges
let check_inv_enabled_ = true (* XXX NUDGE *)
(* check some internal invariants *)
let check_inv_ (self:t) : unit =
if check_inv_enabled_ then (
Log.debug 2 "(cc.check-invariants)";
all_classes self
|> Iter.flat_map N.iter_class
|> Iter.iter
(fun n ->
match n.n_sig0 with
| None -> ()
| Some s ->
let s' = update_sig s in
let ok = match find_signature self s' with
| None -> false
| Some r -> N.equal r n.n_root
in
if not ok then (
Log.debugf 0
(fun k->k "(@[cc.check.fail@ :n %a@ :sig %a@ :actual-sig %a@])"
N.pp n Signature.pp s Signature.pp s')
)
)
)
(* model: return all the classes *)
let get_model (cc:t) : repr Iter.t Iter.t =
check_inv_ cc;
all_classes cc |> Iter.map N.iter_class
end