Numeral Notation: allow parsing from/to Decimal.int or Decimal.uint

 This way, we could fully bypass bigint.ml.

 The previous mechanism of parsing/printing Z is kept for now.
 Currently, the conversion functions accepted by Numeral Notation foo
 may have the following types.

 for parsing:

   int -> foo
   int -> option foo
   uint -> foo
   uint -> option foo
   Z -> foo
   Z -> option foo

 for printing:

   foo -> int
   foo -> option int
   foo -> uint
   foo -> option uint
   foo -> Z
   foo -> option Z

 Notes:

  - The Declare ML Module is directly done in Prelude
  - When doing a Numeral Notation, having the Z datatype around
    isn't mandatory anymore (but the error messages suggest that
    it can still be used).
  - An option (abstract after ...) allows to keep large numbers in
    an abstract form such as (Nat.of_uint 123456) instead of reducing
    to (S (S (S ...))) and ending immediately with Stack Overflow.
  - After checking with Matthieu, there is now a explicit check
    and an error message in case of polymorphic inductive types

0 files changed, 0 insertions, 0 deletions