src/Pure/term_subst.ML
author wenzelm
Mon Mar 10 15:04:01 2014 +0100 (2014-03-10)
changeset 56026 893fe12639bc
parent 45395 830c9b9b0d66
child 67698 67caf783b9ee
permissions -rw-r--r--
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm@20513
     1
(*  Title:      Pure/term_subst.ML
wenzelm@20513
     2
    Author:     Makarius
wenzelm@20513
     3
wenzelm@32016
     4
Efficient type/term substitution.
wenzelm@20513
     5
*)
wenzelm@20513
     6
wenzelm@20513
     7
signature TERM_SUBST =
wenzelm@20513
     8
sig
wenzelm@32016
     9
  val map_atypsT_same: typ Same.operation -> typ Same.operation
wenzelm@32016
    10
  val map_types_same: typ Same.operation -> term Same.operation
wenzelm@32016
    11
  val map_aterms_same: term Same.operation -> term Same.operation
wenzelm@36620
    12
  val generalizeT_same: string list -> int -> typ Same.operation
wenzelm@36620
    13
  val generalize_same: string list * string list -> int -> term Same.operation
wenzelm@36766
    14
  val generalizeT: string list -> int -> typ -> typ
wenzelm@20513
    15
  val generalize: string list * string list -> int -> term -> term
wenzelm@20513
    16
  val instantiateT_maxidx: ((indexname * sort) * (typ * int)) list -> typ -> int -> typ * int
wenzelm@20513
    17
  val instantiate_maxidx:
wenzelm@20513
    18
    ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
wenzelm@20513
    19
    term -> int -> term * int
wenzelm@36766
    20
  val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
wenzelm@36766
    21
  val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
wenzelm@36766
    22
    term Same.operation
wenzelm@36620
    23
  val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
wenzelm@20513
    24
  val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
wenzelm@20513
    25
    term -> term
wenzelm@20513
    26
  val zero_var_indexes: term -> term
wenzelm@21607
    27
  val zero_var_indexes_inst: term list ->
wenzelm@20513
    28
    ((indexname * sort) * typ) list * ((indexname * typ) * term) list
wenzelm@20513
    29
end;
wenzelm@20513
    30
wenzelm@31977
    31
structure Term_Subst: TERM_SUBST =
wenzelm@20513
    32
struct
wenzelm@20513
    33
wenzelm@31980
    34
(* generic mapping *)
wenzelm@31980
    35
wenzelm@31980
    36
fun map_atypsT_same f =
wenzelm@31980
    37
  let
wenzelm@32020
    38
    fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts)
wenzelm@32020
    39
      | typ T = f T;
wenzelm@31980
    40
  in typ end;
wenzelm@31980
    41
wenzelm@31980
    42
fun map_types_same f =
wenzelm@31980
    43
  let
wenzelm@31980
    44
    fun term (Const (a, T)) = Const (a, f T)
wenzelm@31980
    45
      | term (Free (a, T)) = Free (a, f T)
wenzelm@31980
    46
      | term (Var (v, T)) = Var (v, f T)
wenzelm@32020
    47
      | term (Bound _) = raise Same.SAME
wenzelm@31980
    48
      | term (Abs (x, T, t)) =
wenzelm@32016
    49
          (Abs (x, f T, Same.commit term t)
wenzelm@32016
    50
            handle Same.SAME => Abs (x, T, term t))
wenzelm@32016
    51
      | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u);
wenzelm@31980
    52
  in term end;
wenzelm@31980
    53
wenzelm@31980
    54
fun map_aterms_same f =
wenzelm@31980
    55
  let
wenzelm@31980
    56
    fun term (Abs (x, T, t)) = Abs (x, T, term t)
wenzelm@32016
    57
      | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u)
wenzelm@31980
    58
      | term a = f a;
wenzelm@31980
    59
  in term end;
wenzelm@31980
    60
wenzelm@31980
    61
wenzelm@20513
    62
(* generalization of fixed variables *)
wenzelm@20513
    63
wenzelm@32016
    64
fun generalizeT_same [] _ _ = raise Same.SAME
wenzelm@20513
    65
  | generalizeT_same tfrees idx ty =
wenzelm@20513
    66
      let
wenzelm@32020
    67
        fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
wenzelm@32020
    68
          | gen (TFree (a, S)) =
wenzelm@20513
    69
              if member (op =) tfrees a then TVar ((a, idx), S)
wenzelm@32016
    70
              else raise Same.SAME
wenzelm@32020
    71
          | gen _ = raise Same.SAME;
wenzelm@32020
    72
      in gen ty end;
wenzelm@20513
    73
wenzelm@32016
    74
fun generalize_same ([], []) _ _ = raise Same.SAME
wenzelm@20513
    75
  | generalize_same (tfrees, frees) idx tm =
wenzelm@20513
    76
      let
wenzelm@20513
    77
        val genT = generalizeT_same tfrees idx;
wenzelm@20513
    78
        fun gen (Free (x, T)) =
wenzelm@20513
    79
              if member (op =) frees x then
wenzelm@32016
    80
                Var (Name.clean_index (x, idx), Same.commit genT T)
wenzelm@20513
    81
              else Free (x, genT T)
wenzelm@20513
    82
          | gen (Var (xi, T)) = Var (xi, genT T)
wenzelm@20513
    83
          | gen (Const (c, T)) = Const (c, genT T)
wenzelm@32016
    84
          | gen (Bound _) = raise Same.SAME
wenzelm@20513
    85
          | gen (Abs (x, T, t)) =
wenzelm@32016
    86
              (Abs (x, genT T, Same.commit gen t)
wenzelm@32016
    87
                handle Same.SAME => Abs (x, T, gen t))
wenzelm@32016
    88
          | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u);
wenzelm@20513
    89
      in gen tm end;
wenzelm@20513
    90
wenzelm@36766
    91
fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty;
wenzelm@36620
    92
fun generalize names i tm = Same.commit (generalize_same names i) tm;
wenzelm@20513
    93
wenzelm@20513
    94
wenzelm@20513
    95
(* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
wenzelm@20513
    96
wenzelm@20513
    97
local
wenzelm@20513
    98
wenzelm@20513
    99
fun no_index (x, y) = (x, (y, ~1));
wenzelm@20513
   100
fun no_indexes1 inst = map no_index inst;
wenzelm@20513
   101
fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
wenzelm@20513
   102
wenzelm@36620
   103
fun instT_same maxidx instT ty =
wenzelm@20513
   104
  let
wenzelm@21184
   105
    fun maxify i = if i > ! maxidx then maxidx := i else ();
wenzelm@21184
   106
wenzelm@20513
   107
    fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
wenzelm@20513
   108
      | subst_typ (TVar ((a, i), S)) =
wenzelm@20513
   109
          (case AList.lookup Term.eq_tvar instT ((a, i), S) of
wenzelm@20513
   110
            SOME (T, j) => (maxify j; T)
wenzelm@32016
   111
          | NONE => (maxify i; raise Same.SAME))
wenzelm@32016
   112
      | subst_typ _ = raise Same.SAME
wenzelm@20513
   113
    and subst_typs (T :: Ts) =
wenzelm@32016
   114
        (subst_typ T :: Same.commit subst_typs Ts
wenzelm@32016
   115
          handle Same.SAME => T :: subst_typs Ts)
wenzelm@32016
   116
      | subst_typs [] = raise Same.SAME;
wenzelm@20513
   117
  in subst_typ ty end;
wenzelm@20513
   118
wenzelm@36620
   119
fun inst_same maxidx (instT, inst) tm =
wenzelm@20513
   120
  let
wenzelm@21184
   121
    fun maxify i = if i > ! maxidx then maxidx := i else ();
wenzelm@21184
   122
wenzelm@36620
   123
    val substT = instT_same maxidx instT;
wenzelm@20513
   124
    fun subst (Const (c, T)) = Const (c, substT T)
wenzelm@20513
   125
      | subst (Free (x, T)) = Free (x, substT T)
wenzelm@20513
   126
      | subst (Var ((x, i), T)) =
wenzelm@32016
   127
          let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
wenzelm@20513
   128
            (case AList.lookup Term.eq_var inst ((x, i), T') of
wenzelm@20513
   129
               SOME (t, j) => (maxify j; t)
wenzelm@32016
   130
             | NONE => (maxify i; if same then raise Same.SAME else Var ((x, i), T')))
wenzelm@20513
   131
          end
wenzelm@32016
   132
      | subst (Bound _) = raise Same.SAME
wenzelm@20513
   133
      | subst (Abs (x, T, t)) =
wenzelm@32016
   134
          (Abs (x, substT T, Same.commit subst t)
wenzelm@32016
   135
            handle Same.SAME => Abs (x, T, subst t))
wenzelm@32016
   136
      | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
wenzelm@20513
   137
  in subst tm end;
wenzelm@20513
   138
wenzelm@20513
   139
in
wenzelm@20513
   140
wenzelm@20513
   141
fun instantiateT_maxidx instT ty i =
wenzelm@32738
   142
  let val maxidx = Unsynchronized.ref i
wenzelm@36620
   143
  in (Same.commit (instT_same maxidx instT) ty, ! maxidx) end;
wenzelm@20513
   144
wenzelm@20513
   145
fun instantiate_maxidx insts tm i =
wenzelm@32738
   146
  let val maxidx = Unsynchronized.ref i
wenzelm@36620
   147
  in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
wenzelm@20513
   148
wenzelm@36620
   149
fun instantiateT_same [] _ = raise Same.SAME
wenzelm@36620
   150
  | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty;
wenzelm@20513
   151
wenzelm@36620
   152
fun instantiate_same ([], []) _ = raise Same.SAME
wenzelm@36620
   153
  | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm;
wenzelm@20513
   154
wenzelm@36766
   155
fun instantiateT instT ty = Same.commit (instantiateT_same instT) ty;
wenzelm@36766
   156
fun instantiate inst tm = Same.commit (instantiate_same inst) tm;
wenzelm@36766
   157
wenzelm@20513
   158
end;
wenzelm@20513
   159
wenzelm@20513
   160
wenzelm@20513
   161
(* zero var indexes *)
wenzelm@20513
   162
wenzelm@45395
   163
structure TVars = Table(type key = indexname * sort val ord = Term_Ord.tvar_ord);
wenzelm@45395
   164
structure Vars = Table(type key = indexname * typ val ord = Term_Ord.var_ord);
wenzelm@45395
   165
wenzelm@45395
   166
fun zero_var_inst mk (v as ((x, i), X)) (inst, used) =
wenzelm@45395
   167
  let
wenzelm@45395
   168
    val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
wenzelm@45395
   169
  in if x = x' andalso i = 0 then (inst, used') else ((v, mk ((x', 0), X)) :: inst, used') end;
wenzelm@20513
   170
wenzelm@21607
   171
fun zero_var_indexes_inst ts =
wenzelm@20513
   172
  let
wenzelm@45395
   173
    val (instT, _) =
wenzelm@45395
   174
      TVars.fold (zero_var_inst TVar o #1)
wenzelm@45395
   175
        ((fold o fold_types o fold_atyps) (fn TVar v =>
wenzelm@45395
   176
          TVars.insert (K true) (v, ()) | _ => I) ts TVars.empty)
wenzelm@45395
   177
        ([], Name.context);
wenzelm@45395
   178
    val (inst, _) =
wenzelm@45395
   179
      Vars.fold (zero_var_inst Var o #1)
wenzelm@45395
   180
        ((fold o fold_aterms) (fn Var (xi, T) =>
wenzelm@45395
   181
          Vars.insert (K true) ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty)
wenzelm@45395
   182
        ([], Name.context);
wenzelm@20513
   183
  in (instT, inst) end;
wenzelm@20513
   184
wenzelm@21607
   185
fun zero_var_indexes t = instantiate (zero_var_indexes_inst [t]) t;
wenzelm@20513
   186
wenzelm@20513
   187
end;