* ************************************************************************** *)
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;;
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
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
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 =
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) =
| 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)
(* *)
(* 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
;;
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
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,
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 =
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
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
(* 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)))
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,_,_,_) ->
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,_,_,_) ->
*)
;;
-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 *)
projects / helm.git / commitdiff