diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comAssumption.ml | 25 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 24 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 24 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 15 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 22 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 1 |
8 files changed, 73 insertions, 48 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e5db6146ca..a001420f74 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -22,24 +22,6 @@ open Entries module RelDecl = Context.Rel.Declaration (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let axiom_into_instance = ref false - -let () = - let open Goptions in - declare_bool_option - { optdepr = true; - optname = "automatically declare axioms whose type is a typeclass as instances"; - optkey = ["Typeclasses";"Axioms";"Are";"Instances"]; - optread = (fun _ -> !axiom_into_instance); - optwrite = (:=) axiom_into_instance; } - -let should_axiom_into_instance = let open Decls in function - | Context -> - (* The typeclass behaviour of Variable and Context doesn't depend - on section status *) - true - | Definitional | Logical | Conjectural -> !axiom_into_instance - let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let kind = Decls.IsAssumption kind in let decl = Declare.SectionLocalAssum {typ; impl} in @@ -58,7 +40,12 @@ let instance_of_univ_entry = function | Monomorphic_entry _ -> Univ.Instance.empty let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} = - let do_instance = should_axiom_into_instance kind in + let do_instance = let open Decls in match kind with + | Context -> true + (* The typeclass behaviour of Variable and Context doesn't depend + on section status *) + | Definitional | Logical | Conjectural -> false + in let inl = let open Declaremods in match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 80fcb7bc45..2aee9bd47f 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -323,7 +323,7 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg -let template_polymorphism_candidate env uctx params concl = +let template_polymorphism_candidate env ~ctor_levels uctx params concl = match uctx with | Entries.Monomorphic_entry uctx -> let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in @@ -331,7 +331,9 @@ let template_polymorphism_candidate env uctx params concl = else let template_check = Environ.check_template env in let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in - let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in + let params, conclunivs = + IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu + in not (template_check && Univ.LSet.is_empty conclunivs) | Entries.Polymorphic_entry _ -> false @@ -376,14 +378,24 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) -> let template_candidate () = - templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in + templatearity || + let ctor_levels = + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty ctx_params + in + List.fold_left (fun levels c -> add_levels c levels) + param_levels ctypes + in + template_polymorphism_candidate env0 ~ctor_levels uctx ctx_params concl + in let template = match template with | Some template -> if poly && template then user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "Inductive " ++ Id.print indname ++ - str" cannot be made template polymorphic."); template | None -> should_auto_template indname (template_candidate ()) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 45e539b1e4..ef05b213d8 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -77,12 +77,18 @@ val should_auto_template : Id.t -> bool -> bool automatically use template polymorphism. [x] is the name of the inductive under consideration. *) -val template_polymorphism_candidate : - Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate env uctx params conclsort] is - [true] iff an inductive with params [params] and conclusion - [conclsort] would be definable as template polymorphic. It should - have at least one universe in its monomorphic universe context that - can be made parametric in its conclusion sort, if one is given. - If the [Template Check] flag is false we just check that the conclusion sort - is not small. *) +val template_polymorphism_candidate + : Environ.env + -> ctor_levels:Univ.LSet.t + -> Entries.universes_entry + -> Constr.rel_context + -> Sorts.t option + -> bool +(** [template_polymorphism_candidate env ~ctor_levels uctx params + conclsort] is [true] iff an inductive with params [params], + conclusion [conclsort] and universe levels appearing in the + constructor arguments [ctor_levels] would be definable as template + polymorphic. It should have at least one universe in its + monomorphic universe context that can be made parametric in its + conclusion sort, if one is given. If the [Template Check] flag is + false we just check that the conclusion sort is not small. *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 5b97e06b2b..5f088379ca 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -63,7 +63,8 @@ let make_bullet s = | _ -> assert false let parse_compat_version = let open Flags in function - | "8.11" -> Current + | "8.12" -> Current + | "8.11" -> V8_11 | "8.10" -> V8_10 | "8.9" -> V8_9 | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> @@ -938,15 +939,7 @@ GRAMMAR EXTEND Gram | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> { VernacRemoveLoadPath dir } - (* For compatibility *) - | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath -> - { VernacAddLoadPath (false, dir, alias) } - | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath -> - { VernacAddLoadPath (true, dir, alias) } - | IDENT "DelPath"; dir = ne_string -> - { VernacRemoveLoadPath dir } - - (* Type-Checking (pas dans le refman) *) + (* Type-Checking *) | "Type"; c = lconstr -> { VernacGlobalCheck c } (* Printing (careful factorization of entries) *) @@ -1010,7 +1003,7 @@ GRAMMAR EXTEND Gram | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> { fun g -> VernacSearch (SearchRewrite c,g, l) } | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> - { let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) } + { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) } (* compatibility: SearchAbout *) | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 080629ede2..1aa9a4e0f5 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -161,6 +161,8 @@ open Pputils | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchAbout sl -> + keyword "SearchAbout" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + | Search sl -> keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b let pr_option_ref_value = function diff --git a/vernac/record.ml b/vernac/record.ml index 49a73271f0..d85b71df44 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -429,15 +429,31 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let type_constructor = it_mkProd_or_LetIn ind fields in let template = let template_candidate () = - ComInductive.template_polymorphism_candidate (Global.env ()) univs params + (* we use some dummy values for the arities in the rel_context + as univs_of_constr doesn't care about localassums and + getting the real values is too annoying *) + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + let ctor_levels = List.fold_left + (fun univs d -> + let univs = + RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs + in + univs) + param_levels fields + in + ComInductive.template_polymorphism_candidate (Global.env ()) ~ctor_levels univs params (Some (Sorts.sort_of_univ min_univ)) in match template with | Some template, _ -> (* templateness explicitly requested *) if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "record cannot be made template polymorphic on any universe"); template | None, template -> (* auto detect template *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 535aceed15..bb55cd5114 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1785,6 +1785,10 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } +let warn_deprecated_search_about = + CWarnings.create ~name:"deprecated-search-about" ~category:"deprecated" + (fun () -> strbrk "The SearchAbout command is deprecated. Please use Search instead.") + let vernac_search ~pstate ~atts s gopt r = let gopt = query_command_selector gopt in let r = interp_search_restriction r in @@ -1815,6 +1819,10 @@ let vernac_search ~pstate ~atts s gopt r = | SearchHead c -> (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchAbout sl -> + warn_deprecated_search_about (); + (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + Search.prioritize_search) pr_search + | Search sl -> (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> Search.prioritize_search) pr_search diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ce96d9265c..bec6a0d2bb 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -70,6 +70,7 @@ type searchable = | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr | SearchAbout of (bool * search_about_item) list + | Search of (bool * search_about_item) list type locatable = | LocateAny of qualid or_by_notation |