new command Register Scheme

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
 ``````````````````````````````````````````````
 

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: [

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

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:

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

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 *)

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} *)