src/Pure/General/name_space.ML
changeset 30240 5b25fee0362c
parent 29848 a7c164e228e1
child 30242 aea5d7fa7ef5
     1.1 --- a/src/Pure/General/name_space.ML	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -3,15 +3,20 @@
     1.4  
     1.5  Generic name spaces with declared and hidden entries.  Unknown names
     1.6  are considered global; no support for absolute addressing.
     1.7 -Cf. Pure/General/binding.ML
     1.8  *)
     1.9  
    1.10 -type bstring = string;    (*simple names to be bound -- legacy*)
    1.11  type xstring = string;    (*external names*)
    1.12  
    1.13 +signature BASIC_NAME_SPACE =
    1.14 +sig
    1.15 +  val long_names: bool ref
    1.16 +  val short_names: bool ref
    1.17 +  val unique_names: bool ref
    1.18 +end;
    1.19 +
    1.20  signature NAME_SPACE =
    1.21  sig
    1.22 -  include BASIC_BINDING
    1.23 +  include BASIC_NAME_SPACE
    1.24    val hidden: string -> string
    1.25    val is_hidden: string -> bool
    1.26    val separator: string                 (*single char*)
    1.27 @@ -27,8 +32,9 @@
    1.28    val empty: T
    1.29    val intern: T -> xstring -> string
    1.30    val extern: T -> string -> xstring
    1.31 +  val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
    1.32 +    T -> string -> xstring
    1.33    val hide: bool -> string -> T -> T
    1.34 -  val get_accesses: T -> string -> xstring list
    1.35    val merge: T * T -> T
    1.36    type naming
    1.37    val default_naming: naming
    1.38 @@ -41,12 +47,11 @@
    1.39    val qualified_names: naming -> naming
    1.40    val sticky_prefix: string -> naming -> naming
    1.41    type 'a table = T * 'a Symtab.table
    1.42 +  val bind: naming -> binding * 'a -> 'a table -> string * 'a table       (*exception Symtab.DUP*)
    1.43    val empty_table: 'a table
    1.44 -  val bind: naming -> binding * 'a
    1.45 -    -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    1.46 -  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.47 -  val join_tables: (string -> 'a * 'a -> 'a)
    1.48 -    -> 'a table * 'a table -> 'a table
    1.49 +  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table  (*exception Symtab.DUP*)
    1.50 +  val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
    1.51 +    'a table * 'a table -> 'a table                                       (*exception Symtab.DUP*)
    1.52    val dest_table: 'a table -> (string * 'a) list
    1.53    val extern_table: 'a table -> (xstring * 'a) list
    1.54  end;
    1.55 @@ -54,16 +59,13 @@
    1.56  structure NameSpace: NAME_SPACE =
    1.57  struct
    1.58  
    1.59 -open Basic_Binding;
    1.60 -
    1.61 -
    1.62  (** long identifiers **)
    1.63  
    1.64  fun hidden name = "??." ^ name;
    1.65  val is_hidden = String.isPrefix "??.";
    1.66  
    1.67 -val separator = Binding.separator;
    1.68 -val is_qualified = Binding.is_qualified;
    1.69 +val separator = ".";
    1.70 +val is_qualified = exists_string (fn s => s = separator);
    1.71  
    1.72  val implode_name = space_implode separator;
    1.73  val explode_name = space_explode separator;
    1.74 @@ -120,37 +122,28 @@
    1.75  
    1.76  datatype T =
    1.77    NameSpace of
    1.78 -    ((string list * string list) * stamp) Symtab.table *   (*internals, hidden internals*)
    1.79 -    (string list * stamp) Symtab.table;                    (*externals*)
    1.80 +    (string list * string list) Symtab.table *   (*internals, hidden internals*)
    1.81 +    string list Symtab.table;                    (*externals*)
    1.82  
    1.83  val empty = NameSpace (Symtab.empty, Symtab.empty);
    1.84  
    1.85  fun lookup (NameSpace (tab, _)) xname =
    1.86    (case Symtab.lookup tab xname of
    1.87      NONE => (xname, true)
    1.88 -  | SOME (([], []), _) => (xname, true)
    1.89 -  | SOME (([name], _), _) => (name, true)
    1.90 -  | SOME ((name :: _, _), _) => (name, false)
    1.91 -  | SOME (([], name' :: _), _) => (hidden name', true));
    1.92 +  | SOME ([], []) => (xname, true)
    1.93 +  | SOME ([name], _) => (name, true)
    1.94 +  | SOME (name :: _, _) => (name, false)
    1.95 +  | SOME ([], name' :: _) => (hidden name', true));
    1.96  
    1.97 -fun ex_mapsto_in (NameSpace (tab, _)) name xname =
    1.98 -    (case Symtab.lookup tab xname of
    1.99 -      SOME ((name'::_, _), _) => name' = name
   1.100 -    | _ => false);
   1.101 -
   1.102 -fun get_accesses' valid_only (ns as (NameSpace (_, tab))) name =
   1.103 -  (case Symtab.lookup tab name of
   1.104 +fun get_accesses (NameSpace (_, xtab)) name =
   1.105 +  (case Symtab.lookup xtab name of
   1.106      NONE => [name]
   1.107 -  | SOME (xnames, _) => if valid_only
   1.108 -                        then filter (ex_mapsto_in ns name) xnames
   1.109 -                        else xnames);
   1.110 -
   1.111 -val get_accesses = get_accesses' true;
   1.112 +  | SOME xnames => xnames);
   1.113  
   1.114  fun put_accesses name xnames (NameSpace (tab, xtab)) =
   1.115 -  NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
   1.116 +  NameSpace (tab, Symtab.update (name, xnames) xtab);
   1.117  
   1.118 -fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, ((names, _), _)) =>
   1.119 +fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, (names, _)) =>
   1.120    if not (null names) andalso hd names = name then cons xname else I) tab [];
   1.121  
   1.122  
   1.123 @@ -158,28 +151,37 @@
   1.124  
   1.125  fun intern space xname = #1 (lookup space xname);
   1.126  
   1.127 -fun extern space name =
   1.128 +fun extern_flags {long_names, short_names, unique_names} space name =
   1.129    let
   1.130      fun valid unique xname =
   1.131        let val (name', uniq) = lookup space xname
   1.132        in name = name' andalso (uniq orelse not unique) end;
   1.133  
   1.134      fun ext [] = if valid false name then name else hidden name
   1.135 -      | ext (nm :: nms) = if valid (! unique_names) nm then nm else ext nms;
   1.136 +      | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
   1.137    in
   1.138 -    if ! long_names then name
   1.139 -    else if ! short_names then base name
   1.140 -    else ext (get_accesses' false space name)
   1.141 +    if long_names then name
   1.142 +    else if short_names then base name
   1.143 +    else ext (get_accesses space name)
   1.144    end;
   1.145  
   1.146 +val long_names = ref false;
   1.147 +val short_names = ref false;
   1.148 +val unique_names = ref true;
   1.149 +
   1.150 +fun extern space name =
   1.151 +  extern_flags
   1.152 +   {long_names = ! long_names,
   1.153 +    short_names = ! short_names,
   1.154 +    unique_names = ! unique_names} space name;
   1.155 +
   1.156  
   1.157  (* basic operations *)
   1.158  
   1.159  local
   1.160  
   1.161  fun map_space f xname (NameSpace (tab, xtab)) =
   1.162 -  NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
   1.163 -    (fn (entry, _) => (f entry, stamp ())) tab, xtab);
   1.164 +  NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab);
   1.165  
   1.166  in
   1.167  
   1.168 @@ -203,7 +205,7 @@
   1.169        space
   1.170        |> add_name' name name
   1.171        |> fold (del_name name) (if fully then names else names inter_string [base name])
   1.172 -      |> fold (del_name_extra name) (get_accesses' false space name)
   1.173 +      |> fold (del_name_extra name) (get_accesses space name)
   1.174      end;
   1.175  
   1.176  
   1.177 @@ -212,15 +214,13 @@
   1.178  fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
   1.179    let
   1.180      val tab' = (tab1, tab2) |> Symtab.join
   1.181 -      (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
   1.182 -        if stamp1 = stamp2 then raise Symtab.SAME
   1.183 -        else
   1.184 -          ((Library.merge (op =) (names1, names2),
   1.185 -            Library.merge (op =) (names1', names2')), stamp ())));
   1.186 +      (K (fn names as ((names1, names1'), (names2, names2')) =>
   1.187 +        if pointer_eq names then raise Symtab.SAME
   1.188 +        else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
   1.189      val xtab' = (xtab1, xtab2) |> Symtab.join
   1.190 -      (K (fn ((xnames1, stamp1), (xnames2, stamp2)) =>
   1.191 -        if stamp1 = stamp2 then raise Symtab.SAME
   1.192 -        else (Library.merge (op =) (xnames1, xnames2), stamp ())));
   1.193 +      (K (fn xnames =>
   1.194 +        if pointer_eq xnames then raise Symtab.SAME
   1.195 +        else (Library.merge (op =) xnames)));
   1.196    in NameSpace (tab', xtab') end;
   1.197  
   1.198  
   1.199 @@ -272,32 +272,33 @@
   1.200    in fold mk_prefix end;
   1.201  
   1.202  
   1.203 -(* declarations *)
   1.204 +(* full name *)
   1.205 +
   1.206 +fun full (Naming (path, (qualify, _))) = qualify path;
   1.207  
   1.208 -fun full_internal (Naming (path, (qualify, _))) = qualify path;
   1.209 +fun full_name naming binding =
   1.210 +  let
   1.211 +    val (prefix, qualifier, bname) = Binding.dest binding;
   1.212 +    val naming' = apply_prefix (prefix @ qualifier) naming;
   1.213 +  in full naming' bname end;
   1.214 +
   1.215 +
   1.216 +(* declaration *)
   1.217  
   1.218 -fun declare_internal naming name space =
   1.219 -  if is_hidden name then
   1.220 -    error ("Attempt to declare hidden name " ^ quote name)
   1.221 -  else
   1.222 -    let
   1.223 -      val names = explode_name name;
   1.224 -      val _ = (null names orelse exists (fn s => s = "") names
   1.225 -          orelse exists_string (fn s => s = "\"") name) andalso
   1.226 -        error ("Bad name declaration " ^ quote name);
   1.227 -      val (accs, accs') = pairself (map implode_name) (accesses naming names);
   1.228 -    in space |> fold (add_name name) accs |> put_accesses name accs' end;
   1.229 +fun declare naming binding space =
   1.230 +  let
   1.231 +    val (prefix, qualifier, bname) = Binding.dest binding;
   1.232 +    val naming' = apply_prefix (prefix @ qualifier) naming;
   1.233 +    val name = full naming' bname;
   1.234 +    val names = explode_name name;
   1.235  
   1.236 -fun full_name naming b =
   1.237 -  let val (prefix, bname) = Binding.dest b
   1.238 -  in full_internal (apply_prefix prefix naming) bname end;
   1.239 +    val _ = (null names orelse exists (fn s => s = "" orelse s = "??") names
   1.240 +        orelse exists_string (fn s => s = "\"") name) andalso
   1.241 +      error ("Bad name declaration " ^ quote (Binding.str_of binding));
   1.242  
   1.243 -fun declare bnaming b =
   1.244 -  let
   1.245 -    val (prefix, bname) = Binding.dest b;
   1.246 -    val naming = apply_prefix prefix bnaming;
   1.247 -    val name = full_internal naming bname;
   1.248 -  in declare_internal naming name #> pair name end;
   1.249 +    val (accs, accs') = pairself (map implode_name) (accesses naming' names);
   1.250 +    val space' = space |> fold (add_name name) accs |> put_accesses name accs';
   1.251 +  in (name, space') end;
   1.252  
   1.253  
   1.254  
   1.255 @@ -305,12 +306,11 @@
   1.256  
   1.257  type 'a table = T * 'a Symtab.table;
   1.258  
   1.259 -val empty_table = (empty, Symtab.empty);
   1.260 +fun bind naming (binding, x) (space, tab) =
   1.261 +  let val (name, space') = declare naming binding space
   1.262 +  in (name, (space', Symtab.update_new (name, x) tab)) end;
   1.263  
   1.264 -fun bind naming (b, x) (space, tab) =
   1.265 -  let
   1.266 -    val (name, space') = declare naming b space;
   1.267 -  in (name, (space', Symtab.update_new (name, x) tab)) end;
   1.268 +val empty_table = (empty, Symtab.empty);
   1.269  
   1.270  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   1.271    (merge (space1, space2), Symtab.merge eq (tab1, tab2));
   1.272 @@ -331,3 +331,7 @@
   1.273  val explode = explode_name;
   1.274  
   1.275  end;
   1.276 +
   1.277 +structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
   1.278 +open BasicNameSpace;
   1.279 +