From d120acefa62d997341a84ec54cb1532e223dd661 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 21 Apr 2008 09:19:23 +0000 Subject: [PATCH] fix universe handling, newly encountered objects are typed in an empty ugraph that after the cleanup phase is committed into the cic_environement and merged with the current one. minor reformatting of sources and some more for_all --- .../cic_proof_checking/cicTypeChecker.ml | 75 +++++++++++-------- 1 file changed, 42 insertions(+), 33 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index bcdb340bd..44cf6d24a 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -141,12 +141,12 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri n exception CicEnvironmentError;; -let rec type_of_constant ~logger uri (ugraph as orig_ugraph) = +let rec type_of_constant ~logger uri orig_ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj,ugraph = - match CicEnvironment.is_type_checked ~trust:true ugraph uri with + match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> logger#log (`Start_type_checking uri) ; @@ -154,7 +154,7 @@ let rec type_of_constant ~logger uri (ugraph as orig_ugraph) = let inferred_ugraph = match uobj with C.Constant (_,Some te,ty,_,_) -> - let _,ugraph = type_of ~logger ty ugraph in + let _,ugraph = type_of ~logger ty CicUniv.empty_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 @@ -166,17 +166,17 @@ let rec type_of_constant ~logger uri (ugraph as orig_ugraph) = ugraph | C.Constant (_,None,ty,_,_) -> (* only to check that ty is well-typed *) - let _,ugraph = type_of ~logger ty ugraph in + let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in ugraph | C.CurrentProof (_,conjs,te,ty,_,_) -> let _,ugraph = List.fold_left (fun (metasenv,ugraph) ((_,context,ty) as conj) -> let _,ugraph = - type_of_aux' ~logger metasenv context ty ugraph + type_of_aux' ~logger metasenv context ty ugraph in (metasenv @ [conj],ugraph) - ) ([],ugraph) conjs + ) ([],CicUniv.empty_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 @@ -205,17 +205,19 @@ let rec type_of_constant ~logger uri (ugraph as orig_ugraph) = | _ -> raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri))) -and type_of_variable ~logger uri (ugraph as orig_ugraph) = +and type_of_variable ~logger uri orig_ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in (* 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,_,_) as uobj, unchecked_ugraph) -> + match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with + | CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph' + | 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 _,ugraph = type_of ~logger ty ugraph in + let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in let inferred_ugraph = match bo with None -> ugraph @@ -228,7 +230,9 @@ and type_of_variable ~logger uri (ugraph as orig_ugraph) = else ugraph in - let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj 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 orig_ugraph uri with @@ -236,7 +240,8 @@ and type_of_variable ~logger uri (ugraph as orig_ugraph) = | CicEnvironment.CheckedObj _ | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError) | _ -> - raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri))) + raise (TypeCheckerFailure (lazy + ("Unknown variable:" ^ U.string_of_uri uri))) and does_not_occur ?(subst=[]) context n nn te = let module C = Cic in @@ -264,14 +269,15 @@ and does_not_occur ?(subst=[]) context n nn te = with CicUtil.Subst_not_found _ -> true) | C.Cast (te,ty) -> - does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty + does_not_occur ~subst context n nn te && + does_not_occur ~subst context n nn ty | C.Prod (name,so,dest) -> does_not_occur ~subst context n nn so && does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest | C.Lambda (name,so,dest) -> does_not_occur ~subst context n nn so && - does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) + does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) dest | C.LetIn (name,so,ty,dest) -> does_not_occur ~subst context n nn so && @@ -279,16 +285,17 @@ and does_not_occur ?(subst=[]) context n nn te = does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context) (n + 1) (nn + 1) dest | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true + List.for_all (does_not_occur ~subst context n nn) l | C.Var (_,exp_named_subst) | C.Const (_,exp_named_subst) | C.MutInd (_,_,exp_named_subst) | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x) - exp_named_subst true + List.for_all (fun (_,x) -> does_not_occur ~subst context n nn x) + exp_named_subst | C.MutCase (_,_,out,te,pl) -> - does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te && - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true + does_not_occur ~subst context n nn out && + does_not_occur ~subst context n nn te && + List.for_all (does_not_occur ~subst context n nn) pl | C.Fix (_,fl) -> let len = List.length fl in let n_plus_len = n + len in @@ -595,16 +602,18 @@ and check_mutual_inductive_defs uri obj ugraph = lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) -and type_of_mutual_inductive_defs ~logger uri i (ugraph as orig_ugraph) = +and type_of_mutual_inductive_defs ~logger uri i orig_ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj,ugraph1 = - match CicEnvironment.is_type_checked ~trust:true ugraph uri with + match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> logger#log (`Start_type_checking uri) ; - let inferred_ugraph = check_mutual_inductive_defs ~logger uri uobj ugraph in + let inferred_ugraph = + check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_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) ; @@ -613,25 +622,25 @@ and type_of_mutual_inductive_defs ~logger uri i (ugraph as orig_ugraph) = | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError ) in - match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity,ugraph1 - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri))) + match cobj with + | C.InductiveDefinition (dl,_,_,_) -> + let (_,_,arity,_) = List.nth dl i in + arity,ugraph1 + | _ -> + raise (TypeCheckerFailure + (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri))) -and type_of_mutual_inductive_constr ~logger uri i j (ugraph as orig_ugraph) = +and type_of_mutual_inductive_constr ~logger uri i j orig_ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj,ugraph1 = - match CicEnvironment.is_type_checked ~trust:true ugraph uri with + match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> logger#log (`Start_type_checking uri) ; let inferred_ugraph = - check_mutual_inductive_defs ~logger uri uobj ugraph + check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_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); -- 2.39.2