From 1923e2a87e8754e63e8d9edcdfe178a841ff96d2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 24 Oct 2019 21:06:54 +0200 Subject: [inductive] [declare] Move full inductive declaration to declareInd Patch suggested by Gaëtan Gilbert --- vernac/comInductive.ml | 68 +++---------------------------------------------- vernac/comInductive.mli | 21 ++++++--------- vernac/declareInd.ml | 63 +++++++++++++++++++++++++++++++++++++++++++++ vernac/declareInd.mli | 17 ++++++++++--- vernac/record.ml | 2 +- 5 files changed, 88 insertions(+), 83 deletions(-) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 24a141510e..cee5b7c1f4 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -21,11 +21,9 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Impargs open Reductionops open Type_errors open Pretyping -open Indschemes open Context.Rel.Declaration open Entries @@ -79,12 +77,6 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } -let minductive_message = function - | [] -> user_err Pp.(str "No inductive definition.") - | [x] -> (Id.print x ++ str " is defined") - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are defined") - let check_all_names_different indl = let ind_names = List.map (fun ind -> ind.ind_name) indl in let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in @@ -540,62 +532,6 @@ let extract_mutual_inductive_declaration_components indl = let indl = extract_inductive indl in (params,indl), coes, List.flatten ntnl -let is_recursive mie = - let rec is_recursive_constructor lift typ = - match Constr.kind typ with - | Prod (_,arg,rest) -> - not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || - is_recursive_constructor (lift+1) rest - | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest - | _ -> false - in - match mie.mind_entry_inds with - | [ind] -> - let nparams = List.length mie.mind_entry_params in - List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc - | _ -> false - -let warn_non_primitive_record = - CWarnings.create ~name:"non-primitive-record" ~category:"record" - (fun indsp -> - (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++ - strbrk" could not be defined as a primitive record"))) - -let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls = - (* spiwack: raises an error if the structure is supposed to be non-recursive, - but isn't *) - begin match mie.mind_entry_finite with - | Declarations.BiFinite when is_recursive mie -> - if Option.has_some mie.mind_entry_record then - user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") - else - user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) - | _ -> () - end; - let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_, kn), prim = DeclareInd.declare_mind mie in - let mind = Global.mind_of_delta_kn kn in - if primitive_expected && not prim then warn_non_primitive_record (mind,0); - DeclareUniv.declare_univ_binders (GlobRef.IndRef (mind,0)) pl; - List.iteri (fun i (indimpls, constrimpls) -> - let ind = (mind,i) in - let gr = GlobRef.IndRef ind in - maybe_declare_manual_implicits false gr indimpls; - List.iteri - (fun j impls -> - maybe_declare_manual_implicits false - (GlobRef.ConstructRef (ind, succ j)) impls) - constrimpls) - impls; - Flags.if_verbose Feedback.msg_info (minductive_message names); - if mie.mind_entry_private == None - then declare_default_schemes mind; - mind - -type one_inductive_impls = - Impargs.manual_implicits (* for inds *) * - Impargs.manual_implicits list (* for constrs *) - type uniform_inductive_flag = | UniformParameters | NonUniformParameters @@ -606,7 +542,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in (* Declare the mutual inductive block with its associated schemes *) - ignore (declare_mutual_inductive_with_eliminations mie pl impls); + ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) @@ -651,3 +587,5 @@ let make_cases ind = let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) mip.mind_nf_lc [] + +let declare_mutual_inductive_with_eliminations = DeclareInd.declare_mutual_inductive_with_eliminations diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7587bd165f..3e1e9ceaf1 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Entries open Vernacexpr open Constrexpr @@ -42,22 +41,18 @@ val do_mutual_inductive val make_cases : Names.inductive -> string list list +val declare_mutual_inductive_with_eliminations + : ?primitive_expected:bool + -> Entries.mutual_inductive_entry + -> UnivNames.universe_binders + -> DeclareInd.one_inductive_impls list + -> Names.MutInd.t + [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] + (************************************************************************) (** Internal API, exported for Record *) (************************************************************************) -(** Registering a mutual inductive definition together with its - associated schemes *) - -type one_inductive_impls = - Impargs.manual_implicits (* for inds *) * - Impargs.manual_implicits list (* for constrs *) - -val declare_mutual_inductive_with_eliminations : - ?primitive_expected:bool -> - mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> - MutInd.t - val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml index 0f18c3b25d..2375028541 100644 --- a/vernac/declareInd.ml +++ b/vernac/declareInd.ml @@ -149,3 +149,66 @@ let declare_mind mie = Impargs.declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; oname, isprim + +let is_recursive mie = + let open Constr in + let rec is_recursive_constructor lift typ = + match Constr.kind typ with + | Prod (_,arg,rest) -> + not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || + is_recursive_constructor (lift+1) rest + | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest + | _ -> false + in + match mie.mind_entry_inds with + | [ind] -> + let nparams = List.length mie.mind_entry_params in + List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc + | _ -> false + +let warn_non_primitive_record = + CWarnings.create ~name:"non-primitive-record" ~category:"record" + (fun indsp -> + Pp.(hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++ + strbrk" could not be defined as a primitive record"))) + +let minductive_message = function + | [] -> CErrors.user_err Pp.(str "No inductive definition.") + | [x] -> Pp.(Id.print x ++ str " is defined") + | l -> Pp.(hov 0 (prlist_with_sep pr_comma Id.print l ++ + spc () ++ str "are defined")) + +type one_inductive_impls = + Impargs.manual_implicits (* for inds *) * + Impargs.manual_implicits list (* for constrs *) + +let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls = + (* spiwack: raises an error if the structure is supposed to be non-recursive, + but isn't *) + begin match mie.mind_entry_finite with + | Declarations.BiFinite when is_recursive mie -> + if Option.has_some mie.mind_entry_record then + CErrors.user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") + else + CErrors.user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) + | _ -> () + end; + let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in + let (_, kn), prim = declare_mind mie in + let mind = Global.mind_of_delta_kn kn in + if primitive_expected && not prim then warn_non_primitive_record (mind,0); + DeclareUniv.declare_univ_binders (GlobRef.IndRef (mind,0)) pl; + List.iteri (fun i (indimpls, constrimpls) -> + let ind = (mind,i) in + let gr = GlobRef.IndRef ind in + Impargs.maybe_declare_manual_implicits false gr indimpls; + List.iteri + (fun j impls -> + Impargs.maybe_declare_manual_implicits false + (GlobRef.ConstructRef (ind, succ j)) impls) + constrimpls) + impls; + Flags.if_verbose Feedback.msg_info (minductive_message names); + if mie.mind_entry_private == None + then Indschemes.declare_default_schemes mind; + mind diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli index 6db09ad2bd..df8895a999 100644 --- a/vernac/declareInd.mli +++ b/vernac/declareInd.mli @@ -8,7 +8,16 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** [declare_mind me] declares a block of inductive types with - their constructors in the current section; it returns the path of - the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : Entries.mutual_inductive_entry -> Libobject.object_name * bool +(** Registering a mutual inductive definition together with its + associated schemes *) + +type one_inductive_impls = + Impargs.manual_implicits (* for inds *) * + Impargs.manual_implicits list (* for constrs *) + +val declare_mutual_inductive_with_eliminations + : ?primitive_expected:bool + -> Entries.mutual_inductive_entry + -> UnivNames.universe_binders + -> one_inductive_impls list + -> Names.MutInd.t diff --git a/vernac/record.ml b/vernac/record.ml index 831fb53549..b60bfdfa22 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -466,7 +466,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa in let mie = InferCumulativity.infer_inductive (Global.env ()) mie in let impls = List.map (fun _ -> paramimpls, []) record_data in - let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls + let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag in let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) = -- cgit v1.2.3