From 7f2c52bcf588abfcbf30530bae240244229304a4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 27 Mar 2009 17:53:43 +0000
Subject: Parsing files for numerals (+ ascii/string) moved into plugins

 Idea: make coqtop more independant of the standard library.
 In the future, we can imagine loading the syntax for numerals right
 after their definition. For the moment, it is easier to stay lazy
 and load the syntax plugins slightly before the definitions.

 After this commit, the main (sole ?) references to theories/
 from the core ml files are in Coqlib (but many parts of coqlib
 are only used by plugins), and it mainly concerns Init
 (+ Logic/JMeq and maybe a few others).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/syntax/nat_syntax.ml | 78 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100644 plugins/syntax/nat_syntax.ml

(limited to 'plugins/syntax/nat_syntax.ml')

diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
new file mode 100644
index 0000000000..c62c813778
--- /dev/null
+++ b/plugins/syntax/nat_syntax.ml
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(* This file defines the printer for natural numbers in [nat] *)
+
+(*i*)
+open Pcoq
+open Pp
+open Util
+open Names
+open Coqlib
+open Rawterm
+open Libnames
+open Bigint
+open Coqlib
+open Notation
+open Pp
+open Util
+open Names
+(*i*)
+
+(**********************************************************************)
+(* Parsing via scopes *)
+(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
+
+let nat_of_int dloc n =
+  if is_pos_or_zero n then begin
+      if less_than (of_string "5000") n then
+	Flags.if_warn msg_warning 
+	  (strbrk "Stack overflow or segmentation fault happens when " ++
+	   strbrk "working with large numbers in nat (observed threshold " ++
+	   strbrk "may vary from 5000 to 70000 depending on your system " ++
+	   strbrk "limits and on the command executed).");
+      let ref_O = RRef (dloc, glob_O) in
+      let ref_S = RRef (dloc, glob_S) in
+      let rec mk_nat acc n =
+	if n <> zero then 
+	  mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n)
+	else 
+	  acc
+      in 
+      mk_nat ref_O n
+    end
+  else
+      user_err_loc (dloc, "nat_of_int",
+        str "Cannot interpret a negative number as a number of type nat")
+
+(************************************************************************)
+(* Printing via scopes *)
+
+exception Non_closed_number
+
+let rec int_of_nat = function
+  | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
+  | RRef (_,z) when z = glob_O -> zero
+  | _ -> raise Non_closed_number
+	  
+let uninterp_nat p =
+  try 
+    Some (int_of_nat p)
+  with
+    Non_closed_number -> None
+
+(************************************************************************)
+(* Declare the primitive parsers and printers *)
+
+let _ =
+  Notation.declare_numeral_interpreter "nat_scope"
+    (nat_path,["Coq";"Init";"Datatypes"])
+    nat_of_int
+    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, true)
-- 
cgit v1.2.3