From 552bb5aba750785d8f19aa7b333baa59e9199369 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 20 Oct 2018 14:40:23 +0200
Subject: Add parsing of decimal constants (e.g., 1.02e+01)

Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.

This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`

See examples of each use case in the next two commits.
---
 test-suite/output/SearchPattern.out | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'test-suite/output/SearchPattern.out')

diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index b0ac9ea29f..4cd0ffb1dc 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -19,30 +19,31 @@ Nat.div2: nat -> nat
 Nat.log2: nat -> nat
 Nat.succ: nat -> nat
 Nat.sqrt: nat -> nat
+S: nat -> nat
 Nat.pred: nat -> nat
 Nat.double: nat -> nat
 Nat.square: nat -> nat
-S: nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.tail_add: nat -> nat -> nat
 Nat.land: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.mul: nat -> nat -> nat
 Nat.tail_mul: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
 Nat.max: nat -> nat -> nat
 Nat.sub: nat -> nat -> nat
-Nat.mul: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-Nat.add: nat -> nat -> nat
+Nat.ldiff: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
 Nat.of_uint: Decimal.uint -> nat
+Decimal.nb_digits: Decimal.uint -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
 Nat.of_uint_acc: Decimal.uint -> nat -> nat
-Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
+Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 length: forall A : Type, list A -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 Nat.div2: nat -> nat
-- 
cgit v1.2.3