src/Pure/compress.ML
author wenzelm
Tue Nov 28 00:35:21 2006 +0100 (2006-11-28)
changeset 21566 af2932baf068
parent 20548 8ef25fe585a8
child 22846 fb79144af9a3
permissions -rw-r--r--
dest_term: strip_imp_concl;
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@16981
    24
(struct
wenzelm@16981
    25
  val name = "Pure/compress";
wenzelm@16981
    26
  type T = typ Typtab.table ref * term Termtab.table ref;
wenzelm@16981
    27
  val empty : T = (ref Typtab.empty, ref Termtab.empty);
wenzelm@16981
    28
  fun copy (ref typs, ref terms) : T = (ref typs, ref terms);
wenzelm@16981
    29
  val extend = copy;
wenzelm@16981
    30
  fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T =
wenzelm@16981
    31
   (ref (Typtab.merge (K true) (typs1, typs2)),
wenzelm@16981
    32
    ref (Termtab.merge (K true) (terms1, terms2)));
wenzelm@16981
    33
  fun print _ _ = ();
wenzelm@16981
    34
end);
wenzelm@16981
    35
wenzelm@16981
    36
val init_data = CompressData.init;
wenzelm@16981
    37
wenzelm@16981
    38
wenzelm@16981
    39
(* compress types *)
wenzelm@16981
    40
wenzelm@16981
    41
fun typ thy =
wenzelm@16981
    42
  let
wenzelm@16981
    43
    val typs = #1 (CompressData.get thy);
wenzelm@16981
    44
    fun compress T =
wenzelm@17412
    45
      (case Typtab.lookup (! typs) T of
wenzelm@16981
    46
        SOME T' => T'
wenzelm@16981
    47
      | NONE =>
wenzelm@16981
    48
          let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts) | _ => T)
wenzelm@17412
    49
          in change typs (Typtab.update (T', T')); T' end);
wenzelm@16981
    50
  in compress end;
wenzelm@16981
    51
wenzelm@16981
    52
wenzelm@16981
    53
(* compress atomic terms *)
wenzelm@16981
    54
wenzelm@16981
    55
fun 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@20548
    64
  in compress o map_types (typ thy) end;
wenzelm@16981
    65
wenzelm@16981
    66
end;