src/Pure/General/long_name.ML
author wenzelm
Wed, 12 Mar 2025 11:39:00 +0100
changeset 82265 4b875a4c83b0
parent 79319 2d9baa7ee05a
permissions -rw-r--r--
update for release;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/long_name.ML
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
     3
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
     4
Long names.
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
     5
*)
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
     6
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
     7
signature LONG_NAME =
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
     8
sig
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
     9
  val separator: string
77856
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    10
  val append: string -> string -> string
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    11
  val qualify: string -> string -> string
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    12
  val is_qualified: string -> bool
77855
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    13
  val qualifier: string -> string
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    14
  val base_name: string -> string
77857
82041e01f383 minor performance tuning: more elementary operations;
wenzelm
parents: 77856
diff changeset
    15
  val map_base_name: (string -> string) -> string -> string
77854
64533f3818a4 tuned signature;
wenzelm
parents: 77847
diff changeset
    16
  val count: string -> int
55669
4612c450b59c tuned signature;
wenzelm
parents: 30359
diff changeset
    17
  val hidden: string -> string
59916
wenzelm
parents: 59888
diff changeset
    18
  val is_hidden: string -> bool
59888
27e4d0ab0948 tuned signature;
wenzelm
parents: 56800
diff changeset
    19
  val dest_hidden: string -> string option
56162
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56023
diff changeset
    20
  val localN: string
59888
27e4d0ab0948 tuned signature;
wenzelm
parents: 56800
diff changeset
    21
  val dest_local: string -> string option
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    22
  val implode: string list -> string
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    23
  val explode: string -> string list
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    24
  type chunks
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    25
  val count_chunks: chunks -> int
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    26
  val size_chunks: chunks -> int
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    27
  val empty_chunks: chunks
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
    28
  val is_empty_chunks: chunks -> bool
77861
wenzelm
parents: 77858
diff changeset
    29
  val base_chunks: string -> chunks
77913
019186a60c84 tuned signature;
wenzelm
parents: 77861
diff changeset
    30
  val suppress_chunks: int -> bool list -> string -> chunks
019186a60c84 tuned signature;
wenzelm
parents: 77861
diff changeset
    31
  val make_chunks: string -> chunks
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    32
  val explode_chunks: chunks -> string list
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    33
  val implode_chunks: chunks -> string
77964
d4184ea197ec tuned signature;
wenzelm
parents: 77962
diff changeset
    34
  val compare_chunks: chunks ord
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    35
  val eq_chunks: chunks * chunks -> bool
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    36
  structure Chunks: CHANGE_TABLE
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    37
end;
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    38
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    39
structure Long_Name: LONG_NAME =
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    40
struct
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    41
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    42
(* long names separated by "." *)
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    43
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    44
val separator = ".";
77847
3bb6468d202e more operations, following Isabelle/ML conventions;
wenzelm
parents: 77843
diff changeset
    45
val separator_char = String.nth separator 0;
56800
b904ea8edd73 support for long names in Scala;
wenzelm
parents: 56162
diff changeset
    46
77856
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    47
fun append name1 "" = name1
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    48
  | append "" name2 = name2
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    49
  | append name1 name2 = name1 ^ separator ^ name2;
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    50
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    51
fun qualify qual name =
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    52
  if qual = "" orelse name = "" then name
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    53
  else qual ^ separator ^ name;
e6de70b78117 tuned signature;
wenzelm
parents: 77855
diff changeset
    54
77855
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    55
fun last_separator name =
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    56
  let fun last i = if i < 0 orelse String.nth name i = separator_char then i else last (i - 1)
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    57
  in last (size name - 1) end;
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    58
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    59
fun is_qualified name = last_separator name >= 0;
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    60
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    61
fun qualifier name =
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    62
  let val i = last_separator name
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    63
  in if i < 0 then "" else String.substring (name, 0, i) end;
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    64
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    65
fun base_name name =
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    66
  let
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    67
    val i = last_separator name;
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    68
    val j = i + 1;
ff801186ff66 minor performance tuning: more elementary operations;
wenzelm
parents: 77854
diff changeset
    69
  in if i < 0 then name else String.substring (name, j, size name - j) end;
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    70
77857
82041e01f383 minor performance tuning: more elementary operations;
wenzelm
parents: 77856
diff changeset
    71
fun map_base_name f name =
82041e01f383 minor performance tuning: more elementary operations;
wenzelm
parents: 77856
diff changeset
    72
  if name = "" then ""
82041e01f383 minor performance tuning: more elementary operations;
wenzelm
parents: 77856
diff changeset
    73
  else qualify (qualifier name) (f (base_name name));
82041e01f383 minor performance tuning: more elementary operations;
wenzelm
parents: 77856
diff changeset
    74
77854
64533f3818a4 tuned signature;
wenzelm
parents: 77847
diff changeset
    75
fun count "" = 0
64533f3818a4 tuned signature;
wenzelm
parents: 77847
diff changeset
    76
  | count name = String.fold (fn c => c = separator_char ? Integer.add 1) name 1;
64533f3818a4 tuned signature;
wenzelm
parents: 77847
diff changeset
    77
79319
wenzelm
parents: 77993
diff changeset
    78
val hidden_prefix = "??.";
59916
wenzelm
parents: 59888
diff changeset
    79
val hidden = prefix hidden_prefix;
wenzelm
parents: 59888
diff changeset
    80
val is_hidden = String.isPrefix hidden_prefix;
wenzelm
parents: 59888
diff changeset
    81
val dest_hidden = try (unprefix hidden_prefix);
55669
4612c450b59c tuned signature;
wenzelm
parents: 30359
diff changeset
    82
56162
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56023
diff changeset
    83
val localN = "local";
59888
27e4d0ab0948 tuned signature;
wenzelm
parents: 56800
diff changeset
    84
val dest_local = try (unprefix "local.");
56162
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56023
diff changeset
    85
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    86
val implode = space_implode separator;
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    87
val explode = space_explode separator;
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
    88
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    89
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    90
(* compact representation of chunks *)
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    91
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    92
local
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
    93
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
    94
fun failure string msg =
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
    95
  raise Fail ("Malformed qualified name " ^ quote string ^ ":\n  " ^ msg);
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
    96
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
    97
val range_limit = 32768;
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
    98
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
    99
val _ =
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   100
  if ML_Heap.sizeof1 (range_limit * (range_limit - 1)) = 0 then ()
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   101
  else raise Fail ("Bad Long_Name.range_limit for ML platform " ^ ML_System.platform);
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   102
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   103
fun range string index len =
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   104
  if len < range_limit then index * range_limit + len
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   105
  else failure string ("chunk length beyond " ^ string_of_int range_limit);
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   106
77925
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   107
fun range_index r = r div range_limit;
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   108
fun range_length r = r mod range_limit;
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   109
fun range_string s r = String.substring (s, range_index r, range_length r);
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   110
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   111
in
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   112
77962
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm
parents: 77945
diff changeset
   113
abstype chunks = Chunks of {range0: int, ranges: int list (*reverse*), string: string}
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   114
with
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   115
77993
wenzelm
parents: 77964
diff changeset
   116
val empty_chunks = Chunks {range0 = 0, ranges = [], string = ""};
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   117
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   118
fun is_empty_chunks (Chunks {range0, ranges, ...}) =
77993
wenzelm
parents: 77964
diff changeset
   119
  range0 = 0 andalso null ranges;
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   120
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   121
fun count_chunks (chunks as Chunks {ranges, ...}) =
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   122
  if is_empty_chunks chunks then 0
77962
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm
parents: 77945
diff changeset
   123
  else length ranges + 1;
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   124
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   125
fun size_chunks (chunks as Chunks {range0, ranges, ...}) =
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   126
  if is_empty_chunks chunks then 0
77962
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm
parents: 77945
diff changeset
   127
  else fold (fn r => fn n => n + range_length r + 1) ranges (range_length range0);
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   128
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   129
fun base_chunks name =
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   130
  let
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   131
    val i = last_separator name;
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   132
    val j = i + 1;
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   133
  in
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   134
    if i < 0 then empty_chunks
77962
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm
parents: 77945
diff changeset
   135
    else Chunks {range0 = range name j (size name - j), ranges = [], string = name}
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   136
  end;
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   137
77913
019186a60c84 tuned signature;
wenzelm
parents: 77861
diff changeset
   138
fun suppress_chunks suppress1 suppress2 string =
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   139
  let
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   140
    val n = size string;
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   141
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   142
    fun suppr_chunks suppr1 suppr2 i j rs =
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   143
      let
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   144
        val string_end = i >= n;
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   145
        val chunk_end = string_end orelse String.nth string i = separator_char;
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   146
77858
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   147
        val suppr =
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   148
          if suppr1 > 0 then true
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   149
          else if suppr1 < 0 then false
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   150
          else if null suppr2 then false
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   151
          else hd suppr2;
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   152
        val suppr1' =
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   153
          if chunk_end andalso suppr1 > 0 then suppr1 - 1
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   154
          else if chunk_end andalso suppr1 < 0 then suppr1 + 1
77858
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   155
          else suppr1;
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   156
        val suppr2' =
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   157
          if chunk_end andalso suppr1 = 0 andalso not (null suppr2)
77858
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   158
          then tl suppr2 else suppr2;
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   159
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   160
        val i' = i + 1;
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   161
        val j' = if chunk_end then i' else j;
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   162
        val rs' = if chunk_end andalso not suppr then range string j (i - j) :: rs else rs;
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   163
      in
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   164
        if not string_end then suppr_chunks suppr1' suppr2' i' j' rs'
77858
30389d96d0d6 clarified signature: support "suppress" prefix as int, followed by list;
wenzelm
parents: 77857
diff changeset
   165
        else if not (suppr1' = 0 andalso null suppr2') then
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   166
          failure string ("cannot suppress chunks beyond " ^ string_of_int (length rs'))
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   167
        else
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   168
          (case rs' of
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   169
            [] => empty_chunks
77962
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm
parents: 77945
diff changeset
   170
          | r0 :: rest => Chunks {range0 = r0, ranges = rest, string = string})
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   171
      end;
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   172
  in suppr_chunks suppress1 suppress2 0 0 [] end;
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   173
77913
019186a60c84 tuned signature;
wenzelm
parents: 77861
diff changeset
   174
val make_chunks = suppress_chunks 0 [];
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   175
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   176
fun explode_chunks (chunks as Chunks {range0, ranges, string}) =
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   177
  if is_empty_chunks chunks then []
77962
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm
parents: 77945
diff changeset
   178
  else fold (cons o range_string string) ranges [range_string string range0];
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   179
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   180
fun implode_chunks (chunks as Chunks {range0, ranges, string}) =
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   181
  if size_chunks chunks = size string then string
77962
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm
parents: 77945
diff changeset
   182
  else if null ranges then range_string string range0
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   183
  else implode (explode_chunks chunks);
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   184
77925
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   185
val compare_chunks = pointer_eq_ord (fn (chunks1, chunks2) =>
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   186
  let
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   187
    val Chunks {range0 = range01, ranges = ranges1, string = string1} = chunks1;
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   188
    val Chunks {range0 = range02, ranges = ranges2, string = string2} = chunks2;
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   189
    val count1 = count_chunks chunks1;
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   190
    val count2 = count_chunks chunks2;
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   191
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   192
    val range_length_ord = int_ord o apply2 range_length;
77925
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   193
    fun range_substring_ord arg =
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   194
      let
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   195
        val (i, j) = apply2 range_index arg;
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   196
        val (m, n) = apply2 range_length arg;
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   197
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   198
        fun substring_ord k =
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   199
          if k < n then
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   200
            (case Char.compare (String.nth string1 (i + k), String.nth string2 (j + k)) of
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   201
              EQUAL => substring_ord (k + 1)
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   202
            | ord => ord)
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   203
          else EQUAL;
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   204
      in (case int_ord (m, n) of EQUAL => substring_ord 0 | ord => ord) end;
77914
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
wenzelm
parents: 77913
diff changeset
   205
  in
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   206
    if count1 = 0 andalso count2 = 0 then EQUAL
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   207
    else
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   208
      (case int_ord (count1, count2) of
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   209
        EQUAL =>
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   210
          (case range_length_ord (range01, range02) of
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   211
            EQUAL =>
77962
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm
parents: 77945
diff changeset
   212
              (case dict_ord range_length_ord (ranges1, ranges2) of
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   213
                EQUAL =>
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   214
                  (case range_substring_ord (range01, range02) of
77962
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm
parents: 77945
diff changeset
   215
                    EQUAL => dict_ord range_substring_ord (ranges1, ranges2)
77945
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   216
                  | ord => ord)
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   217
              | ord => ord)
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   218
          | ord => ord)
99df2576107f minor performance tuning: more compact, more sharing;
wenzelm
parents: 77944
diff changeset
   219
      | ord => ord)
77925
07e82441c19e minor performance tuning;
wenzelm
parents: 77914
diff changeset
   220
  end);
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   221
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   222
val eq_chunks = is_equal o compare_chunks;
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   223
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
diff changeset
   224
end;
77842
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   225
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   226
end;
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   227
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   228
structure Chunks = Change_Table(type key = chunks val ord = compare_chunks);
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   229
0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents: 65358
diff changeset
   230
end;