Parse.add_bare_numeral

STRUCTURE

SYNOPSIS

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

LIBRARY

Parse

DESCRIPTION

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

add_numeral_form