new universes implementation

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 36bfb28b19cd22c77c7471ec5343dab140f20861..140e4171287a73a4b1164f857306f31368bb2806 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -127,6 +127,7 @@ let rec type_of_constant uri =
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        CicLogger.log (`Start_type_checking uri) ;
+       CicUniv.directly_to_env_begin ();
        (* let's typecheck the uncooked obj *)
        (match uobj with
            C.Constant (_,Some te,ty,_) ->
@@ -160,6 +161,7 @@ let rec type_of_constant uri =
             ("Unknown constant:" ^ U.string_of_uri uri))
        );
        CicEnvironment.set_type_checking_info uri ;
+       CicUniv.directly_to_env_end ();
        CicLogger.log (`Type_checking_completed uri) ;
        match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
@@ -180,6 +182,7 @@ and type_of_variable uri =
      CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
       CicLogger.log (`Start_type_checking uri) ;
+      CicUniv.directly_to_env_begin ();
       (* only to check that ty is well-typed *)
       let _ = type_of ty in
        (match bo with
@@ -190,6 +193,7 @@ and type_of_variable uri =
                 ("Unknown variable:" ^ U.string_of_uri uri))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
+       CicUniv.directly_to_env_end ();
        CicLogger.log (`Type_checking_completed uri) ;
        ty
    |  _ ->
@@ -518,8 +522,10 @@ and type_of_mutual_inductive_defs uri i =
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        CicLogger.log (`Start_type_checking uri) ;
+       CicUniv.directly_to_env_begin ();
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
+       CicUniv.directly_to_env_end ();
        CicLogger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
@@ -543,8 +549,10 @@ and type_of_mutual_inductive_constr uri i j =
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        CicLogger.log (`Start_type_checking uri) ;
+       (*CicUniv.directly_to_env_begin ();*)
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
+       (*CicUniv.directly_to_env_end ();*)
        CicLogger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
@@ -799,7 +807,7 @@ and guarded_by_destructors context n nn kl x safes =
         | Some (_,C.Def (bo,_)) ->
            guarded_by_destructors context m nn kl x safes
             (CicSubstitution.lift m bo)
-       | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
+        | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
       )
    | C.Meta _
    | C.Sort _
@@ -1236,9 +1244,9 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
             C.Sort C.Prop
           | C.Sort C.Set  -> true
-         | C.Sort C.CProp -> true
+          | C.Sort C.CProp -> true
           | C.Sort (C.Type _) ->
-           (* TASSI: da verificare *)
+            (* TASSI: da verificare *)
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,paramsno) ->
                   let (_,_,_,cl) = List.nth itl i in
@@ -1345,7 +1353,7 @@ and type_of_aux' metasenv context t =
           | Some (_,C.Def (bo,None)) ->
              debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
              type_of_aux context (S.lift n bo)
-         | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
+          | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
         with
         _ ->
           raise (TypeCheckerFailure "unbound variable")
@@ -1366,8 +1374,8 @@ and type_of_aux' metasenv context t =
     | 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
+          assert false (* t' is fresh! an error in CicUniv *)
+        else
           C.Sort (C.Type t')
       (* TASSI: CONSTRAINTS *)
     | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ()))
@@ -1587,7 +1595,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
        List.rev
         (List.map
           (fun (n,ty,_) -> 
-           let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
+            let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
       in
        let len = List.length types in
         List.iter
@@ -1660,7 +1668,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
    match (t1', t2') with
       (C.Sort s1, C.Sort s2)
         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
-        (* different from Coq manual!!! *)
+         (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
@@ -1670,7 +1678,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
        C.Sort (C.Type t')
     | (C.Sort _,C.Sort (C.Type t1)) -> 
         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
-       C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+        C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
     | (C.Meta _, C.Sort _) -> t2'
     | (C.Meta _, (C.Meta (_,_) as t))
     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
@@ -1771,15 +1779,18 @@ in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
 *)
 ;;
 
+(* tassi FIXME: not sure where is this called... no history here... *)
 let typecheck uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.is_type_checked ~trust:false uri with
-     CicEnvironment.CheckedObj _ -> ()
+  (*match CicEnvironment.is_type_checked ~trust:false uri with*)
+  match CicEnvironment.is_type_checked ~trust:true uri with
+     CicEnvironment.CheckedObj cobj -> cobj
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
       CicLogger.log (`Start_type_checking uri) ;
+      CicUniv.directly_to_env_begin ();
       (match uobj with
           C.Constant (_,Some te,ty,_) ->
            let _ = type_of ty in
@@ -1819,5 +1830,7 @@ let typecheck uri =
            check_mutual_inductive_defs uri uobj
       ) ;
       CicEnvironment.set_type_checking_info uri ;
-      CicLogger.log (`Type_checking_completed uri)
+      CicUniv.directly_to_env_end ();
+      CicLogger.log (`Type_checking_completed uri);
+      uobj
 ;;