src/Pure/term_subst.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 36766 33e4246edf29
child 43326 47cf4bc789aa
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
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@20513
   163
fun zero_var_inst vars =
wenzelm@20513
   164
  fold (fn v as ((x, i), X) => fn (inst, used) =>
wenzelm@20513
   165
    let
wenzelm@20513
   166
      val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
wenzelm@20513
   167
    in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
wenzelm@20513
   168
  vars ([], Name.context) |> #1;
wenzelm@20513
   169
wenzelm@21607
   170
fun zero_var_indexes_inst ts =
wenzelm@20513
   171
  let
wenzelm@35408
   172
    val tvars = sort Term_Ord.tvar_ord (fold Term.add_tvars ts []);
wenzelm@21607
   173
    val instT = map (apsnd TVar) (zero_var_inst tvars);
wenzelm@35408
   174
    val vars = sort Term_Ord.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
wenzelm@21607
   175
    val inst = map (apsnd Var) (zero_var_inst vars);
wenzelm@20513
   176
  in (instT, inst) end;
wenzelm@20513
   177
wenzelm@21607
   178
fun zero_var_indexes t = instantiate (zero_var_indexes_inst [t]) t;
wenzelm@20513
   179
wenzelm@20513
   180
end;