1
(***********************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
4
(* \VV/ *************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(***********************************************************************)
9
(*i $Id: g_ascii_syntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
21
exception Non_closed_ascii
23
let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
24
let make_kn dir id = Libnames.encode_kn (make_dir dir) (id_of_string id)
25
let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
27
let ascii_module = ["Coq";"Strings";"Ascii"]
29
let ascii_path = make_path ascii_module "ascii"
31
let ascii_kn = make_kn ascii_module "ascii"
32
let path_of_Ascii = ((ascii_kn,0),1)
33
let static_glob_Ascii = ConstructRef path_of_Ascii
35
let make_reference id = find_reference "Ascii interpretation" ascii_module id
36
let glob_Ascii = lazy (make_reference "Ascii")
40
let interp_ascii dloc p =
44
RRef (dloc,if mp = 0 then glob_false else glob_true)
45
:: (aux (n-1) (p/2)) in
46
RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p)
48
let interp_ascii_string dloc s =
50
if String.length s = 1 then int_of_char s.[0]
52
if String.length s = 3 & is_digit s.[0] & is_digit s.[1] & is_digit s.[2]
55
user_err_loc (dloc,"interp_ascii_string",
56
str "Expects a single character or a three-digits ascii code.") in
59
let uninterp_ascii r =
60
let rec uninterp_bool_list n = function
62
| RRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l)
63
| RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
64
| _ -> raise Non_closed_ascii in
66
let rec aux = function
67
| RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
68
| _ -> raise Non_closed_ascii in
71
Non_closed_ascii -> None
73
let make_ascii_string n =
74
if n>=32 && n<=126 then String.make 1 (char_of_int n)
75
else Printf.sprintf "%03d" n
77
let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r)
80
Notation.declare_string_interpreter "char_scope"
81
(ascii_path,ascii_module)
83
([RRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)