74270
|
1 |
(* Title: Pure/term_items.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Scalable collections of term items:
|
|
5 |
- table: e.g. for instantiation
|
|
6 |
- set with order of addition, e.g. occurrences within term
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature TERM_ITEMS =
|
|
10 |
sig
|
77828
|
11 |
structure Key: KEY
|
74270
|
12 |
type key
|
|
13 |
type 'a table
|
|
14 |
val empty: 'a table
|
|
15 |
val build: ('a table -> 'a table) -> 'a table
|
|
16 |
val size: 'a table -> int
|
|
17 |
val is_empty: 'a table -> bool
|
|
18 |
val map: (key -> 'a -> 'b) -> 'a table -> 'b table
|
|
19 |
val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
|
|
20 |
val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
|
|
21 |
val dest: 'a table -> (key * 'a) list
|
|
22 |
val keys: 'a table -> key list
|
|
23 |
val exists: (key * 'a -> bool) -> 'a table -> bool
|
|
24 |
val forall: (key * 'a -> bool) -> 'a table -> bool
|
|
25 |
val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
|
|
26 |
val lookup: 'a table -> key -> 'a option
|
|
27 |
val defined: 'a table -> key -> bool
|
|
28 |
val add: key * 'a -> 'a table -> 'a table
|
|
29 |
val make: (key * 'a) list -> 'a table
|
77878
|
30 |
val make1: key * 'a -> 'a table
|
|
31 |
val make2: key * 'a -> key * 'a -> 'a table
|
|
32 |
val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
|
74270
|
33 |
type set = int table
|
|
34 |
val add_set: key -> set -> set
|
|
35 |
val make_set: key list -> set
|
77878
|
36 |
val make1_set: key -> set
|
|
37 |
val make2_set: key -> key -> set
|
|
38 |
val make3_set: key -> key -> key -> set
|
74270
|
39 |
val list_set: set -> key list
|
|
40 |
val list_set_rev: set -> key list
|
|
41 |
val subset: set * set -> bool
|
|
42 |
val eq_set: set * set -> bool
|
|
43 |
end;
|
|
44 |
|
|
45 |
functor Term_Items(Key: KEY): TERM_ITEMS =
|
|
46 |
struct
|
|
47 |
|
77828
|
48 |
(* keys *)
|
|
49 |
|
|
50 |
structure Key = Key;
|
|
51 |
type key = Key.key;
|
|
52 |
|
|
53 |
|
74270
|
54 |
(* table with length *)
|
|
55 |
|
|
56 |
structure Table = Table(Key);
|
|
57 |
|
77828
|
58 |
datatype 'a table = Table of 'a Table.table;
|
74270
|
59 |
|
77828
|
60 |
val empty = Table Table.empty;
|
74270
|
61 |
fun build (f: 'a table -> 'a table) = f empty;
|
77828
|
62 |
fun is_empty (Table tab) = Table.is_empty tab;
|
74270
|
63 |
|
77828
|
64 |
fun size (Table tab) = Table.size tab;
|
|
65 |
fun dest (Table tab) = Table.dest tab;
|
|
66 |
fun keys (Table tab) = Table.keys tab;
|
|
67 |
fun exists pred (Table tab) = Table.exists pred tab;
|
|
68 |
fun forall pred (Table tab) = Table.forall pred tab;
|
|
69 |
fun get_first get (Table tab) = Table.get_first get tab;
|
|
70 |
fun lookup (Table tab) = Table.lookup tab;
|
|
71 |
fun defined (Table tab) = Table.defined tab;
|
74270
|
72 |
|
77828
|
73 |
fun add entry (Table tab) = Table (Table.default entry tab);
|
77878
|
74 |
fun make es = build (fold add es);
|
|
75 |
fun make1 e = build (add e);
|
|
76 |
fun make2 e1 e2 = build (add e1 #> add e2);
|
|
77 |
fun make3 e1 e2 e3 = build (add e1 #> add e2 #> add e3);
|
74270
|
78 |
|
|
79 |
|
|
80 |
(* set with order of addition *)
|
|
81 |
|
|
82 |
type set = int table;
|
|
83 |
|
77828
|
84 |
fun add_set x (Table tab) =
|
|
85 |
Table (if Table.defined tab x then tab else Table.update_new (x, Table.size tab + 1) tab);
|
74270
|
86 |
|
|
87 |
fun make_set xs = build (fold add_set xs);
|
77878
|
88 |
fun make1_set e = build (add_set e);
|
|
89 |
fun make2_set e1 e2 = build (add_set e1 #> add_set e2);
|
|
90 |
fun make3_set e1 e2 e3 = build (add_set e1 #> add_set e2 #> add_set e3);
|
74270
|
91 |
|
|
92 |
fun subset (A: set, B: set) = forall (defined B o #1) A;
|
77835
|
93 |
fun eq_set (A: set, B: set) = pointer_eq (A, B) orelse size A = size B andalso subset (A, B);
|
74270
|
94 |
|
77828
|
95 |
fun list_set_ord ord (Table tab) = tab |> Table.dest |> sort (ord o apply2 #2) |> map #1;
|
74270
|
96 |
val list_set = list_set_ord int_ord;
|
|
97 |
val list_set_rev = list_set_ord (rev_order o int_ord);
|
|
98 |
|
77828
|
99 |
fun map f (Table tab) = Table (Table.map f tab);
|
|
100 |
fun fold f (Table tab) = Table.fold f tab;
|
|
101 |
fun fold_rev f (Table tab) = Table.fold_rev f tab;
|
74270
|
102 |
|
|
103 |
end;
|
|
104 |
|
|
105 |
|
|
106 |
structure TFrees:
|
|
107 |
sig
|
|
108 |
include TERM_ITEMS
|
|
109 |
val add_tfreesT: typ -> set -> set
|
|
110 |
val add_tfrees: term -> set -> set
|
74278
|
111 |
val add_tfreesT_unless: (string * sort -> bool) -> typ -> set -> set
|
|
112 |
val add_tfrees_unless: (string * sort -> bool) -> term -> set -> set
|
74270
|
113 |
end =
|
|
114 |
struct
|
|
115 |
|
|
116 |
structure Items = Term_Items
|
|
117 |
(
|
|
118 |
type key = string * sort;
|
|
119 |
val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.sort_ord);
|
|
120 |
);
|
|
121 |
open Items;
|
|
122 |
|
|
123 |
val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I);
|
|
124 |
val add_tfrees = fold_types add_tfreesT;
|
|
125 |
|
74278
|
126 |
fun add_tfreesT_unless pred = Term.fold_atyps (fn TFree v => not (pred v) ? add_set v | _ => I);
|
|
127 |
fun add_tfrees_unless pred = fold_types (add_tfreesT_unless pred);
|
|
128 |
|
74270
|
129 |
end;
|
|
130 |
|
|
131 |
|
|
132 |
structure TVars:
|
|
133 |
sig
|
|
134 |
include TERM_ITEMS
|
|
135 |
val add_tvarsT: typ -> set -> set
|
|
136 |
val add_tvars: term -> set -> set
|
|
137 |
end =
|
|
138 |
struct
|
|
139 |
|
|
140 |
structure Term_Items = Term_Items(
|
|
141 |
type key = indexname * sort;
|
|
142 |
val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord);
|
|
143 |
);
|
|
144 |
open Term_Items;
|
|
145 |
|
|
146 |
val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I);
|
|
147 |
val add_tvars = fold_types add_tvarsT;
|
|
148 |
|
|
149 |
end;
|
|
150 |
|
|
151 |
|
|
152 |
structure Frees:
|
|
153 |
sig
|
|
154 |
include TERM_ITEMS
|
|
155 |
val add_frees: term -> set -> set
|
|
156 |
end =
|
|
157 |
struct
|
|
158 |
|
|
159 |
structure Term_Items = Term_Items
|
|
160 |
(
|
|
161 |
type key = string * typ;
|
|
162 |
val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.typ_ord);
|
|
163 |
);
|
|
164 |
open Term_Items;
|
|
165 |
|
|
166 |
val add_frees = fold_aterms (fn Free v => add_set v | _ => I);
|
|
167 |
|
|
168 |
end;
|
|
169 |
|
|
170 |
|
|
171 |
structure Vars:
|
|
172 |
sig
|
|
173 |
include TERM_ITEMS
|
|
174 |
val add_vars: term -> set -> set
|
|
175 |
end =
|
|
176 |
struct
|
|
177 |
|
|
178 |
structure Term_Items = Term_Items
|
|
179 |
(
|
|
180 |
type key = indexname * typ;
|
|
181 |
val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
|
|
182 |
);
|
|
183 |
open Term_Items;
|
|
184 |
|
|
185 |
val add_vars = fold_aterms (fn Var v => add_set v | _ => I);
|
|
186 |
|
|
187 |
end;
|
|
188 |
|
|
189 |
|
|
190 |
structure Names:
|
|
191 |
sig
|
|
192 |
include TERM_ITEMS
|
|
193 |
val add_tfree_namesT: typ -> set -> set
|
|
194 |
val add_tfree_names: term -> set -> set
|
|
195 |
val add_free_names: term -> set -> set
|
|
196 |
end =
|
|
197 |
struct
|
|
198 |
|
|
199 |
structure Term_Items = Term_Items
|
|
200 |
(
|
|
201 |
type key = string;
|
|
202 |
val ord = fast_string_ord
|
|
203 |
);
|
|
204 |
open Term_Items;
|
|
205 |
|
|
206 |
val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I);
|
|
207 |
val add_tfree_names = fold_types add_tfree_namesT;
|
|
208 |
val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I);
|
|
209 |
|
|
210 |
end;
|