1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/term_sharing.ML	Wed Jul 13 22:05:55 2011 +0200
     1.3 @@ -0,0 +1,66 @@
     1.4 +(*  Title:      Pure/term_sharing.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Local sharing of type/term sub-structure, with global interning of
     1.8 +formal entity names.
     1.9 +*)
    1.10 +
    1.11 +signature TERM_SHARING =
    1.12 +sig
    1.13 +  val init: theory -> (typ -> typ) * (term -> term)
    1.14 +  val typs: theory -> typ list -> typ list
    1.15 +  val terms: theory -> term list -> term list
    1.16 +end;
    1.17 +
    1.18 +structure Term_Sharing: TERM_SHARING =
    1.19 +struct
    1.20 +
    1.21 +structure Syntax_Termtab = Table(type key = term val ord = Term_Ord.syntax_term_ord);
    1.22 +
    1.23 +fun init thy =
    1.24 +  let
    1.25 +    val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
    1.26 +
    1.27 +    val sort = perhaps (try (Sorts.certify_sort algebra));
    1.28 +    val tycon = perhaps (Option.map #1 o Symtab.lookup_key types);
    1.29 +    val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
    1.30 +
    1.31 +    val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table);
    1.32 +    val terms = Unsynchronized.ref (Syntax_Termtab.empty: unit Syntax_Termtab.table);
    1.33 +
    1.34 +    fun typ T =
    1.35 +      (case Typtab.lookup_key (! typs) T of
    1.36 +        SOME (T', ()) => T'
    1.37 +      | NONE =>
    1.38 +          let
    1.39 +            val T' =
    1.40 +              (case T of
    1.41 +                Type (a, Ts) => Type (tycon a, map typ Ts)
    1.42 +              | TFree (a, S) => TFree (a, sort S)
    1.43 +              | TVar (a, S) => TVar (a, sort S));
    1.44 +            val _ = Unsynchronized.change typs (Typtab.update (T', ()));
    1.45 +          in T' end);
    1.46 +
    1.47 +    fun term tm =
    1.48 +      (case Syntax_Termtab.lookup_key (! terms) tm of
    1.49 +        SOME (tm', ()) => tm'
    1.50 +      | NONE =>
    1.51 +          let
    1.52 +            val tm' =
    1.53 +              (case tm of
    1.54 +                Const (c, T) => Const (const c, typ T)
    1.55 +              | Free (x, T) => Free (x, typ T)
    1.56 +              | Var (xi, T) => Var (xi, typ T)
    1.57 +              | Bound i => Bound i
    1.58 +              | Abs (x, T, t) => Abs (x, typ T, term t)
    1.59 +              | t $ u => term t $ term u);
    1.60 +            val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ()));
    1.61 +          in tm' end);
    1.62 +
    1.63 +  in (typ, term) end;
    1.64 +
    1.65 +val typs = map o #1 o init;
    1.66 +val terms = map o #2 o init;
    1.67 +
    1.68 +end;
    1.69 +