1 (* Title: Pure/compress.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson and Makarius |
|
4 |
|
5 Compression of terms and types by sharing common subtrees. Saves |
|
6 50-75% on storage requirements. As it is a bit slow, it should be |
|
7 called only for axioms, stored theorems, etc. |
|
8 *) |
|
9 |
|
10 signature COMPRESS = |
|
11 sig |
|
12 val typ: theory -> typ -> typ |
|
13 val term: theory -> term -> term |
|
14 end; |
|
15 |
|
16 structure Compress: COMPRESS = |
|
17 struct |
|
18 |
|
19 |
|
20 (* theory data *) |
|
21 |
|
22 structure CompressData = TheoryDataFun |
|
23 ( |
|
24 type T = typ Typtab.table ref * term Termtab.table ref; |
|
25 val empty : T = (ref Typtab.empty, ref Termtab.empty); |
|
26 fun copy (ref typs, ref terms) : T = (ref typs, ref terms); |
|
27 val extend = copy; |
|
28 fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T = |
|
29 (ref (Typtab.merge (K true) (typs1, typs2)), |
|
30 ref (Termtab.merge (K true) (terms1, terms2))); |
|
31 ); |
|
32 |
|
33 val _ = Context.>> (Context.map_theory CompressData.init); |
|
34 |
|
35 |
|
36 (* compress types *) |
|
37 |
|
38 fun typ thy = |
|
39 let |
|
40 val typs = #1 (CompressData.get thy); |
|
41 fun compress T = |
|
42 (case Typtab.lookup (! typs) T of |
|
43 SOME T' => T' |
|
44 | NONE => |
|
45 let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts) | _ => T) |
|
46 in change typs (Typtab.update (T', T')); T' end); |
|
47 in compress end; |
|
48 |
|
49 |
|
50 (* compress atomic terms *) |
|
51 |
|
52 fun term thy = |
|
53 let |
|
54 val terms = #2 (CompressData.get thy); |
|
55 fun compress (t $ u) = compress t $ compress u |
|
56 | compress (Abs (a, T, t)) = Abs (a, T, compress t) |
|
57 | compress t = |
|
58 (case Termtab.lookup (! terms) t of |
|
59 SOME t' => t' |
|
60 | NONE => (change terms (Termtab.update (t, t)); t)); |
|
61 in compress o map_types (typ thy) end; |
|
62 |
|
63 end; |
|