Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7966 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 137 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index 30a962b67e..67a803ca22 100644
--- a/Makefile
+++ b/Makefile
@@ -174,12 +174,10 @@ PARSING=\
   parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo 
 
 HIGHPARSING=\
-  parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \
   parsing/g_constr.cmo parsing/g_vernac.cmo parsing/g_prim.cmo \
-  parsing/g_proofs.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo 
-
-ARITHSYNTAX=\
-  parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
+  parsing/g_proofs.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo \
+  parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \
+  parsing/g_ascii_syntax.cmo parsing/g_string_syntax.cmo
 
 TACTICS=\
   tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml
new file mode 100644
index 0000000000..4472621f72
--- /dev/null
+++ b/parsing/g_ascii_syntax.ml
@@ -0,0 +1,74 @@
+(***********************************************************************)
+(*  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 Rawterm
+open Topconstr
+open Libnames
+open Coqlib
+open Bigint
+
+exception Non_closed_ascii
+
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let make_path dir id = Libnames.encode_kn dir id
+
+let ascii_module = make_dir ["Coq";"Strings";"Ascii"]
+let ascii_path = make_path ascii_module (id_of_string "ascii")
+
+let glob_ascii  = IndRef (ascii_path,0)
+let path_of_Ascii = ((ascii_path,0),1)
+let glob_Ascii  = ConstructRef path_of_Ascii
+
+let interp_ascii dloc p =
+  let rec aux n p = 
+     if n = 0 then [] else
+     let mp = p mod 2 in
+     RRef (dloc,if mp = 0 then glob_false else glob_true)
+     :: (aux (n-1) (p/2)) in
+  RApp (dloc,RRef(dloc,glob_Ascii), aux 8 p)
+
+let interp_ascii_string dloc s =
+  let p = 
+    if String.length s = 1 then int_of_char s.[0]
+    else
+      if String.length s = 3 & is_digit s.[0] & is_digit s.[1] & is_digit s.[2]
+      then int_of_string s
+      else
+	user_err_loc (dloc,"interp_ascii_string",
+	  str "Expects a single character or a three-digits ascii code") in
+  interp_ascii dloc p
+
+let uninterp_ascii r =
+  let rec uninterp_bool_list n = function
+    | [] when n = 0 -> 0
+    | RRef (_,k)::l when k = glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | _ -> raise Non_closed_ascii in
+  try 
+    let rec aux = function
+    | RApp (_,RRef (_,k),l) when k = glob_Ascii -> uninterp_bool_list 8 l
+    | _ -> raise Non_closed_ascii in
+    Some (aux r)
+  with 
+   Non_closed_ascii -> None
+
+let make_ascii_string n =
+  if n>=32 && n<=126 then String.make 1 (char_of_int n)
+  else Printf.sprintf "%03d" n
+
+let uninterp_ascii_string r = option_app make_ascii_string (uninterp_ascii r)
+
+let _ =
+  Notation.declare_string_interpreter "char_scope"
+    (glob_ascii,["Coq";"Strings";"Ascii"])
+    interp_ascii_string
+    ([RRef (dummy_loc,glob_Ascii)], uninterp_ascii_string, true)
diff --git a/parsing/g_string_syntax.ml b/parsing/g_string_syntax.ml
new file mode 100644
index 0000000000..d4d83f6d27
--- /dev/null
+++ b/parsing/g_string_syntax.ml
@@ -0,0 +1,60 @@
+(***********************************************************************)
+(*  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
+
+exception Non_closed_string
+
+(* make a string term from the string s *)
+
+let string_module = make_dir ["Coq";"Strings";"String"]
+let string_path = make_path string_module (id_of_string "string")
+
+let glob_string  = IndRef (string_path,0)
+let path_of_EmptyString  = ((string_path,0),1)
+let glob_EmptyString  = ConstructRef path_of_EmptyString
+let path_of_String  = ((string_path,0),2)
+let glob_String  = ConstructRef path_of_String
+
+let interp_string dloc s =
+  let le = String.length s in
+  let rec aux n = 
+     if n = le then RRef (dloc, glob_EmptyString) else
+     RApp (dloc,RRef (dloc, 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 = 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 = 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"
+    (glob_string,["Coq";"Strings";"String"])
+    interp_string
+    ([RRef (dummy_loc,glob_String); RRef (dummy_loc,glob_EmptyString)],
+     uninterp_string, true)