3 Author: Makarius |
3 Author: Makarius |
4 |
4 |
5 Structured name bindings. |
5 Structured name bindings. |
6 *) |
6 *) |
7 |
7 |
|
8 type bstring = string; (*primitive names to be bound*) |
|
9 |
8 signature BINDING = |
10 signature BINDING = |
9 sig |
11 sig |
10 val separator: string |
|
11 val is_qualified: string -> bool |
|
12 type binding |
12 type binding |
|
13 val dest: binding -> (string * bool) list * (string * bool) list * bstring |
13 val str_of: binding -> string |
14 val str_of: binding -> string |
14 val name_pos: string * Position.T -> binding |
15 val make: bstring * Position.T -> binding |
15 val name: string -> binding |
16 val name: bstring -> binding |
|
17 val pos_of: binding -> Position.T |
|
18 val name_of: binding -> string |
|
19 val map_name: (bstring -> bstring) -> binding -> binding |
16 val empty: binding |
20 val empty: binding |
17 val map_base: (string -> string) -> binding -> binding |
21 val is_empty: binding -> bool |
18 val qualify: string -> binding -> binding |
22 val qualify: bool -> string -> binding -> binding |
|
23 val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding |
19 val add_prefix: bool -> string -> binding -> binding |
24 val add_prefix: bool -> string -> binding -> binding |
20 val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding |
|
21 val is_empty: binding -> bool |
|
22 val base_name: binding -> string |
|
23 val pos_of: binding -> Position.T |
|
24 val dest: binding -> (string * bool) list * string |
|
25 end; |
25 end; |
26 |
26 |
27 structure Binding: BINDING = |
27 structure Binding: BINDING = |
28 struct |
28 struct |
29 |
29 |
30 (** qualification **) |
30 (** representation **) |
31 |
31 |
32 val separator = "."; |
32 (* datatype *) |
33 val is_qualified = exists_string (fn s => s = separator); |
|
34 |
33 |
35 fun reject_qualified kind s = |
34 type component = string * bool; (*name with mandatory flag*) |
36 if is_qualified s then |
35 |
37 error ("Attempt to declare qualified " ^ kind ^ " " ^ quote s) |
36 datatype binding = Binding of |
38 else s; |
37 {prefix: component list, (*system prefix*) |
|
38 qualifier: component list, (*user qualifier*) |
|
39 name: bstring, (*base name*) |
|
40 pos: Position.T}; (*source position*) |
|
41 |
|
42 fun make_binding (prefix, qualifier, name, pos) = |
|
43 Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos}; |
|
44 |
|
45 fun map_binding f (Binding {prefix, qualifier, name, pos}) = |
|
46 make_binding (f (prefix, qualifier, name, pos)); |
|
47 |
|
48 fun dest (Binding {prefix, qualifier, name, ...}) = (prefix, qualifier, name); |
39 |
49 |
40 |
50 |
41 (** binding representation **) |
51 (* diagnostic output *) |
42 |
52 |
43 datatype binding = Binding of ((string * bool) list * string) * Position.T; |
53 val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?"); |
44 (* (prefix components (with mandatory flag), base name, position) *) |
|
45 |
54 |
46 fun str_of (Binding ((prefix, name), _)) = |
55 fun str_of (Binding {prefix, qualifier, name, pos}) = |
47 let |
56 let |
48 fun mk_prefix (prfx, true) = prfx |
57 val text = |
49 | mk_prefix (prfx, false) = enclose "(" ")" prfx |
58 (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^ |
50 in space_implode "." (map mk_prefix prefix) ^ ":" ^ name end; |
59 str_of_components qualifier ^ ":" ^ name; |
|
60 val props = Position.properties_of pos; |
|
61 in Markup.markup (Markup.properties props (Markup.binding name)) text end; |
51 |
62 |
52 |
63 |
53 fun name_pos (name, pos) = Binding (([], name), pos); |
64 |
54 fun name name = name_pos (name, Position.none); |
65 (** basic operations **) |
|
66 |
|
67 (* name and position *) |
|
68 |
|
69 fun make (name, pos) = make_binding ([], [], name, pos); |
|
70 fun name name = make (name, Position.none); |
|
71 |
|
72 fun pos_of (Binding {pos, ...}) = pos; |
|
73 fun name_of (Binding {name, ...}) = name; |
|
74 |
|
75 fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos)); |
|
76 |
55 val empty = name ""; |
77 val empty = name ""; |
|
78 fun is_empty b = name_of b = ""; |
56 |
79 |
57 fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos); |
|
58 |
80 |
59 val map_base = map_binding o apsnd; |
81 (* user qualifier *) |
60 |
82 |
61 fun qualify_base path name = |
83 fun qualify _ "" = I |
62 if path = "" orelse name = "" then name |
84 | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) => |
63 else path ^ separator ^ name; |
85 (prefix, (qual, mandatory) :: qualifier, name, pos)); |
64 |
86 |
65 val qualify = map_base o qualify_base; |
|
66 (*FIXME should all operations on bare names move here from name_space.ML ?*) |
|
67 |
87 |
68 fun add_prefix sticky "" b = b |
88 (* system prefix *) |
69 | add_prefix sticky prfx b = (map_binding o apfst) |
|
70 (cons ((*reject_qualified "prefix"*) prfx, sticky)) b; |
|
71 |
89 |
72 fun map_prefix f (Binding ((prefix, name), pos)) = |
90 fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) => |
73 f prefix (name_pos (name, pos)); |
91 (f prefix, qualifier, name, pos)); |
74 |
92 |
75 fun is_empty (Binding ((_, name), _)) = name = ""; |
93 fun add_prefix _ "" = I |
76 fun base_name (Binding ((_, name), _)) = name; |
94 | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory)); |
77 fun pos_of (Binding (_, pos)) = pos; |
|
78 fun dest (Binding (prefix_name, _)) = prefix_name; |
|
79 |
95 |
80 end; |
96 end; |
81 |
97 |
82 type binding = Binding.binding; |
98 type binding = Binding.binding; |
83 |
99 |