]> matita.cs.unibo.it Git - helm.git/commitdiff
cicEnvironment refactoring with sound view of Coq`s univ-less terms
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 18 Apr 2008 15:30:40 +0000 (15:30 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 18 Apr 2008 15:30:40 +0000 (15:30 +0000)
helm/software/components/cic_acic/doubleTypeInference.ml
helm/software/components/cic_proof_checking/cicEnvironment.ml
helm/software/components/cic_proof_checking/cicEnvironment.mli
helm/software/components/cic_proof_checking/cicTypeChecker.ml

index 4910275ea48c291662f213bd72fdb3ddd5e462c1..d54d0fbe4dbf56b431d4d2c6daf3eb1919f54562 100644 (file)
@@ -182,7 +182,7 @@ let type_of_constant uri =
   let cobj =
    match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,_) ->
        raise (NotWellTyped "Reference to an unchecked constant")
   in
    match cobj with
@@ -197,7 +197,7 @@ let type_of_variable uri =
  let module U = UriManager in
   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
      CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
-   | CicEnvironment.UncheckedObj (C.Variable _) ->
+   | CicEnvironment.UncheckedObj (C.Variable _,_) ->
       raise (NotWellTyped "Reference to an unchecked variable")
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 ;;
@@ -209,7 +209,7 @@ let type_of_mutual_inductive_defs uri i =
   let cobj =
    match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,_) ->
        raise (NotWellTyped "Reference to an unchecked inductive type")
   in
    match cobj with
@@ -226,7 +226,7 @@ let type_of_mutual_inductive_constr uri i j =
   let cobj =
    match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,_) ->
        raise (NotWellTyped "Reference to an unchecked constructor")
   in
    match cobj with
index ec12c8d01c80a790fec70c836ea5efa7cc4e1d3e..fde76a60b2882f17a85ab060c9a25f5500535518 100644 (file)
@@ -53,9 +53,8 @@ let debug_print = if debug then fun x -> prerr_endline (Lazy.force x) else ignor
  * ************************************************************************** *)
 
 type type_checked_obj =
-   CheckedObj of (Cic.obj * CicUniv.universe_graph)    (* cooked obj *)
- | UncheckedObj of Cic.obj   (* uncooked obj to proof-check *)
-;;
+ | CheckedObj of (Cic.obj * CicUniv.universe_graph)    
+ | UncheckedObj of Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
 
 exception AlreadyCooked of string;;
 exception CircularDependency of string Lazy.t;;
@@ -82,15 +81,14 @@ module Cache :
      get_object_to_add:
        (UriManager.uri -> 
          Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option) -> 
-     Cic.obj * CicUniv.universe_graph * CicUniv.universe list
+     Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
    val can_be_cooked:
      UriManager.uri -> bool
    val unchecked_to_frozen : 
      UriManager.uri -> unit
    val frozen_to_cooked :
-     uri:UriManager.uri -> unit
-   val hack_univ:
-     UriManager.uri -> CicUniv.universe_graph * CicUniv.universe list -> unit
+     uri:UriManager.uri -> 
+     Cic.obj -> CicUniv.universe_graph -> CicUniv.universe list -> unit
    val find_cooked : 
      key:UriManager.uri -> 
        Cic.obj * CicUniv.universe_graph * CicUniv.universe list
@@ -211,17 +209,7 @@ module Cache :
 
     let find_or_add_to_unchecked uri ~get_object_to_add =
      try
-       let o,g_and_l = List.assq uri !unchecked_list in
-         match g_and_l with
-             (* FIXME: we accept both cases, as at the end of this function 
-               * maybe the None universe outside the cache module should be
-               * avoided elsewhere.
-               *
-               * another thing that should be removed if univ generation phase
-               * and lib exportation are unified.
-               *)
-           | None -> o,CicUniv.empty_ugraph,[]
-           | Some (g,l) -> o,g,l
+       List.assq uri !unchecked_list
      with
          Not_found ->
            if List.mem_assq uri !frozen_list then
@@ -245,15 +233,8 @@ module Cache :
              else
                (* OK, it is not already frozen nor cooked *)
                let obj,ugraph_and_univlist = get_object_to_add uri in
-               let ugraph_real, univlist_real = 
-                 match ugraph_and_univlist with
-                     (* FIXME: not sure it is OK*)
-                     None -> CicUniv.empty_ugraph, []
-                   | Some ((g,l) as g_and_l) -> g_and_l
-               in
-               unchecked_list := 
-                 (uri,(obj,ugraph_and_univlist))::!unchecked_list ;
-               obj, ugraph_real, univlist_real
+               unchecked_list := (uri,(obj,ugraph_and_univlist))::!unchecked_list;
+               obj, ugraph_and_univlist
     ;;
 
     let unchecked_to_frozen uri =
@@ -265,70 +246,14 @@ module Cache :
         Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
     ;;
 
-   
-   (************************************************************
-     TASSI: invariant
-     only object with a valid universe graph can be committed
-
-     this should disappear if the universe generation phase and the 
-     library exportation are unified.
-   *************************************************************)
-   let frozen_to_cooked ~uri =
-    try
-      let obj,ugraph_and_univlist = List.assq uri !frozen_list in
-        match ugraph_and_univlist with
-        | None -> assert false (* only NON dummy universes can be committed *)
-        | Some (g,l) ->
-           CicUniv.assert_univs_have_uri g l;
-           frozen_list := List.remove_assq uri !frozen_list ;
-           HT.add cacheOfCookedObjects uri (obj,g,l) 
-    with
-        Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
+   let frozen_to_cooked ~uri o ug ul =
+     CicUniv.assert_univs_have_uri ug ul;
+     frozen_list := List.remove_assq uri !frozen_list ;
+     HT.add cacheOfCookedObjects uri (o,ug,ul) 
    ;;
 
-   let can_be_cooked uri =
-     try
-       let obj,ugraph_and_univlist = List.assq uri !frozen_list in
-         (* FIXME: another thing to remove if univ generation phase and lib
-          * exportation are unified.
-          *)
-         match ugraph_and_univlist with
-             None -> false
-           | Some _ -> true
-     with
-         Not_found -> false
-   ;;
+   let can_be_cooked uri = List.mem_assq uri !frozen_list;;
    
-   (* this function injects a real universe graph in a (uri, (obj, None))
-    * element of the frozen list.
-    *
-    * FIXME: another thing to remove if univ generation phase and lib
-    * exportation are unified.
-    *)
-   let hack_univ uri (real_ugraph, real_univlist)  =
-     try
-       let o,ugraph_and_univlist = List.assq uri !frozen_list in
-         match ugraph_and_univlist with
-             None -> 
-               frozen_list := List.remove_assoc uri !frozen_list;
-               frozen_list := 
-                 (uri,(o,Some (real_ugraph, real_univlist)))::!frozen_list;
-           | Some g -> 
-               debug_print (lazy (
-                 "You are probably hacking an object already hacked or an"^
-                 " object that has the universe file but is not"^
-                 " yet committed."));
-               assert false
-     with
-         Not_found -> 
-           debug_print (lazy (
-             "You are hacking an object that is not in the"^
-             " frozen_list, this means you are probably generating an"^
-             " universe file for an object that already"^
-             " as an universe file"));
-           assert false
-   ;;
-
    let find_cooked ~key:uri = HT.find cacheOfCookedObjects uri ;;
  
    let add_cooked ~key:uri (obj,ugraph,univlist) = 
@@ -407,8 +332,7 @@ let get_object_to_add uri =
     | Http_getter_types.Unresolvable_URI _ ->
       debug_print (lazy (
         "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
-      (* WE SHOULD FAIL (or return None, None *)
-      Some (CicUniv.empty_ugraph, []), None
+      None, None
   in
   obj, ugraph_and_univlist
  with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
@@ -426,41 +350,26 @@ let find_or_add_to_unchecked uri =
 (*                                                              *)
 (* the replacement ugraph must be the one returned by the       *)
 (* typechecker, restricted with the CicUnivUtils.clean_and_fill *)
-let set_type_checking_info ?(replace_ugraph_and_univlist=None) uri =
-(*
-  if not (Cache.can_be_cooked uri) && replace_ugraph <> None then begin
-    debug_print (lazy (
-      "?replace_ugraph must be None if you are not committing an "^
-      "object that has a universe graph associated "^
-      "(can happen only in the fase of universes graphs generation)."));
-    assert false
-  else
-*)
-  match Cache.can_be_cooked uri, replace_ugraph_and_univlist with
-  | true, Some _
-  | false, None ->
-      debug_print (lazy (
-        "?replace_ugraph must be (Some ugraph) when committing an object that "^
-        "has no associated universe graph. If this is in make_univ phase you "^
-        "should drop this exception and let univ_make commit thi object with "^
-        "proper arguments"));
-      assert false
-  | _ ->
-      (match replace_ugraph_and_univlist with 
-      | None -> ()
-      | Some g_and_l -> Cache.hack_univ uri g_and_l);
-      Cache.frozen_to_cooked uri
+let set_type_checking_info uri (o,ug,ul) =
+  if not (Cache.can_be_cooked uri) then assert false
+  else 
+    Cache.frozen_to_cooked ~uri o ug ul
 ;;
 
 (* fetch, unfreeze and commit an uri to the cacheOfCookedObjects and
  * return the object,ugraph
  *)
 let add_trusted_uri_to_cache uri = 
-  let _ = find_or_add_to_unchecked uri in
+  let o,u_and_ul = find_or_add_to_unchecked uri in
   Cache.unchecked_to_frozen uri;
-  set_type_checking_info uri;
-  try
-    Cache.find_cooked uri
+  let u,ul = 
+    match u_and_ul with
+    (* for backward compat with Coq *)
+    | None -> CicUniv.empty_ugraph, []
+    | Some (ug,ul) -> ug, ul
+  in
+  set_type_checking_info uri (o,u,ul);
+  try Cache.find_cooked uri
   with Not_found -> assert false 
 ;;
 
@@ -487,20 +396,6 @@ let get_cooked_obj ?trust base_ugraph uri =
   let o,g,_ = get_cooked_obj_with_univlist ?trust base_ugraph uri in
   o,g
       
-(* This has not the old semantic :( but is what the name suggests
- * 
- *   let is_type_checked ?(trust=true) uri =
- *     try 
- *       let _ = Cache.find_cooked uri in
- *         true
- *     with
- *       Not_found ->
- *         trust && trust_obj uri
- *   ;;
- *
- * as the get_cooked_obj but returns a type_checked_obj
- *   
- *)
 let is_type_checked ?(trust=true) base_ugraph uri =
   try 
     let o,u,l = Cache.find_cooked uri in
@@ -512,9 +407,9 @@ let is_type_checked ?(trust=true) base_ugraph uri =
       let o,u,l = add_trusted_uri_to_cache uri in
         CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
     else
-      let o,u,_ = find_or_add_to_unchecked uri in
+      let o,u_and_ul = find_or_add_to_unchecked uri in
       Cache.unchecked_to_frozen uri;
-        UncheckedObj o
+      UncheckedObj (o,u_and_ul)
 ;;
 
 (* as the get cooked, but if not present the object is only fetched,
@@ -523,12 +418,14 @@ let is_type_checked ?(trust=true) base_ugraph uri =
 let get_obj base_ugraph uri =
   try
     (* the object should be in the cacheOfCookedObjects *)
-    let o,u,l = Cache.find_cooked uri in
-      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
+    let o,u,_ = Cache.find_cooked uri in
+    o,CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)
   with Not_found ->
     (* this should be an error case, but if we trust the uri... *)
-      let o,u,l = find_or_add_to_unchecked uri in
-        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
+      let o,u_and_l = find_or_add_to_unchecked uri in
+      match u_and_l with
+      | None -> o, base_ugraph
+      | Some (ug,_) -> o,CicUniv.merge_ugraphs ~base_ugraph ~increment:(ug,uri)
 ;; 
 
 let in_cache uri =
index e449ade4a83e4cceb6758d57bc26c03cd39ea813..0979d62d27599a9a42e1c209f6c1fdfcedc07b69 100644 (file)
@@ -47,18 +47,9 @@ val get_obj :
     Cic.obj * CicUniv.universe_graph
 
 type type_checked_obj =
-   CheckedObj of (Cic.obj * CicUniv.universe_graph)    (* cooked obj *)
- | UncheckedObj of Cic.obj  (* uncooked obj *)
+ | CheckedObj of (Cic.obj * CicUniv.universe_graph)    
+ | UncheckedObj of Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
 
-(*
- * I think this should be the real semantic:
- * 
- * val is_type_checked: 
- *  ?trust:bool -> UriManager.uri -> bool
- *
- *  but the old semantic is similar to get_cooked_obj, but 
- *  returns an unchecked object intead of a Not_found
- *)
 val is_type_checked : 
   ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->  
     type_checked_obj
@@ -68,18 +59,9 @@ val is_type_checked :
 (* The object whose uri is uri is unfreezed and won't be type-checked *)
 (* again in the future (is_type_checked will return true)             *)
 (*                                                                    *)
-(* Since the universes are not exported directly, but generated       *)
-(* typecheking the library, we can't find them in the library as we   *)
-(* do for the types. This means that when we commit uris during       *)
-(* univ generation we can't associate the uri with the universe graph *)
-(* we find in the library, we have to calculate it and then inject it *)
-(* in the cacke. This is an orrible backdoor used by univ_maker.      *)
-(* see the .ml file for some reassuring invariants                    *)
-(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
-val set_type_checking_info : 
-  ?replace_ugraph_and_univlist:
-    ((CicUniv.universe_graph * CicUniv.universe list) option) -> 
-    UriManager.uri -> unit
+(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker       *)
+val set_type_checking_info : UriManager.uri -> 
+  (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit
 
 (* this function is called by CicTypeChecker.typecheck_obj to add to the *)
 (* environment a new well typed object that is not yet in the library    *)
index 9336cb84ab3c6e8af65624525867ee6f1b9035fc..afa8a774f53c8faab3d1b7941eabd76794105c35 100644 (file)
@@ -54,6 +54,21 @@ let rec split l n =
       raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
 ;;
 
+(* XXX: bug *)
+let ugraph_convertibility ug1 ug2 ul2 = true;;
+
+let check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj =
+ match unchecked_ugraph with
+ | Some (ug,ul) ->
+     if not (ugraph_convertibility inferred_ugraph ug ul) then
+       raise (TypeCheckerFailure (lazy 
+         ("inferred univ graph not equal with declared ugraph")))
+     else 
+      ug,ul,obj
+ | None -> 
+     CicUnivUtils.clean_and_fill uri obj inferred_ugraph
+;;
+
 let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri number_of_types context =
  let rec aux k t =
   let module C = Cic in
@@ -133,67 +148,56 @@ let rec type_of_constant ~logger uri ugraph =
  let cobj,ugraph =
    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
        logger#log (`Start_type_checking uri) ;
        (* let's typecheck the uncooked obj *)
-
-(****************************************************************
-  TASSI: FIXME qui e' inutile ricordarselo, 
-  tanto poi lo richiediamo alla cache che da quello su disco
-*****************************************************************) 
-
-       let ugraph_dust = 
-         (match uobj with
+       let inferred_ugraph = 
+         match uobj with
            C.Constant (_,Some te,ty,_,_) ->
            let _,ugraph = type_of ~logger ty ugraph in
-           let type_of_te,ugraph' = type_of ~logger te ugraph in
-              let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
-              if not b' then
+           let type_of_te,ugraph = type_of ~logger te ugraph in
+              let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
+              if not b then
                raise (TypeCheckerFailure (lazy (sprintf
                 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
                 (CicPp.ppterm ty))))
               else
-                ugraph'
+                ugraph
          | C.Constant (_,None,ty,_,_) ->
            (* only to check that ty is well-typed *)
-           let _,ugraph' = type_of ~logger ty ugraph in 
-           ugraph'
+           let _,ugraph = type_of ~logger ty ugraph in 
+           ugraph
          | C.CurrentProof (_,conjs,te,ty,_,_) ->
-             let _,ugraph1 =
+             let _,ugraph =
               List.fold_left
                (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
-                 let _,ugraph' = 
+                 let _,ugraph = 
                   type_of_aux' ~logger metasenv context ty ugraph 
                 in
-                 (metasenv @ [conj],ugraph')
+                 (metasenv @ [conj],ugraph)
                ) ([],ugraph) conjs
              in
-              let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
-               let type_of_te,ugraph3 = 
-                type_of_aux' ~logger conjs [] te ugraph2 
-              in
-               let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in
+             let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
+             let type_of_te,ugraph = type_of_aux' ~logger conjs [] te ugraph in
+             let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
                if not b then
                  raise (TypeCheckerFailure (lazy (sprintf
                   "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
                   (U.string_of_uri uri) (CicPp.ppterm type_of_te)
                   (CicPp.ppterm ty))))
                else 
-                 ugraph4
+                 ugraph
          | _ ->
              raise
-              (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri))))
+              (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
        in 
-        try
-          CicEnvironment.set_type_checking_info uri;
-          logger#log (`Type_checking_completed uri) ;
-          match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-               CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-             | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
-        with Invalid_argument s ->
-          (*debug_print (lazy s);*)
-          uobj,ugraph_dust       
+       let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+       CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
+       logger#log (`Type_checking_completed uri) ;
+       match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+           CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
   in
    match cobj,ugraph with
       (C.Constant (_,_,ty,_,_)),g -> ty,g
@@ -208,33 +212,29 @@ and type_of_variable ~logger uri ugraph =
   (* 0 because a variable is never cooked => no partial cooking at one level *)
   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
      CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
-   | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
+   | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph) ->
       logger#log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
-      let _,ugraph1 = type_of ~logger ty ugraph in
-      let ugraph2 = 
-       (match bo with
+      let _,ugraph = type_of ~logger ty ugraph in
+      let inferred_ugraph = 
+       match bo with
            None -> ugraph
          | Some bo ->
-            let ty_bo,ugraph' = type_of ~logger bo ugraph1 in
-             let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in
+            let ty_bo,ugraph = type_of ~logger bo ugraph in
+             let b,ugraph = R.are_convertible [] ty_bo ty ugraph in
              if not b then
               raise (TypeCheckerFailure
                 (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
             else
-              ugraph'') 
+              ugraph 
       in
-       (try
-          CicEnvironment.set_type_checking_info uri ;
-          logger#log (`Type_checking_completed uri) ;
-          match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-               CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> 
-                ty,ugraph'
-            | CicEnvironment.CheckedObj _ 
-             | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
-         with Invalid_argument s ->
-           (*debug_print (lazy s);*)
-           ty,ugraph2)
+       let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+       CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
+       logger#log (`Type_checking_completed uri) ;
+       (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+           CicEnvironment.CheckedObj((C.Variable(_,_,ty,_,_)),ugraph)->ty,ugraph
+         | CicEnvironment.CheckedObj _ 
+         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError)
    |  _ ->
        raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
 
@@ -602,23 +602,16 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
   let cobj,ugraph1 =
    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-     | CicEnvironment.UncheckedObj uobj ->
+     | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
         logger#log (`Start_type_checking uri) ;
-        let ugraph1_dust = 
-          check_mutual_inductive_defs ~logger uri uobj ugraph 
-        in
-          (* TASSI: FIXME: check ugraph1 == ugraph ritornato da env *)
-          try 
-            CicEnvironment.set_type_checking_info uri ;
-            logger#log (`Type_checking_completed uri) ;
-            (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-                 CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
-               | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
-            )
-          with
-              Invalid_argument s ->
-                (*debug_print (lazy s);*)
-                uobj,ugraph1_dust
+        let inferred_ugraph = check_mutual_inductive_defs ~logger uri uobj ugraph in
+         let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+        CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
+        logger#log (`Type_checking_completed uri) ;
+        (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+             CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
+           | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
+        )
   in
     match cobj with
        C.InductiveDefinition (dl,_,_,_) ->
@@ -635,25 +628,20 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
   let cobj,ugraph1 =
     match CicEnvironment.is_type_checked ~trust:true ugraph uri with
        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-      | CicEnvironment.UncheckedObj uobj ->
+      | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
          logger#log (`Start_type_checking uri) ;
-         let ugraph1_dust = 
+         let inferred_ugraph = 
            check_mutual_inductive_defs ~logger uri uobj ugraph 
          in
-           (* check ugraph1 validity ??? == ugraph' *)
-           try
-             CicEnvironment.set_type_checking_info uri ;
-             logger#log (`Type_checking_completed uri) ;
-             (match 
-                 CicEnvironment.is_type_checked ~trust:false ugraph uri 
-               with
+          let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+         CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
+         logger#log (`Type_checking_completed uri) ;
+         (match 
+             CicEnvironment.is_type_checked ~trust:false ugraph uri 
+           with
                 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' 
               | CicEnvironment.UncheckedObj _ -> 
                       raise CicEnvironmentError)
-           with
-               Invalid_argument s ->
-                 (*debug_print (lazy s);*)
-                 uobj,ugraph1_dust
   in
     match cobj with
        C.InductiveDefinition (dl,_,_,_) ->
@@ -2052,103 +2040,92 @@ in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res
 *)
 ;;
 
-let typecheck_obj0 ~logger uri ugraph =
+let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) =
  let module C = Cic in
-  function
-     C.Constant (_,Some te,ty,_,_) ->
-      let _,ugraph = type_of ~logger ty ugraph in
-      let ty_te,ugraph = type_of ~logger te ugraph in
-      let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
-       if not b then
-         raise (TypeCheckerFailure
-          (lazy
-            ("the type of the body is not the one expected:\n" ^
-             CicPp.ppterm ty_te ^ "\nvs\n" ^
-             CicPp.ppterm ty)))
-       else
-        ugraph
-   | C.Constant (_,None,ty,_,_) ->
-      (* only to check that ty is well-typed *)
-      let _,ugraph = type_of ~logger ty ugraph in
-       ugraph
-   | C.CurrentProof (_,conjs,te,ty,_,_) ->
-      (* this block is broken since the metasenv should 
-       * be topologically sorted before typing metas *)
-      ignore(assert false);
-      let _,ugraph =
-       List.fold_left
-        (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
-          let _,ugraph = 
-           type_of_aux' ~logger metasenv context ty ugraph 
-          in
-           metasenv @ [conj],ugraph
-        ) ([],ugraph) conjs
-      in
-       let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
-       let type_of_te,ugraph = 
-        type_of_aux' ~logger conjs [] te ugraph
-       in
-       let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
-        if not b then
-          raise (TypeCheckerFailure (lazy (sprintf
-           "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
-           (CicPp.ppterm type_of_te) (CicPp.ppterm ty))))
-        else
+ let ugraph = CicUniv.empty_ugraph in
+ let inferred_ugraph =
+   match obj with
+    | C.Constant (_,Some te,ty,_,_) ->
+        let _,ugraph = type_of ~logger ty ugraph in
+        let ty_te,ugraph = type_of ~logger te ugraph in
+        let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
+         if not b then
+           raise (TypeCheckerFailure
+            (lazy
+              ("the type of the body is not the one expected:\n" ^
+               CicPp.ppterm ty_te ^ "\nvs\n" ^
+               CicPp.ppterm ty)))
+         else
+          ugraph
+     | C.Constant (_,None,ty,_,_) ->
+        (* only to check that ty is well-typed *)
+        let _,ugraph = type_of ~logger ty ugraph in
          ugraph
-   | C.Variable (_,bo,ty,_,_) ->
-      (* only to check that ty is well-typed *)
-      let _,ugraph = type_of ~logger ty ugraph in
-       (match bo with
-           None -> ugraph
-         | Some bo ->
-            let ty_bo,ugraph = type_of ~logger bo ugraph in
-           let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
-             if not b then
-              raise (TypeCheckerFailure
-               (lazy "the body is not the one expected"))
-             else
-              ugraph
-            )
-   | (C.InductiveDefinition _ as obj) ->
-      check_mutual_inductive_defs ~logger uri obj ugraph
+     | C.CurrentProof (_,conjs,te,ty,_,_) ->
+        (* this block is broken since the metasenv should 
+         * be topologically sorted before typing metas *)
+        ignore(assert false);
+        let _,ugraph =
+         List.fold_left
+          (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
+            let _,ugraph = 
+             type_of_aux' ~logger metasenv context ty ugraph 
+            in
+             metasenv @ [conj],ugraph
+          ) ([],ugraph) conjs
+        in
+         let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
+         let type_of_te,ugraph = 
+          type_of_aux' ~logger conjs [] te ugraph
+         in
+         let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
+          if not b then
+            raise (TypeCheckerFailure (lazy (sprintf
+             "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
+             (CicPp.ppterm type_of_te) (CicPp.ppterm ty))))
+          else
+           ugraph
+     | C.Variable (_,bo,ty,_,_) ->
+        (* only to check that ty is well-typed *)
+        let _,ugraph = type_of ~logger ty ugraph in
+         (match bo with
+             None -> ugraph
+           | Some bo ->
+              let ty_bo,ugraph = type_of ~logger bo ugraph in
+           let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
+               if not b then
+                raise (TypeCheckerFailure
+                 (lazy "the body is not the one expected"))
+               else
+                ugraph
+              )
+     | (C.InductiveDefinition _ as obj) ->
+        check_mutual_inductive_defs ~logger uri obj ugraph
+ in
+   check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj
+;;
 
 let typecheck uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
  let logger = new CicLogger.logger in
-   (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
    match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
-     CicEnvironment.CheckedObj (cobj,ugraph') -> 
-       (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*)
-       cobj,ugraph'
-   | CicEnvironment.UncheckedObj uobj ->
+   | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+   | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
       (* let's typecheck the uncooked object *)
       logger#log (`Start_type_checking uri) ;
-      (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *)
-      let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
-       try
-         CicEnvironment.set_type_checking_info uri;
-         logger#log (`Type_checking_completed uri);
-         match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-             CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-           | _ -> raise CicEnvironmentError
-       with
-           (*
-             this is raised if set_type_checking_info is called on an object
-             that has no associated universe file. If we are in univ_maker 
-             phase this is OK since univ_maker will properly commit the 
-             object.
-           *)
-           Invalid_argument s -> 
-             (*debug_print (lazy s);*)
-             uobj,ugraph
+      let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
+      CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
+      logger#log (`Type_checking_completed uri);
+      match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+      | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+      | _ -> raise CicEnvironmentError
 ;;
 
 let typecheck_obj ~logger uri obj =
- let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in
-  CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
+ let ugraph,univlist,obj = typecheck_obj0 ~logger uri (obj,None) in
+ CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
 
 (** wrappers which instantiate fresh loggers *)