Initial commit.

.gitignore

+*.vo
+*.glob
+*.v.d
+*~
+*.cmo
+*.cmi
+*.cmx
+*.cmxs
+*.ml4.d
+*.ml.d
+*.mli.d
+*.o
+*.a
+*.cma
+*.mllib.d
+Makefile.coq
+*.aux
+.coq-native
\ No newline at end of file

_CoqProject

+-I src
+-R theories fast_string
+
+./src/fast_string_syntax.ml
+./theories/fast_string.v

src/fast_string_syntax.ml

+(***********************************************************************)
+(*  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 CErrors
+open Util
+open Names
+open Glob_term
+open Globnames
+open Coqlib
+
+let __coq_plugin_name = "fast_string_syntax"
+let _ = Mltop.add_known_module __coq_plugin_name
+
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
+
+let list_module = ["Coq";"Init";"Datatypes"]
+let list_path = make_path list_module "list"
+let list_kn = make_kn list_module "list"
+
+let glob_nil = ConstructRef ((list_kn,0),1)
+let glob_cons = ConstructRef ((list_kn,0),2)
+
+let string_module = ["fast_string";"fast_string"]
+let string_path = make_path string_module "string"
+let string_kn = make_kn string_module "string"
+
+let glob_String = ConstructRef ((string_kn,0),1)
+
+let char_path = make_path string_module "char"
+let char_kn = make_kn string_module "char"
+
+let glob_char = IndRef (char_kn,0)
+let glob_C n = ConstructRef ((char_kn,0),1 + n)
+
+let interp_char dloc p = GRef(dloc,glob_C p,None)
+
+(* Chars *)
+let interp_char_string dloc s =
+  let p =
+    if Int.equal (String.length s) 1 then int_of_char s.[0]
+    else if Int.equal (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_char_string",
+      str "Expects a single character or a three-digits char code.") in
+  interp_char dloc p
+
+let uninterp_char r =
+  match r with
+  | GRef (_,ConstructRef ((k,0),n),_) when MutInd.equal k char_kn -> Some (n-1)
+  | _ -> None
+
+let make_char_string n =
+  if n>=32 && n<=126 then String.make 1 (char_of_int n)
+  else Printf.sprintf "%03d" n
+
+let uninterp_char_string r = Option.map make_char_string (uninterp_char r)
+
+(* strings *)
+let interp_char_list dloc s =
+  let le = String.length s in
+  let rec aux n =
+    if n = le then
+      GApp (dloc,GRef (dloc, glob_nil, None), [GRef(dloc, glob_char, None)])
+    else
+      GApp (dloc,GRef (dloc, glob_cons, None),
+        [GRef(dloc, glob_char, None);
+         interp_char dloc (int_of_char s.[n]); aux (n+1)])
+  in aux 0
+  
+let interp_string dloc s =
+  GApp(dloc,GRef(dloc,glob_String,None),[interp_char_list dloc s])
+
+let uninterp_char_list r =
+  let b = Buffer.create 16 in
+  let rec aux = function
+    | GApp (_,GRef (_,k,_),[GRef(_,k',_);a;s])
+         when eq_gr k glob_cons && eq_gr k' glob_char ->
+       begin match uninterp_char a with
+       | Some c -> Buffer.add_char b (Char.chr c); aux s
+       | None -> None
+       end
+    | GApp (_,GRef (_,k,_),[GRef(_,k',_)])
+         when eq_gr k glob_nil && eq_gr k' glob_char ->
+       Some (Buffer.contents b)
+    | _ -> None
+  in aux r
+
+let uninterp_string r =
+  match r with
+  | GApp (_,GRef (_,k,_),[r]) when eq_gr k glob_String -> uninterp_char_list r
+  | _ -> None
+
+(* declare parsers and printers *)
+let glob_C_gref_list =
+  let rec aux n =
+    if n = 256 then [] else GRef (Loc.ghost,glob_C n,None) :: aux (n+1)
+  in aux 0
+
+let _ =
+  Notation.declare_string_interpreter "fast_char_scope"
+    (char_path,string_module)
+    interp_char_string
+    (glob_C_gref_list, uninterp_char_string, true)
+let _ =
+  Notation.declare_string_interpreter "fast_string_scope"
+    (string_path,string_module)
+    interp_string
+    ([GRef (Loc.ghost,glob_String,None)], uninterp_string, true)
+