Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / cic_omdoc / doubleTypeInference.ml

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 5b0cc01fc438ebd695508f635fd6bab8f77c6c86..235d8d835b47f7aac01f9ebe91e0c9f2d1d6c2c1 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -41,7 +41,7 @@ let double_work = ref 0;;
 
 let xxx_type_of_aux' m c t =
  let t1 = Sys.time () in
- let res = CicTypeChecker.type_of_aux' m c t in
+ let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
  let t2 = Sys.time () in
  type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
  res
@@ -266,8 +266,8 @@ let type_of_constant uri =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
-      CicEnvironment.CheckedObj cobj -> cobj
+   match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+      CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constant")
   in
@@ -281,8 +281,8 @@ let type_of_variable uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.is_type_checked uri with
-     CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
+  match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),_) -> ty
    | CicEnvironment.UncheckedObj (C.Variable _) ->
       raise (NotWellTyped "Reference to an unchecked variable")
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
@@ -293,8 +293,8 @@ let type_of_mutual_inductive_defs uri i =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
-      CicEnvironment.CheckedObj cobj -> cobj
+   match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+      CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked inductive type")
   in
@@ -310,8 +310,8 @@ let type_of_mutual_inductive_constr uri i j =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
-      CicEnvironment.CheckedObj cobj -> cobj
+   match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+      CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constructor")
   in
@@ -400,11 +400,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
             (* Checks suppressed *)
             CicSubstitution.lift_meta l ty
      | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
-        let t' = CicUniv.fresh() in
-        if not (CicUniv.add_gt t' t ) then
-         assert false (* t' is fresh! an error in CicUniv *)
-       else
-          C.Sort (C.Type t')
+         C.Sort (C.Type (CicUniv.fresh()))
      | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
      | C.Implicit _ -> raise (Impossible 21)
      | C.Cast (te,ty) ->
@@ -541,9 +537,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          (* Checks suppressed *)
          (* Let's visit all the subterms that will not be visited later *)
          let (cl,parsno) =
-           let obj =
+           let obj,_ =
              try
-               CicEnvironment.get_cooked_obj uri
+               CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
              with Not_found -> assert false
            in
           match obj with
@@ -644,9 +640,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
 
  and visit_exp_named_subst context uri exp_named_subst =
   let uris_and_types =
-     let obj =
+     let obj,_ =
        try
-         CicEnvironment.get_cooked_obj uri
+         CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
        with Not_found -> assert false
      in
     match obj with
@@ -656,9 +652,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
     | Cic.InductiveDefinition (_,params,_) ->
        List.map
         (function uri ->
-           let obj =
+           let obj,_ =
              try
-               CicEnvironment.get_cooked_obj uri
+               CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
              with Not_found -> assert false
            in
            match obj with
@@ -690,11 +686,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
-       (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
-       let t' = CicUniv.fresh() in
-       if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
-         assert false ; (* not possible, error in CicUniv *)
-       C.Sort (C.Type t')
+       C.Sort (C.Type (CicUniv.fresh()))
     | (C.Sort _,C.Sort (C.Type t1)) -> 
         (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
        C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)