1 files changed, 125 insertions, 0 deletions
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
new file mode 100644
index 00000000..f85309e6
--- /dev/null
+++ b/plugins/syntax/r_syntax.ml
@@ -0,0 +1,125 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Pp
+open Util
+open Names
+open Pcoq
+open Topconstr
+open Libnames
+
+exception Non_closed_number
+
+(**********************************************************************)
+(* Parsing R via scopes                                               *)
+(**********************************************************************)
+
+open Libnames
+open Rawterm
+open Bigint
+
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
+let make_path dir id = Libnames.make_path dir (id_of_string id)
+
+let r_path = make_path rdefinitions "R"
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_con dir (id_of_string id)
+
+let r_kn = make_path rdefinitions "R"
+let glob_R = ConstRef r_kn
+let glob_R1 = ConstRef (make_path rdefinitions "R1")
+let glob_R0 = ConstRef (make_path rdefinitions "R0")
+let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
+let glob_Rplus = ConstRef (make_path rdefinitions "Rplus")
+let glob_Rmult = ConstRef (make_path rdefinitions "Rmult")
+
+let two = mult_2 one
+let three = add_1 two
+let four = mult_2 two
+
+(* Unary representation of strictly positive numbers *)
+let rec small_r dloc n =
+  if equal one n then RRef (dloc, glob_R1)
+  else RApp(dloc,RRef (dloc,glob_Rplus),
+            [RRef (dloc, glob_R1);small_r dloc (sub_1 n)])
+
+let r_of_posint dloc n =
+  let r1 = RRef (dloc, glob_R1) in
+  let r2 = small_r dloc two in
+  let rec r_of_pos n =
+    if less_than n four then small_r dloc n
+    else
+      let (q,r) = div2_with_rest n in
+      let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
+      if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in
+  if n <> zero then r_of_pos n else RRef(dloc,glob_R0)
+
+let r_of_int dloc z =
+  if is_strictly_neg z then
+    RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
+  else
+    r_of_posint dloc z
+
+(**********************************************************************)
+(* Printing R via scopes                                              *)
+(**********************************************************************)
+
+let bignat_of_r =
+(* for numbers > 1 *)
+let rec bignat_of_pos = function
+  (* 1+1 *)
+  | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)])
+      when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two
+  (* 1+(1+1) *)
+  | RApp (_,RRef (_,p1), [RRef (_,o1);
+      RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])])
+      when p1 = glob_Rplus & p2 = glob_Rplus &
+           o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three
+  (* (1+1)*b *)
+  | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult ->
+      if bignat_of_pos a <> two then raise Non_closed_number;
+      mult_2 (bignat_of_pos b)
+  (* 1+(1+1)*b *)
+  | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])])
+      when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1  ->
+      if bignat_of_pos a <> two then raise Non_closed_number;
+        add_1 (mult_2 (bignat_of_pos b))
+  | _ -> raise Non_closed_number
+in
+let bignat_of_r = function
+  | RRef (_,a) when a = glob_R0 -> zero
+  | RRef (_,a) when a = glob_R1 -> one
+  | r -> bignat_of_pos r
+in
+bignat_of_r
+
+let bigint_of_r = function
+  | RApp (_,RRef (_,o), [a]) when o = glob_Ropp ->
+      let n = bignat_of_r a in
+      if n = zero then raise Non_closed_number;
+      neg n
+  | a -> bignat_of_r a
+
+let uninterp_r p =
+  try
+    Some (bigint_of_r p)
+  with Non_closed_number ->
+    None
+
+let _ = Notation.declare_numeral_interpreter "R_scope"
+  (r_path,["Coq";"Reals";"Rdefinitions"])
+  r_of_int
+  ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
+    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);
+    RRef(dummy_loc,glob_R1)],
+    uninterp_r,
+    false)