aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-12 11:10:46 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-12 11:10:46 +0000
commitf30347427516e70bb720fc7ed1a08a4f055bae9e (patch)
tree2850d3acfa8182e06010b58c2e05881fdc51e018
parent3e5b93760241671c8959da1cdb8023cfa7f62987 (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
-rw-r--r--plugins/syntax/numbers_syntax.ml61
-rw-r--r--test-suite/output/NumbersSyntax.out56
-rw-r--r--test-suite/output/NumbersSyntax.v46
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v4
-rw-r--r--theories/Numbers/Cyclic/Int31/Int31.v6
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v4
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v18
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v4
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v12
-rw-r--r--theories/Numbers/Rational/BigQ/BigQ.v12
10 files changed, 161 insertions, 62 deletions
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 21b7115b6..4375d5e0f 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -14,23 +14,22 @@ open Bigint
open Libnames
open Rawterm
-(*** Constants for locating the int31 and bigN ***)
-
-
+(*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
let make_dir l = Names.make_dirpath (List.map Names.id_of_string (List.rev l))
let make_path dir id = Libnames.make_path (make_dir dir) (Names.id_of_string id)
-(* copied on g_zsyntax.ml, where it is said to be a temporary hack*)
-(* takes a path an identifier in the form of a string list and a string,
- returns a kernel_name *)
-let make_kn dir id = Libnames.encode_mind (make_dir dir) (Names.id_of_string id)
+let make_mind mp id = Names.make_mind mp Names.empty_dirpath (Names.mk_label id)
+let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
+let make_mind_mpdot dir modname id =
+ let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.mk_label modname)
+ in make_mind mp id
(* int31 stuff *)
let int31_module = ["Coq"; "Numbers"; "Cyclic"; "Int31"; "Int31"]
let int31_path = make_path int31_module "int31"
-let int31_id = make_kn int31_module
+let int31_id = make_mind_mpfile int31_module
let int31_scope = "int31_scope"
let int31_construct = ConstructRef ((int31_id "int31",0),1)
@@ -42,18 +41,14 @@ let int31_1 = ConstructRef ((int31_id "digits",0),2)
(* bigN stuff*)
let zn2z_module = ["Coq"; "Numbers"; "Cyclic"; "DoubleCyclic"; "DoubleType"]
let zn2z_path = make_path zn2z_module "zn2z"
-let zn2z_id = make_kn zn2z_module
+let zn2z_id = make_mind_mpfile zn2z_module
let zn2z_W0 = ConstructRef ((zn2z_id "zn2z",0),1)
let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2)
let bigN_module = ["Coq"; "Numbers"; "Natural"; "BigN"; "BigN" ]
let bigN_path = make_path (bigN_module@["BigN"]) "t"
-(* big ugly hack *)
-let bigN_id id = let kn =
- ((Names.MPdot ((Names.MPfile (make_dir bigN_module)),
- Names.mk_label "BigN")),
- [], Names.id_of_string id) in (Obj.magic (kn,kn) : Names.mutual_inductive)
+let bigN_t = make_mind_mpdot bigN_module "BigN" "t_"
let bigN_scope = "bigN_scope"
(* number of inlined level of bigN (actually the level 0 to n_inlined-1 are inlined) *)
@@ -71,7 +66,7 @@ let bigN_constructor =
2*(to_int quo)
in
fun i ->
- ConstructRef ((bigN_id "t_",0),
+ ConstructRef ((bigN_t,0),
if less_than i n_inlined then
(to_int i)+1
else
@@ -81,25 +76,20 @@ let bigN_constructor =
(*bigZ stuff*)
let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ" ]
let bigZ_path = make_path (bigZ_module@["BigZ"]) "t"
-(* big ugly hack bis *)
-let bigZ_id id = let kn = ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)),
- Names.mk_label "BigZ")),
- [], Names.id_of_string id) in (Obj.magic (kn,kn): Names.mutual_inductive)
+let bigZ_t = make_mind_mpdot bigZ_module "BigZ" "t_"
let bigZ_scope = "bigZ_scope"
-let bigZ_pos = ConstructRef ((bigZ_id "t_",0),1)
-let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2)
+let bigZ_pos = ConstructRef ((bigZ_t,0),1)
+let bigZ_neg = ConstructRef ((bigZ_t,0),2)
(*bigQ stuff*)
let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"]
-let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake_base"]
let bigQ_path = make_path (bigQ_module@["BigQ"]) "t"
-(* big ugly hack bis *)
-let bigQ_id = make_kn qmake_module
+let bigQ_t = make_mind_mpdot bigQ_module "BigQ" "t_"
let bigQ_scope = "bigQ_scope"
-let bigQ_z = ConstructRef ((bigQ_id "q_type",0),1)
+let bigQ_z = ConstructRef ((bigQ_t,0),1)
(*** Definition of the Non_closed exception, used in the pretty printing ***)
@@ -311,7 +301,7 @@ let uninterp_bigZ rc =
with Non_closed ->
None
-(* Actually declares the interpreter for bigN *)
+(* Actually declares the interpreter for bigZ *)
let _ = Notation.declare_numeral_interpreter bigZ_scope
(bigZ_path, bigZ_module)
interp_bigZ
@@ -323,21 +313,18 @@ let _ = Notation.declare_numeral_interpreter bigZ_scope
(*** Parsing for bigQ in digital notation ***)
let interp_bigQ dloc n =
let ref_z = RRef (dloc, bigQ_z) in
- let ref_pos = RRef (dloc, bigZ_pos) in
- let ref_neg = RRef (dloc, bigZ_neg) in
- if is_pos_or_zero n then
- RApp (dloc, ref_z,
- [RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])])
- else
- RApp (dloc, ref_z,
- [RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])])
-
-let uninterp_bigQ rc = None
+ RApp (dloc, ref_z, [interp_bigZ dloc n])
+let uninterp_bigQ rc =
+ try match rc with
+ | RApp (_, RRef(_,c), [one_arg]) when c = bigQ_z ->
+ Some (bigint_of_bigZ one_arg)
+ | _ -> None (* we don't pretty-print yet fractions *)
+ with Non_closed -> None
(* Actually declares the interpreter for bigQ *)
let _ = Notation.declare_numeral_interpreter bigQ_scope
(bigQ_path, bigQ_module)
interp_bigQ
- ([], uninterp_bigQ,
+ ([RRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
true)
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.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 67d15b499..7d795cf50 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -24,8 +24,8 @@ Require Import BigNumPrelude.
Require Import CyclicAxioms.
Require Import ROmega.
-Open Scope nat_scope.
-Open Scope int31_scope.
+Local Open Scope nat_scope.
+Local Open Scope int31_scope.
Section Basics.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 1168e7fd6..23c2c36a2 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -40,7 +40,9 @@ Inductive digits : Type := D0 | D1.
(** The type [int31] has a unique constructor [I31] that expects
31 arguments of type [digits]. *)
-Inductive int31 : Type := I31 : nfun digits size int31.
+Definition digits31 t := Eval compute in nfun digits size t.
+
+Inductive int31 : Type := I31 : digits31 int31.
(* spiwack: Registration of the type of integers, so that the matchs in
the functions below perform dynamic decompilation (otherwise some segfault
@@ -50,7 +52,7 @@ Register int31 as int31 type in "coq_int31" by True.
Delimit Scope int31_scope with int31.
Bind Scope int31_scope with int31.
-Open Scope int31_scope.
+Local Open Scope int31_scope.
(** * Constants *)
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 6e8ca37ca..2e7604b0d 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -46,11 +46,11 @@ Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
-Open Scope bigZ_scope.
+Local Open Scope bigZ_scope.
(** Some additional results about [BigZ] *)
-Theorem spec_to_Z: forall n:bigZ,
+Theorem spec_to_Z: forall n : bigZ,
BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.
Proof.
intros n; case n; simpl; intros p;
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index e2be10ad9..d3f4776a6 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -19,15 +19,15 @@ Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig.
Delimit Scope NumScope with Num.
Bind Scope NumScope with Z.t.
Local Open Scope NumScope.
-Notation "[ x ]" := (Z.to_Z x) : NumScope.
-Infix "==" := Z.eq (at level 70) : NumScope.
-Notation "0" := Z.zero : NumScope.
-Infix "+" := Z.add : NumScope.
-Infix "-" := Z.sub : NumScope.
-Infix "*" := Z.mul : NumScope.
-Notation "- x" := (Z.opp x) : NumScope.
-Infix "<=" := Z.le : NumScope.
-Infix "<" := Z.lt : NumScope.
+Local Notation "[ x ]" := (Z.to_Z x) : NumScope.
+Local Infix "==" := Z.eq (at level 70) : NumScope.
+Local Notation "0" := Z.zero : NumScope.
+Local Infix "+" := Z.add : NumScope.
+Local Infix "-" := Z.sub : NumScope.
+Local Infix "*" := Z.mul : NumScope.
+Local Notation "- x" := (Z.opp x) : NumScope.
+Local Infix "<=" := Z.le : NumScope.
+Local Infix "<" := Z.lt : NumScope.
Hint Rewrite
Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 4cc867898..ba457ffb8 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -51,11 +51,11 @@ Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
-Open Scope bigN_scope.
+Local Open Scope bigN_scope.
(** Example of reasoning about [BigN] *)
-Theorem succ_pred: forall q:bigN,
+Theorem succ_pred: forall q : bigN,
0 < q -> BigN.succ (BigN.pred q) == q.
Proof.
intros; apply succ_pred.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 2b199858f..49e7d7256 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -20,12 +20,12 @@ Module NSig_NAxioms (N:NType) <: NAxiomsSig.
Delimit Scope NumScope with Num.
Bind Scope NumScope with N.t.
Local Open Scope NumScope.
-Notation "[ x ]" := (N.to_Z x) : NumScope.
-Infix "==" := N.eq (at level 70) : NumScope.
-Notation "0" := N.zero : NumScope.
-Infix "+" := N.add : NumScope.
-Infix "-" := N.sub : NumScope.
-Infix "*" := N.mul : NumScope.
+Local Notation "[ x ]" := (N.to_Z x) : NumScope.
+Local Infix "==" := N.eq (at level 70) : NumScope.
+Local Notation "0" := N.zero : NumScope.
+Local Infix "+" := N.add : NumScope.
+Local Infix "-" := N.sub : NumScope.
+Local Infix "*" := N.mul : NumScope.
Hint Rewrite
N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub : num.
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 38542c12b..eb0237f4a 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -10,7 +10,8 @@
(*i $Id$ i*)
-Require Import Field Qfield BigN BigZ QSig QMake.
+Require Export BigZ.
+Require Import Field Qfield QSig QMake.
(** We choose for BigQ an implemention with
multiple representation of 0: 0, 1/0, 2/0 etc.
@@ -43,6 +44,13 @@ Notation bigQ := BigQ.t.
Delimit Scope bigQ_scope with bigQ.
Bind Scope bigQ_scope with bigQ.
Bind Scope bigQ_scope with BigQ.t.
+Bind Scope bigQ_scope with BigQ.t_.
+
+(** BUG: the previous Bind Scope don't seem to work, and idem with BigN/BigZ.
+ For instance "Check (BigQ.opp 10)" fails when bigQ_scope is closed.
+ (whereas "Check (Int31.add31 10 10)" is ok). Something with modules ?
+ Adding an Arguments Scope helps, but this isn't a satisfactory solution.
+*)
Infix "+" := BigQ.add : bigQ_scope.
Infix "-" := BigQ.sub : bigQ_scope.
@@ -58,7 +66,7 @@ Notation "x > y" := (BigQ.lt y x)(only parsing) : bigQ_scope.
Notation "x >= y" := (BigQ.le y x)(only parsing) : bigQ_scope.
Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope.
-Open Scope bigQ_scope.
+Local Open Scope bigQ_scope.
(** [BigQ] is a setoid *)