name spaces and name bindings
authorhaftmann
Thu Nov 20 14:51:40 2008 +0100 (2008-11-20)
changeset 28860b1d46059d502
parent 28859 d50b523c55db
child 28861 f53abb0733ee
name spaces and name bindings
src/Pure/General/name_space.ML
src/Pure/name.ML
     1.1 --- a/src/Pure/General/name_space.ML	Thu Nov 20 10:29:35 2008 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Nov 20 14:51:40 2008 +0100
     1.3 @@ -16,6 +16,19 @@
     1.4    val unique_names: bool ref
     1.5  end;
     1.6  
     1.7 +signature NAME_BINDING =
     1.8 +sig
     1.9 +  type binding
    1.10 +  val binding_pos: string * Position.T -> binding
    1.11 +  val binding: string -> binding
    1.12 +  val no_binding: binding
    1.13 +  val dest_binding: binding -> (string * bool) list * string
    1.14 +  val is_nothing: binding -> bool
    1.15 +  val pos_of: binding -> Position.T
    1.16 +  val map_binding: ((string * bool) list * string -> (string * bool) list * string)
    1.17 +    -> binding -> binding
    1.18 +end
    1.19 +
    1.20  signature NAME_SPACE =
    1.21  sig
    1.22    include BASIC_NAME_SPACE
    1.23 @@ -46,8 +59,15 @@
    1.24    val no_base_names: naming -> naming
    1.25    val qualified_names: naming -> naming
    1.26    val sticky_prefix: string -> naming -> naming
    1.27 +  include NAME_BINDING
    1.28 +  val full_binding: naming -> binding -> string
    1.29 +  val declare_binding: naming -> binding -> T -> string * T
    1.30    type 'a table = T * 'a Symtab.table
    1.31    val empty_table: 'a table
    1.32 +  val table_declare: naming -> binding * 'a
    1.33 +    -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    1.34 +  val table_declare_permissive: naming -> binding * 'a
    1.35 +    -> 'a table -> string * 'a table
    1.36    val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    1.37    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.38    val dest_table: 'a table -> (string * 'a) list
    1.39 @@ -220,6 +240,23 @@
    1.40  
    1.41  
    1.42  
    1.43 +(** generic name bindings **)
    1.44 +
    1.45 +datatype binding = Binding of ((string * bool) list * string) * Position.T;
    1.46 +
    1.47 +fun binding_pos (name, pos) = Binding (([], name), pos);
    1.48 +fun binding name = binding_pos (name, Position.none);
    1.49 +val no_binding = binding "";
    1.50 +
    1.51 +fun pos_of (Binding (_, pos)) = pos;
    1.52 +fun dest_binding (Binding (prefix_name, _)) = prefix_name;
    1.53 +
    1.54 +fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
    1.55 +
    1.56 +fun is_nothing (Binding ((_, name), _)) = name = "";
    1.57 +
    1.58 +
    1.59 +
    1.60  (** naming contexts **)
    1.61  
    1.62  (* datatype naming *)
    1.63 @@ -235,23 +272,6 @@
    1.64  fun external_names naming = map implode_name o #2 o accesses naming o explode_name;
    1.65  
    1.66  
    1.67 -(* declarations *)
    1.68 -
    1.69 -fun full (Naming (path, (qualify, _))) = qualify path;
    1.70 -
    1.71 -fun declare naming name space =
    1.72 -  if is_hidden name then
    1.73 -    error ("Attempt to declare hidden name " ^ quote name)
    1.74 -  else
    1.75 -    let
    1.76 -      val names = explode_name name;
    1.77 -      val _ = (null names orelse exists (fn s => s = "") names
    1.78 -          orelse exists_string (fn s => s = "\"") name) andalso
    1.79 -        error ("Bad name declaration " ^ quote name);
    1.80 -      val (accs, accs') = pairself (map implode_name) (accesses naming names);
    1.81 -    in space |> fold (add_name name) accs |> put_accesses name accs' end;
    1.82 -
    1.83 -
    1.84  (* manipulate namings *)
    1.85  
    1.86  fun reject_qualified name =
    1.87 @@ -277,6 +297,36 @@
    1.88    Naming (append path prfx,
    1.89      (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
    1.90  
    1.91 +val apply_prefix =
    1.92 +  let
    1.93 +    fun mk_prefix (prfx, true) = sticky_prefix prfx
    1.94 +      | mk_prefix (prfx, false) = add_path prfx;
    1.95 +  in fold mk_prefix end;
    1.96 +
    1.97 +
    1.98 +(* declarations *)
    1.99 +
   1.100 +fun full (Naming (path, (qualify, _))) = qualify path;
   1.101 +
   1.102 +fun declare naming name space =
   1.103 +  if is_hidden name then
   1.104 +    error ("Attempt to declare hidden name " ^ quote name)
   1.105 +  else
   1.106 +    let
   1.107 +      val names = explode_name name;
   1.108 +      val _ = (null names orelse exists (fn s => s = "") names
   1.109 +          orelse exists_string (fn s => s = "\"") name) andalso
   1.110 +        error ("Bad name declaration " ^ quote name);
   1.111 +      val (accs, accs') = pairself (map implode_name) (accesses naming names);
   1.112 +    in space |> fold (add_name name) accs |> put_accesses name accs' end;
   1.113 +
   1.114 +fun declare_binding bnaming (Binding ((prefix, bname), _)) =
   1.115 +  let
   1.116 +    val naming = apply_prefix prefix bnaming;
   1.117 +    val dname = full bnaming bname;
   1.118 +    val name = full naming bname;
   1.119 +  in declare naming name #> pair name end;
   1.120 +
   1.121  
   1.122  
   1.123  (** name spaces coupled with symbol tables **)
   1.124 @@ -285,6 +335,17 @@
   1.125  
   1.126  val empty_table = (empty, Symtab.empty);
   1.127  
   1.128 +fun gen_table_declare update naming (binding, x) (space, tab) =
   1.129 +  let
   1.130 +    val (name, space') = declare_binding naming binding space;
   1.131 +  in (name, (space', update (name, x) tab)) end;
   1.132 +
   1.133 +fun table_declare naming = gen_table_declare Symtab.update_new naming;
   1.134 +fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
   1.135 +
   1.136 +fun full_binding naming (Binding ((prefix, bname), _)) =
   1.137 +  full (apply_prefix prefix naming) bname;
   1.138 +
   1.139  fun extend_table naming bentries (space, tab) =
   1.140    let val entries = map (apfst (full naming)) bentries
   1.141    in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
     2.1 --- a/src/Pure/name.ML	Thu Nov 20 10:29:35 2008 +0100
     2.2 +++ b/src/Pure/name.ML	Thu Nov 20 14:51:40 2008 +0100
     2.3 @@ -28,26 +28,22 @@
     2.4    val variants: string list -> context -> string list * context
     2.5    val variant_list: string list -> string list -> string list
     2.6    val variant: string list -> string -> string
     2.7 -  type binding
     2.8 -  val binding_pos: string * Position.T -> binding
     2.9 -  val binding: string -> binding
    2.10 -  val no_binding: binding
    2.11 -  val prefix_of: binding -> (string * bool) list
    2.12 -  val name_of: binding -> string
    2.13 -  val name_with_prefix: binding -> string (*FIXME*)
    2.14 -  val is_nothing: binding -> bool
    2.15 -  val pos_of: binding -> Position.T
    2.16 +
    2.17 +  include NAME_BINDING
    2.18    val add_prefix: bool -> string -> binding -> binding
    2.19    val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
    2.20 -  val map_name: (string -> string) -> binding -> binding
    2.21 -  val qualified: string -> binding -> binding
    2.22 -  val namify: NameSpace.naming -> binding -> NameSpace.naming * string
    2.23 -  val output: binding -> string
    2.24 +  val name_of: binding -> string (*FIMXE legacy*)
    2.25 +  val map_name: (string -> string) -> binding -> binding (*FIMXE legacy*)
    2.26 +  val qualified: string -> binding -> binding (*FIMXE legacy*)
    2.27 +  val display: binding -> string
    2.28 +  val namify: NameSpace.naming -> binding -> NameSpace.naming * string (*FIMXE legacy*)
    2.29  end;
    2.30  
    2.31  structure Name: NAME =
    2.32  struct
    2.33  
    2.34 +open NameSpace;
    2.35 +
    2.36  (** common defaults **)
    2.37  
    2.38  val uu = "uu";
    2.39 @@ -155,45 +151,37 @@
    2.40  fun variant used = singleton (variant_list used);
    2.41  
    2.42  
    2.43 -
    2.44  (** generic name bindings **)
    2.45  
    2.46 -datatype binding = Binding of ((string * bool) list * string) * Position.T;
    2.47 -
    2.48 -fun prefix_of (Binding ((prefix, _), _)) = prefix;
    2.49 -fun name_of (Binding ((_, name), _)) = name;
    2.50 -fun pos_of (Binding (_, pos)) = pos;
    2.51 -
    2.52 -fun binding_pos (name, pos) = Binding (([], name), pos);
    2.53 -fun binding name = binding_pos (name, Position.none);
    2.54 -val no_binding = binding "";
    2.55 +fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
    2.56 +  else (map_binding o apfst) (cons (prfx, sticky)) b;
    2.57  
    2.58 -fun map_binding f (Binding bnd) = Binding (f bnd);
    2.59 -
    2.60 -fun add_prefix sticky prfx binding = if prfx = "" then error "empty name prefix"
    2.61 -  else (map_binding o apfst o apfst) (cons (prfx, sticky)) binding;
    2.62 -
    2.63 -fun map_prefix f (Binding ((prefix, name), pos)) =
    2.64 -  f prefix (binding_pos (name, pos));
    2.65 -
    2.66 -val map_name = map_binding o apfst o apsnd;
    2.67 +val prefix_of = fst o dest_binding;
    2.68 +val name_of = snd o dest_binding;
    2.69 +val map_name = map_binding o apsnd;
    2.70  val qualified = map_name o NameSpace.qualified;
    2.71  
    2.72 -fun is_nothing (Binding ((_, name), _)) = name = "";
    2.73 +fun map_prefix f b =
    2.74 +  let
    2.75 +    val (prefix, name) = dest_binding b;
    2.76 +    val pos = pos_of b;
    2.77 +  in f prefix (binding_pos (name, pos)) end;
    2.78  
    2.79 -fun name_with_prefix (Binding ((prefix, name), _)) =
    2.80 -  NameSpace.implode (map_filter
    2.81 -    (fn (prfx, sticky) => if sticky then SOME prfx else NONE) prefix @ [name]);
    2.82 -
    2.83 -fun namify naming (Binding ((prefix, name), _)) =
    2.84 +fun namify naming b =
    2.85    let
    2.86 -    fun mk_prefix (prfx, true) = NameSpace.sticky_prefix prfx
    2.87 -      | mk_prefix (prfx, false) = NameSpace.add_path prfx;
    2.88 +    val (prefix, name) = dest_binding b
    2.89 +    fun mk_prefix (prfx, true) = sticky_prefix prfx
    2.90 +      | mk_prefix (prfx, false) = add_path prfx;
    2.91      val naming' = fold mk_prefix prefix naming;
    2.92 -  in (naming', NameSpace.full naming' name) end;
    2.93 +  in (naming', full naming' name) end;
    2.94  
    2.95 -fun output (Binding ((prefix, name), _)) =
    2.96 -  if null prefix orelse name = "" then name
    2.97 -  else NameSpace.implode (map fst prefix) ^ " / " ^ name;
    2.98 +fun display b =
    2.99 +  let
   2.100 +    val (prefix, name) = dest_binding b
   2.101 +    fun mk_prefix (prfx, true) = prfx
   2.102 +      | mk_prefix (prfx, false) = enclose "(" ")" prfx
   2.103 +  in if not (! NameSpace.long_names) orelse null prefix orelse name = "" then name
   2.104 +    else NameSpace.implode (map mk_prefix prefix) ^ ":" ^ name
   2.105 +  end;
   2.106  
   2.107  end;