author | wenzelm |
Tue, 03 Mar 2009 21:49:34 +0100 | |
changeset 30232 | 8f551a13ee99 |
parent 30222 | 4102bbf2af21 |
child 30242 | aea5d7fa7ef5 |
permissions | -rw-r--r-- |
28941 | 1 |
(* Title: Pure/General/binding.ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
30214
f84c9f10292a
moved name space externalization flags back to name_space.ML;
wenzelm
parents:
29617
diff
changeset
|
3 |
Author: Makarius |
28941 | 4 |
|
5 |
Structured name bindings. |
|
6 |
*) |
|
7 |
||
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
8 |
type bstring = string; (*primitive names to be bound*) |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
9 |
|
30214
f84c9f10292a
moved name space externalization flags back to name_space.ML;
wenzelm
parents:
29617
diff
changeset
|
10 |
signature BINDING = |
28941 | 11 |
sig |
29581 | 12 |
type binding |
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
13 |
val dest: binding -> (string * bool) list * (string * bool) list * bstring |
30232 | 14 |
val verbose: bool ref |
30217
894eb2034f02
renamed Binding.display to Binding.str_of, which is slightly more canonical;
wenzelm
parents:
30214
diff
changeset
|
15 |
val str_of: binding -> string |
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
16 |
val make: bstring * Position.T -> binding |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
17 |
val name: bstring -> binding |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
18 |
val pos_of: binding -> Position.T |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
19 |
val name_of: binding -> string |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
20 |
val map_name: (bstring -> bstring) -> binding -> binding |
29617 | 21 |
val empty: binding |
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
22 |
val is_empty: binding -> bool |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
23 |
val qualify: bool -> string -> binding -> binding |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
24 |
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding |
29617 | 25 |
val add_prefix: bool -> string -> binding -> binding |
26 |
end; |
|
28941 | 27 |
|
30217
894eb2034f02
renamed Binding.display to Binding.str_of, which is slightly more canonical;
wenzelm
parents:
30214
diff
changeset
|
28 |
structure Binding: BINDING = |
28941 | 29 |
struct |
30 |
||
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
31 |
(** representation **) |
29338 | 32 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
33 |
(* datatype *) |
29338 | 34 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
35 |
type component = string * bool; (*name with mandatory flag*) |
29338 | 36 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
37 |
datatype binding = Binding of |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
38 |
{prefix: component list, (*system prefix*) |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
39 |
qualifier: component list, (*user qualifier*) |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
40 |
name: bstring, (*base name*) |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
41 |
pos: Position.T}; (*source position*) |
28941 | 42 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
43 |
fun make_binding (prefix, qualifier, name, pos) = |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
44 |
Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos}; |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
45 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
46 |
fun map_binding f (Binding {prefix, qualifier, name, pos}) = |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
47 |
make_binding (f (prefix, qualifier, name, pos)); |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
48 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
49 |
fun dest (Binding {prefix, qualifier, name, ...}) = (prefix, qualifier, name); |
30217
894eb2034f02
renamed Binding.display to Binding.str_of, which is slightly more canonical;
wenzelm
parents:
30214
diff
changeset
|
50 |
|
894eb2034f02
renamed Binding.display to Binding.str_of, which is slightly more canonical;
wenzelm
parents:
30214
diff
changeset
|
51 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
52 |
(* diagnostic output *) |
28941 | 53 |
|
30232 | 54 |
val verbose = ref false; |
55 |
||
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
56 |
val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?"); |
28941 | 57 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
58 |
fun str_of (Binding {prefix, qualifier, name, pos}) = |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
59 |
let |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
60 |
val text = |
30232 | 61 |
if ! verbose then |
62 |
(if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^ |
|
63 |
str_of_components qualifier ^ name |
|
64 |
else name; |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
65 |
val props = Position.properties_of pos; |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
66 |
in Markup.markup (Markup.properties props (Markup.binding name)) text end; |
28965 | 67 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
68 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
69 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
70 |
(** basic operations **) |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
71 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
72 |
(* name and position *) |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
73 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
74 |
fun make (name, pos) = make_binding ([], [], name, pos); |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
75 |
fun name name = make (name, Position.none); |
28965 | 76 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
77 |
fun pos_of (Binding {pos, ...}) = pos; |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
78 |
fun name_of (Binding {name, ...}) = name; |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
79 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
80 |
fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos)); |
28941 | 81 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
82 |
val empty = name ""; |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
83 |
fun is_empty b = name_of b = ""; |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
84 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
85 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
86 |
(* user qualifier *) |
28941 | 87 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
88 |
fun qualify _ "" = I |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
89 |
| qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) => |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
90 |
(prefix, (qual, mandatory) :: qualifier, name, pos)); |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
91 |
|
28965 | 92 |
|
30222
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
93 |
(* system prefix *) |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
94 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
95 |
fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) => |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
96 |
(f prefix, qualifier, name, pos)); |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
97 |
|
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
98 |
fun add_prefix _ "" = I |
4102bbf2af21
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents:
30217
diff
changeset
|
99 |
| add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory)); |
28941 | 100 |
|
101 |
end; |
|
102 |
||
30214
f84c9f10292a
moved name space externalization flags back to name_space.ML;
wenzelm
parents:
29617
diff
changeset
|
103 |
type binding = Binding.binding; |
f84c9f10292a
moved name space externalization flags back to name_space.ML;
wenzelm
parents:
29617
diff
changeset
|
104 |