src/Pure/compress.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 17412 e26cb20ef0cc
child 20548 8ef25fe585a8
permissions -rw-r--r--
simplified type attribute;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
50-75% 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
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
    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
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
    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
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
    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
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
    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;