added assertions about graph in the environment having Some uris

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 44bccc62b281715cbb7c35d882747dd8f25f157a..7f8266876ddbcaf891d03c8e8bc0bc8086eba685 100644 (file)
--- 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 d2b2483a19b5b331b7c9a601d5ebe674e9051950..7bd224946afd02b181d58d38cbef232dc1d31d69 100644 (file)
--- 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
 *)