src/Pure/compress.ML
author wenzelm
Mon May 07 00:49:59 2007 +0200 (2007-05-07)
changeset 22846 fb79144af9a3
parent 20548 8ef25fe585a8
child 23922 707639e9497d
permissions -rw-r--r--
simplified DataFun interfaces;
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@16981
    39
fun 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@16981
    50
wenzelm@16981
    51
(* compress atomic terms *)
wenzelm@16981
    52
wenzelm@16981
    53
fun term thy =
wenzelm@16981
    54
  let
wenzelm@16981
    55
    val terms = #2 (CompressData.get thy);
wenzelm@16981
    56
    fun compress (t $ u) = compress t $ compress u
wenzelm@16981
    57
      | compress (Abs (a, T, t)) = Abs (a, T, compress t)
wenzelm@16981
    58
      | compress t =
wenzelm@17412
    59
          (case Termtab.lookup (! terms) t of
wenzelm@16981
    60
            SOME t' => t'
wenzelm@17412
    61
          | NONE => (change terms (Termtab.update (t, t)); t));
wenzelm@20548
    62
  in compress o map_types (typ thy) end;
wenzelm@16981
    63
wenzelm@16981
    64
end;