author | wenzelm |
Wed, 12 Mar 2025 11:39:00 +0100 | |
changeset 82265 | 4b875a4c83b0 |
parent 79319 | 2d9baa7ee05a |
permissions | -rw-r--r-- |
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 | 10 |
val append: string -> string -> string |
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 | 16 |
val count: string -> int |
55669 | 17 |
val hidden: string -> string |
59916 | 18 |
val is_hidden: string -> bool |
59888 | 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 | 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 | 29 |
val base_chunks: string -> chunks |
77913 | 30 |
val suppress_chunks: int -> bool list -> string -> chunks |
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 | 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 | 46 |
|
77856 | 47 |
fun append name1 "" = name1 |
48 |
| append "" name2 = name2 |
|
49 |
| append name1 name2 = name1 ^ separator ^ name2; |
|
50 |
||
51 |
fun qualify qual name = |
|
52 |
if qual = "" orelse name = "" then name |
|
53 |
else qual ^ separator ^ name; |
|
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 | 75 |
fun count "" = 0 |
76 |
| count name = String.fold (fn c => c = separator_char ? Integer.add 1) name 1; |
|
77 |
||
79319 | 78 |
val hidden_prefix = "??."; |
59916 | 79 |
val hidden = prefix hidden_prefix; |
80 |
val is_hidden = String.isPrefix hidden_prefix; |
|
81 |
val dest_hidden = try (unprefix hidden_prefix); |
|
55669 | 82 |
|
56162
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56023
diff
changeset
|
83 |
val localN = "local"; |
59888 | 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 | 107 |
fun range_index r = r div range_limit; |
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 | 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 | 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 | 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 | 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 | 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 | 193 |
fun range_substring_ord arg = |
194 |
let |
|
195 |
val (i, j) = apply2 range_index arg; |
|
196 |
val (m, n) = apply2 range_length arg; |
|
197 |
||
198 |
fun substring_ord k = |
|
199 |
if k < n then |
|
200 |
(case Char.compare (String.nth string1 (i + k), String.nth string2 (j + k)) of |
|
201 |
EQUAL => substring_ord (k + 1) |
|
202 |
| ord => ord) |
|
203 |
else EQUAL; |
|
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 | 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; |