src/Pure/General/name_space.ML
changeset 30412 7f5b0a020ccd
parent 30359 3f9b3ff851ca
child 30418 b5044aca0729
     1.1 --- a/src/Pure/General/name_space.ML	Tue Mar 10 16:48:27 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 10 16:51:08 2009 +0100
     1.3 @@ -32,7 +32,6 @@
     1.4    val declare: naming -> binding -> T -> string * T
     1.5    val full_name: naming -> binding -> string
     1.6    val external_names: naming -> string -> string list
     1.7 -  val path_of: naming -> string
     1.8    val add_path: string -> naming -> naming
     1.9    val no_base_names: naming -> naming
    1.10    val qualified_names: naming -> naming
    1.11 @@ -50,38 +49,14 @@
    1.12  structure NameSpace: NAME_SPACE =
    1.13  struct
    1.14  
    1.15 -(** long identifiers **)
    1.16 +
    1.17 +(** name spaces **)
    1.18 +
    1.19 +(* hidden entries *)
    1.20  
    1.21  fun hidden name = "??." ^ name;
    1.22  val is_hidden = String.isPrefix "??.";
    1.23  
    1.24 -(* standard accesses *)
    1.25 -
    1.26 -infixr 6 @@;
    1.27 -fun ([] @@ yss) = []
    1.28 -  | ((xs :: xss) @@ yss) = map (fn ys => xs @ ys) yss @ (xss @@ yss);
    1.29 -
    1.30 -fun suffixes_prefixes list =
    1.31 -  let
    1.32 -    val (xs, ws) = chop (length list - 1) list;
    1.33 -    val sfxs = suffixes xs @@ [ws];
    1.34 -    val pfxs = prefixes1 xs @@ [ws];
    1.35 -  in (sfxs @ pfxs, sfxs) end;
    1.36 -
    1.37 -fun suffixes_prefixes_split i k list =
    1.38 -  let
    1.39 -    val (((xs, ys), zs), ws) = list |> chop i ||>> chop k ||>> chop (length list - (i + k + 1));
    1.40 -    val sfxs =
    1.41 -      [ys] @@ suffixes zs @@ [ws] @
    1.42 -      suffixes1 xs @@ [ys @ zs @ ws];
    1.43 -    val pfxs =
    1.44 -      prefixes1 xs @@ [ys @ ws] @
    1.45 -      [xs @ ys] @@ prefixes1 zs @@ [ws];
    1.46 -  in (sfxs @ pfxs, sfxs) end;
    1.47 -
    1.48 -
    1.49 -
    1.50 -(** name spaces **)
    1.51  
    1.52  (* datatype T *)
    1.53  
    1.54 @@ -196,74 +171,95 @@
    1.55  (* datatype naming *)
    1.56  
    1.57  datatype naming = Naming of
    1.58 -  string *                                                 (*path*)
    1.59 -  ((string -> string -> string) *                          (*qualify*)
    1.60 -   (string list -> string list list * string list list));  (*accesses*)
    1.61 + {path: (string * bool) list,
    1.62 +  no_base_names: bool,
    1.63 +  qualified_names: bool};
    1.64  
    1.65 -fun path_of (Naming (path, _)) = path;
    1.66 -fun accesses (Naming (_, (_, accs))) = accs;
    1.67 +fun make_naming (path, no_base_names, qualified_names) =
    1.68 +  Naming {path = path, no_base_names = no_base_names, qualified_names = qualified_names};
    1.69  
    1.70 -fun external_names naming = map Long_Name.implode o #2 o accesses naming o Long_Name.explode;
    1.71 +fun map_naming f (Naming {path, no_base_names, qualified_names}) =
    1.72 +  make_naming (f (path, no_base_names, qualified_names));
    1.73 +
    1.74 +fun path_of (Naming {path, ...}) = path;
    1.75  
    1.76  
    1.77 -(* manipulate namings *)
    1.78 -
    1.79 -fun reject_qualified name =
    1.80 -  if Long_Name.is_qualified name then
    1.81 -    error ("Attempt to declare qualified name " ^ quote name)
    1.82 -  else name;
    1.83 +(* configure naming *)
    1.84  
    1.85 -val default_naming =
    1.86 -  Naming ("", (fn path => Long_Name.qualify path o reject_qualified, suffixes_prefixes));
    1.87 -
    1.88 -fun add_path elems (Naming (path, policy)) =
    1.89 -  if elems = "//" then Naming ("", (Long_Name.qualify, #2 policy))
    1.90 -  else if elems = "/" then Naming ("", policy)
    1.91 -  else if elems = ".." then Naming (Long_Name.qualifier path, policy)
    1.92 -  else Naming (Long_Name.append path elems, policy);
    1.93 +val default_naming = make_naming ([], false, false);
    1.94  
    1.95 -fun no_base_names (Naming (path, (qualify, accs))) =
    1.96 -  Naming (path, (qualify, pairself (filter_out (fn [_] => true | _ => false)) o accs));
    1.97 -
    1.98 -fun qualified_names (Naming (path, (_, accs))) = Naming (path, (Long_Name.qualify, accs));
    1.99 +fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
   1.100 +  if elems = "//" then ([], no_base_names, true)
   1.101 +  else if elems = "/" then ([], no_base_names, qualified_names)
   1.102 +  else if elems = ".." then (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names)
   1.103 +  else (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
   1.104  
   1.105 -fun sticky_prefix prfx (Naming (path, (qualify, _))) =
   1.106 -  Naming (Long_Name.append path prfx,
   1.107 -    (qualify,
   1.108 -      suffixes_prefixes_split (length (Long_Name.explode path)) (length (Long_Name.explode prfx))));
   1.109 +fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
   1.110 +  (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
   1.111  
   1.112 -val apply_prefix =
   1.113 -  let
   1.114 -    fun mk_prefix (prfx, true) = sticky_prefix prfx
   1.115 -      | mk_prefix (prfx, false) = add_path prfx;
   1.116 -  in fold mk_prefix end;
   1.117 +val no_base_names = map_naming (fn (path, _, qualified_names) => (path, true, qualified_names));
   1.118 +val qualified_names = map_naming (fn (path, no_base_names, _) => (path, no_base_names, true));
   1.119  
   1.120  
   1.121  (* full name *)
   1.122  
   1.123 -fun full (Naming (path, (qualify, _))) = qualify path;
   1.124 +fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
   1.125  
   1.126 -fun full_name naming binding =
   1.127 +fun name_spec (Naming {path, qualified_names, ...}) binding =
   1.128    let
   1.129 -    val (prfx, bname) = Binding.dest binding;
   1.130 -    val naming' = apply_prefix prfx naming;
   1.131 -  in full naming' bname end;
   1.132 +    val (prefix, name) = Binding.dest binding;
   1.133 +    val _ = not qualified_names andalso Long_Name.is_qualified name andalso err_bad binding;
   1.134 +
   1.135 +    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
   1.136 +    val spec2 =
   1.137 +      (case try split_last (Long_Name.explode name) of
   1.138 +        NONE => []
   1.139 +      | SOME (qual, base) => map (rpair false) qual @ [(base, true)]);
   1.140 +
   1.141 +    val spec = spec1 @ spec2;
   1.142 +    val _ =
   1.143 +      exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
   1.144 +      andalso err_bad binding;
   1.145 +  in if null spec2 then [] else spec end;
   1.146 +
   1.147 +fun full naming = name_spec naming #> map fst;
   1.148 +fun full_name naming = full naming #> Long_Name.implode;
   1.149 +
   1.150 +
   1.151 +(* accesses *)
   1.152 +
   1.153 +fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
   1.154 +
   1.155 +fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
   1.156 +and mandatory_prefixes1 [] = []
   1.157 +  | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
   1.158 +  | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
   1.159 +
   1.160 +fun mandatory_suffixes1 xs = map rev (mandatory_prefixes1 (rev xs));
   1.161 +fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
   1.162 +
   1.163 +fun accesses (naming as Naming {no_base_names, ...}) binding =
   1.164 +  let
   1.165 +    val spec = name_spec naming binding;
   1.166 +    val sfxs = mandatory_suffixes spec;
   1.167 +    val pfxs = mandatory_prefixes spec;
   1.168 +  in
   1.169 +    (sfxs @ pfxs, sfxs)
   1.170 +    |> pairself (no_base_names ? filter (fn [_] => false | _ => true))
   1.171 +    |> pairself (map Long_Name.implode)
   1.172 +  end;
   1.173 +
   1.174 +fun external_names naming = #2 o accesses naming o Binding.qualified_name;
   1.175  
   1.176  
   1.177  (* declaration *)
   1.178  
   1.179  fun declare naming binding space =
   1.180    let
   1.181 -    val (prfx, bname) = Binding.dest binding;
   1.182 -    val naming' = apply_prefix prfx naming;
   1.183 -    val name = full naming' bname;
   1.184 -    val names = Long_Name.explode name;
   1.185 -
   1.186 -    val _ = (null names orelse exists (fn s => s = "" orelse s = "??") names
   1.187 -        orelse exists_string (fn s => s = "\"") name) andalso
   1.188 -      error ("Bad name declaration " ^ quote (Binding.str_of binding));
   1.189 -
   1.190 -    val (accs, accs') = pairself (map Long_Name.implode) (accesses naming' names);
   1.191 +    val names = full naming binding;
   1.192 +    val name = Long_Name.implode names;
   1.193 +    val _ = name = "" andalso err_bad binding;
   1.194 +    val (accs, accs') = accesses naming binding;
   1.195      val space' = space |> fold (add_name name) accs |> put_accesses name accs';
   1.196    in (name, space') end;
   1.197