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/SearchPattern.out | 77 ++++++++++++++++++++++--------------- 1 file changed, 46 insertions(+), 31 deletions(-) (limited to 'test-suite/output/SearchPattern.out') diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 36fc1a5914..13d0a9e55b 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -1,47 +1,61 @@ false: bool true: bool negb: bool -> bool -implb: bool -> bool -> bool -orb: bool -> bool -> bool -andb: bool -> bool -> bool xorb: bool -> bool -> bool -Nat.even: nat -> bool +andb: bool -> bool -> bool +orb: bool -> bool -> bool +implb: bool -> bool -> bool Nat.odd: nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool +Nat.even: nat -> bool +Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +Hexadecimal.hexadecimal_beq: + Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool +Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool +Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool +Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool +Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool +Decimal.int_beq: Decimal.int -> Decimal.int -> bool +Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool (use "About" for full details on implicit arguments) Nat.two: nat -Nat.one: nat Nat.zero: nat +Nat.one: nat O: nat +Nat.double: nat -> nat +Nat.sqrt: nat -> nat 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.succ: nat -> nat +Nat.ldiff: nat -> nat -> nat +Nat.add: nat -> nat -> nat Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.sub: nat -> nat -> nat Nat.mul: nat -> nat -> nat Nat.tail_mul: nat -> nat -> nat -Nat.div: 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.tail_add: nat -> nat -> nat Nat.pow: nat -> nat -> nat -Nat.lxor: nat -> nat -> nat -Nat.ldiff: nat -> nat -> nat Nat.min: nat -> nat -> nat -Nat.add: nat -> nat -> nat +Nat.modulo: nat -> nat -> nat +Nat.div: nat -> nat -> nat +Nat.lor: nat -> nat -> nat +Nat.gcd: nat -> nat -> nat +Hexadecimal.nb_digits: Hexadecimal.uint -> nat +Nat.of_hex_uint: Hexadecimal.uint -> nat +Nat.of_num_uint: Numeral.uint -> nat Nat.of_uint: Decimal.uint -> nat Decimal.nb_digits: Decimal.uint -> nat Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat @@ -53,29 +67,30 @@ Nat.div2: nat -> nat Nat.sqrt: nat -> nat Nat.log2: nat -> nat Nat.double: nat -> nat -Nat.pred: nat -> nat +S: nat -> nat Nat.square: nat -> nat Nat.succ: nat -> nat -S: nat -> nat +Nat.pred: nat -> nat +Nat.land: nat -> nat -> nat +Nat.max: nat -> nat -> nat +Nat.gcd: nat -> nat -> nat +Nat.modulo: nat -> nat -> nat Nat.ldiff: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat Nat.pow: nat -> nat -> nat -Nat.land: nat -> nat -> nat Nat.lxor: nat -> nat -> nat Nat.div: nat -> nat -> nat Nat.lor: nat -> nat -> nat -Nat.tail_mul: nat -> nat -> nat -Nat.modulo: nat -> nat -> nat -Nat.sub: nat -> nat -> nat Nat.mul: nat -> nat -> nat -Nat.gcd: nat -> nat -> nat -Nat.max: nat -> nat -> nat -Nat.tail_add: nat -> nat -> nat -Nat.add: nat -> nat -> nat Nat.min: nat -> nat -> nat +Nat.add: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> 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.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat +Nat.log2_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat (use "About" for full details on implicit arguments) mult_n_Sm: forall n m : nat, n * m + n = n * S m -- cgit v1.2.3