From e174574339e22f1d6a518f9b272ad412a0cd7a90 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 25 Oct 2005 11:11:40 +0000 Subject: [PATCH] ~subst fixed everywhere in the type-checker: 1. sometimes it was not passed to functions 2. sometimes it was passed but it was not used/useful/correct 3. sometimes it was not passed recursively --- .../cic_proof_checking/cicTypeChecker.ml | 243 +++++++++--------- 1 file changed, 126 insertions(+), 117 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index b24c5fc8e..007962097 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -232,42 +232,47 @@ and type_of_variable ~logger uri ugraph = | _ -> raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri)) -and does_not_occur context n nn te = +and does_not_occur ?(subst=[]) context n nn te = let module C = Cic in (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *) (*CSC: venga mangiata durante la whd sembra presentare problemi di *) (*CSC: universi *) - match CicReduction.whd context te with + match CicReduction.whd ~subst context te with C.Rel m when m > n && m <= nn -> false | C.Rel _ - | C.Meta _ (* CSC: Are we sure? No recursion?*) | C.Sort _ | C.Implicit _ -> true + | C.Meta (_,l) -> + List.fold_right + (fun x i -> + match x with + None -> i + | Some x -> i && does_not_occur ~subst context n nn x) l true | C.Cast (te,ty) -> - does_not_occur context n nn te && does_not_occur 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 context n nn so && - does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) - 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 context n nn so && - does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) + does_not_occur ~subst context n nn so && + does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest | C.LetIn (name,so,dest) -> - does_not_occur context n nn so && - does_not_occur ((Some (name,(C.Def (so,None))))::context) + does_not_occur ~subst context n nn so && + does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context) (n + 1) (nn + 1) dest | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur context n nn x) l true + 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) | C.MutInd (_,_,exp_named_subst) | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x) + List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true | C.MutCase (_,_,out,te,pl) -> - does_not_occur context n nn out && does_not_occur context n nn te && - List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true + 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 | C.Fix (_,fl) -> let len = List.length fl in let n_plus_len = n + len in @@ -277,8 +282,8 @@ and does_not_occur context n nn te = in List.fold_right (fun (_,_,ty,bo) i -> - i && does_not_occur context n nn ty && - does_not_occur (tys @ context) n_plus_len nn_plus_len bo + 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 @@ -289,8 +294,8 @@ and does_not_occur context n nn te = in List.fold_right (fun (_,ty,bo) i -> - i && does_not_occur context n nn ty && - does_not_occur (tys @ context) n_plus_len nn_plus_len bo + i && does_not_occur ~subst context n nn ty && + does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo ) fl true (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) @@ -304,7 +309,7 @@ and weakly_positive context n nn uri te = let dummy_mutind = C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[]) in - (*CSC mettere in cicSubstitution *) + (*CSC: mettere in cicSubstitution *) let rec subst_inductive_type_with_dummy_mutind = function C.MutInd (uri',0,_) when UriManager.eq uri' uri -> @@ -438,7 +443,7 @@ and strictly_positive context n nn te = ) cl' true | t -> does_not_occur context n nn t -(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) +(* the inductive type indexes are s.t. n < x <= nn *) and are_all_occurrences_positive context uri indparamsno i n nn te = let module C = Cic in match CicReduction.whd context te with @@ -647,7 +652,7 @@ and recursive_args context n nn te = | C.Fix _ | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *) -and get_new_safes ?(subst = []) context p c rl safes n nn x = +and get_new_safes ~subst context p c rl safes n nn x = let module C = Cic in let module U = UriManager in let module R = CicReduction in @@ -678,16 +683,16 @@ and get_new_safes ?(subst = []) context p c rl safes n nn x = (Printf.sprintf "Get New Safes: c=%s ; p=%s" (CicPp.ppterm c) (CicPp.ppterm p))) -and split_prods ?(subst = []) context n te = +and split_prods ~subst context n te = let module C = Cic in let module R = CicReduction in - match (n, R.whd context te) with + match (n, R.whd ~subst context te) with (0, _) -> context,te | (n, C.Prod (name,so,ta)) when n > 0 -> split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta | (_, _) -> raise (AssertFailure "8") -and eat_lambdas ?(subst = []) context n te = +and eat_lambdas ~subst context n te = let module C = Cic in let module R = CicReduction in match (n, R.whd ~subst context te) with @@ -701,12 +706,12 @@ and eat_lambdas ?(subst = []) context n te = raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te))) (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) -and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = +and check_is_really_smaller_arg ~subst context n nn kl x safes te = (*CSC: forse la whd si puo' fare solo quando serve veramente. *) (*CSC: cfr guarded_by_destructors *) let module C = Cic in let module U = UriManager in - match CicReduction.whd context te with + match CicReduction.whd ~subst context te with C.Rel m when List.mem m safes -> true | C.Rel _ -> false | C.Var _ @@ -829,7 +834,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = recursive_args tys 0 len debrujinedte in let (e, safes',n',nn',x',context') = - get_new_safes context p c rl' safes n nn x + get_new_safes ~subst context p c rl' safes n nn x in i && check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e @@ -867,7 +872,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = x_plus_len safes' bo ) fl true -and guarded_by_destructors ?(subst = []) context n nn kl x safes = +and guarded_by_destructors ~subst context n nn kl x safes = let module C = Cic in let module U = UriManager in function @@ -876,7 +881,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = (match List.nth context (n-1) with Some (_,C.Decl _) -> true | Some (_,C.Def (bo,_)) -> - guarded_by_destructors context m nn kl x safes + guarded_by_destructors ~subst context m nn kl x safes (CicSubstitution.lift m bo) | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") ) @@ -884,19 +889,19 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = | C.Sort _ | C.Implicit _ -> true | C.Cast (te,ty) -> - guarded_by_destructors context n nn kl x safes te && - guarded_by_destructors context n nn kl x safes ty + guarded_by_destructors ~subst context n nn kl x safes te && + guarded_by_destructors ~subst context n nn kl x safes ty | C.Prod (name,so,ta) -> - guarded_by_destructors context n nn kl x safes so && - guarded_by_destructors ((Some (name,(C.Decl so)))::context) + guarded_by_destructors ~subst context n nn kl x safes so && + guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Lambda (name,so,ta) -> - guarded_by_destructors context n nn kl x safes so && - guarded_by_destructors ((Some (name,(C.Decl so)))::context) + guarded_by_destructors ~subst context n nn kl x safes so && + guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.LetIn (name,so,ta) -> - guarded_by_destructors context n nn kl x safes so && - guarded_by_destructors ((Some (name,(C.Def (so,None))))::context) + guarded_by_destructors ~subst context n nn kl x safes so && + guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> let k = List.nth kl (m - n - 1) in @@ -904,22 +909,22 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = else List.fold_right (fun param i -> - i && guarded_by_destructors context n nn kl x safes param + i && guarded_by_destructors ~subst context n nn kl x safes param ) tl true && check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k) | C.Appl tl -> List.fold_right - (fun t i -> i && guarded_by_destructors context n nn kl x safes t) + (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t) tl true | C.Var (_,exp_named_subst) | C.Const (_,exp_named_subst) | C.MutInd (_,_,exp_named_subst) | C.MutConstruct (_,_,_,exp_named_subst) -> List.fold_right - (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t) + (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t) exp_named_subst true | C.MutCase (uri,i,outtype,term,pl) -> - (match CicReduction.whd context term with + (match CicReduction.whd ~subst context term with C.Rel m when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in @@ -946,12 +951,12 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = UriManager.string_of_uri uri)) in if not isinductive then - guarded_by_destructors context n nn kl x safes outtype && - guarded_by_destructors context n nn kl x safes term && + guarded_by_destructors ~subst context n nn kl x safes outtype && + guarded_by_destructors ~subst context n nn kl x safes term && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right (fun p i -> - i && guarded_by_destructors context n nn kl x safes p) + i && guarded_by_destructors ~subst context n nn kl x safes p) pl true else let pl_and_cl = @@ -961,16 +966,16 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = Invalid_argument _ -> raise (TypeCheckerFailure "not enough patterns") in - guarded_by_destructors context n nn kl x safes outtype && + guarded_by_destructors ~subst context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right (fun (p,(_,c,brujinedc)) i -> let rl' = recursive_args tys 0 len brujinedc in let (e,safes',n',nn',x',context') = - get_new_safes context p c rl' safes n nn x + get_new_safes ~subst context p c rl' safes n nn x in i && - guarded_by_destructors context' n' nn' kl x' safes' e + guarded_by_destructors ~subst context' n' nn' kl x' safes' e ) pl_and_cl true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = @@ -994,12 +999,12 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = UriManager.string_of_uri uri)) in if not isinductive then - guarded_by_destructors context n nn kl x safes outtype && - guarded_by_destructors context n nn kl x safes term && + guarded_by_destructors ~subst context n nn kl x safes outtype && + guarded_by_destructors ~subst context n nn kl x safes term && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right (fun p i -> - i && guarded_by_destructors context n nn kl x safes p) + i && guarded_by_destructors ~subst context n nn kl x safes p) pl true else let pl_and_cl = @@ -1009,11 +1014,11 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = Invalid_argument _ -> raise (TypeCheckerFailure "not enough patterns") in - guarded_by_destructors context n nn kl x safes outtype && + guarded_by_destructors ~subst context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right (fun t i -> - i && guarded_by_destructors context n nn kl x safes t) + i && guarded_by_destructors ~subst context n nn kl x safes t) tl true && List.fold_right (fun (p,(_,c)) i -> @@ -1022,17 +1027,17 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = recursive_args tys 0 len debrujinedte in let (e, safes',n',nn',x',context') = - get_new_safes context p c rl' safes n nn x + get_new_safes ~subst context p c rl' safes n nn x in i && - guarded_by_destructors context' n' nn' kl x' safes' e + guarded_by_destructors ~subst context' n' nn' kl x' safes' e ) pl_and_cl true | _ -> - guarded_by_destructors context n nn kl x safes outtype && - guarded_by_destructors context n nn kl x safes term && + guarded_by_destructors ~subst context n nn kl x safes outtype && + guarded_by_destructors ~subst context n nn kl x safes term && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right - (fun p i -> i && guarded_by_destructors context n nn kl x safes p) + (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p) pl true ) | C.Fix (_, fl) -> @@ -1044,8 +1049,8 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> - i && guarded_by_destructors context n nn kl x_plus_len safes' ty && - guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl + i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && + guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl x_plus_len safes' bo ) fl true | C.CoFix (_, fl) -> @@ -1058,21 +1063,20 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = List.fold_right (fun (_,ty,bo) i -> i && - guarded_by_destructors context n nn kl x_plus_len safes' ty && - guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl + guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && + guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl x_plus_len safes' bo ) fl true (* 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. *) -(*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *) -and guarded_by_constructors context n nn h te args coInductiveTypeURI = +and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = 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 *) - match CicReduction.whd context te with + match CicReduction.whd ~subst context te with C.Rel m when m > n && m <= nn -> h | C.Rel _ -> true | C.Meta _ @@ -1084,12 +1088,12 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = (* the term has just been type-checked *) raise (AssertFailure "17") | C.Lambda (name,so,de) -> - does_not_occur context n nn so && - guarded_by_constructors ((Some (name,(C.Decl so)))::context) + 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 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> h && - List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true + 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,_ = @@ -1107,12 +1111,12 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = UriManager.string_of_uri uri)) in let rec analyse_branch context ty te = - match CicReduction.whd context ty with + match CicReduction.whd ~subst context ty with C.Meta _ -> raise (AssertFailure "34") | C.Rel _ | C.Var _ | C.Sort _ -> - does_not_occur context n nn te + does_not_occur ~subst context n nn te | C.Implicit _ | C.Cast _ -> raise (AssertFailure "24")(* due to type-checking *) @@ -1123,16 +1127,19 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = raise (AssertFailure "25")(* due to type-checking *) | C.Appl ((C.MutInd (uri,_,_))::_) as ty when uri == coInductiveTypeURI -> - guarded_by_constructors context n nn true te [] coInductiveTypeURI + guarded_by_constructors ~subst context n nn true te [] + coInductiveTypeURI | C.Appl ((C.MutInd (uri,_,_))::_) as ty -> - guarded_by_constructors context n nn true te tl coInductiveTypeURI + guarded_by_constructors ~subst context n nn true te tl + coInductiveTypeURI | C.Appl _ -> - does_not_occur context n nn te + does_not_occur ~subst context n nn te | C.Const _ -> raise (AssertFailure "26") | C.MutInd (uri,_,_) when uri == coInductiveTypeURI -> - guarded_by_constructors context n nn true te [] coInductiveTypeURI + guarded_by_constructors ~subst context n nn true te [] + coInductiveTypeURI | C.MutInd _ -> - does_not_occur context n nn te + does_not_occur ~subst context n nn te | C.MutConstruct _ -> raise (AssertFailure "27") (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) (*CSC: in head position. *) @@ -1142,7 +1149,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = raise (AssertFailure "28")(* due to type-checking *) in let rec analyse_instantiated_type context ty l = - match CicReduction.whd context ty with + match CicReduction.whd ~subst context ty with C.Rel _ | C.Var _ | C.Meta _ @@ -1163,11 +1170,11 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = raise (AssertFailure "30")(* due to type-checking *) | C.Appl _ -> List.fold_left - (fun i x -> i && does_not_occur context n nn x) true l + (fun i x -> i && does_not_occur ~subst context n nn x) true l | C.Const _ -> raise (AssertFailure "31") | C.MutInd _ -> List.fold_left - (fun i x -> i && does_not_occur context n nn x) true l + (fun i x -> i && does_not_occur ~subst context n nn x) true l | C.MutConstruct _ -> raise (AssertFailure "32") (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) (*CSC: in head position. *) @@ -1180,7 +1187,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = function [] -> true | tlhe::tltl as l -> - let consty' = CicReduction.whd context consty in + let consty' = CicReduction.whd ~subst context consty in match args with he::tl -> begin @@ -1188,7 +1195,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = C.Prod (_,_,de) -> let instantiated_de = CicSubstitution.subst he de in (*CSC: siamo sicuri che non sia troppo forte? *) - does_not_occur context n nn tlhe & + does_not_occur ~subst context n nn tlhe & instantiate_type tl instantiated_de tltl | _ -> (*CSC:We do not consider backbones with a MutCase, a *) @@ -1200,7 +1207,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = in instantiate_type args consty tl | C.Appl ((C.CoFix (_,fl))::tl) -> - List.fold_left (fun i x -> i && does_not_occur context n nn x) true 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 @@ -1208,36 +1215,38 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in List.fold_right (fun (_,ty,bo) i -> - i && does_not_occur context n nn ty && - guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo - args coInductiveTypeURI + 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 context n nn x) true tl && - does_not_occur context n nn out && - does_not_occur context n nn te && + 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 context n nn h x args coInductiveTypeURI + 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 context n nn x) l true + 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 context n nn x) exp_named_subst true + (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 context n nn x) exp_named_subst true + (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true | C.MutCase (_,_,out,te,pl) -> - does_not_occur context n nn out && - does_not_occur context n nn te && + 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 context n nn h x args coInductiveTypeURI + guarded_by_constructors ~subst context n nn h x args + coInductiveTypeURI ) pl true | C.Fix (_,fl) -> let len = List.length fl in @@ -1247,8 +1256,8 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in List.fold_right (fun (_,_,ty,bo) i -> - i && does_not_occur context n nn ty && - does_not_occur (tys@context) n_plus_len nn_plus_len bo + 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 @@ -1258,8 +1267,9 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in List.fold_right (fun (_,ty,bo) i -> - i && does_not_occur context n nn ty && - guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo + 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 @@ -1384,10 +1394,10 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i CicReduction.are_convertible ~subst ~metasenv context so ind ugraph | (_,_) -> false,ugraph -and type_of_branch context argsno need_dummy outtype term constype = +and type_of_branch ~subst context argsno need_dummy outtype term constype = let module C = Cic in let module R = CicReduction in - match R.whd context constype with + match R.whd ~subst context constype with C.MutInd (_,_,_) -> if need_dummy then outtype @@ -1406,7 +1416,7 @@ and type_of_branch context argsno need_dummy outtype term constype = C.Appl l -> C.Appl (l@[C.Rel 1]) | t -> C.Appl [t ; C.Rel 1] in - C.Prod (C.Anonymous,so,type_of_branch + C.Prod (C.Anonymous,so,type_of_branch ~subst ((Some (name,(C.Decl so)))::context) argsno need_dummy (CicSubstitution.lift 1 outtype) term' de) | _ -> raise (AssertFailure "20") @@ -1416,7 +1426,7 @@ metavariable is consitent - up to relocation via the relocation list l - with the actual context *) -and check_metasenv_consistency ~logger ?(subst=[]) metasenv context +and check_metasenv_consistency ~logger ~subst metasenv context canonical_context l ugraph = let module C = Cic in @@ -1573,7 +1583,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (* The type of the LetIn is reduced. Much faster than the previous solution. Moreover the inferred type is probably very different from the expected one. - (CicReduction.whd context + (CicReduction.whd ~subst context (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))) *) (* One-step LetIn reduction. Even faster than the previous solution. @@ -1665,7 +1675,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (* let (parameters, arguments, exp_named_subst),ugraph2 = let ty,ugraph2 = type_of_aux context term ugraph1 in - match R.whd context ty with + match R.whd ~subst context ty with (*CSC manca il caso dei CAST *) (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *) (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *) @@ -1780,7 +1790,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in (* 2 is skipped *) let ty_branch = - type_of_branch context parsno need_dummy outtype cons + type_of_branch ~subst context parsno need_dummy outtype cons ty_cons in let b1,ugraph4 = R.are_convertible @@ -1835,7 +1845,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let's control the guarded by destructors conditions D{f,k,x,M} *) - if not (guarded_by_destructors context' eaten + if not (guarded_by_destructors ~subst context' eaten (len + eaten) kl 1 [] m) then raise (TypeCheckerFailure @@ -1872,7 +1882,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = if b then begin (* let's control that the returned type is coinductive *) - match returns_a_coinductive context ty with + match returns_a_coinductive ~subst context ty with None -> raise (TypeCheckerFailure @@ -1882,8 +1892,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let's control the guarded by constructors conditions C{f,M} *) - if not (guarded_by_constructors (types @ context) - 0 len false bo [] uri) then + if not (guarded_by_constructors ~subst + (types @ context) 0 len false bo [] uri) then raise (TypeCheckerFailure ("CoFix: not guarded by constructors")) @@ -1898,7 +1908,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let (_,ty,_) = List.nth fl i in ty,ugraph2 - and check_exp_named_subst ~logger ?(subst = []) context ugraph = + and check_exp_named_subst ~logger ~subst context ugraph = let rec check_exp_named_subst_aux ~logger esubsts l ugraph = match l with [] -> ugraph @@ -1926,7 +1936,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in check_exp_named_subst_aux ~logger [] ugraph - and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph = + and sort_of_prod ~subst context (name,s) (t1, t2) ugraph = let module C = Cic in let t1' = CicReduction.whd ~subst context t1 in let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in @@ -1952,7 +1962,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1') (CicPp.ppterm t2'))) - and eat_prods ?(subst = []) context hetype l ugraph = + and eat_prods ~subst context hetype l ugraph = (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) (*CSC: cucinati *) match l with @@ -1989,9 +1999,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = "Appl: this is not a function, it cannot be applied") ) - and returns_a_coinductive context ty = + and returns_a_coinductive ~subst context ty = let module C = Cic in - match CicReduction.whd context ty with + match CicReduction.whd ~subst context ty with C.MutInd (uri,i,_) -> (*CSC: definire una funzioncina per questo codice sempre replicato *) let obj,_ = @@ -2020,7 +2030,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = UriManager.string_of_uri uri)) ) | C.Prod (n,so,de) -> - returns_a_coinductive ((Some (n,C.Decl so))::context) de + returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de | _ -> None in @@ -2040,7 +2050,6 @@ and is_small ~logger context paramsno c ugraph = let module C = Cic in match CicReduction.whd context c with C.Prod (n,so,de) -> - (*CSC: [] is an empty metasenv. Is it correct? *) let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in if b then @@ -2049,7 +2058,7 @@ and is_small ~logger context paramsno c ugraph = false,ugraph1 | _ -> true,ugraph (*CSC: we trust the type-checker *) in - let (context',dx) = split_prods context paramsno c in + let (context',dx) = split_prods ~subst:[] context paramsno c in is_small_aux ~logger context' dx ugraph and type_of ~logger t ugraph = -- 2.39.2