From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- kernel/inductive.ml | 169 ++++++++++++++++++++++++++++------------------------ 1 file changed, 91 insertions(+), 78 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3c4c2796..9bed598b 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,16 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* = Array.length mib.mind_packets then - error "Inductive.lookup_mind_specif: invalid inductive index"; + user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index"); (mib, mib.mind_packets.(tyi)) let find_rectype env c = let (t, l) = decompose_app (whd_all env c) in - match kind_of_term t with + match kind t with | Ind ind -> (ind, l) | _ -> raise Not_found let find_inductive env c = let (t, l) = decompose_app (whd_all env c) in - match kind_of_term t with + match kind t with | Ind ind - when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = let (t, l) = decompose_app (whd_all env c) in - match kind_of_term t with + match kind t with | Ind ind - when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == CoFinite -> (ind, l) | _ -> raise Not_found let inductive_params (mib,_) = mib.mind_nparams @@ -54,9 +56,11 @@ let inductive_paramdecls (mib,u) = Vars.subst_instance_context u mib.mind_params_ctxt let instantiate_inductive_constraints mib u = - if mib.mind_polymorphic then - Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes) - else Univ.Constraint.empty + let process auctx = Univ.AUContext.instantiate u auctx in + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Constraint.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) (************************************************************************) @@ -75,11 +79,11 @@ let constructor_instantiate mind u mib c = let instantiate_params full t u args sign = let fail () = - anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in + anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in let (rem_args, subs, ty) = Context.Rel.fold_outside (fun decl (largs,subs,ty) -> - match (decl, largs, kind_of_term ty) with + match (decl, largs, kind 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) @@ -92,9 +96,9 @@ let instantiate_params full t u args sign = substl subs ty let full_inductive_instantiate mib u params sign = - let dummy = prop_sort in - let t = mkArity (Vars.subst_instance_context u sign,dummy) in - fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) + let dummy = Sorts.prop in + let t = Term.mkArity (Vars.subst_instance_context u sign,dummy) in + fst (Term.destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = let inst_ind = constructor_instantiate mind u mib t in @@ -126,7 +130,7 @@ where Remark: Set (predicative) is encoded as Type(0) *) -let sort_as_univ = function +let sort_as_univ = let open Sorts in function | Type u -> u | Prop Null -> Universe.type0m | Prop Pos -> Universe.type0 @@ -190,11 +194,11 @@ let instantiate_universes env ctx ar argsorts = let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) - if is_type0m_univ level then prop_sort + if is_type0m_univ level then Sorts.prop (* Non singleton type not containing types are interpretable in Set *) - else if is_type0_univ level then set_sort + else if is_type0_univ level then Sorts.set (* This is a Type with constraints *) - else Type level + else Sorts.Type level in (ctx, ty) @@ -209,9 +213,9 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. the situation where a non-Prop singleton inductive becomes Prop when applied to Prop params *) - if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s + if not polyprop && not (is_type0m_univ ar.template_level) && Sorts.is_prop s then raise (SingletonInductiveBecomesProp mip.mind_typename); - mkArity (List.rev ctx,s) + Term.mkArity (List.rev ctx,s) let type_of_inductive env pind = type_of_inductive_gen env pind [||] @@ -231,7 +235,7 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = (* The max of an array of universes *) -let cumulate_constructor_univ u = function +let cumulate_constructor_univ u = let open Sorts in function | Prop Null -> u | Prop Pos -> Universe.sup Universe.type0 u | Type u' -> Universe.sup u u' @@ -247,7 +251,7 @@ let type_of_constructor (cstr, u) (mib,mip) = let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type."; + if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = @@ -274,8 +278,8 @@ let type_of_constructors (ind,u) (mib,mip) = let inductive_sort_family mip = match mip.mind_arity with - | RegularArity s -> family_of_sort s.mind_sort - | TemplateArity _ -> InType + | RegularArity s -> Sorts.family s.mind_sort + | TemplateArity _ -> Sorts.InType let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip @@ -294,19 +298,20 @@ let is_primitive_record (mib,_) = let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in - applist + Term.applist (mkIndU ind, List.map (lift mip.mind_nrealdecls) params - @ Context.Rel.to_extended_list 0 realargs) + @ Context.Rel.to_extended_list mkRel 0 realargs) (* This exception is local *) -exception LocalArity of (sorts_family * sorts_family * arity_error) option +exception LocalArity of (Sorts.family * Sorts.family * arity_error) option let check_allowed_sort ksort specif = + let open Sorts in let eq_ksort s = match ksort, s with | InProp, InProp | InSet, InSet | InType, InType -> true | _ -> false in - if not (List.exists eq_ksort (elim_sorts specif)) then + if not (CList.exists eq_ksort (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(ksort,s,error_elim_explain ksort s))) @@ -314,7 +319,7 @@ let is_correct_arity env c pj ind specif params = let arsign,_ = get_instantiated_arity ind specif params in let rec srec env pt ar = let pt' = whd_all env pt in - match kind_of_term pt', ar with + match kind pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> let () = try conv env a1 a1' @@ -323,8 +328,8 @@ let is_correct_arity env c pj ind specif params = (* 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 - let ksort = match kind_of_term (whd_all env' a2) with - | Sort s -> family_of_sort s + let ksort = match kind (whd_all env' a2) with + | Sort s -> Sorts.family s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in let _ = @@ -349,22 +354,22 @@ 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 (cstrsign,ccl) = decompose_prod_assum typi in + let (cstrsign,ccl) = Term.decompose_prod_assum typi 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@(Context.Rel.to_extended_list 0 cstrsign)) in + let dep_cstr = Term.applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 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 + let base = Term.lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in + Term.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 (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c]))) + whd_betaiota env (Term.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 @@ -587,7 +592,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let rec ienv_decompose_prod (env,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else let c' = whd_all env c in - match kind_of_term c' with + match kind c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in ienv_decompose_prod ienv' (n-1) b @@ -619,7 +624,7 @@ compute the number of recursive arguments. *) let get_recargs_approx env tree ind args = let rec build_recargs (env, ra_env as ienv) tree c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> assert (List.is_empty largs); build_recargs (ienv_push_var ienv (na, b, mk_norec)) tree d @@ -678,7 +683,7 @@ let get_recargs_approx env tree ind args = and build_recargs_constructors ienv trees c = let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in @@ -707,7 +712,7 @@ let restrict_spec env spec p = let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in let i,args = decompose_app (whd_all env s) in - match kind_of_term i with + match kind i with | Ind i -> begin match spec with | Dead_code -> spec @@ -728,7 +733,7 @@ let restrict_spec env spec p = let rec subterm_specif renv stack t = (* maybe reduction is not always necessary! *) let f,l = decompose_app (whd_all renv.env t) in - match kind_of_term f with + match kind f with | Rel k -> subterm_var k renv | Case (ci,p,c,lbr) -> let stack' = push_stack_closures renv l stack in @@ -771,7 +776,7 @@ let rec subterm_specif renv stack t = let decrArg = recindxs.(i) in let theBody = bodies.(i) in let nbOfAbst = decrArg+1 in - let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in + let sign,strippedBody = Term.decompose_lam_n_assum nbOfAbst theBody in (* pushing the fix parameters *) let stack' = push_stack_closures renv l stack in let renv'' = push_ctxt_renv renv' sign in @@ -793,21 +798,24 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in - (match subt with - | 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) + (match subt with + | 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 + spec_of_tree (List.nth wf_args n) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) + + | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ + | Construct _ | CoFix _ -> Not_subterm + (* Other terms are not subterms *) - | _ -> Not_subterm and lazy_subterm_specif renv stack t = lazy (subterm_specif renv stack t) @@ -855,11 +863,13 @@ let filter_stack_domain env ci p stack = else let env = push_rel_context absctx env in let rec filter_stack env ar stack = let t = whd_all env ar in - match stack, kind_of_term t with + match stack, kind t with | elt :: stack', Prod (n,a,c0) -> let d = LocalAssum (n,a) in + let ctx, a = dest_prod_assum env a in + let env = push_rel_context ctx env in let ty, args = decompose_app (whd_all env a) in - let elt = match kind_of_term ty with + let elt = match kind ty with | Ind ind -> let spec' = stack_element_specif elt in (match (Lazy.force spec') with @@ -890,7 +900,7 @@ let check_one_fix renv recpos trees def = if noccur_with_meta renv.rel_min nfi t then () else let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in - match kind_of_term f with + match kind f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) if renv.rel_min <= p && p < renv.rel_min+nfi then @@ -920,7 +930,7 @@ let check_one_fix renv recpos trees def = | LocalDef (_,c,_) -> try List.iter (check_rec_call renv []) l with FixGuardError _ -> - check_rec_call renv stack (applist(lift p c,l)) + check_rec_call renv stack (Term.applist(lift p c,l)) end | Case (ci,p,c_0,lrest) -> @@ -966,7 +976,7 @@ let check_one_fix renv recpos trees def = if evaluable_constant kn renv.env then try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> - let value = (applist(constant_value_in renv.env cu, l)) in + let value = (Term.applist(constant_value_in renv.env cu, l)) in check_rec_call renv stack value else List.iter (check_rec_call renv []) l @@ -1003,7 +1013,7 @@ let check_one_fix renv recpos trees def = | LocalDef (_,c,_) -> try List.iter (check_rec_call renv []) l with (FixGuardError _) -> - check_rec_call renv stack (applist(c,l)) + check_rec_call renv stack (Term.applist(c,l)) end | Sort _ -> @@ -1018,12 +1028,12 @@ let check_one_fix renv recpos trees def = if Int.equal decr 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body else - match kind_of_term body with + match kind body with | Lambda (x,a,b) -> check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b - | _ -> anomaly (Pp.str "Not enough abstractions in fix body") + | _ -> anomaly (Pp.str "Not enough abstractions in fix body.") in check_rec_call renv [] def @@ -1039,7 +1049,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = || not (Int.equal (Array.length names) nbfix) || bodynum < 0 || bodynum >= nbfix - then anomaly (Pp.str "Ill-formed fix term"); + then anomaly (Pp.str "Ill-formed fix term."); let fixenv = push_rec_types recdef env in let vdefj = judgment_of_fixpoint recdef in let raise_err env i err = @@ -1049,7 +1059,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (* check fi does not appear in the k+1 first abstractions, gives the type of the k+1-eme abstraction (must be an inductive) *) let rec check_occur env n def = - match kind_of_term (whd_all env def) with + match kind (whd_all env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then let env' = push_rel (LocalAssum (x,a)) env in @@ -1059,9 +1069,12 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = try find_inductive env a with Not_found -> raise_err env i (RecursionNotOnInductiveType a) in + let mib,_ = lookup_mind_specif env (out_punivs mind) in + if mib.mind_finite != Finite then + raise_err env i (RecursionNotOnInductiveType a); (mind, (env', b)) else check_occur env' (n+1) b - else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call") + else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) @@ -1090,8 +1103,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = () (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) @@ -1100,11 +1113,11 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; exception CoFixGuardError of env * guard_error let anomaly_ill_typed () = - anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") + anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.") let rec codomain_is_coind env c = let b = whd_all env c in - match kind_of_term b with + match kind b with | Prod (x,a,b) -> codomain_is_coind (push_rel (LocalAssum (x,a)) env) b | _ -> @@ -1116,7 +1129,7 @@ let check_one_cofix env nbfix def deftype = let rec check_rec_call env alreadygrd n tree vlra t = if not (noccur_with_meta n nbfix t) then let c,args = decompose_app (whd_all env t) in - match kind_of_term c with + match kind c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive call allowed *) @@ -1188,8 +1201,8 @@ let check_one_cofix env nbfix def deftype = | Meta _ -> () | Evar _ -> List.iter (check_rec_call env alreadygrd n tree vlra) args - - | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in + | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ + | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in let vlra = lookup_subterms env mind in -- cgit v1.2.3