added universes

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index e9ce2e81ca002ea8572bf46a0e1209279a53a62a..d267b52b1ff39ab713b815914e5448bb799bb563 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -318,7 +318,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
         Cic.Meta (index, cic_subst)
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
-    | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
+    | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
     | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index bcfd6c9f62282e15163a5e988beb3a736702d41a..4622f67a6f1eff41881d7c3939a3dfe55fc9097d 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -425,7 +425,7 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type" -> `Type
+    | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp" -> `CProp
     ]
   ];

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 3e48d36792d3a33ce508e07dfa48179ae7f42a6c..1c3ad438687b731a39a02833bcce8590c1ff6405 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -116,7 +116,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Num (num, _) -> num
     | Ast.Sort `Set -> "Set"
     | Ast.Sort `Prop -> "Prop"
-    | Ast.Sort `Type -> "Type"
+    | Ast.Sort (`Type _) -> "Type"
     | Ast.Sort `CProp -> "CProp"
     | Ast.Symbol (name, _) -> "'" ^ name
 

diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml
index ca00d35396771622d890785a69dd9425d71893c6..bce1599373b96c0d3cba5820891fe10741765094 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -27,7 +27,7 @@
 
 type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
 type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
 type fold_kind = [ `Left | `Right ]
 
 type location = Lexing.position * Lexing.position

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 3d684fe39b0ff27f57fd3eb6cd23180d30042f20..0029e3db5570f95b2015211869e817257339ee20 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -116,7 +116,7 @@ let string_of_sort_kind = function
   | `Prop -> "Prop"
   | `Set -> "Set"
   | `CProp -> "CProp"
-  | `Type -> "Type"
+  | `Type _ -> "Type"
 
 let pp_ast0 t k =
   let rec aux =
@@ -275,7 +275,7 @@ let ast_of_acic0 term_info acic k =
       Hashtbl.find term_info.sort id
     with Not_found ->
       prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
-      `Type
+      `Type (CicUniv.fresh ())
   in
   let aux_substs substs =
     Some
@@ -298,13 +298,13 @@ let ast_of_acic0 term_info acic k =
     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l))
     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
-    | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type)
+    | Cic.ASort (id,Cic.Type u) ->idref id (Ast.Sort (`Type u))
     | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
     | Cic.AImplicit _ -> assert false
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type -> `Pi
+          | `Set | `Type _ -> `Pi
           | `Prop | `CProp -> `Forall
         in
         idref id (Ast.Binder (binder_kind,

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 69c91cdb3eb959d07fa1e8592ddf80adc518de02..0d3127c3176be7c7d2b514895f28257ac927b689 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -23,25 +23,18 @@
  * http://cs.unibo.it/helm/.
  *)
 
-type sort_kind = [ `Prop | `Set | `Type | `CProp ]
-
-let sort_of_string = function
-  | "Prop" -> `Prop
-  | "Set" -> `Set
-  | "Type" -> `Type
-  | "CProp" -> `CProp
-  | _ -> assert false
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
 
 let string_of_sort = function
   | `Prop -> "Prop"
   | `Set -> "Set"
-  | `Type -> "Type"
+  | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u)
   | `CProp -> "CProp"
 
 let sort_of_sort = function
   | Cic.Prop  -> `Prop
   | Cic.Set   -> `Set
-  | Cic.Type _ -> `Type
+  | Cic.Type u -> `Type u
   | Cic.CProp -> `CProp
 
 (* let hashtbl_add_time = ref 0.0;; *)
@@ -134,8 +127,8 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
        match CicReduction.whd context t with 
           C.Sort C.Prop  -> `Prop
         | C.Sort C.Set   -> `Set
-        | C.Sort (C.Type _)
-        | C.Meta _       -> `Type
+        | C.Sort (C.Type u) -> `Type u
+        | C.Meta _       -> `Type (CicUniv.fresh())
         | C.Sort C.CProp -> `CProp
         | t              ->
             prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
@@ -188,7 +181,8 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
         with
          Not_found ->  (* l'inner-type non e' nella tabella ==> sort <> Prop *)
           (* CSC: Type or Set? I can not tell *)
-          None,Cic.Sort (Cic.Type (CicUniv.fresh())),`Type,false 
+          let u = CicUniv.fresh() in
+          None,Cic.Sort (Cic.Type u),`Type u,false 
          (* TASSI non dovrebbe fare danni *)
 (* *)
        in

diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli
index abe61f38769871fb007e1e53c83e686dabfd7dc4..b5a194951abd8871f5b2a4a640ccd3f2c08350f3 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.mli
+++ b/helm/ocaml/cic_omdoc/cic2acic.mli
@@ -31,10 +31,10 @@ type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
 
-type sort_kind = [ `Prop | `Set | `Type | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
 
 val string_of_sort: sort_kind -> string
-val sort_of_string: string -> sort_kind
+(*val sort_of_string: string -> sort_kind*)
 val sort_of_sort: Cic.sort -> sort_kind
 
 val acic_object_of_cic_object :

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index ff80809831a167aeb9fe94577ea9141360659051..72699f7e3cb2b584da6617a278a1b1f611945abd 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -345,7 +345,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  let sort = 
                    (try
                      Hashtbl.find ids_to_inner_sorts idr 
-                    with Not_found -> `Type) in 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
                  if sort = `Prop then 
                     K.Premise 
                       { K.premise_id = gen_id premise_prefix seed;
@@ -358,7 +358,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  let sort = 
                    (try
                      Hashtbl.find ids_to_inner_sorts id 
-                    with Not_found -> `Type) in 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
                  if sort = `Prop then 
                     K.Lemma 
                       { K.lemma_id = gen_id lemma_prefix seed;
@@ -370,7 +370,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  let sort = 
                    (try
                      Hashtbl.find ids_to_inner_sorts id 
-                    with Not_found -> `Type) in 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
                  if sort = `Prop then 
                     let inductive_types =
                       (let o,_ = 
@@ -731,7 +731,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   let idarg = get_id arg in
                   let sortarg = 
                     (try (Hashtbl.find ids_to_inner_sorts idarg)
-                     with Not_found -> `Type) in
+                     with Not_found -> `Type (CicUniv.fresh())) in
                   let hdarg = 
                     if sortarg = `Prop then
                       let (co,bo) = 
@@ -816,7 +816,7 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   else 
                     let aid = get_id a in
                     let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
-                      with Not_found -> `Type) in
+                      with Not_found -> `Type (CicUniv.fresh())) in
                     if asort = `Prop then
                       K.ArgProof (aux a)
                     else K.Term a in