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=4a78e324a687b0b2b651892144b5272372c590b0;hpb=3b74f626ef19a7ffccb8264f3230fb5efeb7ec6e;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 4a78e324a..a5e745af3 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -66,7 +66,7 @@ let check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj = else ug,ul,obj | None -> - CicUnivUtils.clean_and_fill uri obj inferred_ugraph + CicUnivUtils.clean_and_fill uri obj inferred_ugraph ;; let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri number_of_types context = @@ -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 = +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 = 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 = 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 @@ -195,7 +195,7 @@ let rec type_of_constant ~logger uri ugraph = 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 + match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError in @@ -205,17 +205,19 @@ 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,_,_) 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,15 +230,18 @@ and type_of_variable ~logger uri 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 ugraph uri with + (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,49 +602,51 @@ 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,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) ; - (match CicEnvironment.is_type_checked ~trust:false ugraph uri with + (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,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); logger#log (`Type_checking_completed uri) ; (match - CicEnvironment.is_type_checked ~trust:false ugraph uri + CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj _ -> @@ -737,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 @@ -764,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 @@ -878,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 @@ -983,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 *) + let rec_params = + let c = + debrujin_constructor ~check_exp_named_subst:false + indURI len_tys context consty 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 *) - 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 = @@ -1843,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")) @@ -2118,7 +2022,7 @@ let typecheck uri = 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 + match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | _ -> raise CicEnvironmentError ;;