src/Pure/compress.ML
author haftmann
Tue Sep 06 08:30:43 2005 +0200 (2005-09-06)
changeset 17271 2756a73f63a5
parent 17221 6cd180204582
child 17412 e26cb20ef0cc
permissions -rw-r--r--
introduced some new-style AList operations
     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 (struct
    25   val name = "Pure/compress";
    26   type T = typ Typtab.table ref * term Termtab.table ref;
    27   val empty : T = (ref Typtab.empty, ref Termtab.empty);
    28   fun copy (ref typs, ref terms) : T = (ref typs, ref terms);
    29   val extend = copy;
    30   fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T =
    31    (ref (Typtab.merge (K true) (typs1, typs2)),
    32     ref (Termtab.merge (K true) (terms1, terms2)));
    33   fun print _ _ = ();
    34 end);
    35 
    36 val init_data = CompressData.init;
    37 
    38 
    39 (* compress types *)
    40 
    41 fun typ thy =
    42   let
    43     val typs = #1 (CompressData.get thy);
    44     fun compress T =
    45       (case Typtab.curried_lookup (! typs) T of
    46         SOME T' => T'
    47       | NONE =>
    48           let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts) | _ => T)
    49           in change typs (Typtab.curried_update (T', T')); T' end);
    50   in compress end;
    51 
    52 
    53 (* compress atomic terms *)
    54 
    55 fun 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.curried_lookup (! terms) t of
    62             SOME t' => t'
    63           | NONE => (change terms (Termtab.curried_update (t, t)); t));
    64   in compress o map_term_types (typ thy) end;
    65 
    66 end;