28941
|
1 |
(* Title: Pure/General/binding.ML
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
|
|
4 |
Structured name bindings.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature BASIC_BINDING =
|
|
8 |
sig
|
|
9 |
val long_names: bool ref
|
|
10 |
val short_names: bool ref
|
|
11 |
val unique_names: bool ref
|
|
12 |
end;
|
|
13 |
|
|
14 |
signature BINDING =
|
|
15 |
sig
|
|
16 |
include BASIC_BINDING
|
|
17 |
type T
|
28965
|
18 |
val name_pos: string * Position.T -> T
|
|
19 |
val name: string -> T
|
|
20 |
val empty: T
|
|
21 |
val map_base: (string -> string) -> T -> T
|
|
22 |
val qualify: string -> T -> T
|
28941
|
23 |
val add_prefix: bool -> string -> T -> T
|
|
24 |
val map_prefix: ((string * bool) list -> T -> T) -> T -> T
|
28965
|
25 |
val is_empty: T -> bool
|
29006
|
26 |
val base_name: T -> string
|
28965
|
27 |
val pos_of: T -> Position.T
|
|
28 |
val dest: T -> (string * bool) list * string
|
28941
|
29 |
val display: T -> string
|
|
30 |
end
|
|
31 |
|
|
32 |
structure Binding : BINDING =
|
|
33 |
struct
|
|
34 |
|
|
35 |
(** global flags **)
|
|
36 |
|
|
37 |
val long_names = ref false;
|
|
38 |
val short_names = ref false;
|
|
39 |
val unique_names = ref true;
|
|
40 |
|
|
41 |
|
|
42 |
(** binding representation **)
|
|
43 |
|
|
44 |
datatype T = Binding of ((string * bool) list * string) * Position.T;
|
|
45 |
(* (prefix components (with mandatory flag), base name, position) *)
|
|
46 |
|
28965
|
47 |
fun name_pos (name, pos) = Binding (([], name), pos);
|
|
48 |
fun name name = name_pos (name, Position.none);
|
|
49 |
val empty = name "";
|
28941
|
50 |
|
|
51 |
fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
|
|
52 |
|
28965
|
53 |
val map_base = map_binding o apsnd;
|
|
54 |
|
|
55 |
fun qualify_base path name =
|
|
56 |
if path = "" orelse name = "" then name
|
|
57 |
else path ^ "." ^ name;
|
|
58 |
|
|
59 |
val qualify = map_base o qualify_base;
|
29006
|
60 |
(*FIXME should all operations on bare names move here from name_space.ML ?*)
|
28941
|
61 |
|
|
62 |
fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
|
|
63 |
else (map_binding o apfst) (cons (prfx, sticky)) b;
|
|
64 |
|
|
65 |
fun map_prefix f (Binding ((prefix, name), pos)) =
|
28965
|
66 |
f prefix (name_pos (name, pos));
|
|
67 |
|
|
68 |
fun is_empty (Binding ((_, name), _)) = name = "";
|
29006
|
69 |
fun base_name (Binding ((_, name), _)) = name;
|
28965
|
70 |
fun pos_of (Binding (_, pos)) = pos;
|
|
71 |
fun dest (Binding (prefix_name, _)) = prefix_name;
|
28941
|
72 |
|
|
73 |
fun display (Binding ((prefix, name), _)) =
|
|
74 |
let
|
|
75 |
fun mk_prefix (prfx, true) = prfx
|
|
76 |
| mk_prefix (prfx, false) = enclose "(" ")" prfx
|
|
77 |
in if not (! long_names) orelse null prefix orelse name = "" then name
|
|
78 |
else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
|
|
79 |
end;
|
|
80 |
|
|
81 |
end;
|
|
82 |
|
|
83 |
structure Basic_Binding : BASIC_BINDING = Binding;
|
|
84 |
open Basic_Binding;
|