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