----------------------------------------------------------------------
add_bare_numeral_form                                          (Parse)
----------------------------------------------------------------------
add_bare_numeral_form : (char * string option) -> unit

SYNOPSIS
Adds support for annotated numerals to the parser/pretty-printer.

KEYWORDS
Parsing, pretty-printing.

LIBRARY
Parse

DESCRIBE
The function {add_bare_numeral_form} allows the user to give special
meaning to strings of digits that are suffixed with single characters.
A call to this function with pair argument {(c, s)} adds {c} as a
possible suffix.  Subsequently, if a sequence of digits is parsed, and
it has the character {c} directly after the digits, then the natural
number corresponding to these digits is made the argument of the
“map function” corresponding to {s}.

This map function is computed as follows: if the {s} option value is
{NONE}, then the function is considered to be the identity and never
really appears; the digits denote a natural number.  If the value of
{s} is {SOME s'}, then the parser translates the string to an
application of {s'} to the natural number denoted by the digits.

FAILURE
Fails if the suffix character is not a letter.

EXAMPLE
The following function, {binary_of}, defined with equations:

   val bthm =
     |- binary_of n = if n = 0 then 0
                      else n MOD 10 + 2 * binary_of (n DIV 10) : thm

can be used to convert numbers whose decimal notation is
{x}, to numbers whose binary notation is {x} (as long as {x} only
involves zeroes and ones).

The following call to {add_bare_numeral_form} then sets up a numeral
form that could be used by users wanting to deal with binary numbers:

   - add_bare_numeral_form(#"b", SOME "binary_of");
   > val it = () : unit

   - Term`1011b`;
   > val it = `1011b` : term

   - dest_comb it;
   > val it = (`binary_of`, `1011`) : term * term


COMMENTS
It is highly recommended that users avoid using suffixes that
might be interpreted as hexadecimal digits A to F, in either upper or
lower case.  Further, HOL convention has it that suffix character
should be lower case.

USES
If one has a range of values that are usefully indexed by natural
numbers, the function {add_bare_numeral_form} provides a syntactically
convenient way of reading and writing these values.  If there are
other functions in the range type such that the mapping function is a
homomorphism from the natural numbers, then {add_numeral_form} could
be used, and the appropriate operators ({+}, {*} etc) overloaded.

SEEALSO
Parse.add_numeral_form.

----------------------------------------------------------------------