X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=a5e745af3592ac08dd47fb3f6dc59ebba80ceb1f;hb=7fa28badba2091f1e3d207f13743a1f68d6bf1f3;hp=9336cb84ab3c6e8af65624525867ee6f1b9035fc;hpb=6ebe894ff0fee5d99bad615ce053128292657dee;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 9336cb84a..a5e745af3 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 @@ -126,74 +141,63 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri n exception CicEnvironmentError;; -let rec type_of_constant ~logger uri 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 -> + | 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 _,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 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 CicUniv.empty_ugraph in + ugraph | C.CurrentProof (_,conjs,te,ty,_,_) -> - let _,ugraph1 = + let _,ugraph = List.fold_left (fun (metasenv,ugraph) ((_,context,ty) as conj) -> - let _,ugraph' = - type_of_aux' ~logger metasenv context ty ugraph + let _,ugraph = + type_of_aux' ~logger metasenv context ty ugraph in - (metasenv @ [conj],ugraph') - ) ([],ugraph) conjs + (metasenv @ [conj],ugraph) + ) ([],CicUniv.empty_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 orig_ugraph uri with + CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError in match cobj,ugraph with (C.Constant (_,_,ty,_,_)),g -> ty,g @@ -201,42 +205,43 @@ let rec type_of_constant ~logger uri ugraph = | _ -> raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri))) -and type_of_variable ~logger uri 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,_,_)) -> + 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 _,ugraph1 = type_of ~logger ty ugraph in - let ugraph2 = - (match bo with + let _,ugraph = type_of ~logger ty CicUniv.empty_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 orig_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))) + 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,65 +602,55 @@ 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 = +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 -> + | 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 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) ; + (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with + CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,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 = +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 -> + | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> logger#log (`Start_type_checking uri) ; - let ugraph1_dust = - check_mutual_inductive_defs ~logger uri uobj ugraph + let inferred_ugraph = + check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_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 orig_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,_,_,_) -> @@ -749,7 +746,7 @@ and specialize_inductive_type ~logger ~subst ~metasenv context t = cl in name, isind, arity, cl) - tl + tl, paramsno | _ -> assert false) | _ -> assert false @@ -776,11 +773,15 @@ and check_is_really_smaller_arg | C.MutCase (uri,i,outtype,term,pl) -> (match term with | C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x -> - let tys = + let tys,_ = specialize_inductive_type ~logger ~subst ~metasenv context term in - let tys_ctx = - List.map (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys + let tys_ctx,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ([],0) tys in let _,isinductive,_,cl = List.nth tys i in if not isinductive then @@ -890,12 +891,15 @@ and guarded_by_destructors List.for_all (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) tl && - let tys = + let tys,_ = specialize_inductive_type ~logger ~subst ~metasenv context t in - let tys_ctx = - List.map - (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys + let tys_ctx,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ([],0) tys in let _,isinductive,_,cl = List.nth tys i in if not isinductive then @@ -995,224 +999,112 @@ and guarded_by_destructors (* the boolean h means already protected *) (* args is the list of arguments the type of the constructor that may be *) (* found in head position must be applied to. *) -and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = +and guarded_by_constructors ~logger ~subst ~metasenv indURI = let module C = Cic in - (*CSC: There is a lot of code replication between the cases X and *) - (*CSC: (C.Appl X tl). Maybe it will be better to define a function *) - (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *) + let rec aux context n nn h te = match CicReduction.whd ~subst context te with - C.Rel m when m > n && m <= nn -> h - | C.Rel _ -> true - | C.Meta _ + | C.Rel m when m > n && m <= nn -> h + | C.Rel _ + | C.Meta _ -> true | C.Sort _ | C.Implicit _ | C.Cast _ | C.Prod _ - | C.LetIn _ -> - (* the term has just been type-checked *) - raise (AssertFailure (lazy "17")) + | C.MutInd _ + | C.LetIn _ -> raise (AssertFailure (lazy "17")) | C.Lambda (name,so,de) -> does_not_occur ~subst context n nn so && - guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context) - (n + 1) (nn + 1) h de args coInductiveTypeURI + aux ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) h de | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> - h && - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true - | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) -> - let consty = - let obj,_ = - try - CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri - with Not_found -> assert false - in - match obj with - C.InductiveDefinition (itl,_,_,_) -> - let (_,_,_,cl) = List.nth itl i in - let (_,cons) = List.nth cl (j - 1) in - CicSubstitution.subst_vars exp_named_subst cons - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) + h && List.for_all (does_not_occur ~subst context n nn) tl + | C.MutConstruct (_,_,_,exp_named_subst) -> + List.for_all + (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst + | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) as t -> + List.for_all + (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst && + let consty, len_tys, tys_ctx, paramsno = + let tys, paramsno = + specialize_inductive_type ~logger ~subst ~metasenv context t in + let _,_,_,cl = List.nth tys i in + let _,ty = List.nth cl (j-1) in + ty, List.length tys, + fst(List.fold_left + (fun (types,len) (n,_,ty,_) -> + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) + ([],0) tys), paramsno in - let rec analyse_branch context ty te = - match CicReduction.whd ~subst context ty with - C.Meta _ -> raise (AssertFailure (lazy "34")) - | C.Rel _ - | C.Var _ - | C.Sort _ -> - does_not_occur ~subst context n nn te - | C.Implicit _ - | C.Cast _ -> - raise (AssertFailure (lazy "24"))(* due to type-checking *) - | C.Prod (name,so,de) -> - analyse_branch ((Some (name,(C.Decl so)))::context) de te - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "25"))(* due to type-checking *) - | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI -> - guarded_by_constructors ~subst context n nn true te [] - coInductiveTypeURI - | C.Appl ((C.MutInd (uri,_,_))::_) -> - guarded_by_constructors ~subst context n nn true te tl - coInductiveTypeURI - | C.Appl _ -> - does_not_occur ~subst context n nn te - | C.Const _ -> raise (AssertFailure (lazy "26")) - | C.MutInd (uri,_,_) when uri == coInductiveTypeURI -> - guarded_by_constructors ~subst context n nn true te [] - coInductiveTypeURI - | C.MutInd _ -> - does_not_occur ~subst context n nn te - | C.MutConstruct _ -> raise (AssertFailure (lazy "27")) - (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) - (*CSC: in head position. *) - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> - raise (AssertFailure (lazy "28"))(* due to type-checking *) - in - let rec analyse_instantiated_type context ty l = - match CicReduction.whd ~subst context ty with - C.Rel _ - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *) - | C.Prod (name,so,de) -> - begin - match l with - [] -> true - | he::tl -> - analyse_branch context so he && - analyse_instantiated_type - ((Some (name,(C.Decl so)))::context) de tl - end - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "30"))(* due to type-checking *) - | C.Appl _ -> - List.fold_left - (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.Const _ -> raise (AssertFailure (lazy "31")) - | C.MutInd _ -> - List.fold_left - (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.MutConstruct _ -> raise (AssertFailure (lazy "32")) - (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) - (*CSC: in head position. *) - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> - raise (AssertFailure (lazy "33"))(* due to type-checking *) - in - let rec instantiate_type args consty = - function - [] -> true - | tlhe::tltl as l -> - let consty' = CicReduction.whd ~subst context consty in - match args with - he::tl -> - begin - match consty' with - C.Prod (_,_,de) -> - let instantiated_de = CicSubstitution.subst he de in - (*CSC: siamo sicuri che non sia troppo forte? *) - does_not_occur ~subst context n nn tlhe & - instantiate_type tl instantiated_de tltl - | _ -> - (*CSC:We do not consider backbones with a MutCase, a *) - (*CSC:FixPoint, a CoFixPoint and so on in head position.*) - raise (AssertFailure (lazy "23")) - end - | [] -> analyse_instantiated_type context consty' l - (* These are all the other cases *) + let rec_params = + let c = + debrujin_constructor ~check_exp_named_subst:false + indURI len_tys context consty in - instantiate_type args consty tl - | C.Appl ((C.CoFix (_,fl))::tl) -> - List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl && - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len - h bo args coInductiveTypeURI - ) fl true - | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) -> - List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl && - does_not_occur ~subst context n nn out && - does_not_occur ~subst context n nn te && - List.fold_right - (fun x i -> - i && - guarded_by_constructors ~subst context n nn h x args - coInductiveTypeURI - ) pl true - | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true - | C.Var (_,exp_named_subst) - | C.Const (_,exp_named_subst) -> - List.fold_right - (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true - | C.MutInd _ -> assert false - | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right - (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true - | C.MutCase (_,_,out,te,pl) -> + let len_ctx = List.length context in + recursive_args (context@tys_ctx) len_ctx (len_ctx+len_tys) c + in + let rec analyse_instantiated_type rec_spec args = + match rec_spec, args with + | h::rec_spec, he::args -> + aux context n nn h he && + analyse_instantiated_type rec_spec args + | _,[] -> true + | _ -> raise (AssertFailure (lazy + ("Too many args for constructor: " ^ String.concat " " + (List.map (fun x-> CicPp.ppterm x) args)))) + in + let left, args = HExtlib.split_nth paramsno tl in + List.for_all (does_not_occur ~subst context n nn) left && + analyse_instantiated_type rec_params args + | C.Appl ((C.MutCase (_,_,out,te,pl))::_) + | C.MutCase (_,_,out,te,pl) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in + List.for_all (does_not_occur ~subst context n nn) tl && does_not_occur ~subst context n nn out && - does_not_occur ~subst context n nn te && - List.fold_right - (fun x i -> - i && - guarded_by_constructors ~subst context n nn h x args - coInductiveTypeURI - ) pl true - | C.Fix (_,fl) -> + does_not_occur ~subst context n nn te && + List.for_all (aux context n nn h ) pl + | C.Fix (_,fl) + | C.Appl (C.Fix (_,fl)::_) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in let len = List.length fl in let n_plus_len = n + len and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) and tys,_ = List.fold_left (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in - List.fold_right - (fun (_,_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo - ) fl true - | C.CoFix (_,fl) -> - let len = List.length fl in + List.for_all (does_not_occur ~subst context n nn) tl && + List.for_all + (fun (_,_,ty,bo) -> + does_not_occur ~subst context n nn ty && + aux (tys@context) n_plus_len nn_plus_len h bo) + fl + | C.Appl ((C.CoFix (_,fl))::_) + | C.CoFix (_,fl) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in + let len = List.length fl in let n_plus_len = n + len and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) and tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len - h bo - args coInductiveTypeURI - ) fl true + List.for_all (does_not_occur ~subst context n nn) tl && + List.for_all + (fun (_,ty,bo) -> + does_not_occur ~subst context n nn ty && + aux (tys@context) n_plus_len nn_plus_len h bo) + fl + | C.Var _ + | C.Const _ + | C.Appl _ as t -> does_not_occur ~subst context n nn t + in + aux and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i need_dummy ind arity1 arity2 ugraph = @@ -1855,8 +1747,8 @@ end; let's control the guarded by constructors conditions C{f,M} *) - if not (guarded_by_constructors ~subst - (types @ context) 0 len false bo [] uri) then + if not (guarded_by_constructors ~logger ~subst ~metasenv uri + (types @ context) 0 len false bo) then raise (TypeCheckerFailure (lazy "CoFix: not guarded by constructors")) @@ -2052,103 +1944,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 CicUniv.empty_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 *) @@ -2186,10 +2067,10 @@ Deannotate.type_of_aux' := (match el with None -> () | Some (_,Cic.Decl ty) -> - ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph) + ignore (type_of_aux' [] context ty CicUniv.empty_ugraph) | Some (_,Cic.Def (bo,ty)) -> - ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph); - ignore (type_of_aux' [] context bo CicUniv.oblivion_ugraph)); + ignore (type_of_aux' [] context ty CicUniv.empty_ugraph); + ignore (type_of_aux' [] context bo CicUniv.empty_ugraph)); el::context ) context []); - fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);; + fst (type_of_aux' [] context t CicUniv.empty_ugraph);;