diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 3f955403f7e13..83240abb4ac09 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1175,6 +1175,19 @@ Exposing constants to OCaml libraries List the currently registered constants. +.. cmd:: Register Scheme @qualid__1 as @qualid__2 for @qualid__3 + + Make the constant :n:`@qualid__1` accessible to the "scheme" + mechanism for scheme kind :n:`@qualid__2` and inductive + :n:`@qualid__3`. + +.. cmd:: Print Registered Schemes + + List the currently registered constants. + + This can be useful to find information about the (currently + undocumented) scheme kinds. + Inlining hints for the fast reduction machines `````````````````````````````````````````````` diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 06bd1cb772121..3dc36168af7a8 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -817,6 +817,7 @@ gallina: [ | "Scheme" "Boolean" "Equality" "for" smart_global | "Combined" "Scheme" identref "from" LIST1 identref SEP "," | "Register" global "as" qualid +| "Register" "Scheme" global "as" qualid "for" global | "Register" "Inline" global | "Primitive" ident_decl OPT [ ":" lconstr ] ":=" register_token | "Universe" LIST1 identref @@ -1319,6 +1320,7 @@ printable: [ | "Strategy" smart_global | "Strategies" | "Registered" +| "Registered" "Schemes" ] printunivs_subgraph: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index cd07e06667248..f47ccc12880a7 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -764,6 +764,7 @@ command: [ | "Print" "Strategy" reference | "Print" "Strategies" | "Print" "Registered" +| "Print" "Registered" "Schemes" | "Print" OPT "Term" reference OPT univ_name_list | "Print" "Module" "Type" qualid | "Print" "Module" qualid @@ -899,6 +900,7 @@ command: [ | "Scheme" OPT "Boolean" "Equality" "for" reference | "Combined" "Scheme" ident "from" LIST1 ident SEP "," | "Register" qualid "as" qualid +| "Register" "Scheme" qualid "as" qualid "for" qualid | "Register" "Inline" qualid | "Primitive" ident_decl OPT [ ":" term ] ":=" "#" ident | "Universe" LIST1 ident diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index bac9800e0caae..0b5cb98a587d6 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -264,6 +264,8 @@ GRAMMAR EXTEND Gram l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) } | IDENT "Register"; g = global; "as"; quid = qualid -> { VernacRegister(g, RegisterCoqlib quid) } + | IDENT "Register"; IDENT "Scheme"; g = global; "as"; qid = qualid; IDENT "for"; g' = global -> + { VernacRegister(g, RegisterScheme {inductive = g'; scheme_kind = qid}) } | IDENT "Register"; IDENT "Inline"; g = global -> { VernacRegister(g, RegisterInline) } | IDENT "Primitive"; id = ident_decl; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token -> @@ -1092,6 +1094,7 @@ GRAMMAR EXTEND Gram | IDENT "Strategy"; qid = smart_global -> { PrintStrategy (Some qid) } | IDENT "Strategies" -> { PrintStrategy None } | IDENT "Registered" -> { PrintRegistered } + | IDENT "Registered"; IDENT "Schemes" -> { PrintRegisteredSchemes } ] ] ; printunivs_subgraph: diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 2810b6718431c..c4f1e313aef55 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -667,6 +667,8 @@ let pr_printable = function keyword "Print Strategy" ++ pr_smart_global qid | PrintRegistered -> keyword "Print Registered" + | PrintRegisteredSchemes -> + keyword "Print Registered Schemes" | PrintNotation (Constrexpr.InConstrEntry, ntn_key) -> keyword "Print Notation" ++ spc() ++ str ntn_key | PrintNotation (Constrexpr.InCustomEntry ent, ntn_key) -> @@ -1209,6 +1211,12 @@ let pr_synpure_vernac_expr v = (keyword "Register" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as" ++ spc () ++ pr_qualid name) ) + | VernacRegister (qid, RegisterScheme {inductive; scheme_kind}) -> + return ( + hov 2 + (keyword "Register" ++ spc() ++ keyword "Scheme" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as" + ++ spc () ++ pr_qualid scheme_kind ++ spc() ++ str "for" ++ spc() ++ pr_qualid inductive) + ) | VernacRegister (qid, RegisterInline) -> return ( hov 2 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b7dafbd7f6f07..b4f73a030c8a2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -311,6 +311,16 @@ let print_registered () = in hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ()) +let print_registered_schemes () = + let schemes = DeclareScheme.all_schemes() in + let pr_one_scheme ind (kind, c) = + pr_global (ConstRef c) ++ str " registered as " ++ str kind ++ str " for " ++ pr_global (IndRef ind) + in + let pr_schemes_of_ind (ind, schemes) = + prlist_with_sep fnl (pr_one_scheme ind) (CString.Map.bindings schemes) + in + hov 0 (prlist_with_sep fnl pr_schemes_of_ind (Indmap.bindings schemes)) + let dump_universes output g = let open Univ in let dump_arc u = function @@ -2019,6 +2029,7 @@ let vernac_print ~pstate = Printer.pr_assumptionset env sigma nassums | PrintStrategy r -> print_strategy r | PrintRegistered -> print_registered () + | PrintRegisteredSchemes -> print_registered_schemes () let vernac_search ~pstate ~atts s gopt r = let open ComSearch in @@ -2048,13 +2059,16 @@ let vernac_locate ~pstate = let open Constrexpr in function | LocateOther (s, qid) -> Prettyp.print_located_other s qid | LocateFile f -> locate_file f +let warn_unknown_scheme_kind = CWarnings.create ~name:"unknown-scheme-kind" + Pp.(fun sk -> str "Unknown scheme kind " ++ Libnames.pr_qualid sk ++ str ".") + let vernac_register qid r = let gr = Smartlocate.global_with_alias qid in match r with | RegisterInline -> begin match gr with | GlobRef.ConstRef c -> Global.register_inline c - | _ -> CErrors.user_err (Pp.str "Register Inline: expecting a constant.") + | _ -> CErrors.user_err ?loc:qid.loc (Pp.str "Register Inline: expecting a constant.") end | RegisterCoqlib n -> let ns, id = Libnames.repr_qualid n in @@ -2068,13 +2082,25 @@ let vernac_register qid r = | "ind_cmp" -> CPrimitives.(PIE PIT_cmp) | "ind_f_cmp" -> CPrimitives.(PIE PIT_f_cmp) | "ind_f_class" -> CPrimitives.(PIE PIT_f_class) - | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the \"kernel\" namespace.") + | k -> CErrors.user_err ?loc:n.loc Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the \"kernel\" namespace.") in match gr with | GlobRef.IndRef ind -> Global.register_inductive ind pind - | _ -> CErrors.user_err (Pp.str "Register in kernel: expecting an inductive type.") + | _ -> CErrors.user_err ?loc:qid.loc (Pp.str "Register in kernel: expecting an inductive type.") end else Coqlib.register_ref (Libnames.string_of_qualid n) gr + | RegisterScheme { inductive; scheme_kind } -> + let gr = match gr with + | ConstRef c -> c + | _ -> CErrors.user_err ?loc:qid.loc Pp.(str "Register Scheme: expecing a constant.") + in + let scheme_kind_s = Libnames.string_of_qualid scheme_kind in + let () = if not (Ind_tables.is_declared_scheme_object scheme_kind_s) then + warn_unknown_scheme_kind ?loc:scheme_kind.loc scheme_kind + in + let ind = Smartlocate.global_inductive_with_alias inductive in + Dumpglob.add_glob ?loc:inductive.loc (IndRef ind); + DeclareScheme.declare_scheme scheme_kind_s (ind,gr) (********************) (* Proof management *) diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli index 25abfa90417b2..e48175ff9a1b7 100644 --- a/vernac/vernacexpr.mli +++ b/vernac/vernacexpr.mli @@ -63,6 +63,7 @@ type printable = | PrintAssumptions of bool * bool * qualid or_by_notation | PrintStrategy of qualid or_by_notation option | PrintRegistered + | PrintRegisteredSchemes | PrintNotation of Constrexpr.notation_entry * string type glob_search_where = InHyp | InConcl | Anywhere @@ -297,6 +298,7 @@ type section_subset_expr = type register_kind = | RegisterInline | RegisterCoqlib of qualid + | RegisterScheme of { inductive : qualid; scheme_kind : qualid } (** {6 Types concerning the module layer} *)