(* Title: Pure/General/long_name.ML
Author: Makarius
Long names.
*)
signature LONG_NAME =
sig
val separator: string
val append: string -> string -> string
val qualify: string -> string -> string
val is_qualified: string -> bool
val qualifier: string -> string
val base_name: string -> string
val map_base_name: (string -> string) -> string -> string
val count: string -> int
val hidden: string -> string
val is_hidden: string -> bool
val dest_hidden: string -> string option
val localN: string
val dest_local: string -> string option
val implode: string list -> string
val explode: string -> string list
type chunks
val count_chunks: chunks -> int
val size_chunks: chunks -> int
val empty_chunks: chunks
val is_empty_chunks: chunks -> bool
val base_chunks: string -> chunks
val suppress_chunks: int -> bool list -> string -> chunks
val make_chunks: string -> chunks
val explode_chunks: chunks -> string list
val implode_chunks: chunks -> string
val compare_chunks: chunks ord
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.nth separator 0;
fun append name1 "" = name1
| append "" name2 = name2
| append name1 name2 = name1 ^ separator ^ name2;
fun qualify qual name =
if qual = "" orelse name = "" then name
else qual ^ separator ^ name;
fun last_separator name =
let fun last i = if i < 0 orelse String.nth name i = separator_char then i else last (i - 1)
in last (size name - 1) end;
fun is_qualified name = last_separator name >= 0;
fun qualifier name =
let val i = last_separator name
in if i < 0 then "" else String.substring (name, 0, i) end;
fun base_name name =
let
val i = last_separator name;
val j = i + 1;
in if i < 0 then name else String.substring (name, j, size name - j) end;
fun map_base_name f name =
if name = "" then ""
else qualify (qualifier name) (f (base_name name));
fun count "" = 0
| count name = String.fold (fn c => c = separator_char ? Integer.add 1) name 1;
val hidden_prefix = "??.";
val hidden = prefix hidden_prefix;
val is_hidden = String.isPrefix hidden_prefix;
val dest_hidden = try (unprefix hidden_prefix);
val localN = "local";
val dest_local = try (unprefix "local.");
val implode = space_implode separator;
val explode = space_explode separator;
(* compact representation of chunks *)
local
fun failure string msg =
raise Fail ("Malformed qualified name " ^ quote string ^ ":\n " ^ msg);
val range_limit = 32768;
val _ =
if ML_Heap.sizeof1 (range_limit * (range_limit - 1)) = 0 then ()
else raise Fail ("Bad Long_Name.range_limit for ML platform " ^ ML_System.platform);
fun range string index len =
if len < range_limit then index * range_limit + len
else failure string ("chunk length beyond " ^ string_of_int range_limit);
fun range_index r = r div range_limit;
fun range_length r = r mod range_limit;
fun range_string s r = String.substring (s, range_index r, range_length r);
in
abstype chunks = Chunks of {range0: int, ranges: int list (*reverse*), string: string}
with
val empty_chunks = Chunks {range0 = 0, ranges = [], string = ""};
fun is_empty_chunks (Chunks {range0, ranges, ...}) =
range0 = 0 andalso null ranges;
fun count_chunks (chunks as Chunks {ranges, ...}) =
if is_empty_chunks chunks then 0
else length ranges + 1;
fun size_chunks (chunks as Chunks {range0, ranges, ...}) =
if is_empty_chunks chunks then 0
else fold (fn r => fn n => n + range_length r + 1) ranges (range_length range0);
fun base_chunks name =
let
val i = last_separator name;
val j = i + 1;
in
if i < 0 then empty_chunks
else Chunks {range0 = range name j (size name - j), ranges = [], string = name}
end;
fun suppress_chunks suppress1 suppress2 string =
let
val n = size string;
fun suppr_chunks suppr1 suppr2 i j rs =
let
val string_end = i >= n;
val chunk_end = string_end orelse String.nth string i = separator_char;
val suppr =
if suppr1 > 0 then true
else if suppr1 < 0 then false
else if null suppr2 then false
else hd suppr2;
val suppr1' =
if chunk_end andalso suppr1 > 0 then suppr1 - 1
else if chunk_end andalso suppr1 < 0 then suppr1 + 1
else suppr1;
val suppr2' =
if chunk_end andalso suppr1 = 0 andalso not (null suppr2)
then tl suppr2 else suppr2;
val i' = i + 1;
val j' = if chunk_end then i' else j;
val rs' = if chunk_end andalso not suppr then range string j (i - j) :: rs else rs;
in
if not string_end then suppr_chunks suppr1' suppr2' i' j' rs'
else if not (suppr1' = 0 andalso null suppr2') then
failure string ("cannot suppress chunks beyond " ^ string_of_int (length rs'))
else
(case rs' of
[] => empty_chunks
| r0 :: rest => Chunks {range0 = r0, ranges = rest, string = string})
end;
in suppr_chunks suppress1 suppress2 0 0 [] end;
val make_chunks = suppress_chunks 0 [];
fun explode_chunks (chunks as Chunks {range0, ranges, string}) =
if is_empty_chunks chunks then []
else fold (cons o range_string string) ranges [range_string string range0];
fun implode_chunks (chunks as Chunks {range0, ranges, string}) =
if size_chunks chunks = size string then string
else if null ranges then range_string string range0
else implode (explode_chunks chunks);
val compare_chunks = pointer_eq_ord (fn (chunks1, chunks2) =>
let
val Chunks {range0 = range01, ranges = ranges1, string = string1} = chunks1;
val Chunks {range0 = range02, ranges = ranges2, string = string2} = chunks2;
val count1 = count_chunks chunks1;
val count2 = count_chunks chunks2;
val range_length_ord = int_ord o apply2 range_length;
fun range_substring_ord arg =
let
val (i, j) = apply2 range_index arg;
val (m, n) = apply2 range_length arg;
fun substring_ord k =
if k < n then
(case Char.compare (String.nth string1 (i + k), String.nth string2 (j + k)) of
EQUAL => substring_ord (k + 1)
| ord => ord)
else EQUAL;
in (case int_ord (m, n) of EQUAL => substring_ord 0 | ord => ord) end;
in
if count1 = 0 andalso count2 = 0 then EQUAL
else
(case int_ord (count1, count2) of
EQUAL =>
(case range_length_ord (range01, range02) of
EQUAL =>
(case dict_ord range_length_ord (ranges1, ranges2) of
EQUAL =>
(case range_substring_ord (range01, range02) of
EQUAL => dict_ord range_substring_ord (ranges1, ranges2)
| ord => ord)
| ord => ord)
| ord => ord)
| ord => ord)
end);
val eq_chunks = is_equal o compare_chunks;
end;
end;
structure Chunks = Change_Table(type key = chunks val ord = compare_chunks);
end;