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