src/Pure/compress.ML
author wenzelm
Wed Mar 26 22:40:03 2008 +0100 (2008-03-26)
changeset 26413 003dd6155870
parent 25697 a4b7eb4e20fd
child 26427 f33d1b522316
permissions -rw-r--r--
added thread data (formerly global ref in ML/ml_context.ML);
renamed ML_Context.>> to Context.>> (again);
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@25697
    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@25697
    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@25697
    62
  in compress o map_types (typ thy) end;
wenzelm@16981
    63
wenzelm@16981
    64
end;