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

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 *)