diff options
| -rw-r--r-- | library/decl_kinds.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 16 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 32 | ||||
| -rw-r--r-- | vernac/record.ml | 14 | ||||
| -rw-r--r-- | vernac/record.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
8 files changed, 42 insertions, 40 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 5c479255df..17746645ee 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -8,10 +8,4 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Informal mathematical status of declarations *) - type binding_kind = Explicit | Implicit - -type private_flag = bool - -type cumulative_inductive_flag = bool diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index bb4e745fe9..bcad6cedf1 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1506,7 +1506,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false ~poly:false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds ~cumulative:false ~poly:false ~private_ind:false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 283e5ff50a..d99d3e65fd 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -349,7 +349,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum ~poly prv finite = +let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite = check_all_names_different indl; List.iter check_param paramsl; if not (List.is_empty uparamsl) && not (List.is_empty notations) @@ -453,24 +453,24 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indimpls, List.map (fun impls -> userimpls @ impls) cimpls) indimpls constructors in - let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in + let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; mind_entry_record = None; mind_entry_finite = finite; mind_entry_inds = entries; - mind_entry_private = if prv then Some false else None; + mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; mind_entry_variance = variance; } in - (if poly && cum then + (if poly && cumulative then InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum ~poly prv finite = - interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum ~poly prv finite +let interp_mutual_inductive ~template udecl (paramsl,indl) notations ~cumulative ~poly ~private_ind finite = + interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations ~cumulative ~poly ~private_ind finite (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -564,11 +564,11 @@ type uniform_inductive_flag = | UniformParameters | NonUniformParameters -let do_mutual_inductive ~template udecl indl cum ~poly prv ~uniform finite = +let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite = let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) 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 cum ~poly prv finite 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); (* Declare the possible notations of inductive types *) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 2d4cd7cac2..97f930c0a1 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -13,7 +13,6 @@ open Entries open Libnames open Vernacexpr open Constrexpr -open Decl_kinds (** {6 Inductive and coinductive types} *) @@ -23,11 +22,16 @@ type uniform_inductive_flag = | UniformParameters | NonUniformParameters -val do_mutual_inductive : - template:bool option -> universe_decl_expr option -> - (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - poly:bool -> private_flag -> uniform:uniform_inductive_flag -> - Declarations.recursivity_kind -> unit +val do_mutual_inductive + : template:bool option + -> universe_decl_expr option + -> (one_inductive_expr * decl_notation list) list + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> uniform:uniform_inductive_flag + -> Declarations.recursivity_kind + -> unit (************************************************************************) (** Internal API *) @@ -71,12 +75,16 @@ val extract_mutual_inductive_declaration_components : structured_inductive_expr * (*coercions:*) qualid list * decl_notation list (** Typing mutual inductive definitions *) - -val interp_mutual_inductive : - template:bool option -> universe_decl_expr option -> structured_inductive_expr -> - decl_notation list -> cumulative_inductive_flag -> - poly:bool -> private_flag -> Declarations.recursivity_kind -> - mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list +val interp_mutual_inductive + : template:bool option + -> universe_decl_expr option + -> structured_inductive_expr + -> decl_notation list + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> Declarations.recursivity_kind + -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name diff --git a/vernac/record.ml b/vernac/record.ml index 7c29130383..fe89303d33 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -401,7 +401,7 @@ let inStruc : Recordops.struc_tuple -> obj = let declare_structure_entry o = Lib.add_anonymous_leaf (inStruc o) -let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=Decls.StructureComponent) ?name record_data = +let declare_structure ~cumulative finite ubinders univs paramimpls params template ?(kind=Decls.StructureComponent) ?name record_data = let nparams = List.length params in let poly, ctx = match univs with @@ -410,7 +410,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki | Polymorphic_entry (nas, ctx) -> true, Polymorphic_entry (nas, ctx) in - let variance = if poly && cum then Some (InferCumulativity.dummy_variance ctx) else None in + let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance ctx) else None in let binder_name = match name with | None -> @@ -479,7 +479,7 @@ let implicits_of_context ctx = List.map (fun name -> CAst.make (Some (name,true))) (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class def cum ubinders univs id idbuild paramimpls params arity +let declare_class def cumulative ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -526,7 +526,7 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity | _ -> let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in - let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls + let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls params template ~kind:Decls.Method ~name:[|binder_name|] record_data in let coers = List.map2 (fun coe pri -> @@ -679,7 +679,7 @@ let extract_record_data records = (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances. *) -let definition_structure udecl kind ~template cum ~poly finite records = +let definition_structure udecl kind ~template ~cumulative ~poly finite records = let () = check_unique_names records in let () = check_priorities kind records in let ps, data = extract_record_data records in @@ -695,7 +695,7 @@ let definition_structure udecl kind ~template cum ~poly finite records = in let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in - declare_class def cum ubinders univs id.CAst.v idbuild + declare_class def cumulative ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> let map impls = implpars @ [CAst.make None] @ impls in @@ -709,5 +709,5 @@ let definition_structure udecl kind ~template cum ~poly finite records = id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in - let inds = declare_structure ~cum finite ubinders univs implpars params template data in + let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in List.map (fun ind -> IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index 3165448d0c..571fd9536e 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -35,7 +35,7 @@ val definition_structure : universe_decl_expr option -> inductive_kind -> template:bool option - -> Decl_kinds.cumulative_inductive_flag + -> cumulative:bool -> poly:bool -> Declarations.recursivity_kind -> (coercion_flag * diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index cfa25b03bc..335075e1e0 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -635,7 +635,7 @@ let should_treat_as_uniform () = else ComInductive.NonUniformParameters let vernac_record ~template udecl cum k poly finite records = - let is_cumulative = should_treat_as_cumulative cum poly in + let cumulative = should_treat_as_cumulative cum poly in let map ((coe, id), binders, sort, nameopt, cfs) = let const = match nameopt with | None -> add_prefix "Build_" id.v @@ -656,7 +656,7 @@ let vernac_record ~template udecl cum k poly finite records = coe, id, binders, cfs, const, sort in let records = List.map map records in - ignore(Record.definition_structure ~template udecl k is_cumulative ~poly finite records) + ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records) let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) = match indl with @@ -754,9 +754,9 @@ let vernac_inductive ~atts cum lo finite indl = | RecordDecl _ -> assert false (* ruled out above *) in let indl = List.map unpack indl in - let is_cumulative = should_treat_as_cumulative cum poly in + let cumulative = should_treat_as_cumulative cum poly in let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template udecl indl is_cumulative ~poly 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") (* diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index eb1bca410a..ee1f839b8d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -282,7 +282,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 * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list |