1(*  Title:      Pure/General/binding.ML
2    Author:     Florian Haftmann, TU Muenchen
3    Author:     Makarius
4
5Structured name bindings.
6*)
7
8type bstring = string;    (*primitive names to be bound*)
9
10signature BINDING =
11sig
12  eqtype scope
13  val new_scope: unit -> scope
14  eqtype binding
15  val path_of: binding -> (string * bool) list
16  val make: bstring * Position.T -> binding
17  val pos_of: binding -> Position.T
18  val set_pos: Position.T -> binding -> binding
19  val reset_pos: binding -> binding
20  val default_pos: binding -> binding
21  val default_pos_of: binding -> Position.T
22  val name: bstring -> binding
23  val name_of: binding -> bstring
24  val map_name: (bstring -> bstring) -> binding -> binding
25  val prefix_name: string -> binding -> binding
26  val suffix_name: string -> binding -> binding
27  val eq_name: binding * binding -> bool
28  val empty: binding
29  val is_empty: binding -> bool
30  val empty_atts: binding * 'a list
31  val is_empty_atts: binding * 'a list -> bool
32  val conglomerate: binding list -> binding
33  val qualify: bool -> string -> binding -> binding
34  val qualify_name: bool -> binding -> string -> binding
35  val qualified_name: string -> binding
36  val prefix_of: binding -> (string * bool) list
37  val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
38  val prefix: bool -> string -> binding -> binding
39  val restricted: (bool * scope) option -> binding -> binding
40  val concealed: binding -> binding
41  val pretty: binding -> Pretty.T
42  val print: binding -> string
43  val bad: binding -> string
44  val check: binding -> unit
45  val name_spec: scope list -> (string * bool) list -> binding ->
46    {restriction: bool option, concealed: bool, spec: (string * bool) list}
47end;
48
49structure Binding: BINDING =
50struct
51
52(** representation **)
53
54(* scope of restricted entries *)
55
56datatype scope = Scope of serial;
57
58fun new_scope () = Scope (serial ());
59
60
61(* binding *)
62
63datatype binding = Binding of
64 {restricted: (bool * scope) option,  (*entry is private (true) or qualified (false) wrt. scope*)
65  concealed: bool,  (*entry is for foundational purposes -- please ignore*)
66  prefix: (string * bool) list,  (*system prefix*)
67  qualifier: (string * bool) list,  (*user qualifier*)
68  name: bstring,  (*base name*)
69  pos: Position.T};  (*source position*)
70
71fun make_binding (restricted, concealed, prefix, qualifier, name, pos) =
72  Binding {restricted = restricted, concealed = concealed, prefix = prefix,
73    qualifier = qualifier, name = name, pos = pos};
74
75fun map_binding f (Binding {restricted, concealed, prefix, qualifier, name, pos}) =
76  make_binding (f (restricted, concealed, prefix, qualifier, name, pos));
77
78fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
79
80fun make (name, pos) = make_binding (NONE, false, [], [], name, pos);
81
82
83
84(** basic operations **)
85
86(* position *)
87
88fun pos_of (Binding {pos, ...}) = pos;
89
90fun set_pos pos =
91  map_binding (fn (restricted, concealed, prefix, qualifier, name, _) =>
92    (restricted, concealed, prefix, qualifier, name, pos));
93
94val reset_pos = set_pos Position.none;
95
96fun default_pos b =
97  if pos_of b = Position.none then set_pos (Position.thread_data ()) b else b;
98
99fun default_pos_of b =
100  let val pos = pos_of b
101  in if pos = Position.none then Position.thread_data () else pos end;
102
103
104(* name *)
105
106fun name name = make (name, Position.none);
107fun name_of (Binding {name, ...}) = name;
108
109fun eq_name (b, b') = name_of b = name_of b';
110
111fun map_name f =
112  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
113    (restricted, concealed, prefix, qualifier, f name, pos));
114
115val prefix_name = map_name o prefix;
116val suffix_name = map_name o suffix;
117
118val empty = name "";
119fun is_empty b = name_of b = "";
120
121val empty_atts = (empty, []);
122fun is_empty_atts (b, atts) = is_empty b andalso null atts;
123
124fun conglomerate [b] = b
125  | conglomerate bs = name (space_implode "_" (map name_of (filter_out is_empty bs)));
126
127
128(* user qualifier *)
129
130fun qualify _ "" = I
131  | qualify mandatory qual =
132      map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
133        (restricted, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
134
135fun qualify_name mandatory binding name' =
136  binding |> map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
137    let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
138    in (restricted, concealed, prefix, qualifier', name', pos) end);
139
140fun qualified_name "" = empty
141  | qualified_name s =
142      let val (qualifier, name) = split_last (Long_Name.explode s)
143      in make_binding (NONE, false, [], map (rpair false) qualifier, name, Position.none) end;
144
145
146(* system prefix *)
147
148fun prefix_of (Binding {prefix, ...}) = prefix;
149
150fun map_prefix f =
151  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
152    (restricted, concealed, f prefix, qualifier, name, pos));
153
154fun prefix _ "" = I
155  | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
156
157
158(* visibility flags *)
159
160fun restricted default =
161  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
162    (if is_some restricted then restricted else default, concealed, prefix, qualifier, name, pos));
163
164val concealed =
165  map_binding (fn (restricted, _, prefix, qualifier, name, pos) =>
166    (restricted, true, prefix, qualifier, name, pos));
167
168
169(* print *)
170
171fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
172  if name = "" then Pretty.str "\"\""
173  else
174    Pretty.markup (Position.markup pos Markup.binding)
175      [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
176    |> Pretty.quote;
177
178val print = Pretty.unformatted_string_of o pretty;
179
180val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o reset_pos);
181
182
183(* check *)
184
185fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding);
186
187fun check binding =
188  if Symbol_Pos.is_identifier (name_of binding) then ()
189  else legacy_feature (bad binding);
190
191
192
193(** resulting name_spec **)
194
195val bad_specs = ["", "??", "__"];
196
197fun name_spec scopes path binding =
198  let
199    val Binding {restricted, concealed, prefix, qualifier, name, ...} = binding;
200    val _ = Long_Name.is_qualified name andalso error (bad binding);
201
202    val restriction =
203      (case restricted of
204        NONE => NONE
205      | SOME (strict, scope) => if member (op =) scopes scope then NONE else SOME strict);
206
207    val spec1 =
208      maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
209    val spec2 = if name = "" then [] else [(name, true)];
210    val spec = spec1 @ spec2;
211    val _ =
212      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
213      andalso error (bad binding);
214  in {restriction = restriction, concealed = concealed, spec = if null spec2 then [] else spec} end;
215
216
217end;
218
219type binding = Binding.binding;
220