From 692c642672f863546b423d72c714c1417164e506 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 26 Mar 2020 08:20:09 +0100
Subject: Add hexadecimal numerals

We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?

This is unfortunately a rather large commit. I suggest reading it in
the following order:

* test-suite/output/ZSyntax.{v,out}       new test
* test-suite/output/Int63Syntax.{v,out}   ''
* test-suite/output/QArithSyntax.{v,out}  ''
* test-suite/output/RealSyntax.{v,out}    ''
* test-suite/output/FloatSyntax.{v,out}   ''

* interp/numTok.ml{i,}  extending numeral tokens

* theories/Init/Hexadecimal.v  adaptation of Decimal.v
                               for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v  new interface for Numeral Notation (basically,
                           a numeral is either a decimal or an hexadecimal)

* theories/Init/Nat.v            add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v    ''                                  positive
* theories/ZArith/BinIntDef.v    ''                                  Z
* theories/NArith/BinNatDef.v    ''                                  N
* theories/QArith/QArith_base.v  ''                                  Q

* interp/notation.ml{i,}     adapting implementation of numeral notations
* plugins/syntax/numeral.ml  ''

* plugins/syntax/r_syntax.ml  adapt parser for real numbers

* plugins/syntax/float_syntax.ml  adapt parser for primitive floats

* theories/Init/Prelude.v  register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
  and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
  had to be permuted)
---
 test-suite/output/Int63Syntax.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite/output/Int63Syntax.v')

diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index 0385e529bf..c49616d918 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -5,6 +5,19 @@ Check (2 + 2)%int63.
 Open Scope int63_scope.
 Check 2.
 Check 9223372036854775807.
+Check 0x1ab.
+Check 0X1ab.
+Check 0x1Ab.
+Check 0x1aB.
+Check 0x1AB.
+Fail Check 0x1ap5.  (* exponents not implemented (yet?) *)
+Fail Check 0x1aP5.
+Check 0x0.
+Check 0x000.
+Fail Check 0xg.
+Fail Check 0xG.
+Fail Check 00x1.
+Fail Check 0x.
 Check (Int63.add 2 2).
 Check (2+2).
 Eval vm_compute in 2+2.
-- 
cgit v1.2.3