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
68
69
70

(***********************************************************************)
(*  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 Globnames
open Ascii_syntax_plugin.Ascii_syntax
open Glob_term
open Coqlib

(* Poor's man DECLARE PLUGIN *)
let __coq_plugin_name = "string_syntax_plugin"
let () = Mltop.add_known_module __coq_plugin_name

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")

let is_gr c gr = match DAst.get c with
| GRef (r, _) -> Globnames.eq_gr r gr
| _ -> false

open Lazy

let interp_string ?loc s =
  let le = String.length s in
  let rec aux n =
     if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else
     DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None),
       [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
  in aux 0

let uninterp_string (AnyGlobConstr r) =
  try
    let b = Buffer.create 16 in
    let rec aux c = match DAst.get c with
    | GApp (k,[a;s]) when is_gr 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 eq_gr 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
    ([DAst.make @@ GRef (static_glob_String,None);
      DAst.make @@ GRef (static_glob_EmptyString,None)],
     uninterp_string, true)