From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Apr 2005 12:13:58 +0000 (+0000)
Subject: added orrible hack to make the current uri visible in the parser so that named univer... 
X-Git-Tag: single_binding~134
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03d2302343e8e1b282c1b2afec8db7913413d9d1;p=helm.git

added orrible hack to make the current uri visible in the parser so that named universes are generated
---

diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml
index 8e6d276d5..940e03e2b 100644
--- a/helm/ocaml/cic/cicParser3.ml
+++ b/helm/ocaml/cic/cicParser3.ml
@@ -43,6 +43,11 @@ exception IllFormedXml of int;;
 
 (* Utility functions to map a markup attribute to something useful *)
 
+let uri = ref (UriManager.uri_of_string "cic:/none.con")
+
+let set_uri u = 
+  uri := u
+
 let cic_attr_of_xml_attr =
  function
     Pxp_types.Value s       -> Cic.Name s
@@ -53,7 +58,8 @@ let cic_sort_of_xml_attr =
  function
     Pxp_types.Value "Prop" -> Cic.Prop
   | Pxp_types.Value "Set"  -> Cic.Set
-  | Pxp_types.Value "Type" -> Cic.Type (CicUniv.fresh ()) (* TASSI: sure? *)
+  | Pxp_types.Value "Type" -> 
+      Cic.Type (CicUniv.fresh ~uri:!uri ()) (* ORRIBLE HACK *)
   | _            -> raise (IllFormedXml 2)
 
 let int_of_xml_attr =
diff --git a/helm/ocaml/cic/cicParser3.mli b/helm/ocaml/cic/cicParser3.mli
index 3c2f5d94c..8fc0704d4 100644
--- a/helm/ocaml/cic/cicParser3.mli
+++ b/helm/ocaml/cic/cicParser3.mli
@@ -61,3 +61,6 @@ class virtual cic_term :
 (* The definition of domspec, an hashtable that maps each node type to the *)
 (* object that must be linked to it. Used by markup.                       *)
 val domspec : cic_term Pxp_document.spec
+
+val set_uri: UriManager.uri -> unit
+
diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 7f8266876..c986ae866 100644
--- a/helm/ocaml/cic/cicUniv.ml
+++ b/helm/ocaml/cic/cicUniv.ml
@@ -128,8 +128,8 @@ let are_ugraph_eq = are_ugraph_eq307
 let string_of_universe (i,u) = 
   match u with
       Some u ->
-	((string_of_int i) ^ " " ^ (UriManager.string_of_uri u))
-    | None -> (string_of_int i)
+	"(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
+    | None -> "(" ^ (string_of_int i) ^ ",None)"
 
 let string_of_universe_set l = 
   SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
@@ -142,7 +142,7 @@ let string_of_node n =
   "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n"
 
 let string_of_arc (a,u,v) = 
-  "(" ^ (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v) ^ ")"
+  (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v)
   
 let string_of_mal m =
   let rc = ref "" in
@@ -178,7 +178,7 @@ let partial = ref 0.0 ;;
 let reset_spent_time () = time_spent := 0.0;;
 let get_spent_time () = !time_spent ;;
 let begin_spending () =
-  assert (!partial = 0.0);
+  (*assert (!partial = 0.0);*)
   partial := Unix.gettimeofday ()
 ;;
 
@@ -419,11 +419,14 @@ exception UniverseInconsistency of string
 
 let error arc node1 closure_type node2 closure =
   let s = "\n  ===== Universe Inconsistency detected =====\n\n" ^
-   "\tUnable to add "^ (string_of_arc arc) ^ " cause " ^ 
-   (string_of_universe node1) ^ " is in the " ^
-   closure_type ^ " closure {" ^
-   (string_of_universe_set closure) ^ "} of " ^ 
-   (string_of_universe node2) ^ "\n\n" ^
+   "   Unable to add\n" ^ 
+   "\t" ^ (string_of_arc arc) ^ "\n" ^
+   "   cause\n" ^ 
+   "\t" ^ (string_of_universe node1) ^ "\n" ^
+   "   is in the " ^ closure_type ^ " closure\n" ^
+   "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
+   "   of\n" ^ 
+   "\t" ^ (string_of_universe node2) ^ "\n\n" ^
    "  ===== Universe Inconsistency detected =====\n" in
   prerr_endline s;
   raise (UniverseInconsistency s)
@@ -463,13 +466,22 @@ type universe_graph = bag
 
 let empty_ugraph = empty_bag
 
-let current_index = ref (-1)
+let current_index_anon = ref (-1)
+let current_index_named = ref (-1)
 
-let restart_numbering () = current_index := (-1) 
+let restart_numbering () = current_index_named := (-1) 
 
-let fresh () =
-  current_index := !current_index + 1;
-  (!current_index,None)
+let fresh ?uri () =
+  let i =
+    match uri with
+    | None -> 
+        current_index_anon := !current_index_anon + 1;
+        !current_index_anon
+    | Some _ -> 
+        current_index_named := !current_index_named + 1;
+        !current_index_named
+  in
+  (i,uri)
 
 let print_ugraph g = 
   prerr_endline (string_of_bag g)
diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli
index 7bd224946..74af1ccc4 100644
--- a/helm/ocaml/cic/cicUniv.mli
+++ b/helm/ocaml/cic/cicUniv.mli
@@ -43,7 +43,9 @@ type universe_graph
   returns a fresh universe
 *)
 val fresh: 
-  unit -> universe
+  ?uri:UriManager.uri ->
+  unit -> 
+    universe
 
 (*
   really useful at the begin and in all the functions that don't care