author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 17412  e26cb20ef0cc 
child 20548  8ef25fe585a8 
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 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

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

25 
val name = "Pure/compress"; 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

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

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

28 
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

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

30 
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

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

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

33 
fun print _ _ = (); 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

34 
end); 
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 
val init_data = CompressData.init; 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

37 

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

38 

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

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

40 

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

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

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

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

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

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

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

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

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

51 

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 

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

55 
fun term thy = 
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)); 
16981
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

64 
in compress o map_term_types (typ thy) end; 
2ae3f621d076
compression of terms and types by sharing common subtrees;
wenzelm
parents:
diff
changeset

65 

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

66 
end; 