|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
DECLARE PLUGIN "rocq-runtime.plugins.number_string_notation"
{
open Notation
open Number_string
open Pp
open Stdarg
open Procq.Prim
let pr_number_after = function
| Nop -> mt ()
| Warning n -> str "warning after " ++ NumTok.UnsignedNat.print n
| Abstract n -> str "abstract after " ++ NumTok.UnsignedNat.print n
let pr_number_string_mapping (b, n, n') =
if b then
str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc ()
++ Libnames.pr_qualid n'
else
Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc ()
++ Libnames.pr_qualid n'
let pr_number_string_via (n, l) =
str "via " ++ Libnames.pr_qualid n ++ str " mapping ["
++ prlist_with_sep pr_comma pr_number_string_mapping l ++ str "]"
let pr_number_modifier = function
| After a -> pr_number_after a
| Via nl -> pr_number_string_via nl
let pr_number_options l =
str "(" ++ prlist_with_sep pr_comma pr_number_modifier l ++ str ")"
let pr_string_option l =
str "(" ++ pr_number_string_via l ++ str ")"
}
VERNAC ARGUMENT EXTEND number_string_mapping
PRINTED BY { pr_number_string_mapping }
| [ reference(n) "=>" reference(n') ] -> { false, n, n' }
| [ "[" reference(n) "]" "=>" reference(n') ] -> { true, n, n' }
END
VERNAC ARGUMENT EXTEND number_string_via
PRINTED BY { pr_number_string_via }
| [ "via" reference(n) "mapping" "[" ne_number_string_mapping_list_sep(l, ",") "]" ] -> { n, l }
END
VERNAC ARGUMENT EXTEND number_modifier
PRINTED BY { pr_number_modifier }
| [ "warning" "after" bignat(waft) ] -> { After (Warning (NumTok.UnsignedNat.of_string waft)) }
| [ "abstract" "after" bignat(n) ] -> { After (Abstract (NumTok.UnsignedNat.of_string n)) }
| [ number_string_via(v) ] -> { Via v }
END
VERNAC ARGUMENT EXTEND number_options
PRINTED BY { pr_number_options }
| [ "(" ne_number_modifier_list_sep(l, ",") ")" ] -> { l }
END
VERNAC ARGUMENT EXTEND string_option
PRINTED BY { pr_string_option }
| [ "(" number_string_via(v) ")" ] -> { v }
END
VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF
| #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) number_options_opt(nl) ":"
preident(sc) ] ->
{ vernac_number_notation (Locality.make_module_locality locality) ty f g (Option.default [] nl) sc }
END
VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
| #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) string_option_opt(o) ":"
preident(sc) ] ->
{ vernac_string_notation (Locality.make_module_locality locality) ty f g o sc }
END
[ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
]
|
