diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/syntax/string_syntax.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
-rw-r--r-- | plugins/syntax/string_syntax.ml | 69 |
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 00000000..bc02357a --- /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) |