43796
|
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 = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
|
|
23 |
|
|
24 |
val sort = perhaps (try (Sorts.certify_sort algebra));
|
|
25 |
val tycon = perhaps (Option.map #1 o Symtab.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, sort S)
|
|
40 |
| TVar (a, S) => TVar (a, sort 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 |
in (typ, term) end;
|
|
61 |
|
|
62 |
val typs = map o #1 o init;
|
|
63 |
val terms = map o #2 o init;
|
|
64 |
|
|
65 |
end;
|
|
66 |
|