diff options
29 files changed, 204 insertions, 145 deletions
diff --git a/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh new file mode 100644 index 0000000000..913b39c30c --- /dev/null +++ b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "11557" ] || [ "$CI_BRANCH" = "template-directify" ]; then + + equations_CI_REF=template-directify + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + paramcoq_CI_REF=template-directify + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + + elpi_CI_REF=template-directify + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + +fi diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 2b09b2b42e..58c2fcc68a 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -127,9 +127,9 @@ in time. - [ ] Send an e-mail on Coqdev announcing that the tag has been put so that package managers can start preparing package updates (including a `coq-bignums` compatible version). -- [ ] Ping `@erikmd` to update the Docker images in `coqorg/coq` - (requires `coq-bignums` in `extra-dev` for a beta / in `released` - for a final release). +- [ ] When opening the corresponding PR for `coq` in the opam repository ([`coq/opam-coq-archive`](https://github.com/coq/opam-coq-archive) or [`ocaml/opam-repository`](https://github.com/ocaml/opam-repository)), + the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq) + (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built). - [ ] Draft a release on GitHub. - [ ] Get `@maximedenes` to sign the Windows and MacOS packages and upload them on GitHub. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 09090ce89a..721c7a7a51 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1063,6 +1063,9 @@ Parameterized inductive types | cons3 : A -> list3 -> list3. End list3. + Attributes ``uniform`` and ``nonuniform`` respectively enable and + disable uniform parameters for a single inductive declaration block. + .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1f9178f4b6..85d86bed62 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -270,7 +270,7 @@ class GallinaObject(PlainObject): :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. """ subdomain = "thm" - index_suffix = "(thm)" + index_suffix = "(theorem)" annotation = "Theorem" class VernacObject(NotationObject): @@ -283,7 +283,7 @@ class VernacObject(NotationObject): This command is equivalent to :n:`…`. """ subdomain = "cmd" - index_suffix = "(cmd)" + index_suffix = "(command)" annotation = "Command" def _name_from_signature(self, signature): @@ -306,7 +306,7 @@ class VernacVariantObject(VernacObject): This is equivalent to :n:`Axiom @ident : @term`. """ - index_suffix = "(cmdv)" + index_suffix = "(command variant)" annotation = "Variant" def _name_from_signature(self, signature): @@ -322,7 +322,7 @@ class TacticNotationObject(NotationObject): :token:`expr` is evaluated to ``v`` which must be a tactic value. … """ subdomain = "tacn" - index_suffix = "(tacn)" + index_suffix = "(tactic)" annotation = None class TacticNotationVariantObject(TacticNotationObject): @@ -342,7 +342,7 @@ class TacticNotationVariantObject(TacticNotationObject): The number is the failure level. If no level is specified, it defaults to 0. … """ - index_suffix = "(tacnv)" + index_suffix = "(tactic variant)" annotation = "Variant" class OptionObject(NotationObject): @@ -357,7 +357,7 @@ class OptionObject(NotationObject): application of a tactic. """ subdomain = "opt" - index_suffix = "(opt)" + index_suffix = "(option)" annotation = "Option" def _name_from_signature(self, signature): @@ -534,7 +534,7 @@ class ExceptionObject(NotationObject): Raised if :n:`@tactic` does not fully solve the goal. """ subdomain = "exn" - index_suffix = "(err)" + index_suffix = "(error)" annotation = "Error" # Uses “exn” since “err” already is a CSS class added by “writer_aux”. @@ -557,7 +557,7 @@ class WarningObject(NotationObject): valid coercion paths are ignored. """ subdomain = "warn" - index_suffix = "(warn)" + index_suffix = "(warning)" annotation = "Warning" # Generate names automatically diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 3771454db5..b6b8e5265c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -158,7 +158,7 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let auxntyp = 1 in let specif = (lookup_mind_specif env mi, u) in - let ty = type_of_inductive env specif in + let ty = type_of_inductive specif in let env' = let r = (snd (fst specif)).mind_relevance in let anon = Context.make_annot Anonymous r in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 5d8e1f0fdb..c6035f78ff 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -143,9 +143,16 @@ let remember_subst u subst = Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst with Not_found -> subst +type param_univs = (unit -> Universe.t) list + +let make_param_univs env argtys = + Array.map_to_list (fun arg () -> + Sorts.univ_of_sort (snd (Reduction.dest_arity env arg))) + argtys + (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let make_subst env = +let make_subst = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) @@ -158,8 +165,8 @@ let make_subst env = (* arity is a global level which, at typing time, will be enforce *) (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) - let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in - make (cons_subst u s subst) (sign, exp, args) + let s = a () in + make (cons_subst u s subst) (sign, exp, args) | 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 *) @@ -178,9 +185,8 @@ let make_subst env = exception SingletonInductiveBecomesProp of Id.t -let instantiate_universes env ctx ar argsorts = - let args = Array.to_list argsorts in - let subst = make_subst env (ctx,ar.template_param_levels,args) in +let instantiate_universes ctx ar args = + let subst = make_subst (ctx,ar.template_param_levels,args) in 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 *) @@ -204,13 +210,13 @@ let check_instance mib u = | Polymorphic uctx -> Instance.length u = AUContext.size uctx) then CErrors.anomaly Pp.(str "bad instance length on mutind.") -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps = check_instance mib u; match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes env ctx ar paramtyps in + let ctx,s = instantiate_universes ctx ar paramtyps in (* 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 *) @@ -218,21 +224,21 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = then raise (SingletonInductiveBecomesProp mip.mind_typename); Term.mkArity (List.rev ctx,s) -let type_of_inductive env pind = - type_of_inductive_gen env pind [||] +let type_of_inductive pind = + type_of_inductive_gen pind [] -let constrained_type_of_inductive env ((mib,_mip),u as pind) = - let ty = type_of_inductive env pind in +let constrained_type_of_inductive ((mib,_mip),u as pind) = + let ty = type_of_inductive pind in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args = - let ty = type_of_inductive_gen env pind args in +let constrained_type_of_inductive_knowing_parameters ((mib,_mip),u as pind) args = + let ty = type_of_inductive_gen pind args in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = - type_of_inductive_gen ~polyprop env mip args +let type_of_inductive_knowing_parameters ?(polyprop=true) mip args = + type_of_inductive_gen ~polyprop mip args (* The max of an array of universes *) @@ -589,7 +595,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let push_ind specif env = let r = specif.mind_relevance in let anon = Context.make_annot Anonymous r in - let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive ((mib,specif),u)) lpar) in push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 8c40c318c5..b690fe1157 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -41,16 +41,22 @@ val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_contex val instantiate_inductive_constraints : mutual_inductive_body -> Instance.t -> Constraint.t -val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained +type param_univs = (unit -> Universe.t) list + +val make_param_univs : Environ.env -> constr array -> param_univs +(** The constr array is the types of the arguments to a template + polymorphic inductive. *) + +val constrained_type_of_inductive : mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : - env -> mind_specif puniverses -> types Lazy.t array -> types constrained + mind_specif puniverses -> param_univs -> types constrained val relevance_of_inductive : env -> inductive -> Sorts.relevance -val type_of_inductive : env -> mind_specif puniverses -> types +val type_of_inductive : mind_specif puniverses -> types val type_of_inductive_knowing_parameters : - env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types + ?polyprop:bool -> mind_specif puniverses -> param_univs -> types val elim_sort : mind_specif -> Sorts.family @@ -117,8 +123,8 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : env -> Constr.rel_context -> - template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t +val instantiate_universes : Constr.rel_context -> + template_arity -> param_univs -> Constr.rel_context * Sorts.t (** {6 Debug} *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 0a654adf7f..11c455de73 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -150,8 +150,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let ty1 = type_of_inductive env ((mib1, p1), inst) in - let ty2 = type_of_inductive env ((mib2, p2), inst) in + let ty1 = type_of_inductive ((mib1, p1), inst) in + let ty2 = type_of_inductive ((mib2, p2), inst) in let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in cst in diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 2a35f87db8..80accc1ced 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -372,7 +372,7 @@ let type_of_inductive_knowing_parameters env (ind,u) args = let (mib,_mip) as spec = lookup_mind_specif env ind in check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - env (spec,u) args + (spec,u) (Inductive.make_param_univs env args) in check_constraints cst env; t @@ -380,7 +380,7 @@ let type_of_inductive_knowing_parameters env (ind,u) args = let type_of_inductive env (ind,u) = let (mib,mip) = lookup_mind_specif env ind in check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + let t,cst = Inductive.constrained_type_of_inductive ((mib,mip),u) in check_constraints cst env; t @@ -461,8 +461,7 @@ let type_of_global_in_context env r = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in let inst = Univ.make_abstract_instance univs in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Inductive.type_of_inductive env (specif, inst), univs + Inductive.type_of_inductive (specif, inst), univs | ConstructRef cstr -> let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) @@ -515,8 +514,7 @@ let rec execute env cstr = let f', ft = match kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> - let args = Array.map (fun t -> lazy t) argst in - f, type_of_inductive_knowing_parameters env ind args + f, type_of_inductive_knowing_parameters env ind argst | _ -> (* No template polymorphism *) execute env f diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a4469b7ec1..9b30ddd958 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -437,7 +437,7 @@ and extract_really_ind env kn mib = Array.mapi (fun i mip -> let (_,u),_ = UnivGen.fresh_inductive_instance env (kn,i) in - let ar = Inductive.type_of_inductive env ((mib,mip),u) in + let ar = Inductive.type_of_inductive ((mib,mip),u) in let ar = EConstr.of_constr ar in let info = (fst (flag_of_type env sg ar) = Info) in let s,v = if info then type_sign_vl env sg ar else [],[] in @@ -526,7 +526,7 @@ and extract_really_ind env kn mib = (* Is this record officially declared with its projections ? *) (* If so, we use this information. *) begin try - let ty = Inductive.type_of_inductive env ((mib,mip0),u) in + let ty = Inductive.type_of_inductive ((mib,mip0),u) in let n = nb_default_params env sg (EConstr.of_constr ty) in let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 84f09c385f..fdbad2ab9e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1512,12 +1512,12 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ msg in @@ -1527,12 +1527,12 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ CErrors.print reraise in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 816a8c4703..a4406aeba1 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -29,7 +29,7 @@ open Context.Rel.Declaration let type_of_inductive env (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; - Inductive.type_of_inductive env (specif,u) + Inductive.type_of_inductive (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bfee07e7f0..838bf22c66 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1707,7 +1707,7 @@ let splay_arity env sigma c = let l, c = splay_prod env sigma c in match EConstr.kind sigma c with | Sort s -> l,s - | _ -> invalid_arg "splay_arity" + | _ -> raise Reduction.NotArity let sort_of_arity env sigma c = snd (splay_arity env sigma c) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index e72f5f2793..c539ec55ed 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -236,12 +236,20 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr +val splay_prod_assum : env -> evar_map -> constr -> rel_context * constr + val splay_arity : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t +(** Raises [Reduction.NotArity] *) + val sort_of_arity : env -> evar_map -> constr -> ESorts.t +(** Raises [Reduction.NotArity] *) + val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr +(** Raises [Invalid_argument] *) + val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr -val splay_prod_assum : - env -> evar_map -> constr -> rel_context * constr +(** Raises [Invalid_argument] *) + type 'a miota_args = { mP : constr; (** the result type *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index d2af957b54..87fe4cfcda 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -168,15 +168,21 @@ let retype ?(polyprop=true) sigma = | _ -> decomp_sort env sigma (type_of env t) and type_of_global_reference_knowing_parameters env c args = - let argtyps = - Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in match EConstr.kind sigma c with | Ind (ind, u) -> let u = EInstance.kind sigma u in let mip = lookup_mind_specif env ind in - EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters - ~polyprop env (mip, u) argtyps - with Reduction.NotArity -> retype_error NotAnArity) + let paramtyps = Array.map_to_list (fun arg () -> + let t = type_of env arg in + let s = try Reductionops.sort_of_arity env sigma t + with Reduction.NotArity -> retype_error NotAnArity + in + Sorts.univ_of_sort (ESorts.kind sigma s)) + args + in + EConstr.of_constr + (Inductive.type_of_inductive_knowing_parameters + ~polyprop (mip, u) paramtyps) | Construct (cstr, u) -> let u = EInstance.kind sigma u in EConstr.of_constr (type_of_constructor env (cstr, u)) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b4c19775a7..f067c075bf 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -38,8 +38,11 @@ let meta_type evd mv = let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in - let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in - Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp + let paramstyp = Array.map_to_list (fun j () -> + let s = Reductionops.sort_of_arity env sigma j.uj_type in + Sorts.univ_of_sort (EConstr.ESorts.kind sigma s)) jl + in + Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with @@ -307,7 +310,7 @@ let type_of_inductive env sigma (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in - let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in + let ty, csts = Inductive.constrained_type_of_inductive (specif,u) in let sigma = Evd.add_constraints sigma csts in sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind))) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 885fc8980d..b04e59734d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -98,7 +98,7 @@ let construct_of_constr_const env tag typ = let construct_of_constr_block = construct_of_constr false let type_of_ind env (ind, u) = - type_of_inductive env (Inductive.lookup_mind_specif env ind, u) + type_of_inductive (Inductive.lookup_mind_specif env ind, u) let build_branches_type env sigma (mind,_ as _ind) mib mip u params p = let rtbl = mip.mind_reloc_tbl in diff --git a/printing/printmod.ml b/printing/printmod.ml index a5fd7f69ed..b84113bde2 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -85,8 +85,8 @@ let print_constructors envpar sigma names types = in hv 0 (str " " ++ pc) -let build_ind_type env mip = - Inductive.type_of_inductive env mip +let build_ind_type mip = + Inductive.type_of_inductive mip let print_one_inductive env sigma mib ((_,i) as ind) = let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in @@ -94,7 +94,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in let envpar = push_rel_context params env in @@ -146,7 +146,7 @@ let print_record env mind mib udecl = let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index c5b3e0931b..65ef2ca8c6 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -131,7 +131,7 @@ let classify_vernac e = VtSideff ([id.CAst.v], VtLater) | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater) | VernacInductive (_, _,_,l) -> - let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with + let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ CList.map_filter (function diff --git a/test-suite/README.md b/test-suite/README.md index a2d5905710..96926f70b9 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -67,7 +67,7 @@ See [`test-suite/Makefile`](Makefile) for more information. ## Adding a test Regression tests for closed bugs should be added to -[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number. +[`bugs/closed`](bugs/closed), as `bug_1234.v` where `1234` is the bug number. Files in this directory are tested for successful compilation. When you fix a bug, you should usually add a regression test here as well. diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v index 42236a5313..651247937d 100644 --- a/test-suite/success/uniform_inductive_parameters.v +++ b/test-suite/success/uniform_inductive_parameters.v @@ -1,13 +1,23 @@ +Module Att. + #[uniform] Inductive list (A : Type) := + | nil : list + | cons : A -> list -> list. + Check (list : Type -> Type). + Check (cons : forall A, A -> list A -> list A). +End Att. + Set Uniform Inductive Parameters. Inductive list (A : Type) := - | nil : list - | cons : A -> list -> list. +| nil : list +| cons : A -> list -> list. Check (list : Type -> Type). Check (cons : forall A, A -> list A -> list A). Inductive list2 (A : Type) (A' := prod A A) := - | nil2 : list2 - | cons2 : A' -> list2 -> list2. +| nil2 : list2 +| cons2 : A' -> list2 -> list2. Check (list2 : Type -> Type). Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). + +#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)). diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index 645b92c302..26ffe000ad 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -236,7 +236,7 @@ let pattern_vars pat = in aux () Id.Set.empty pat -let abstract_vars loc vars tac = +let abstract_vars loc ?typ vars tac = let get_name = function Name id -> Some id | Anonymous -> None in let def = try Some (List.find_map get_name vars) with Not_found -> None in let na, tac = match def with @@ -258,7 +258,15 @@ let abstract_vars loc vars tac = let tac = CAst.make ?loc @@ CTacLet (false, bnd, tac) in (Name id0, tac) in - CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar na], tac) + let pat = CAst.make ?loc @@ CPatVar na in + let pat = match typ with + | None -> pat + | Some typ -> + let t_array = coq_core "array" in + let typ = CAst.make ?loc @@ CTypRef (AbsKn (Other t_array), [typ]) in + CAst.make ?loc @@ CPatCnv (pat, typ) + in + CAst.make ?loc @@ CTacFun ([pat], tac) let of_pattern p = inj_wit ?loc:p.CAst.loc wit_pattern p @@ -400,7 +408,12 @@ let of_constr_matching {loc;v=m} = (* Order of elements is crucial here! *) let vars = Id.Set.elements vars in let vars = List.map (fun id -> Name id) vars in - let e = abstract_vars loc vars tac in + (* Annotate the bound array variable with constr type *) + let typ = + let t_constr = coq_core "constr" in + CAst.make ?loc @@ CTypRef (AbsKn (Other t_constr), []) + in + let e = abstract_vars loc ~typ vars tac in let e = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar na], e) in let pat = inj_wit ?loc:ploc wit_pattern pat in of_tuple [knd; pat; e] diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index fb61a1089f..46f616c4ff 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -239,7 +239,6 @@ and traverse_inductive (curr, data, ax2ty) mind obj = in (* Build the context of all arities *) let arities_ctx = - let global_env = Global.env () in let instance = let open Univ in Instance.of_array @@ -250,7 +249,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj = in Array.fold_left (fun accu oib -> let pspecif = ((mib, oib), instance) in - let ind_type = Inductive.type_of_inductive global_env pspecif in + let ind_type = Inductive.type_of_inductive pspecif in let indr = oib.mind_relevance in let ind_name = Name oib.mind_typename in Context.Rel.add (Context.Rel.Declaration.LocalAssum (make_annot ind_name indr, ind_type)) accu) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 6bdb3159cf..bdf8511cce 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -178,7 +178,7 @@ let build_beq_scheme mode kn = (* current inductive we are working on *) let cur_packet = mib.mind_packets.(snd (fst ind)) in (* Inductive toto : [rettyp] := *) - let rettyp = Inductive.type_of_inductive env ((mib,cur_packet),u) in + let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in (* split rettyp in a list without the non rec params and the last -> e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *) let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index d0374bc4fa..74249301d7 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -21,7 +21,6 @@ open Constrexpr_ops open Extend open Decls open Declaremods -open Declarations open Namegen open Tok (* necessary for camlp5 *) @@ -200,9 +199,7 @@ GRAMMAR EXTEND Gram (* Gallina inductive declarations *) | cum = OPT cumulativity_token; priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> - { let (k,f) = f in - let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (cum, priv,f,indl) } + { VernacInductive (cum, priv, f, indl) } | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> { VernacFixpoint (NoDischarge, recs) } | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -337,12 +334,12 @@ GRAMMAR EXTEND Gram ] ] ; finite_token: - [ [ IDENT "Inductive" -> { (Inductive_kw,Finite) } - | IDENT "CoInductive" -> { (CoInductive,CoFinite) } - | IDENT "Variant" -> { (Variant,BiFinite) } - | IDENT "Record" -> { (Record,BiFinite) } - | IDENT "Structure" -> { (Structure,BiFinite) } - | IDENT "Class" -> { (Class true,BiFinite) } ] ] + [ [ IDENT "Inductive" -> { Inductive_kw } + | IDENT "CoInductive" -> { CoInductive } + | IDENT "Variant" -> { Variant } + | IDENT "Record" -> { Record } + | IDENT "Structure" -> { Structure } + | IDENT "Class" -> { Class true } ] ] ; cumulativity_token: [ [ IDENT "Cumulative" -> { VernacCumulative } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 82132a1af6..6240120cb0 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -476,7 +476,7 @@ let string_of_theorem_kind = let open Decls in function let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn - let pr_record_decl b c fs = + let pr_record_decl c fs = pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") @@ -802,7 +802,7 @@ let string_of_definition_object_kind = let open Decls in function (if coe then str":>" else str":") ++ Flags.without_option Flags.beautify pr_spc_lconstr c) in - let pr_constructor_list b l = match l with + let pr_constructor_list l = match l with | Constructors [] -> mt() | Constructors l -> let fst_sep = match l with [_] -> " " | _ -> " | " in @@ -810,21 +810,20 @@ let string_of_definition_object_kind = let open Decls in function fnl() ++ str fst_sep ++ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l | RecordDecl (c,fs) -> - pr_record_decl b c fs + pr_record_decl c fs in - let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) = + let pr_oneind key (((coe,iddecl),indpar,s,lc),ntn) = hov 0 ( str key ++ spc() ++ (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++ pr_and_type_binders_arg indpar ++ pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++ - str" :=") ++ pr_constructor_list k lc ++ + str" :=") ++ pr_constructor_list lc ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn in let key = - let (_,_,_,k,_),_ = List.hd l in let kind = - match k with Record -> "Record" | Structure -> "Structure" + match f with Record -> "Record" | Structure -> "Structure" | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" | Class _ -> "Class" | Variant -> "Variant" in diff --git a/vernac/record.ml b/vernac/record.ml index 27bd390714..3e44cd85cc 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -622,7 +622,7 @@ let add_inductive_class env sigma ind = let env = push_context ~strict:false (Univ.AUContext.repr univs) env in let env = push_rel_context ctx env in let inst = Univ.make_abstract_instance univs in - let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in + let ty = Inductive.type_of_inductive ((mind, oneind), inst) in let r = Inductive.relevance_of_inductive env ind in { cl_univs = univs; cl_impl = GlobRef.IndRef ind; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f8eef68997..e469323f50 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -623,16 +623,18 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && is_polymorphic_inductive_cumulativity () -let get_uniform_inductive_parameters = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Uniform"; "Inductive"; "Parameters"] - ~value:false - -let should_treat_as_uniform () = - if get_uniform_inductive_parameters () - then ComInductive.UniformParameters - else ComInductive.NonUniformParameters +let uniform_att = + let get_uniform_inductive_parameters = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Uniform"; "Inductive"; "Parameters"] + ~value:false + in + let open Attributes.Notations in + Attributes.bool_attribute ~name:"uniform" ~on:"uniform" ~off:"nonuniform" >>= fun u -> + let u = match u with Some u -> u | None -> get_uniform_inductive_parameters () in + let u = if u then ComInductive.UniformParameters else ComInductive.NonUniformParameters in + return u let vernac_record ~template udecl cum k poly finite records = let cumulative = should_treat_as_cumulative cum poly in @@ -661,25 +663,29 @@ let vernac_record ~template udecl cum k poly finite records = let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) = match indl with | [] -> assert false - | (((coe,(id,udecl)),b,c,k,d),e) :: rest -> - let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) -> + | (((coe,(id,udecl)),b,c,d),e) :: rest -> + let rest = List.map (fun (((coe,(id,udecl)),b,c,d),e) -> if Option.has_some udecl then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.") - else (((coe,id),b,c,k,d),e)) + else (((coe,id),b,c,d),e)) rest in - udecl, (((coe,id),b,c,k,d),e) :: rest + udecl, (((coe,id),b,c,d),e) :: rest + +let finite_of_kind = let open Declarations in function + | Inductive_kw -> Finite + | CoInductive -> CoFinite + | Variant | Record | Structure | Class _ -> BiFinite (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) -let vernac_inductive ~atts cum lo finite indl = - let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in +let vernac_inductive ~atts cum lo kind indl = let open Pp in let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then - List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> + List.iter (fun (((coe,lid), _, _, cstrs), _) -> match cstrs with | Constructors cstrs -> Dumpglob.dump_definition lid false "ind"; @@ -688,16 +694,17 @@ let vernac_inductive ~atts cum lo finite indl = | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; + let finite = finite_of_kind kind in let is_record = function - | ((_ , _ , _ , _, RecordDecl _), _) -> true + | ((_ , _ , _ , RecordDecl _), _) -> true | _ -> false in let is_constructor = function - | ((_ , _ , _ , _, Constructors _), _) -> true + | ((_ , _ , _ , Constructors _), _) -> true | _ -> false in - let is_defclass = match indl with - | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l) + let is_defclass = match kind, indl with + | Class _, [ ( id , bl , c , Constructors [l]), [] ] -> Some (id, bl, c, l) | _ -> None in if Option.has_some is_defclass then @@ -706,42 +713,42 @@ let vernac_inductive ~atts cum lo finite indl = let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), - { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in + { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } + in + let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) - let check_kind ((_, _, _, kind, _), _) = match kind with - | Variant -> - user_err (str "The Variant keyword does not support syntax { ... }.") - | Record | Structure | Class _ | Inductive_kw | CoInductive -> () + let () = match kind with + | Variant -> + user_err (str "The Variant keyword does not support syntax { ... }.") + | Record | Structure | Class _ | Inductive_kw | CoInductive -> () in - let () = List.iter check_kind indl in - let check_where ((_, _, _, _, _), wh) = match wh with + let check_where ((_, _, _, _), wh) = match wh with | [] -> () | _ :: _ -> user_err (str "where clause not supported for records") in let () = List.iter check_where indl in - let unpack ((id, bl, c, _, decl), _) = match decl with + let unpack ((id, bl, c, decl), _) = match decl with | RecordDecl (oc, fs) -> (id, bl, c, oc, fs) | Constructors _ -> assert false (* ruled out above *) in - let ((_, _, _, kind, _), _) = List.hd indl in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in + let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in vernac_record ~template udecl cum kind poly finite recordl else if List.for_all is_constructor indl then (* Mutual inductive case *) - let check_kind ((_, _, _, kind, _), _) = match kind with + let () = match kind with | (Record | Structure) -> user_err (str "The Record keyword is for types defined using the syntax { ... }.") | Class _ -> user_err (str "Inductive classes not supported") | Variant | Inductive_kw | CoInductive -> () in - let () = List.iter check_kind indl in - let check_name ((na, _, _, _, _), _) = match na with + let check_name ((na, _, _, _), _) = match na with | (true, _) -> user_err (str "Variant types do not handle the \"> Name\" \ syntax, which is reserved for records. Use the \":>\" \ @@ -749,26 +756,19 @@ let vernac_inductive ~atts cum lo finite indl = | _ -> () in let () = List.iter check_name indl in - let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with + let unpack (((_, id) , bl, c, decl), ntn) = match decl with | Constructors l -> (id, bl, c, l), ntn | RecordDecl _ -> assert false (* ruled out above *) in let indl = List.map unpack indl in + let (template, poly), uniform = + Attributes.(parse Notations.(template ++ polymorphic ++ uniform_att) atts) + in let cumulative = should_treat_as_cumulative cum poly in - let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly + ~private_ind:lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") -(* - - match indl with - | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> - let f = - let (coe, ({loc;v=id}, ce)) = l in - let coe' = if coe then Some true else None in - (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), []) - in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] - *) let vernac_fixpoint_common ~atts discharge l = if Dumpglob.dump () then diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 22a8de7f99..8ead56dfdf 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -104,7 +104,6 @@ type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) -type inductive_flag = Declarations.recursivity_kind type onlyparsing_flag = { onlyparsing : bool } (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version @@ -165,7 +164,7 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * (local_decl_expr * record_field_attr) list type inductive_expr = - ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * + ident_decl with_coercion * local_binder_expr list * constr_expr option * constructor_list_or_record_decl_expr type one_inductive_expr = @@ -306,7 +305,7 @@ type nonrec vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_kind * (inductive_expr * decl_notation list) list | VernacFixpoint of discharge * fixpoint_expr list | VernacCoFixpoint of discharge * cofixpoint_expr list | VernacScheme of (lident option * scheme) list |