Adding BigQ and proofs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10265 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 32 insertions, 1 deletions

diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml
index 7abafb070e..b1a8ae3485 100644
--- a/parsing/g_intsyntax.ml
+++ b/parsing/g_intsyntax.ml
@@ -8,7 +8,7 @@
 
 (*i $ $ i*)
 
-(* digit-based syntax for int31, bigN and bigZ *)
+(* digit-based syntax for int31, bigN bigZ and bigQ *)
 
 open Bigint
 open Libnames
@@ -90,6 +90,15 @@ let bigZ_pos = ConstructRef ((bigZ_id "t_",0),1)
 let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2)
 
 
+(*bigQ stuff*)
+let bigQ_module = ["Coq"; "Ints"; "num"; "BigQ"]
+let qmake_module = ["Coq"; "Ints"; "num"; "QMake_base"]
+let bigQ_path = make_path bigQ_module "bigQ"
+(* big ugly hack bis *)
+let bigQ_id = make_kn qmake_module
+let bigQ_scope = "bigQ_scope"
+
+let bigQ_z =  ConstructRef ((bigQ_id "q_type",0),1)
 
 
 (*** Definition of the Non_closed exception, used in the pretty printing ***)
@@ -309,3 +318,25 @@ let _ = Notation.declare_numeral_interpreter bigZ_scope
     RRef (Util.dummy_loc, bigZ_neg)],
    uninterp_bigZ,
    true)
+
+(*** 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
+
+
+(* Actually declares the interpreter for bigQ *)
+let _ = Notation.declare_numeral_interpreter bigQ_scope
+  (bigQ_path, bigQ_module)
+  interp_bigQ
+  ([], uninterp_bigQ,
+   true)