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

1 files changed, 69 insertions, 0 deletions

diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
new file mode 100644
index 000000000..d1c263dc8
--- /dev/null
+++ b/plugins/syntax/string_syntax.ml
@@ -0,0 +1,69 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \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 Libnames
+open Topconstr
+open Ascii_syntax
+open Rawterm
+open Coqlib
+
+exception Non_closed_string
+
+(* make a string term from the string s *)
+
+let string_module = ["Coq";"Strings";"String"]
+
+let string_path = make_path string_module "string"
+
+let string_kn = make_kn string_module "string"
+let static_glob_EmptyString  = ConstructRef ((string_kn,0),1)
+let static_glob_String  = ConstructRef ((string_kn,0),2)
+
+let make_reference id = find_reference "String interpretation" string_module id
+let glob_String = lazy (make_reference "String")
+let glob_EmptyString = lazy (make_reference "EmptyString")
+
+open Lazy
+
+let interp_string dloc s =
+  let le = String.length s in
+  let rec aux n = 
+     if n = le then RRef (dloc, force glob_EmptyString) else
+     RApp (dloc,RRef (dloc, force glob_String),
+       [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
+  in aux 0
+
+let uninterp_string r =
+  try 
+    let b = Buffer.create 16 in
+    let rec aux = function
+    | RApp (_,RRef (_,k),[a;s]) when k = force glob_String ->
+	(match uninterp_ascii a with
+	  | Some c -> Buffer.add_char b (Char.chr c); aux s
+	  | _ -> raise Non_closed_string)
+    | RRef (_,z) when z = force glob_EmptyString ->
+	Some (Buffer.contents b)
+    | _ ->
+	raise Non_closed_string
+    in aux r
+  with 
+   Non_closed_string -> None
+
+let _ =
+  Notation.declare_string_interpreter "string_scope"
+    (string_path,["Coq";"Strings";"String"])
+    interp_string
+    ([RRef (dummy_loc,static_glob_String); 
+      RRef (dummy_loc,static_glob_EmptyString)],
+     uninterp_string, true)