1 files changed, 67 insertions, 0 deletions
diff --git a/parsing/g_string_syntax.ml b/parsing/g_string_syntax.ml
new file mode 100644
index 00000000..6d879fb2
--- /dev/null
+++ b/parsing/g_string_syntax.ml
@@ -0,0 +1,67 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+open Pp
+open Util
+open Names
+open Pcoq
+open Libnames
+open Topconstr
+open G_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)