src/Pure/term_sharing.ML
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 45595 fe57d786fd5b
child 56025 d74fed45fa8b
permissions -rw-r--r--
tuned signature;
tuned comments;
wenzelm@43796
     1
(*  Title:      Pure/term_sharing.ML
wenzelm@43796
     2
    Author:     Makarius
wenzelm@43796
     3
wenzelm@43796
     4
Local sharing of type/term sub-structure, with global interning of
wenzelm@43796
     5
formal entity names.
wenzelm@43796
     6
*)
wenzelm@43796
     7
wenzelm@43796
     8
signature TERM_SHARING =
wenzelm@43796
     9
sig
wenzelm@43796
    10
  val init: theory -> (typ -> typ) * (term -> term)
wenzelm@43796
    11
  val typs: theory -> typ list -> typ list
wenzelm@43796
    12
  val terms: theory -> term list -> term list
wenzelm@43796
    13
end;
wenzelm@43796
    14
wenzelm@43796
    15
structure Term_Sharing: TERM_SHARING =
wenzelm@43796
    16
struct
wenzelm@43796
    17
wenzelm@43796
    18
structure Syntax_Termtab = Table(type key = term val ord = Term_Ord.syntax_term_ord);
wenzelm@43796
    19
wenzelm@43796
    20
fun init thy =
wenzelm@43796
    21
  let
wenzelm@43796
    22
    val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
wenzelm@43796
    23
wenzelm@45595
    24
    val class = perhaps (try (#1 o Graph.get_entry (Sorts.classes_of algebra)));
wenzelm@43796
    25
    val tycon = perhaps (Option.map #1 o Symtab.lookup_key types);
wenzelm@43796
    26
    val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
wenzelm@43796
    27
wenzelm@43796
    28
    val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table);
wenzelm@43796
    29
    val terms = Unsynchronized.ref (Syntax_Termtab.empty: unit Syntax_Termtab.table);
wenzelm@43796
    30
wenzelm@43796
    31
    fun typ T =
wenzelm@43796
    32
      (case Typtab.lookup_key (! typs) T of
wenzelm@43796
    33
        SOME (T', ()) => T'
wenzelm@43796
    34
      | NONE =>
wenzelm@43796
    35
          let
wenzelm@43796
    36
            val T' =
wenzelm@43796
    37
              (case T of
wenzelm@43796
    38
                Type (a, Ts) => Type (tycon a, map typ Ts)
wenzelm@45595
    39
              | TFree (a, S) => TFree (a, map class S)
wenzelm@45595
    40
              | TVar (a, S) => TVar (a, map class S));
wenzelm@43796
    41
            val _ = Unsynchronized.change typs (Typtab.update (T', ()));
wenzelm@43796
    42
          in T' end);
wenzelm@43796
    43
wenzelm@43796
    44
    fun term tm =
wenzelm@43796
    45
      (case Syntax_Termtab.lookup_key (! terms) tm of
wenzelm@43796
    46
        SOME (tm', ()) => tm'
wenzelm@43796
    47
      | NONE =>
wenzelm@43796
    48
          let
wenzelm@43796
    49
            val tm' =
wenzelm@43796
    50
              (case tm of
wenzelm@43796
    51
                Const (c, T) => Const (const c, typ T)
wenzelm@43796
    52
              | Free (x, T) => Free (x, typ T)
wenzelm@43796
    53
              | Var (xi, T) => Var (xi, typ T)
wenzelm@43796
    54
              | Bound i => Bound i
wenzelm@43796
    55
              | Abs (x, T, t) => Abs (x, typ T, term t)
wenzelm@43796
    56
              | t $ u => term t $ term u);
wenzelm@43796
    57
            val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ()));
wenzelm@43796
    58
          in tm' end);
wenzelm@43796
    59
wenzelm@43950
    60
    fun check eq f x =
wenzelm@43950
    61
      let val x' = f x in
wenzelm@43950
    62
        if eq (x, x') then x'
wenzelm@43950
    63
        else raise Fail "Something is utterly wrong"
wenzelm@43950
    64
      end;
wenzelm@43950
    65
wenzelm@43950
    66
  in (check (op =) typ, check (op =) term) end;
wenzelm@43796
    67
wenzelm@43796
    68
val typs = map o #1 o init;
wenzelm@43796
    69
val terms = map o #2 o init;
wenzelm@43796
    70
wenzelm@43796
    71
end;
wenzelm@43796
    72