From 9d3dcd6970c1e24c8191f268c441e42c8d8b6c89 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 29 Apr 2005 08:07:05 +0000 Subject: [PATCH] added assertions about graph in the environment having Some uris --- helm/ocaml/cic/cicUniv.ml | 21 +++++++++++++++++++++ helm/ocaml/cic/cicUniv.mli | 4 ++++ 2 files changed, 25 insertions(+) diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index 44bccc62b..7f8266876 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -929,4 +929,25 @@ let recons_graph graph = MAL.add (recons_univ universe) (recons_entry entry) map) graph MAL.empty +let assert_univs_have_uri graph = + let assert_univ u = + match u with + | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole") + | _ -> () + in + let assert_set s = + SOF.iter (fun u -> assert_univ u) s + in + let assert_entry e = + assert_set e.eq_closure; + assert_set e.ge_closure; + assert_set e.gt_closure; + assert_set e.in_gegt_of; + assert_set e.one_s_eq; + assert_set e.one_s_ge; + assert_set e.one_s_gt; + in + MAL.iter (fun k v -> assert_univ k; assert_entry v)graph + + (* EOF *) diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli index d2b2483a1..7bd224946 100644 --- a/helm/ocaml/cic/cicUniv.mli +++ b/helm/ocaml/cic/cicUniv.mli @@ -118,6 +118,10 @@ val restart_numbering: * CicEnvironment.restore_from_channel *) val recons_graph: universe_graph -> universe_graph + (** consistency chek that should be done before committin the graph to the + * cache *) +val assert_univs_have_uri: universe_graph -> unit + (* Benchmarking stuff *) -- 2.39.2