1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 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 Ascii_syntax
open Glob_term
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 GRef (dloc, force glob_EmptyString) else
GApp (dloc,GRef (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
| GApp (_,GRef (_,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)
| GRef (_,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
([GRef (dummy_loc,static_glob_String);
GRef (dummy_loc,static_glob_EmptyString)],
uninterp_string, true)
|