--- a/src/Pure/General/long_name.ML Thu Apr 13 14:54:03 2023 +0200
+++ b/src/Pure/General/long_name.ML Fri Apr 14 10:12:30 2023 +0200
@@ -21,12 +21,26 @@
val qualifier: string -> string
val base_name: string -> string
val map_base_name: (string -> string) -> string -> string
+ type chunks
+ val count_chunks: chunks -> int
+ val size_chunks: chunks -> int
+ val empty_chunks: chunks
+ val make_chunks: bool list -> string -> chunks
+ val chunks: string -> chunks
+ val explode_chunks: chunks -> string list
+ val implode_chunks: chunks -> string
+ val compare_chunks: chunks * chunks -> order
+ val eq_chunks: chunks * chunks -> bool
+ structure Chunks: CHANGE_TABLE
end;
structure Long_Name: LONG_NAME =
struct
+(* long names separated by "." *)
+
val separator = ".";
+val separator_char = String.sub (separator, 0);
val is_qualified = exists_string (fn s => s = separator);
@@ -52,15 +66,130 @@
if qual = "" orelse name = "" then name
else qual ^ separator ^ name;
-fun qualifier "" = ""
- | qualifier name = implode (#1 (split_last (explode name)));
-
-fun base_name "" = ""
- | base_name name = List.last (explode name);
-
fun map_base_name _ "" = ""
| map_base_name f name =
let val names = explode name
in implode (nth_map (length names - 1) f names) end;
+
+(* compact representation of chunks *)
+
+local
+
+fun mask_bad s = s = 0w0;
+fun mask_set s m = Word.orb (m, s);
+fun mask_push s = Word.<< (s, 0w1);
+fun mask_next m = Word.>> (m, 0w1);
+fun mask_keep m = Word.andb (m, 0w1) = 0w0;
+
+fun string_ops string =
+ let
+ val n = size string;
+ fun char i = String.sub (string, i);
+ fun string_end i = i >= n;
+ fun chunk_end i = string_end i orelse char i = separator_char;
+ in {string_end = string_end, chunk_end = chunk_end} end;
+
+in
+
+abstype chunks = Chunks of {count: int, size: int, mask: word, string: string}
+with
+
+fun count_chunks (Chunks {count, ...}) = count;
+fun size_chunks (Chunks {size, ...}) = size;
+
+val empty_chunks = Chunks {count = 0, size = 0, mask = 0w0, string = ""};
+
+fun make_chunks suppress string =
+ let
+ val {string_end, chunk_end, ...} = string_ops string;
+
+ fun err msg = raise Fail ("Malformed qualified name " ^ quote string ^ ":\n " ^ msg);
+
+ fun make suppr i k l m s =
+ let
+ val is_end = chunk_end i;
+ val keep = null suppr orelse not (hd suppr);
+
+ val suppr' = if is_end andalso not (null suppr) then tl suppr else suppr;
+ val l' = if keep then l + 1 else l;
+ val k' = if is_end andalso keep andalso l' > 0 then k + 1 else k;
+ val m' =
+ if not is_end orelse keep then m
+ else if mask_bad s then
+ err ("cannot suppress chunks beyond word size " ^ string_of_int Word.wordSize)
+ else mask_set s m;
+ val s' = if is_end then mask_push s else s;
+ in
+ if not (string_end i) then make suppr' (i + 1) k' l' m' s'
+ else if not (null suppr') then err ("cannot suppress chunks beyond " ^ string_of_int k')
+ else if k' = 0 then empty_chunks
+ else Chunks {count = k', size = Int.max (0, l' - 1), mask = m', string = string}
+ end;
+ in make suppress 0 0 0 0w0 0w1 end;
+
+val chunks = make_chunks [];
+
+fun expand_chunks f (Chunks {count, size, mask, string}) =
+ let
+ val {string_end, chunk_end, ...} = string_ops string;
+
+ fun explode bg en m acc =
+ let
+ val is_end = chunk_end en;
+
+ val en' = en + 1;
+ val bg' = if is_end then en' else bg;
+ val m' = if is_end then mask_next m else m;
+ val acc' = if is_end andalso mask_keep m then f (string, bg, en - bg) :: acc else acc;
+ in if string_end en then rev acc' else explode bg' en' m' acc' end;
+ in
+ if count = 0 then []
+ else if count = 1 andalso size = String.size string then [f (string, 0, size)]
+ else explode 0 0 mask []
+ end;
+
+val explode_chunks = expand_chunks String.substring;
+val implode_chunks = implode o explode_chunks;
+
+val compare_chunks =
+ pointer_eq_ord (fn (chunks1, chunks2) =>
+ let
+ val Chunks args1 = chunks1;
+ val Chunks args2 = chunks2;
+ val ord1 =
+ int_ord o apply2 #size |||
+ int_ord o apply2 #count;
+ val ord2 =
+ dict_ord int_ord o apply2 (expand_chunks #3) |||
+ dict_ord Substring.compare o apply2 (expand_chunks Substring.substring);
+ in
+ (case ord1 (args1, args2) of
+ EQUAL =>
+ if #mask args1 = #mask args2 andalso #string args1 = #string args2 then EQUAL
+ else ord2 (chunks1, chunks2)
+ | ord => ord)
+ end);
+
+val eq_chunks = is_equal o compare_chunks;
+
end;
+
+end;
+
+structure Chunks = Change_Table(type key = chunks val ord = compare_chunks);
+
+
+(* split name *)
+
+fun qualifier name =
+ if is_qualified name
+ then String.substring (name, 0, Int.max (0, List.last (expand_chunks #2 (chunks name)) - 1))
+ else "";
+
+fun base_name name =
+ if is_qualified name
+ then String.substring (List.last (expand_chunks I (chunks name)))
+ else name;
+
+end;
--- a/src/Pure/General/name_space.ML Thu Apr 13 14:54:03 2023 +0200
+++ b/src/Pure/General/name_space.ML Fri Apr 14 10:12:30 2023 +0200
@@ -126,7 +126,8 @@
(* internal names *)
-type internals = (string list * string list) Change_Table.T; (*xname -> visible, hidden*)
+type internal = string list * string list; (*visible, hidden*)
+type internals = internal Change_Table.T; (*xname -> internal*)
fun map_internals f xname : internals -> internals =
Change_Table.map_default (xname, ([], [])) f;
@@ -140,57 +141,59 @@
(* external accesses *)
-type accesses = (xstring list * xstring list); (*input / output fragments*)
-type entries = (accesses * entry) Change_Table.T; (*name -> accesses, entry*)
+type external = {accesses: xstring list, accesses': xstring list, entry: entry};
+type externals = external Change_Table.T; (*name -> external*)
(* datatype T *)
-datatype T = Name_Space of {kind: string, internals: internals, entries: entries};
+datatype T = Name_Space of {kind: string, internals: internals, externals: externals};
-fun make_name_space (kind, internals, entries) =
- Name_Space {kind = kind, internals = internals, entries = entries};
+fun make_name_space (kind, internals, externals) =
+ Name_Space {kind = kind, internals = internals, externals = externals};
-fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
- make_name_space (f (kind, internals, entries));
+fun map_name_space f (Name_Space {kind = kind, internals = internals, externals = externals}) =
+ make_name_space (f (kind, internals, externals));
-fun change_base_space begin = map_name_space (fn (kind, internals, entries) =>
- (kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries));
+fun change_base_space begin = map_name_space (fn (kind, internals, externals) =>
+ (kind, Change_Table.change_base begin internals, Change_Table.change_base begin externals));
-val change_ignore_space = map_name_space (fn (kind, internals, entries) =>
- (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries));
+val change_ignore_space = map_name_space (fn (kind, internals, externals) =>
+ (kind, Change_Table.change_ignore internals, Change_Table.change_ignore externals));
fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty);
fun kind_of (Name_Space {kind, ...}) = kind;
+fun lookup_internals (Name_Space {internals, ...}) = Change_Table.lookup internals;
+fun lookup_externals (Name_Space {externals, ...}) = Change_Table.lookup externals;
-fun gen_markup def (Name_Space {kind, entries, ...}) name =
- (case Change_Table.lookup entries name of
+fun gen_markup def space name =
+ (case lookup_externals space name of
NONE => Markup.intensify
- | SOME (_, entry) => entry_markup def kind (name, entry));
+ | SOME {entry, ...} => entry_markup def (kind_of space) (name, entry));
val markup = gen_markup {def = false};
val markup_def = gen_markup {def = true};
-fun undefined (space as Name_Space {kind, entries, ...}) bad =
+fun undefined (space as Name_Space {kind, externals, ...}) bad =
let
val (prfx, sfx) =
(case Long_Name.dest_hidden bad of
SOME name =>
- if Change_Table.defined entries name
+ if Change_Table.defined externals name
then ("Inaccessible", Markup.markup (markup space name) (quote name))
else ("Undefined", quote name)
| NONE => ("Undefined", quote bad));
in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
-fun get_names (Name_Space {entries, ...}) =
- Change_Table.fold (cons o #1) entries [];
+fun get_names (Name_Space {externals, ...}) =
+ Change_Table.fold (cons o #1) externals [];
-fun the_entry (space as Name_Space {entries, ...}) name =
- (case Change_Table.lookup entries name of
+fun the_entry space name =
+ (case lookup_externals space name of
NONE => error (undefined space name)
- | SOME (_, entry) => entry);
+ | SOME {entry, ...} => entry);
fun the_entry_theory_name space name =
Long_Name.base_name (#theory_long_name (the_entry space name));
@@ -203,8 +206,8 @@
(* intern *)
-fun intern' (Name_Space {internals, ...}) xname =
- (case the_default ([], []) (Change_Table.lookup internals xname) of
+fun intern' space xname =
+ (case the_default ([], []) (lookup_internals space xname) of
([name], _) => (name, true)
| (name :: _, _) => (name, false)
| ([], []) => (Long_Name.hidden xname, true)
@@ -212,13 +215,8 @@
val intern = #1 oo intern';
-fun get_accesses (Name_Space {entries, ...}) name =
- (case Change_Table.lookup entries name of
- NONE => ([], [])
- | SOME (accesses, _) => accesses);
-
-fun is_valid_access (Name_Space {internals, ...}) name xname =
- (case Change_Table.lookup internals xname of
+fun is_valid_access space name xname =
+ (case lookup_internals space xname of
SOME (name' :: _, _) => name = name'
| _ => false);
@@ -239,12 +237,15 @@
let val (name', is_unique) = intern' space xname
in name = name' andalso (not require_unique orelse is_unique) end;
- fun ext [] = if valid false name then name else Long_Name.hidden name
- | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
+ fun extern [] = if valid false name then name else Long_Name.hidden name
+ | extern (a :: bs) = if valid names_unique a then a else extern bs;
in
if names_long then name
else if names_short then Long_Name.base_name name
- else ext (#2 (get_accesses space name))
+ else
+ (case lookup_externals space name of
+ NONE => extern []
+ | SOME {accesses', ...} => extern accesses')
end;
fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
@@ -301,8 +302,8 @@
(* merge *)
fun merge
- (Name_Space {kind = kind1, internals = internals1, entries = entries1},
- Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
+ (Name_Space {kind = kind1, internals = internals1, externals = externals1},
+ Name_Space {kind = kind2, internals = internals2, externals = externals2}) =
let
val kind' =
if kind1 = kind2 then kind1
@@ -313,11 +314,11 @@
if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
then raise Change_Table.SAME
else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
- val entries' = (entries1, entries2) |> Change_Table.join
- (fn name => fn ((_, entry1), (_, entry2)) =>
+ val externals' = (externals1, externals2) |> Change_Table.join
+ (fn name => fn ({entry = entry1, ...}, {entry = entry2, ...}) =>
if #serial entry1 = #serial entry2 then raise Change_Table.SAME
else err_dup kind' (name, entry1) (name, entry2) Position.none);
- in make_name_space (kind', internals', entries') end;
+ in make_name_space (kind', internals', externals') end;
@@ -427,15 +428,15 @@
fun name_spec naming binding =
Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
-fun full_name naming =
- name_spec naming #> #spec #> map #1 #> Long_Name.implode;
-
-val base_name = full_name global_naming #> Long_Name.base_name;
+val full_name = #full_name oo name_spec;
+val base_name = Long_Name.base_name o full_name global_naming;
(* accesses *)
-fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
+local
+
+fun mandatory xs = fold_rev (fn (x, b) => b ? cons x) xs [];
fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
and mandatory_prefixes1 [] = []
@@ -444,46 +445,57 @@
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
+in
+
fun make_accesses naming binding =
- (case name_spec naming binding of
- {restriction = SOME true, ...} => ([], [])
- | {restriction, spec, ...} =>
- let
- val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
- val sfxs = restrict (mandatory_suffixes spec);
- val pfxs = restrict (mandatory_prefixes spec);
- in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
+ let
+ val args as {restriction, spec, ...} = name_spec naming binding;
+ val accesses =
+ if restriction = SOME true then ([], [])
+ else
+ let
+ val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
+ val sfxs = restrict (mandatory_suffixes spec);
+ val pfxs = restrict (mandatory_prefixes spec);
+ in apply2 (map Long_Name.implode o distinct op =) (sfxs @ pfxs, sfxs) end;
+ in (accesses, args) end;
+
+end;
(* hide *)
fun hide fully name space =
- space |> map_name_space (fn (kind, internals, entries) =>
+ space |> map_name_space (fn (kind, internals, externals) =>
let
val _ = the_entry space name;
- val (accs, accs') = get_accesses space name;
- val xnames = filter (is_valid_access space name) accs;
+ val (accesses, accesses') =
+ (case lookup_externals space name of
+ NONE => ([], [])
+ | SOME {accesses, accesses', ...} => (accesses, accesses'));
+ val xnames = filter (is_valid_access space name) accesses;
val internals' = internals
|> hide_name name
|> fold (del_name name)
(if fully then xnames else inter (op =) [Long_Name.base_name name] xnames)
- |> fold (del_name_extra name) accs';
- in (kind, internals', entries) end);
+ |> fold (del_name_extra name) accesses';
+ in (kind, internals', externals) end);
(* alias *)
fun alias naming binding name space =
- space |> map_name_space (fn (kind, internals, entries) =>
+ space |> map_name_space (fn (kind, internals, externals) =>
let
val _ = the_entry space name;
- val (more_accs, more_accs') = make_accesses naming binding;
+ val (more_accs, more_accs') = #1 (make_accesses naming binding);
val internals' = internals |> fold (add_name name) more_accs;
- val entries' = entries
- |> Change_Table.map_entry name (apfst (fn (accs, accs') =>
- (fold_rev (update op =) more_accs accs,
- fold_rev (update op =) more_accs' accs')))
- in (kind, internals', entries') end);
+ val externals' = externals
+ |> Change_Table.map_entry name (fn {accesses, accesses', entry} =>
+ {accesses = fold_rev (update op =) more_accs accesses,
+ accesses' = fold_rev (update op =) more_accs' accesses',
+ entry = entry});
+ in (kind, internals', externals') end);
@@ -512,16 +524,13 @@
(* declaration *)
-fun declared (Name_Space {entries, ...}) = Change_Table.defined entries;
+fun declared (Name_Space {externals, ...}) = Change_Table.defined externals;
fun declare context strict binding space =
let
val naming = naming_of context;
val Naming {group, theory_long_name, ...} = naming;
- val {concealed, spec, ...} = name_spec naming binding;
- val accesses = make_accesses naming binding;
-
- val name = Long_Name.implode (map fst spec);
+ val ((accesses, accesses'), {concealed, full_name = name, ...}) = make_accesses naming binding;
val _ = name = "" andalso error (Binding.bad binding);
val (proper_pos, pos) = Position.default (Binding.pos_of binding);
@@ -532,16 +541,16 @@
pos = pos,
serial = serial ()};
val space' =
- space |> map_name_space (fn (kind, internals, entries) =>
+ space |> map_name_space (fn (kind, internals, externals) =>
let
- val internals' = internals |> fold (add_name name) (#1 accesses);
- val entries' =
+ val internals' = internals |> fold (add_name name) accesses;
+ val externals' =
(if strict then Change_Table.update_new else Change_Table.update)
- (name, (accesses, entry)) entries
+ (name, {accesses = accesses, accesses' = accesses', entry = entry}) externals
handle Change_Table.DUP dup =>
- err_dup kind (dup, #2 (the (Change_Table.lookup entries dup)))
+ err_dup kind (dup, #entry (the (lookup_externals space dup)))
(name, entry) (#pos entry);
- in (kind, internals', entries') end);
+ in (kind, internals', externals') end);
val _ =
if proper_pos andalso Context_Position.is_reported_generic context pos then
Position.report pos (entry_markup {def = true} (kind_of space) (name, entry))