From b3d97c2147418f44fc704807d3812b04921591af Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 15:36:57 +0200 Subject: Univs: fix bug #4251, handling of template polymorphic constants. --- kernel/inductive.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 87c139f48d..a02d5e2055 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -165,7 +165,10 @@ let rec make_subst env = (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in - make (cons_subst u s subst) (sign, exp, args) + if Univ.Universe.is_levels s then + make (cons_subst u s subst) (sign, exp, args) + else (* Cannot handle substitution by i+n universes. *) + make subst (sign, exp, args) | (na,None,t)::sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) -- cgit v1.2.3 From 50183ce7200d6059b4146c0cc4933aa524178c02 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 12 Oct 2015 15:39:20 +0200 Subject: Univs: be more restrictive for template polymorphic constants: only direct aliases are ok, and indices should not be made polymorphic. Fixes NFix. --- kernel/inductive.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index a02d5e2055..1f8706652f 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -165,10 +165,7 @@ let rec make_subst env = (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in - if Univ.Universe.is_levels s then - make (cons_subst u s subst) (sign, exp, args) - else (* Cannot handle substitution by i+n universes. *) - make subst (sign, exp, args) + make (cons_subst u s subst) (sign, exp, args) | (na,None,t)::sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) -- cgit v1.2.3 From e3e86829780f664ae7a81582a4c6251ceec4f622 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 5 Dec 2015 09:51:32 +0100 Subject: A few renaming and simplification in inductive.ml. --- kernel/inductive.ml | 20 ++++---------------- 1 file changed, 4 insertions(+), 16 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1f8706652f..e06ea75e6a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -270,18 +270,6 @@ let type_of_constructors (ind,u) (mib,mip) = (* Type of case predicates *) -let local_rels ctxt = - let (rels,_) = - Context.fold_rel_context_reverse - (fun (rels,n) (_,copt,_) -> - match copt with - None -> (mkRel n :: rels, n+1) - | Some _ -> (rels, n+1)) - ~init:([],1) - ctxt - in - rels - (* Get type of inductive, with parameters instantiated *) let inductive_sort_family mip = @@ -369,16 +357,16 @@ let is_correct_arity env c pj ind specif params = let build_branches_type (ind,u) (_,mip as specif) params p = let build_one_branch i cty = let typi = full_constructor_instantiate (ind,u,specif,params) cty in - let (args,ccl) = decompose_prod_assum typi in - let nargs = rel_context_length args in + let (cstrsign,ccl) = decompose_prod_assum typi in + let nargs = rel_context_length cstrsign in let (_,allargs) = decompose_app ccl in let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstructU (cstr,u),lparams@(local_rels args)) in + let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in vargs @ [dep_cstr] in let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in - it_mkProd_or_LetIn base args in + it_mkProd_or_LetIn base cstrsign in Array.mapi build_one_branch mip.mind_nf_lc (* [p] is the predicate, [c] is the match object, [realargs] is the -- cgit v1.2.3 From ff8d99117f142dd6851eb7cecc0ae84ec8642fe1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 5 Dec 2015 09:51:42 +0100 Subject: Contracting one extra beta-redex on the fly when typing branches of "match". --- kernel/inductive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index e06ea75e6a..cefb5eca54 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -365,7 +365,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let cstr = ith_constructor_of_inductive ind (i+1) in let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in vargs @ [dep_cstr] in - let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in + let base = betazeta_appvect (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base cstrsign in Array.mapi build_one_branch mip.mind_nf_lc -- cgit v1.2.3 From 6899d3aa567436784a08af4e179c2ef1fa504a02 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 21 Nov 2015 00:17:21 +0100 Subject: Moving extended_rel_vect/extended_rel_list to the kernel. It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file. --- kernel/inductive.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cefb5eca54..466d487153 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -292,14 +292,6 @@ let is_primitive_record (mib,_) = | Some (Some _) -> true | _ -> false -let extended_rel_list n hyps = - let rec reln l p = function - | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 hyps - let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist -- cgit v1.2.3 From e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 17:11:39 +0100 Subject: Unifying betazeta_applist and prod_applist into a clearer interface. - prod_applist - prod_applist_assum - lambda_applist - lambda_applist_assum expect an instance matching the quantified context. They are now in term.ml, with "list" being possibly "vect". Names are a bit arbitrary. Better propositions are welcome. They are put in term.ml in that reduction is after all not needed, because the intent is not to do β or ι on the fly but rather to substitute a λΓ.c or ∀Γ.c (seen as internalization of a Γ⊢c) into one step, independently of the idea of reducing. On the other side: - beta_applist - beta_appvect are seen as optimizations of application doing reduction on the fly only if possible. They are then kept as functions relevant for reduction.ml. --- kernel/inductive.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 466d487153..632b4daeae 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -357,14 +357,14 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let cstr = ith_constructor_of_inductive ind (i+1) in let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in vargs @ [dep_cstr] in - let base = betazeta_appvect (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in + let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base cstrsign in Array.mapi build_one_branch mip.mind_nf_lc (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) let build_case_type env n p c realargs = - whd_betaiota env (betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) + whd_betaiota env (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c]))) let type_case_branches env (pind,largs) pj c = let specif = lookup_mind_specif env (fst pind) in -- cgit v1.2.3 From cbd815a289db52f58235f23f5afba3be49cc8eed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Dec 2015 13:54:18 +0100 Subject: Removing dead code. --- kernel/inductive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 632b4daeae..d0df5c7b38 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -151,7 +151,7 @@ let remember_subst u subst = (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let rec make_subst env = +let make_subst env = let rec make subst = function | (_,Some _,_)::sign, exp, args -> make subst (sign, exp, args) -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- kernel/inductive.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 632b4daeae..f9a6e04c12 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Declarations open Declareops open Environ @@ -77,7 +76,7 @@ let instantiate_params full t u args sign = let fail () = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = - Context.fold_rel_context + Context.Rel.fold_outside (fun (_,copt,_) (largs,subs,ty) -> match (copt, largs, kind_of_term ty) with | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) @@ -297,7 +296,7 @@ let build_dependent_inductive ind (_,mip) params = applist (mkIndU ind, List.map (lift mip.mind_nrealdecls) params - @ extended_rel_list 0 realargs) + @ Context.Rel.to_extended_list 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option @@ -350,12 +349,12 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let build_one_branch i cty = let typi = full_constructor_instantiate (ind,u,specif,params) cty in let (cstrsign,ccl) = decompose_prod_assum typi in - let nargs = rel_context_length cstrsign in + let nargs = Context.Rel.length cstrsign in let (_,allargs) = decompose_app ccl in let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in + let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in vargs @ [dep_cstr] in let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base cstrsign in @@ -499,7 +498,7 @@ let subterm_var p renv = with Failure _ | Invalid_argument _ -> Not_subterm let push_ctxt_renv renv ctxt = - let n = rel_context_length ctxt in + let n = Context.Rel.length ctxt in { env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv } @@ -701,7 +700,7 @@ let restrict_spec env spec p = else let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) - if noccur_with_meta 1 (rel_context_length absctx) ar then spec + if noccur_with_meta 1 (Context.Rel.length absctx) ar then spec else let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in @@ -843,7 +842,7 @@ let filter_stack_domain env ci p stack = let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) - if noccur_with_meta 1 (rel_context_length absctx) ar then stack + if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack else let env = push_rel_context absctx env in let rec filter_stack env ar stack = let t = whd_betadeltaiota env ar in -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/inductive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1f8706652f..80dc690422 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- kernel/inductive.ml | 50 ++++++++++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 24 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index dd49c4a1b7..ca29d83f6a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -17,6 +17,7 @@ open Declareops open Environ open Reduction open Type_errors +open Context.Rel.Declaration type mind_specif = mutual_inductive_body * one_inductive_body @@ -77,10 +78,10 @@ let instantiate_params full t u args sign = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = Context.Rel.fold_outside - (fun (_,copt,_) (largs,subs,ty) -> - match (copt, largs, kind_of_term ty) with - | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) - | (Some b,_,LetIn(_,_,_,t)) -> + (fun decl (largs,subs,ty) -> + match (decl, largs, kind_of_term ty) with + | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t) + | (LocalDef (_,b,_), _, LetIn(_,_,_,t)) -> (largs, (substl subs (subst_instance_constr u b))::subs, t) | (_,[],_) -> if full then fail() else ([], subs, ty) | _ -> fail ()) @@ -152,7 +153,7 @@ let remember_subst u subst = (* Propagate the new levels in the signature *) let make_subst env = let rec make subst = function - | (_,Some _,_)::sign, exp, args -> + | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) | d::sign, None::exp, args -> let args = match args with _::args -> args | [] -> [] in @@ -165,7 +166,7 @@ let make_subst env = (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in make (cons_subst u s subst) (sign, exp, args) - | (na,None,t)::sign, Some u::exp, [] -> + | LocalAssum (na,t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) (* template, it is identity substitution otherwise (ie. when u is *) @@ -314,14 +315,14 @@ let is_correct_arity env c pj ind specif params = let rec srec env pt ar = let pt' = whd_betadeltaiota env pt in match kind_of_term pt', ar with - | Prod (na1,a1,t), (_,None,a1')::ar' -> + | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> let () = try conv env a1 a1' with NotConvertible -> raise (LocalArity None) in - srec (push_rel (na1,None,a1) env) t ar' + srec (push_rel (LocalAssum (na1,a1)) env) t ar' (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (na1,None,a1) env in + let env' = push_rel (LocalAssum (na1,a1)) env in let ksort = match kind_of_term (whd_betadeltaiota env' a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in @@ -330,7 +331,7 @@ let is_correct_arity env c pj ind specif params = try conv env a1 dep_ind with NotConvertible -> raise (LocalArity None) in check_allowed_sort ksort specif - | _, (_,Some _,_ as d)::ar' -> + | _, (LocalDef _ as d)::ar' -> srec (push_rel d env) (lift 1 pt') ar' | _ -> raise (LocalArity None) @@ -482,7 +483,7 @@ let make_renv env recarg tree = genv = [Lazy.lazy_from_val(Subterm(Large,tree))] } let push_var renv (x,ty,spec) = - { env = push_rel (x,None,ty) renv.env; + { env = push_rel (LocalAssum (x,ty)) renv.env; rel_min = renv.rel_min+1; genv = spec:: renv.genv } @@ -568,14 +569,14 @@ let check_inductive_codomain env p = (* The following functions are almost duplicated from indtypes.ml, except that they carry here a poorer environment (containing less information). *) let ienv_push_var (env, lra) (x,a,ra) = - (push_rel (x,None,a) env, (Norec,ra)::lra) + (push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra) let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind specif env = - push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env + let decl = LocalAssum (Anonymous, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in @@ -848,7 +849,7 @@ let filter_stack_domain env ci p stack = let t = whd_betadeltaiota env ar in match stack, kind_of_term t with | elt :: stack', Prod (n,a,c0) -> - let d = (n,None,a) in + let d = LocalAssum (n,a) in let ty, args = decompose_app (whd_betadeltaiota env a) in let elt = match kind_of_term ty with | Ind ind -> @@ -905,10 +906,10 @@ let check_one_fix renv recpos trees def = end else begin - match pi2 (lookup_rel p renv.env) with - | None -> + match lookup_rel p renv.env with + | LocalAssum _ -> List.iter (check_rec_call renv []) l - | Some c -> + | LocalDef (_,c,_) -> try List.iter (check_rec_call renv []) l with FixGuardError _ -> check_rec_call renv stack (applist(lift p c,l)) @@ -983,10 +984,11 @@ let check_one_fix renv recpos trees def = | Var id -> begin - match pi2 (lookup_named id renv.env) with - | None -> + let open Context.Named.Declaration in + match lookup_named id renv.env with + | LocalAssum _ -> List.iter (check_rec_call renv []) l - | Some c -> + | LocalDef (_,c,_) -> try List.iter (check_rec_call renv []) l with (FixGuardError _) -> check_rec_call renv stack (applist(c,l)) @@ -1040,7 +1042,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = match kind_of_term (whd_betadeltaiota env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then - let env' = push_rel (x, None, a) env in + let env' = push_rel (LocalAssum (x,a)) env in if Int.equal n (k + 1) then (* get the inductive type of the fixpoint *) let (mind, _) = @@ -1090,7 +1092,7 @@ let rec codomain_is_coind env c = let b = whd_betadeltaiota env c in match kind_of_term b with | Prod (x,a,b) -> - codomain_is_coind (push_rel (x, None, a) env) b + codomain_is_coind (push_rel (LocalAssum (x,a)) env) b | _ -> (try find_coinductive env b with Not_found -> @@ -1131,7 +1133,7 @@ let check_one_cofix env nbfix def deftype = | Lambda (x,a,b) -> let () = assert (List.is_empty args) in if noccur_with_meta n nbfix a then - let env' = push_rel (x, None, a) env in + let env' = push_rel (LocalAssum (x,a)) env in check_rec_call env' alreadygrd (n+1) tree vlra b else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) -- cgit v1.2.3 From 4f041384cb27f0d24fa14b272884b4b7f69cacbe Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 15 Feb 2016 11:55:43 +0100 Subject: CLEANUP: Simplifying the changes done in "kernel/*" ... ... ... ... ... ... ... ... ... ... ... ... ... ... --- kernel/inductive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ca29d83f6a..229508ea34 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -319,7 +319,7 @@ let is_correct_arity env c pj ind specif params = let () = try conv env a1 a1' with NotConvertible -> raise (LocalArity None) in - srec (push_rel (LocalAssum (na1,a1)) env) t ar' + srec (push_rel (LocalAssum (na1,a1)) env) t ar' (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) let env' = push_rel (LocalAssum (na1,a1)) env in -- cgit v1.2.3 From 120053a50f87bd53398eedc887fa5e979f56f112 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 18:17:56 +0100 Subject: This fix is probably not enough to justify that there are no problems with primitive projections and prop. ext. or univalence, but at least it prevents known proofs of false (see discussion on #4588). --- kernel/inductive.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 80dc690422..fbe0920bcf 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -814,7 +814,15 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in (match subt with - | Subterm (s, wf) -> Subterm (Strict, wf) + | Subterm (s, wf) -> + (* We take the subterm specs of the constructor of the record *) + let wf_args = (dest_subterms wf).(0) in + (* We extract the tree of the projected argument *) + let kn = Projection.constant p in + let cb = lookup_constant kn renv.env in + let pb = Option.get cb.const_proj in + let n = pb.proj_arg in + Subterm (Strict, List.nth wf_args n) | Dead_code -> Dead_code | Not_subterm -> Not_subterm) -- cgit v1.2.3 From 10e3c8e59664ed5137cd650ba6e0704943c511e8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Mar 2016 14:17:48 +0100 Subject: Removing OCaml deprecated function names from the Lazy module. --- kernel/inductive.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 551632962b..499cbf0dfd 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -480,7 +480,7 @@ type guard_env = let make_renv env recarg tree = { env = env; rel_min = recarg+2; (* recarg = 0 ==> Rel 1 -> recarg; Rel 2 -> fix *) - genv = [Lazy.lazy_from_val(Subterm(Large,tree))] } + genv = [Lazy.from_val(Subterm(Large,tree))] } let push_var renv (x,ty,spec) = { env = push_rel (LocalAssum (x,ty)) renv.env; @@ -817,7 +817,7 @@ and stack_element_specif = function |SArg x -> x and extract_stack renv a = function - | [] -> Lazy.lazy_from_val Not_subterm , [] + | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t (* Check term c can be applied to one of the mutual fixpoints. *) -- cgit v1.2.3