From afcc11c0cf6751122dc3907f130b819851099a49 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 18 Apr 2008 15:30:40 +0000 Subject: [PATCH 1/1] cicEnvironment refactoring with sound view of Coq`s univ-less terms --- .../cic_acic/doubleTypeInference.ml | 8 +- .../cic_proof_checking/cicEnvironment.ml | 173 ++-------- .../cic_proof_checking/cicEnvironment.mli | 28 +- .../cic_proof_checking/cicTypeChecker.ml | 305 ++++++++---------- 4 files changed, 185 insertions(+), 329 deletions(-) diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index 4910275ea..d54d0fbe4 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -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 diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml index ec12c8d01..fde76a60b 100644 --- a/helm/software/components/cic_proof_checking/cicEnvironment.ml +++ b/helm/software/components/cic_proof_checking/cicEnvironment.ml @@ -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 = diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.mli b/helm/software/components/cic_proof_checking/cicEnvironment.mli index e449ade4a..0979d62d2 100644 --- a/helm/software/components/cic_proof_checking/cicEnvironment.mli +++ b/helm/software/components/cic_proof_checking/cicEnvironment.mli @@ -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 *) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 9336cb84a..afa8a774f 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -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 *) -- 2.39.2