From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 parsing/g_rsyntax.ml | 125 ---------------------------------------------------
 1 file changed, 125 deletions(-)
 delete mode 100644 parsing/g_rsyntax.ml

(limited to 'parsing/g_rsyntax.ml')

diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
deleted file mode 100644
index b3425899..00000000
--- a/parsing/g_rsyntax.ml
+++ /dev/null
@@ -1,125 +0,0 @@
-(************************************************************************)
-(*  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: g_rsyntax.ml 10739 2008-04-01 14:45:20Z herbelin $ 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)
-- 
cgit v1.2.3