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