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