src/Pure/term_subst.ML
author wenzelm
Sat, 20 Jul 2024 21:17:22 +0200
changeset 80599 f8c070249502
parent 79409 e1895596e1b9
child 80607 e23aab2df03c
permissions -rw-r--r--
clarified modules (see also e063c0403650);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/term_subst.ML
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
     3
32016
597b3b69b8d8 use structure Same;
wenzelm
parents: 31980
diff changeset
     4
Efficient type/term substitution.
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
     5
*)
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
     6
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
     7
signature TERM_SUBST =
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
     8
sig
74266
612b7e0d6721 clarified signature;
wenzelm
parents: 74232
diff changeset
     9
  val generalizeT_same: Names.set -> int -> typ Same.operation
612b7e0d6721 clarified signature;
wenzelm
parents: 74232
diff changeset
    10
  val generalize_same: Names.set * Names.set -> int -> term Same.operation
612b7e0d6721 clarified signature;
wenzelm
parents: 74232
diff changeset
    11
  val generalizeT: Names.set -> int -> typ -> typ
612b7e0d6721 clarified signature;
wenzelm
parents: 74232
diff changeset
    12
  val generalize: Names.set * Names.set -> int -> term -> term
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    13
  val instantiateT_frees_same: typ TFrees.table -> typ Same.operation
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    14
  val instantiate_frees_same: typ TFrees.table * term Frees.table -> term Same.operation
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    15
  val instantiateT_frees: typ TFrees.table -> typ -> typ
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    16
  val instantiate_frees: typ TFrees.table * term Frees.table -> term -> term
74576
wenzelm
parents: 74266
diff changeset
    17
  val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
wenzelm
parents: 74266
diff changeset
    18
  val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
wenzelm
parents: 74266
diff changeset
    19
    term -> int -> term * int
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
    20
  val instantiate_beta_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
    21
    term -> int -> term * int
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    22
  val instantiateT_same: typ TVars.table -> typ Same.operation
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    23
  val instantiate_same: typ TVars.table * term Vars.table -> term Same.operation
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
    24
  val instantiate_beta_same: typ TVars.table * term Vars.table -> term Same.operation
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    25
  val instantiateT: typ TVars.table -> typ -> typ
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    26
  val instantiate: typ TVars.table * term Vars.table -> term -> term
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
    27
  val instantiate_beta: typ TVars.table * term Vars.table -> term -> term
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    28
  val zero_var_indexes_inst: Name.context -> term list -> typ TVars.table * term Vars.table
68234
07eb13eb4065 tuned signature;
wenzelm
parents: 67698
diff changeset
    29
  val zero_var_indexes: term -> term
07eb13eb4065 tuned signature;
wenzelm
parents: 67698
diff changeset
    30
  val zero_var_indexes_list: term list -> term list
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    31
end;
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    32
31977
e03059ae2d82 renamed structure TermSubst to Term_Subst;
wenzelm
parents: 29269
diff changeset
    33
structure Term_Subst: TERM_SUBST =
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    34
struct
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    35
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    36
(* generalization of fixed variables *)
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    37
74200
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    38
fun generalizeT_same tfrees idx ty =
74266
612b7e0d6721 clarified signature;
wenzelm
parents: 74232
diff changeset
    39
  if Names.is_empty tfrees then raise Same.SAME
74200
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    40
  else
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    41
    let
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    42
      fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    43
        | gen (TFree (a, S)) =
74266
612b7e0d6721 clarified signature;
wenzelm
parents: 74232
diff changeset
    44
            if Names.defined tfrees a then TVar ((a, idx), S)
74200
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    45
            else raise Same.SAME
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    46
        | gen _ = raise Same.SAME;
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    47
    in gen ty end;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    48
74200
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    49
fun generalize_same (tfrees, frees) idx tm =
74266
612b7e0d6721 clarified signature;
wenzelm
parents: 74232
diff changeset
    50
  if Names.is_empty tfrees andalso Names.is_empty frees then raise Same.SAME
74200
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    51
  else
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    52
    let
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    53
      val genT = generalizeT_same tfrees idx;
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    54
      fun gen (Free (x, T)) =
74266
612b7e0d6721 clarified signature;
wenzelm
parents: 74232
diff changeset
    55
            if Names.defined frees x then
74200
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    56
              Var (Name.clean_index (x, idx), Same.commit genT T)
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    57
            else Free (x, genT T)
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    58
        | gen (Var (xi, T)) = Var (xi, genT T)
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    59
        | gen (Const (c, T)) = Const (c, genT T)
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    60
        | gen (Bound _) = raise Same.SAME
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    61
        | gen (Abs (x, T, t)) =
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    62
            (Abs (x, genT T, Same.commit gen t)
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    63
              handle Same.SAME => Abs (x, T, gen t))
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    64
        | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u);
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69023
diff changeset
    65
    in gen tm end;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    66
36766
wenzelm
parents: 36765
diff changeset
    67
fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty;
36620
e6bb250402b5 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
wenzelm
parents: 35408
diff changeset
    68
fun generalize names i tm = Same.commit (generalize_same names i) tm;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    69
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
    70
67698
67caf783b9ee explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents: 45395
diff changeset
    71
(* instantiation of free variables (types before terms) *)
67caf783b9ee explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents: 45395
diff changeset
    72
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    73
fun instantiateT_frees_same instT ty =
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    74
  if TFrees.is_empty instT then raise Same.SAME
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    75
  else
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    76
    let
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    77
      fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    78
        | subst (TFree v) =
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    79
            (case TFrees.lookup instT v of
74578
wenzelm
parents: 74577
diff changeset
    80
              SOME T' => T'
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    81
            | NONE => raise Same.SAME)
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    82
        | subst _ = raise Same.SAME;
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    83
    in subst ty end;
67698
67caf783b9ee explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents: 45395
diff changeset
    84
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    85
fun instantiate_frees_same (instT, inst) tm =
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    86
  if TFrees.is_empty instT andalso Frees.is_empty inst then raise Same.SAME
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    87
  else
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    88
    let
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    89
      val substT = instantiateT_frees_same instT;
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    90
      fun subst (Const (c, T)) = Const (c, substT T)
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    91
        | subst (Free (x, T)) =
79129
2933e71f4e09 clarified signature;
wenzelm
parents: 74578
diff changeset
    92
            let val (T', same) = Same.commit_id substT T in
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    93
              (case Frees.lookup inst (x, T') of
74578
wenzelm
parents: 74577
diff changeset
    94
                 SOME t' => t'
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    95
               | NONE => if same then raise Same.SAME else Free (x, T'))
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    96
            end
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    97
        | subst (Var (xi, T)) = Var (xi, substT T)
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    98
        | subst (Bound _) = raise Same.SAME
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
    99
        | subst (Abs (x, T, t)) =
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   100
            (Abs (x, substT T, Same.commit subst t)
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   101
              handle Same.SAME => Abs (x, T, subst t))
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   102
        | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   103
    in subst tm end;
67698
67caf783b9ee explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents: 45395
diff changeset
   104
67caf783b9ee explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents: 45395
diff changeset
   105
fun instantiateT_frees instT ty = Same.commit (instantiateT_frees_same instT) ty;
67caf783b9ee explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents: 45395
diff changeset
   106
fun instantiate_frees inst tm = Same.commit (instantiate_frees_same inst) tm;
67caf783b9ee explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents: 45395
diff changeset
   107
67caf783b9ee explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents: 45395
diff changeset
   108
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   109
(* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   110
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   111
local
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   112
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   113
fun no_indexesT instT = TVars.map (fn _ => rpair ~1) instT;
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   114
fun no_indexes inst = Vars.map (fn _ => rpair ~1) inst;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   115
36620
e6bb250402b5 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
wenzelm
parents: 35408
diff changeset
   116
fun instT_same maxidx instT ty =
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   117
  let
21184
35baf14cfb6d instantiate: avoid global references;
wenzelm
parents: 20513
diff changeset
   118
    fun maxify i = if i > ! maxidx then maxidx := i else ();
35baf14cfb6d instantiate: avoid global references;
wenzelm
parents: 20513
diff changeset
   119
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   120
    fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   121
      | subst_typ (TVar ((a, i), S)) =
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   122
          (case TVars.lookup instT ((a, i), S) of
74578
wenzelm
parents: 74577
diff changeset
   123
            SOME (T', j) => (maxify j; T')
32016
597b3b69b8d8 use structure Same;
wenzelm
parents: 31980
diff changeset
   124
          | NONE => (maxify i; raise Same.SAME))
597b3b69b8d8 use structure Same;
wenzelm
parents: 31980
diff changeset
   125
      | subst_typ _ = raise Same.SAME
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   126
    and subst_typs (T :: Ts) =
32016
597b3b69b8d8 use structure Same;
wenzelm
parents: 31980
diff changeset
   127
        (subst_typ T :: Same.commit subst_typs Ts
597b3b69b8d8 use structure Same;
wenzelm
parents: 31980
diff changeset
   128
          handle Same.SAME => T :: subst_typs Ts)
597b3b69b8d8 use structure Same;
wenzelm
parents: 31980
diff changeset
   129
      | subst_typs [] = raise Same.SAME;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   130
  in subst_typ ty end;
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   131
36620
e6bb250402b5 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
wenzelm
parents: 35408
diff changeset
   132
fun inst_same maxidx (instT, inst) tm =
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   133
  let
21184
35baf14cfb6d instantiate: avoid global references;
wenzelm
parents: 20513
diff changeset
   134
    fun maxify i = if i > ! maxidx then maxidx := i else ();
35baf14cfb6d instantiate: avoid global references;
wenzelm
parents: 20513
diff changeset
   135
36620
e6bb250402b5 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
wenzelm
parents: 35408
diff changeset
   136
    val substT = instT_same maxidx instT;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   137
    fun subst (Const (c, T)) = Const (c, substT T)
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   138
      | subst (Free (x, T)) = Free (x, substT T)
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   139
      | subst (Var ((x, i), T)) =
79129
2933e71f4e09 clarified signature;
wenzelm
parents: 74578
diff changeset
   140
          let val (T', same) = Same.commit_id substT T in
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   141
            (case Vars.lookup inst ((x, i), T') of
74578
wenzelm
parents: 74577
diff changeset
   142
               SOME (t', j) => (maxify j; t')
32016
597b3b69b8d8 use structure Same;
wenzelm
parents: 31980
diff changeset
   143
             | NONE => (maxify i; if same then raise Same.SAME else Var ((x, i), T')))
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   144
          end
32016
597b3b69b8d8 use structure Same;
wenzelm
parents: 31980
diff changeset
   145
      | subst (Bound _) = raise Same.SAME
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   146
      | subst (Abs (x, T, t)) =
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   147
          (Abs (x, substT T, subst_commit t)
32016
597b3b69b8d8 use structure Same;
wenzelm
parents: 31980
diff changeset
   148
            handle Same.SAME => Abs (x, T, subst t))
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   149
      | subst (t $ u) = (subst t $ subst_commit u handle Same.SAME => t $ subst u)
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   150
    and subst_commit t = Same.commit subst t;
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   151
  in subst tm end;
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   152
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   153
(*version with local beta reduction*)
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   154
fun inst_beta_same maxidx (instT, inst) tm =
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   155
  let
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   156
    fun maxify i = if i > ! maxidx then maxidx := i else ();
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   157
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   158
    val substT = instT_same maxidx instT;
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   159
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   160
    fun expand_head t =
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   161
      (case Term.head_of t of
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   162
        Var ((x, i), T) =>
79129
2933e71f4e09 clarified signature;
wenzelm
parents: 74578
diff changeset
   163
          let val (T', same) = Same.commit_id substT T in
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   164
            (case Vars.lookup inst ((x, i), T') of
74578
wenzelm
parents: 74577
diff changeset
   165
              SOME (t', j) => (maxify j; SOME t')
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   166
            | NONE => (maxify i; if same then NONE else SOME (Var ((x, i), T'))))
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   167
          end
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   168
      | _ => NONE);
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   169
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   170
    fun subst t =
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   171
      (case expand_head t of
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   172
        NONE =>
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   173
          (case t of
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   174
            Const (c, T) => Const (c, substT T)
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   175
          | Free (x, T) => Free (x, substT T)
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   176
          | Var _ => raise Same.SAME
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   177
          | Bound _ => raise Same.SAME
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   178
          | Abs (x, T, b) =>
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   179
              (Abs (x, substT T, subst_commit b)
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   180
                handle Same.SAME => Abs (x, T, subst b))
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   181
          | _ $ _ => subst_comb t)
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   182
      | SOME (u as Abs _) => Term.betapplys (u, map subst_commit (Term.args_of t))
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   183
      | SOME u => subst_head u t)
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   184
    and subst_comb (t $ u) = (subst_comb t $ subst_commit u handle Same.SAME => t $ subst u)
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   185
      | subst_comb (Var _) = raise Same.SAME
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   186
      | subst_comb t = subst t
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   187
    and subst_head h (t $ u) = subst_head h t $ subst_commit u
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   188
      | subst_head h _ = h
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   189
    and subst_commit t = Same.commit subst t;
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   190
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   191
  in subst tm end;
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   192
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   193
in
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   194
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   195
fun instantiateT_maxidx instT ty i =
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32020
diff changeset
   196
  let val maxidx = Unsynchronized.ref i
36620
e6bb250402b5 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
wenzelm
parents: 35408
diff changeset
   197
  in (Same.commit (instT_same maxidx instT) ty, ! maxidx) end;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   198
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   199
fun instantiate_maxidx insts tm i =
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32020
diff changeset
   200
  let val maxidx = Unsynchronized.ref i
36620
e6bb250402b5 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
wenzelm
parents: 35408
diff changeset
   201
  in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   202
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   203
fun instantiate_beta_maxidx insts tm i =
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   204
  let val maxidx = Unsynchronized.ref i
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   205
  in (Same.commit (inst_beta_same maxidx insts) tm, ! maxidx) end;
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   206
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   207
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   208
fun instantiateT_same instT ty =
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   209
  if TVars.is_empty instT then raise Same.SAME
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   210
  else instT_same (Unsynchronized.ref ~1) (no_indexesT instT) ty;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   211
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   212
fun instantiate_same (instT, inst) tm =
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   213
  if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   214
  else inst_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   215
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   216
fun instantiate_beta_same (instT, inst) tm =
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   217
  if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   218
  else inst_beta_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm;
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   219
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   220
36766
wenzelm
parents: 36765
diff changeset
   221
fun instantiateT instT ty = Same.commit (instantiateT_same instT) ty;
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   222
36766
wenzelm
parents: 36765
diff changeset
   223
fun instantiate inst tm = Same.commit (instantiate_same inst) tm;
wenzelm
parents: 36765
diff changeset
   224
74577
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   225
fun instantiate_beta inst tm = Same.commit (instantiate_beta_same inst) tm;
d4829a7333e2 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
wenzelm
parents: 74576
diff changeset
   226
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   227
end;
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   228
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   229
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   230
(* zero var indexes *)
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   231
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   232
fun zero_var_inst ins mk (v as ((x, i), X)) (inst, used) =
80599
f8c070249502 clarified modules (see also e063c0403650);
wenzelm
parents: 79409
diff changeset
   233
  let val (x', used') = Name.variant_bound x used
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   234
  in if x = x' andalso i = 0 then (inst, used') else (ins (v, mk ((x', 0), X)) inst, used') end;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   235
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 68234
diff changeset
   236
fun zero_var_indexes_inst used ts =
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   237
  let
45395
830c9b9b0d66 more scalable zero_var_indexes, depending on canonical order within table;
wenzelm
parents: 43326
diff changeset
   238
    val (instT, _) =
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   239
      (TVars.empty, used) |> TVars.fold (zero_var_inst TVars.add TVar o #1)
74232
1091880266e5 clarified signature;
wenzelm
parents: 74227
diff changeset
   240
        (TVars.build (ts |> (fold o fold_types o fold_atyps)
1091880266e5 clarified signature;
wenzelm
parents: 74227
diff changeset
   241
          (fn TVar v => TVars.add (v, ()) | _ => I)));
45395
830c9b9b0d66 more scalable zero_var_indexes, depending on canonical order within table;
wenzelm
parents: 43326
diff changeset
   242
    val (inst, _) =
74220
c49134ee16c1 more scalable data structure (but: rarely used many arguments);
wenzelm
parents: 74200
diff changeset
   243
      (Vars.empty, used) |> Vars.fold (zero_var_inst Vars.add Var o #1)
74232
1091880266e5 clarified signature;
wenzelm
parents: 74227
diff changeset
   244
        (Vars.build (ts |> (fold o fold_aterms)
1091880266e5 clarified signature;
wenzelm
parents: 74227
diff changeset
   245
          (fn Var (xi, T) => Vars.add ((xi, instantiateT instT T), ()) | _ => I)));
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   246
  in (instT, inst) end;
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   247
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 68234
diff changeset
   248
fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst Name.context ts)) ts;
68234
07eb13eb4065 tuned signature;
wenzelm
parents: 67698
diff changeset
   249
val zero_var_indexes = singleton zero_var_indexes_list;
20513
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   250
4294eb252283 Efficient term substitution -- avoids copying.
wenzelm
parents:
diff changeset
   251
end;