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') 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 From 7e1243a174e28535d9b35b558ed94f1548acd78c Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 13 Oct 2018 22:17:27 +0200 Subject: Make R parser parse decimals (e.g., 1.02e+01) RealField.v is slightly modified so that the ring/field tactics consider the term (IZR (Z.pow_pos 10 _)) produced when parsing exponents as constants. --- test-suite/success/RealSyntax.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 test-suite/success/RealSyntax.v (limited to 'test-suite') diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v new file mode 100644 index 0000000000..2765200991 --- /dev/null +++ b/test-suite/success/RealSyntax.v @@ -0,0 +1,19 @@ +Require Import Reals. +Open Scope R_scope. +Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). +Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). +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.5 = IZR (-5) / IZR (Z.pow_pos 10 1)). + +Goal 254e3 = 2540 * 10 ^ 2. +ring. +Qed. + +Require Import Psatz. + +Goal 254e3 = 2540 * 10 ^ 2. +lra. +Qed. -- cgit v1.2.3 From 49c5de7ead9d008d91a63316e6037bcc9c1f1d52 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 14 Oct 2018 15:33:31 +0200 Subject: Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10) --- test-suite/micromega/square.v | 2 +- test-suite/success/QArithSyntax.v | 9 +++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 test-suite/success/QArithSyntax.v (limited to 'test-suite') diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 7266b662fa..9efb81a901 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -54,7 +54,7 @@ Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq. - assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by + assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). assert (Hnx : (Qnum x <> 0)%Z) by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq). diff --git a/test-suite/success/QArithSyntax.v b/test-suite/success/QArithSyntax.v new file mode 100644 index 0000000000..2f2ee0134a --- /dev/null +++ b/test-suite/success/QArithSyntax.v @@ -0,0 +1,9 @@ +Require Import QArith. +Open Scope Q_scope. +Check (eq_refl : 1.02 = 102 # 100). +Check (eq_refl : 1.02e1 = 102 # 10). +Check (eq_refl : 1.02e+03 = 1020). +Check (eq_refl : 1.02e+02 = 102 # 1). +Check (eq_refl : 10.2e-1 = 1.02). +Check (eq_refl : -0.0001 = -1 # 10000). +Check (eq_refl : -0.50 = - 50 # 100). -- cgit v1.2.3