# HG changeset patch
# User wenzelm
# Date 1310587555 -7200
# Node ID 7293403dc38b5f20bbe1115386c956d7efb9145b
# Parent  ca5896a836baf2530bff6a48f8a6e5639650f472
added term_sharing.ML;

diff -r ca5896a836ba -r 7293403dc38b src/Pure/term_sharing.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term_sharing.ML	Wed Jul 13 22:05:55 2011 +0200
@@ -0,0 +1,66 @@
+(*  Title:      Pure/term_sharing.ML
+    Author:     Makarius
+
+Local sharing of type/term sub-structure, with global interning of
+formal entity names.
+*)
+
+signature TERM_SHARING =
+sig
+  val init: theory -> (typ -> typ) * (term -> term)
+  val typs: theory -> typ list -> typ list
+  val terms: theory -> term list -> term list
+end;
+
+structure Term_Sharing: TERM_SHARING =
+struct
+
+structure Syntax_Termtab = Table(type key = term val ord = Term_Ord.syntax_term_ord);
+
+fun init thy =
+  let
+    val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
+
+    val sort = perhaps (try (Sorts.certify_sort algebra));
+    val tycon = perhaps (Option.map #1 o Symtab.lookup_key types);
+    val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
+
+    val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table);
+    val terms = Unsynchronized.ref (Syntax_Termtab.empty: unit Syntax_Termtab.table);
+
+    fun typ T =
+      (case Typtab.lookup_key (! typs) T of
+        SOME (T', ()) => T'
+      | NONE =>
+          let
+            val T' =
+              (case T of
+                Type (a, Ts) => Type (tycon a, map typ Ts)
+              | TFree (a, S) => TFree (a, sort S)
+              | TVar (a, S) => TVar (a, sort S));
+            val _ = Unsynchronized.change typs (Typtab.update (T', ()));
+          in T' end);
+
+    fun term tm =
+      (case Syntax_Termtab.lookup_key (! terms) tm of
+        SOME (tm', ()) => tm'
+      | NONE =>
+          let
+            val tm' =
+              (case tm of
+                Const (c, T) => Const (const c, typ T)
+              | Free (x, T) => Free (x, typ T)
+              | Var (xi, T) => Var (xi, typ T)
+              | Bound i => Bound i
+              | Abs (x, T, t) => Abs (x, typ T, term t)
+              | t $ u => term t $ term u);
+            val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ()));
+          in tm' end);
+
+  in (typ, term) end;
+
+val typs = map o #1 o init;
+val terms = map o #2 o init;
+
+end;
+