author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24058  81aafd465662 
child 25697  a4b7eb4e20fd 
permissions  rwrr 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/compress.ML 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

3 
Author: Lawrence C Paulson and Makarius 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

4 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

5 
Compression of terms and types by sharing common subtrees. Saves 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

6 
5075% on storage requirements. As it is a bit slow, it should be 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

7 
called only for axioms, stored theorems, etc. 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

8 
*) 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

9 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

10 
signature COMPRESS = 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

11 
sig 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

12 
val init_data: theory > theory 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

13 
val typ: theory > typ > typ 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

14 
val term: theory > term > term 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

15 
end; 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

16 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

17 
structure Compress: COMPRESS = 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

18 
struct 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

19 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

20 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

21 
(* theory data *) 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

22 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

23 
structure CompressData = TheoryDataFun 
22846  24 
( 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

25 
type T = typ Typtab.table ref * term Termtab.table ref; 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

26 
val empty : T = (ref Typtab.empty, ref Termtab.empty); 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

27 
fun copy (ref typs, ref terms) : T = (ref typs, ref terms); 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

28 
val extend = copy; 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

29 
fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T = 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

30 
(ref (Typtab.merge (K true) (typs1, typs2)), 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

31 
ref (Termtab.merge (K true) (terms1, terms2))); 
22846  32 
); 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

33 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

34 
val init_data = CompressData.init; 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

35 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

36 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

37 
(* compress types *) 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

38 

23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22846
diff
changeset

39 
fun compress_typ thy = 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

40 
let 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

41 
val typs = #1 (CompressData.get thy); 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

42 
fun compress T = 
17412  43 
(case Typtab.lookup (! typs) T of 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

44 
SOME T' => T' 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

45 
 NONE => 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

46 
let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts)  _ => T) 
17412  47 
in change typs (Typtab.update (T', T')); T' end); 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

48 
in compress end; 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

49 

24058  50 
fun typ ty = NAMED_CRITICAL "compress" (fn () => compress_typ ty); 
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22846
diff
changeset

51 

16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

52 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

53 
(* compress atomic terms *) 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

54 

23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22846
diff
changeset

55 
fun compress_term thy = 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

56 
let 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

57 
val terms = #2 (CompressData.get thy); 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

58 
fun compress (t $ u) = compress t $ compress u 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

59 
 compress (Abs (a, T, t)) = Abs (a, T, compress t) 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

60 
 compress t = 
17412  61 
(case Termtab.lookup (! terms) t of 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

62 
SOME t' => t' 
17412  63 
 NONE => (change terms (Termtab.update (t, t)); t)); 
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22846
diff
changeset

64 
in compress o map_types (compress_typ thy) end; 
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22846
diff
changeset

65 

24058  66 
fun term tm = NAMED_CRITICAL "compress" (fn () => compress_term tm); 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

67 

2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

68 
end; 