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