src/Pure/compress.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24058 81aafd465662
child 25697 a4b7eb4e20fd
permissions -rw-r--r--
Name.uu, Name.aT;
wenzelm@16981
     1
(*  Title:      Pure/compress.ML
wenzelm@16981
     2
    ID:         $Id$
wenzelm@16981
     3
    Author:     Lawrence C Paulson and Makarius
wenzelm@16981
     4
wenzelm@16981
     5
Compression of terms and types by sharing common subtrees.  Saves
wenzelm@16981
     6
50-75% on storage requirements.  As it is a bit slow, it should be
wenzelm@16981
     7
called only for axioms, stored theorems, etc.
wenzelm@16981
     8
*)
wenzelm@16981
     9
wenzelm@16981
    10
signature COMPRESS =
wenzelm@16981
    11
sig
wenzelm@16981
    12
  val init_data: theory -> theory
wenzelm@16981
    13
  val typ: theory -> typ -> typ
wenzelm@16981
    14
  val term: theory -> term -> term
wenzelm@16981
    15
end;
wenzelm@16981
    16
wenzelm@16981
    17
structure Compress: COMPRESS =
wenzelm@16981
    18
struct
wenzelm@16981
    19
wenzelm@16981
    20
wenzelm@16981
    21
(* theory data *)
wenzelm@16981
    22
wenzelm@16981
    23
structure CompressData = TheoryDataFun
wenzelm@22846
    24
(
wenzelm@16981
    25
  type T = typ Typtab.table ref * term Termtab.table ref;
wenzelm@16981
    26
  val empty : T = (ref Typtab.empty, ref Termtab.empty);
wenzelm@16981
    27
  fun copy (ref typs, ref terms) : T = (ref typs, ref terms);
wenzelm@16981
    28
  val extend = copy;
wenzelm@16981
    29
  fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T =
wenzelm@16981
    30
   (ref (Typtab.merge (K true) (typs1, typs2)),
wenzelm@16981
    31
    ref (Termtab.merge (K true) (terms1, terms2)));
wenzelm@22846
    32
);
wenzelm@16981
    33
wenzelm@16981
    34
val init_data = CompressData.init;
wenzelm@16981
    35
wenzelm@16981
    36
wenzelm@16981
    37
(* compress types *)
wenzelm@16981
    38
wenzelm@23922
    39
fun compress_typ thy =
wenzelm@16981
    40
  let
wenzelm@16981
    41
    val typs = #1 (CompressData.get thy);
wenzelm@16981
    42
    fun compress T =
wenzelm@17412
    43
      (case Typtab.lookup (! typs) T of
wenzelm@16981
    44
        SOME T' => T'
wenzelm@16981
    45
      | NONE =>
wenzelm@16981
    46
          let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts) | _ => T)
wenzelm@17412
    47
          in change typs (Typtab.update (T', T')); T' end);
wenzelm@16981
    48
  in compress end;
wenzelm@16981
    49
wenzelm@24058
    50
fun typ ty = NAMED_CRITICAL "compress" (fn () => compress_typ ty);
wenzelm@23922
    51
wenzelm@16981
    52
wenzelm@16981
    53
(* compress atomic terms *)
wenzelm@16981
    54
wenzelm@23922
    55
fun compress_term thy =
wenzelm@16981
    56
  let
wenzelm@16981
    57
    val terms = #2 (CompressData.get thy);
wenzelm@16981
    58
    fun compress (t $ u) = compress t $ compress u
wenzelm@16981
    59
      | compress (Abs (a, T, t)) = Abs (a, T, compress t)
wenzelm@16981
    60
      | compress t =
wenzelm@17412
    61
          (case Termtab.lookup (! terms) t of
wenzelm@16981
    62
            SOME t' => t'
wenzelm@17412
    63
          | NONE => (change terms (Termtab.update (t, t)); t));
wenzelm@23922
    64
  in compress o map_types (compress_typ thy) end;
wenzelm@23922
    65
wenzelm@24058
    66
fun term tm = NAMED_CRITICAL "compress" (fn () => compress_term tm);
wenzelm@16981
    67
wenzelm@16981
    68
end;