diff options
author | 2009-11-12 11:10:46 +0000 | |
---|---|---|
committer | 2009-11-12 11:10:46 +0000 | |
commit | f30347427516e70bb720fc7ed1a08a4f055bae9e (patch) | |
tree | 2850d3acfa8182e06010b58c2e05881fdc51e018 /test-suite | |
parent | 3e5b93760241671c8959da1cdb8023cfa7f62987 (diff) |
Repair interpretation of numeral for BigQ, add a printer (close #2160)
on the way:
- Added a testsuite output file
- Try to avoid nasty unfolding (fix nfun ...) in type of I31.
Idealy we would need a "Eval compute in" for the type of a inductive
constructor
- Stop opening Scopes for BigQ, BigN, BigZ by default
The user should do some Open Scope.
TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope
(and so on for other operations), even with some Bind Scope around.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12504 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/output/NumbersSyntax.out | 56 | ||||
-rw-r--r-- | test-suite/output/NumbersSyntax.v | 46 |
2 files changed, 102 insertions, 0 deletions
diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out new file mode 100644 index 000000000..1a8f4eff1 --- /dev/null +++ b/test-suite/output/NumbersSyntax.out @@ -0,0 +1,56 @@ +I31 + : digits31 int31 +2 + : int31 +660865024 + : int31 +2 + 2 + : int31 +2 + 2 + : int31 + = 4 + : int31 + = 710436486 + : int31 +2 + : BigN.t_ +1000000000000000000 + : BigN.t_ +2 + 2 + : BigN.t_ +2 + 2 + : BigN.t_ + = 4 + : BigN.t_ + = 37151199385380486 + : BigN.t_ +2 + : BigZ.t_ +-1000000000000000000 + : BigZ.t_ +2 + 2 + : BigZ.t_ +2 + 2 + : BigZ.t_ + = 4 + : BigZ.t_ + = 37151199385380486 + : BigZ.t_ +2 + : BigQ.t_ +-1000000000000000000 + : BigQ.t_ +2 + 2 + : bigQ +2 + 2 + : bigQ + = 4 + : bigQ + = 37151199385380486 + : bigQ +BigQ.Qq 6562%bigZ 456%bigN + : BigQ.t_ + = BigQ.Qq 3281%bigZ 228%bigN + : bigQ + = BigQ.Qq 1%bigZ 10000%bigN + : bigQ diff --git a/test-suite/output/NumbersSyntax.v b/test-suite/output/NumbersSyntax.v new file mode 100644 index 000000000..3f6a40bcb --- /dev/null +++ b/test-suite/output/NumbersSyntax.v @@ -0,0 +1,46 @@ + +Require Import BigQ. + +Open Scope int31_scope. +Check I31. (* Would be nice to have I31 : digits->digits->...->int31 + For the moment, I31 : digits31 int31, which is better + than (fix nfun .....) size int31 *) +Check 2. +Check 1000000000000000000. (* = 660865024, after modulo 2^31 *) +Check (add31 2 2). +Check (2+2). +Eval compute in 2+2. +Eval compute in 65675757 * 565675998. +Close Scope int31_scope. + +Open Scope bigN_scope. +Check 2. +Check 1000000000000000000. +Check (BigN.add 2 2). +Check (2+2). +Eval compute in 2+2. +Eval compute in 65675757 * 565675998. +Close Scope bigN_scope. + +Open Scope bigZ_scope. +Check 2. +Check -1000000000000000000. +Check (BigZ.add 2 2). +Check (2+2). +Eval compute in 2+2. +Eval compute in 65675757 * 565675998. +Close Scope bigN_scope. + +Open Scope bigQ_scope. +Check 2. +Check -1000000000000000000. +Check (BigQ.add 2 2). +Check (2+2). +Eval compute in 2+2. +Eval compute in 65675757 * 565675998. +(* fractions *) +Check (BigQ.Qq 6562%bigZ 456%bigN). + (* Having to say %bigZ and %bigN is a BUG! *) +Eval compute in (BigQ.red (BigQ.Qq 6562%bigZ 456%bigN)). +Eval compute in (1/10000). +Close Scope bigQ_scope. |