added assertions about graph in the environment having Some uris

[helm.git] / helm / ocaml / cic / cicUniv.ml

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 *)