src/Pure/General/name_space.ML
author wenzelm
Tue Mar 03 18:31:59 2009 +0100 (2009-03-03)
changeset 30222 4102bbf2af21
parent 30215 47cce3d47e62
child 30233 6eb726e43ed1
permissions -rw-r--r--
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names;
type binding: maintain explicit qualifier, indepently of base name;
tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused);
Binding.str_of: include markup with position properties;
misc tuning;
     1 (*  Title:      Pure/General/name_space.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Generic name spaces with declared and hidden entries.  Unknown names
     5 are considered global; no support for absolute addressing.
     6 Cf. Pure/General/binding.ML
     7 *)
     8 
     9 type xstring = string;    (*external names*)
    10 
    11 signature BASIC_NAME_SPACE =
    12 sig
    13   val long_names: bool ref
    14   val short_names: bool ref
    15   val unique_names: bool ref
    16 end;
    17 
    18 signature NAME_SPACE =
    19 sig
    20   include BASIC_NAME_SPACE
    21   val hidden: string -> string
    22   val is_hidden: string -> bool
    23   val separator: string                 (*single char*)
    24   val is_qualified: string -> bool
    25   val implode: string list -> string
    26   val explode: string -> string list
    27   val append: string -> string -> string
    28   val qualified: string -> string -> string
    29   val base: string -> string
    30   val qualifier: string -> string
    31   val map_base: (string -> string) -> string -> string
    32   type T
    33   val empty: T
    34   val intern: T -> xstring -> string
    35   val extern: T -> string -> xstring
    36   val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
    37     T -> string -> xstring
    38   val hide: bool -> string -> T -> T
    39   val merge: T * T -> T
    40   type naming
    41   val default_naming: naming
    42   val declare: naming -> binding -> T -> string * T
    43   val full_name: naming -> binding -> string
    44   val external_names: naming -> string -> string list
    45   val path_of: naming -> string
    46   val add_path: string -> naming -> naming
    47   val no_base_names: naming -> naming
    48   val qualified_names: naming -> naming
    49   val sticky_prefix: string -> naming -> naming
    50   type 'a table = T * 'a Symtab.table
    51   val empty_table: 'a table
    52   val bind: naming -> binding * 'a
    53     -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    54   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    55   val join_tables: (string -> 'a * 'a -> 'a)
    56     -> 'a table * 'a table -> 'a table
    57   val dest_table: 'a table -> (string * 'a) list
    58   val extern_table: 'a table -> (xstring * 'a) list
    59 end;
    60 
    61 structure NameSpace: NAME_SPACE =
    62 struct
    63 
    64 (** long identifiers **)
    65 
    66 fun hidden name = "??." ^ name;
    67 val is_hidden = String.isPrefix "??.";
    68 
    69 val separator = ".";
    70 val is_qualified = exists_string (fn s => s = separator);
    71 
    72 val implode_name = space_implode separator;
    73 val explode_name = space_explode separator;
    74 
    75 fun append name1 "" = name1
    76   | append "" name2 = name2
    77   | append name1 name2 = name1 ^ separator ^ name2;
    78 
    79 fun qualified path name =
    80   if path = "" orelse name = "" then name
    81   else path ^ separator ^ name;
    82 
    83 fun base "" = ""
    84   | base name = List.last (explode_name name);
    85 
    86 fun qualifier "" = ""
    87   | qualifier name = implode_name (#1 (split_last (explode_name name)));
    88 
    89 fun map_base _ "" = ""
    90   | map_base f name =
    91       let val names = explode_name name
    92       in implode_name (nth_map (length names - 1) f names) end;
    93 
    94 
    95 (* standard accesses *)
    96 
    97 infixr 6 @@;
    98 fun ([] @@ yss) = []
    99   | ((xs :: xss) @@ yss) = map (fn ys => xs @ ys) yss @ (xss @@ yss);
   100 
   101 fun suffixes_prefixes list =
   102   let
   103     val (xs, ws) = chop (length list - 1) list;
   104     val sfxs = suffixes xs @@ [ws];
   105     val pfxs = prefixes1 xs @@ [ws];
   106   in (sfxs @ pfxs, sfxs) end;
   107 
   108 fun suffixes_prefixes_split i k list =
   109   let
   110     val (((xs, ys), zs), ws) = list |> chop i ||>> chop k ||>> chop (length list - (i + k + 1));
   111     val sfxs =
   112       [ys] @@ suffixes zs @@ [ws] @
   113       suffixes1 xs @@ [ys @ zs @ ws];
   114     val pfxs =
   115       prefixes1 xs @@ [ys @ ws] @
   116       [xs @ ys] @@ prefixes1 zs @@ [ws];
   117   in (sfxs @ pfxs, sfxs) end;
   118 
   119 
   120 
   121 (** name spaces **)
   122 
   123 (* datatype T *)
   124 
   125 datatype T =
   126   NameSpace of
   127     ((string list * string list) * stamp) Symtab.table *   (*internals, hidden internals*)
   128     (string list * stamp) Symtab.table;                    (*externals*)
   129 
   130 val empty = NameSpace (Symtab.empty, Symtab.empty);
   131 
   132 fun lookup (NameSpace (tab, _)) xname =
   133   (case Symtab.lookup tab xname of
   134     NONE => (xname, true)
   135   | SOME (([], []), _) => (xname, true)
   136   | SOME (([name], _), _) => (name, true)
   137   | SOME ((name :: _, _), _) => (name, false)
   138   | SOME (([], name' :: _), _) => (hidden name', true));
   139 
   140 fun get_accesses (NameSpace (_, tab)) name =
   141   (case Symtab.lookup tab name of
   142     NONE => [name]
   143   | SOME (xnames, _) => xnames);
   144 
   145 fun put_accesses name xnames (NameSpace (tab, xtab)) =
   146   NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
   147 
   148 fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, ((names, _), _)) =>
   149   if not (null names) andalso hd names = name then cons xname else I) tab [];
   150 
   151 
   152 (* intern and extern *)
   153 
   154 fun intern space xname = #1 (lookup space xname);
   155 
   156 fun extern_flags {long_names, short_names, unique_names} space name =
   157   let
   158     fun valid unique xname =
   159       let val (name', uniq) = lookup space xname
   160       in name = name' andalso (uniq orelse not unique) end;
   161 
   162     fun ext [] = if valid false name then name else hidden name
   163       | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
   164   in
   165     if long_names then name
   166     else if short_names then base name
   167     else ext (get_accesses space name)
   168   end;
   169 
   170 val long_names = ref false;
   171 val short_names = ref false;
   172 val unique_names = ref true;
   173 
   174 fun extern space name =
   175   extern_flags
   176    {long_names = ! long_names,
   177     short_names = ! short_names,
   178     unique_names = ! unique_names} space name;
   179 
   180 
   181 (* basic operations *)
   182 
   183 local
   184 
   185 fun map_space f xname (NameSpace (tab, xtab)) =
   186   NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
   187     (fn (entry, _) => (f entry, stamp ())) tab, xtab);
   188 
   189 in
   190 
   191 val del_name = map_space o apfst o remove (op =);
   192 fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
   193 val add_name = map_space o apfst o update (op =);
   194 val add_name' = map_space o apsnd o update (op =);
   195 
   196 end;
   197 
   198 
   199 (* hide *)
   200 
   201 fun hide fully name space =
   202   if not (is_qualified name) then
   203     error ("Attempt to hide global name " ^ quote name)
   204   else if is_hidden name then
   205     error ("Attempt to hide hidden name " ^ quote name)
   206   else
   207     let val names = valid_accesses space name in
   208       space
   209       |> add_name' name name
   210       |> fold (del_name name) (if fully then names else names inter_string [base name])
   211       |> fold (del_name_extra name) (get_accesses space name)
   212     end;
   213 
   214 
   215 (* merge *)
   216 
   217 fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
   218   let
   219     val tab' = (tab1, tab2) |> Symtab.join
   220       (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
   221         if stamp1 = stamp2 then raise Symtab.SAME
   222         else
   223           ((Library.merge (op =) (names1, names2),
   224             Library.merge (op =) (names1', names2')), stamp ())));
   225     val xtab' = (xtab1, xtab2) |> Symtab.join
   226       (K (fn ((xnames1, stamp1), (xnames2, stamp2)) =>
   227         if stamp1 = stamp2 then raise Symtab.SAME
   228         else (Library.merge (op =) (xnames1, xnames2), stamp ())));
   229   in NameSpace (tab', xtab') end;
   230 
   231 
   232 
   233 (** naming contexts **)
   234 
   235 (* datatype naming *)
   236 
   237 datatype naming = Naming of
   238   string *                                                 (*path*)
   239   ((string -> string -> string) *                          (*qualify*)
   240    (string list -> string list list * string list list));  (*accesses*)
   241 
   242 fun path_of (Naming (path, _)) = path;
   243 fun accesses (Naming (_, (_, accs))) = accs;
   244 
   245 fun external_names naming = map implode_name o #2 o accesses naming o explode_name;
   246 
   247 
   248 (* manipulate namings *)
   249 
   250 fun reject_qualified name =
   251   if is_qualified name then
   252     error ("Attempt to declare qualified name " ^ quote name)
   253   else name;
   254 
   255 val default_naming =
   256   Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
   257 
   258 fun add_path elems (Naming (path, policy)) =
   259   if elems = "//" then Naming ("", (qualified, #2 policy))
   260   else if elems = "/" then Naming ("", policy)
   261   else if elems = ".." then Naming (qualifier path, policy)
   262   else Naming (append path elems, policy);
   263 
   264 fun no_base_names (Naming (path, (qualify, accs))) =
   265   Naming (path, (qualify, pairself (filter_out (fn [_] => true | _ => false)) o accs));
   266 
   267 fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
   268 
   269 fun sticky_prefix prfx (Naming (path, (qualify, _))) =
   270   Naming (append path prfx,
   271     (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
   272 
   273 val apply_prefix =
   274   let
   275     fun mk_prefix (prfx, true) = sticky_prefix prfx
   276       | mk_prefix (prfx, false) = add_path prfx;
   277   in fold mk_prefix end;
   278 
   279 
   280 (* declarations *)
   281 
   282 fun full_internal (Naming (path, (qualify, _))) = qualify path;
   283 
   284 fun declare_internal naming name space =
   285   if is_hidden name then
   286     error ("Attempt to declare hidden name " ^ quote name)
   287   else
   288     let
   289       val names = explode_name name;
   290       val _ = (null names orelse exists (fn s => s = "") names
   291           orelse exists_string (fn s => s = "\"") name) andalso
   292         error ("Bad name declaration " ^ quote name);
   293       val (accs, accs') = pairself (map implode_name) (accesses naming names);
   294     in space |> fold (add_name name) accs |> put_accesses name accs' end;
   295 
   296 fun full_name naming b =
   297   let val (prefix, qualifier, bname) = Binding.dest b
   298   in full_internal (apply_prefix (prefix @ qualifier) naming) bname end;
   299 
   300 fun declare bnaming b =
   301   let
   302     val (prefix, qualifier, bname) = Binding.dest b;
   303     val naming = apply_prefix (prefix @ qualifier) bnaming;
   304     val name = full_internal naming bname;
   305   in declare_internal naming name #> pair name end;
   306 
   307 
   308 
   309 (** name spaces coupled with symbol tables **)
   310 
   311 type 'a table = T * 'a Symtab.table;
   312 
   313 val empty_table = (empty, Symtab.empty);
   314 
   315 fun bind naming (b, x) (space, tab) =
   316   let
   317     val (name, space') = declare naming b space;
   318   in (name, (space', Symtab.update_new (name, x) tab)) end;
   319 
   320 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   321   (merge (space1, space2), Symtab.merge eq (tab1, tab2));
   322 
   323 fun join_tables f ((space1, tab1), (space2, tab2)) =
   324   (merge (space1, space2), Symtab.join f (tab1, tab2));
   325 
   326 fun ext_table (space, tab) =
   327   Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
   328   |> Library.sort_wrt (#2 o #1);
   329 
   330 fun dest_table tab = map (apfst #1) (ext_table tab);
   331 fun extern_table tab = map (apfst #2) (ext_table tab);
   332 
   333 
   334 (*final declarations of this structure!*)
   335 val implode = implode_name;
   336 val explode = explode_name;
   337 
   338 end;
   339 
   340 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
   341 open BasicNameSpace;
   342