From 9d3dcd6970c1e24c8191f268c441e42c8d8b6c89 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
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