Universes introduction

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 14c69a4571900d956f041581595c55071def654d..b3525d3182bcec3737d02c2883cd7402d1acf730 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -161,9 +161,15 @@ and type_of_aux' metasenv context t =
          check_metasenv_consistency n subst metasenv context canonical_context l
         in
         CicSubstitution.lift_meta l ty, subst', metasenv'
-    | C.Sort s ->
-       C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
-        subst,metasenv
+     (* TASSI: CONSTRAINT *)
+    | C.Sort (C.Type t) ->
+        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'),subst,metasenv
+     (* TASSI: CONSTRAINT *)
+    | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
     | C.Implicit _ -> raise (AssertFailure "21")
     | C.Cast (te,ty) ->
        let _,subst',metasenv' =
@@ -479,9 +485,15 @@ and type_of_aux' metasenv context t =
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
           C.Sort s2,subst,metasenv
-     | (C.Sort s1, C.Sort s2) ->
-         (*CSC manca la gestione degli universi!!! *)
-         C.Sort C.Type,subst,metasenv
+     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
+       (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+       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'),subst,metasenv
+     | (C.Sort _,C.Sort (C.Type t1)) -> 
+       (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+       C.Sort (C.Type t1),subst,metasenv
      | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
      | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
          (* TODO how can we force the meta to become a sort? If we don't we