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/RealSyntax.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'test-suite/output/RealSyntax.v') diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index e5f9d06316..69ce3ef5f9 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -14,6 +14,12 @@ Check (eq_refl : 1.02e+02 = IZR 102). Check (eq_refl : 10.2e-1 = 1.02). Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)). +Check (eq_refl : -0x1a = - 26). +Check (eq_refl : 0xb.2c = IZR 2860 / IZR (Z.pow_pos 2 8)). +Check (eq_refl : -0x1ae2 = -6882). +Check (eq_refl : 0xb.2cp2 = IZR 2860 / IZR (Z.pow_pos 2 6)). +Check (eq_refl : 0xb.2cp8 = 2860). +Check (eq_refl : -0xb.2cp-2 = - IZR 2860 / IZR (Z.pow_pos 2 10)). Require Import Reals. -- cgit v1.2.3