Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990(************************************************************************)(* * 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 PrimNotationsopen Number_stringopen Ppopen Stdargopen 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