src/Pure/envir.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 58949 e9559088ba29
child 63615 d786d54efc70
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm@247
     1
(*  Title:      Pure/envir.ML
wenzelm@247
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@10485
     3
wenzelm@32031
     4
Free-form environments.  The type of a term variable / sort of a type variable is
wenzelm@32031
     5
part of its name.  The lookup function must apply type substitutions,
berghofe@15797
     6
since they may change the identity of a variable.
clasohm@0
     7
*)
clasohm@0
     8
wenzelm@247
     9
signature ENVIR =
clasohm@0
    10
sig
wenzelm@32018
    11
  type tenv = (typ * term) Vartab.table
wenzelm@32031
    12
  datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv}
wenzelm@32031
    13
  val maxidx_of: env -> int
wenzelm@32031
    14
  val term_env: env -> tenv
berghofe@15797
    15
  val type_env: env -> Type.tyenv
wenzelm@32031
    16
  val is_empty: env -> bool
wenzelm@32031
    17
  val empty: int -> env
wenzelm@32031
    18
  val merge: env * env -> env
wenzelm@26638
    19
  val insert_sorts: env -> sort list -> sort list
wenzelm@10485
    20
  val genvars: string -> env * typ list -> env * term list
wenzelm@10485
    21
  val genvar: string -> env * typ -> env * term
wenzelm@51700
    22
  val lookup1: tenv -> indexname * typ -> term option
wenzelm@51700
    23
  val lookup: env -> indexname * typ -> term option
wenzelm@51700
    24
  val update: (indexname * typ) * term -> env -> env
wenzelm@19861
    25
  val above: env -> int -> bool
wenzelm@51700
    26
  val vupdate: (indexname * typ) * term -> env -> env
wenzelm@32018
    27
  val norm_type_same: Type.tyenv -> typ Same.operation
wenzelm@32018
    28
  val norm_types_same: Type.tyenv -> typ list Same.operation
berghofe@15797
    29
  val norm_type: Type.tyenv -> typ -> typ
wenzelm@32018
    30
  val norm_term_same: env -> term Same.operation
wenzelm@32018
    31
  val norm_term: env -> term -> term
wenzelm@10485
    32
  val beta_norm: term -> term
berghofe@12231
    33
  val head_norm: env -> term -> term
wenzelm@52131
    34
  val eta_long: typ list -> term -> term
wenzelm@18937
    35
  val eta_contract: term -> term
wenzelm@18937
    36
  val beta_eta_contract: term -> term
wenzelm@52131
    37
  val aeconv: term * term -> bool
wenzelm@52221
    38
  val body_type: env -> typ -> typ
wenzelm@52221
    39
  val binder_types: env -> typ -> typ list
wenzelm@52221
    40
  val strip_type: env -> typ -> typ list * typ
berghofe@12231
    41
  val fastype: env -> typ list -> term -> typ
wenzelm@32034
    42
  val subst_type_same: Type.tyenv -> typ Same.operation
wenzelm@32034
    43
  val subst_term_types_same: Type.tyenv -> term Same.operation
wenzelm@32034
    44
  val subst_term_same: Type.tyenv * tenv -> term Same.operation
wenzelm@32034
    45
  val subst_type: Type.tyenv -> typ -> typ
wenzelm@32034
    46
  val subst_term_types: Type.tyenv -> term -> term
wenzelm@32034
    47
  val subst_term: Type.tyenv * tenv -> term -> term
wenzelm@19422
    48
  val expand_atom: typ -> typ * term -> term
wenzelm@21695
    49
  val expand_term: (term -> (typ * term) option) -> term -> term
wenzelm@21795
    50
  val expand_term_frees: ((string * typ) * term) list -> term -> term
clasohm@0
    51
end;
clasohm@0
    52
wenzelm@32031
    53
structure Envir: ENVIR =
clasohm@0
    54
struct
clasohm@0
    55
wenzelm@32031
    56
(** datatype env **)
wenzelm@32031
    57
wenzelm@32031
    58
(*Updating can destroy environment in 2 ways!
wenzelm@32031
    59
   (1) variables out of range
wenzelm@32031
    60
   (2) circular assignments
clasohm@0
    61
*)
wenzelm@32031
    62
wenzelm@32018
    63
type tenv = (typ * term) Vartab.table;
berghofe@15797
    64
clasohm@0
    65
datatype env = Envir of
wenzelm@32031
    66
 {maxidx: int,          (*upper bound of maximum index of vars*)
wenzelm@32031
    67
  tenv: tenv,           (*assignments to Vars*)
wenzelm@32031
    68
  tyenv: Type.tyenv};   (*assignments to TVars*)
wenzelm@32031
    69
wenzelm@32796
    70
fun make_env (maxidx, tenv, tyenv) =
wenzelm@32796
    71
  Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
wenzelm@32031
    72
wenzelm@32031
    73
fun maxidx_of (Envir {maxidx, ...}) = maxidx;
wenzelm@32031
    74
fun term_env (Envir {tenv, ...}) = tenv;
wenzelm@32031
    75
fun type_env (Envir {tyenv, ...}) = tyenv;
wenzelm@32031
    76
wenzelm@32031
    77
fun is_empty env =
wenzelm@32031
    78
  Vartab.is_empty (term_env env) andalso
wenzelm@32031
    79
  Vartab.is_empty (type_env env);
clasohm@0
    80
wenzelm@32031
    81
wenzelm@32031
    82
(* build env *)
wenzelm@32031
    83
wenzelm@32031
    84
fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty);
clasohm@0
    85
wenzelm@32031
    86
fun merge
wenzelm@32031
    87
   (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1},
wenzelm@32031
    88
    Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) =
wenzelm@32031
    89
  make_env (Int.max (maxidx1, maxidx2),
wenzelm@32031
    90
    Vartab.merge (op =) (tenv1, tenv2),
wenzelm@32031
    91
    Vartab.merge (op =) (tyenv1, tyenv2));
wenzelm@32031
    92
wenzelm@32031
    93
wenzelm@32031
    94
(*NB: type unification may invent new sorts*)  (* FIXME tenv!? *)
wenzelm@26638
    95
val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
wenzelm@26638
    96
clasohm@0
    97
(*Generate a list of distinct variables.
clasohm@0
    98
  Increments index to make them distinct from ALL present variables. *)
wenzelm@32031
    99
fun genvars name (Envir {maxidx, tenv, tyenv}, Ts) : env * term list =
wenzelm@32018
   100
  let
wenzelm@32018
   101
    fun genvs (_, [] : typ list) : term list = []
wenzelm@32018
   102
      | genvs (n, [T]) = [Var ((name, maxidx + 1), T)]
wenzelm@32018
   103
      | genvs (n, T :: Ts) =
wenzelm@32018
   104
          Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T)
wenzelm@32018
   105
            :: genvs (n + 1, Ts);
wenzelm@32031
   106
  in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, genvs (0, Ts)) end;
clasohm@0
   107
clasohm@0
   108
(*Generate a variable.*)
wenzelm@32018
   109
fun genvar name (env, T) : env * term =
wenzelm@32018
   110
  let val (env', [v]) = genvars name (env, [T])
wenzelm@32018
   111
  in (env', v) end;
clasohm@0
   112
wenzelm@32031
   113
fun var_clash xi T T' =
wenzelm@51701
   114
  raise TYPE ("Variable has two distinct types", [], [Var (xi, T'), Var (xi, T)]);
clasohm@0
   115
wenzelm@32031
   116
fun lookup_check check tenv (xi, T) =
wenzelm@32031
   117
  (case Vartab.lookup tenv xi of
wenzelm@32018
   118
    NONE => NONE
wenzelm@32031
   119
  | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
berghofe@15797
   120
wenzelm@51700
   121
(*When dealing with environments produced by matching instead
wenzelm@51700
   122
  of unification, there is no need to chase assigned TVars.
wenzelm@51700
   123
  In this case, we can simply ignore the type substitution
wenzelm@51700
   124
  and use = instead of eq_type.*)
wenzelm@51707
   125
fun lookup1 tenv = lookup_check (op =) tenv;
berghofe@15797
   126
wenzelm@58949
   127
fun lookup (Envir {tenv, tyenv, ...}) = lookup_check (Type.unified tyenv) tenv;
clasohm@0
   128
wenzelm@51700
   129
fun update ((xi, T), t) (Envir {maxidx, tenv, tyenv}) =
wenzelm@32031
   130
  Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
wenzelm@247
   131
paulson@2142
   132
(*Determine if the least index updated exceeds lim*)
wenzelm@32031
   133
fun above (Envir {tenv, tyenv, ...}) lim =
wenzelm@52049
   134
  (case Vartab.min tenv of SOME ((_, i), _) => i > lim | NONE => true) andalso
wenzelm@52049
   135
  (case Vartab.min tyenv of SOME ((_, i), _) => i > lim | NONE => true);
wenzelm@247
   136
clasohm@0
   137
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
wenzelm@51700
   138
fun vupdate (aU as (a, U), t) (env as Envir {tyenv, ...}) =
wenzelm@32031
   139
  (case t of
wenzelm@32031
   140
    Var (nT as (name', T)) =>
wenzelm@32031
   141
      if a = name' then env     (*cycle!*)
wenzelm@35408
   142
      else if Term_Ord.indexname_ord (a, name') = LESS then
wenzelm@51700
   143
        (case lookup env nT of  (*if already assigned, chase*)
wenzelm@51700
   144
          NONE => update (nT, Var (a, T)) env
wenzelm@51700
   145
        | SOME u => vupdate (aU, u) env)
wenzelm@51700
   146
      else update (aU, t) env
wenzelm@51700
   147
  | _ => update (aU, t) env);
clasohm@0
   148
clasohm@0
   149
clasohm@0
   150
wenzelm@32031
   151
(** beta normalization wrt. environment **)
clasohm@0
   152
wenzelm@32031
   153
(*Chases variables in env.  Does not exploit sharing of variable bindings
wenzelm@32031
   154
  Does not check types, so could loop.*)
paulson@1500
   155
wenzelm@32018
   156
local
wenzelm@32018
   157
wenzelm@32031
   158
fun norm_type0 tyenv : typ Same.operation =
wenzelm@32018
   159
  let
wenzelm@32018
   160
    fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
wenzelm@32018
   161
      | norm (TFree _) = raise Same.SAME
wenzelm@32018
   162
      | norm (TVar v) =
wenzelm@32031
   163
          (case Type.lookup tyenv v of
wenzelm@32018
   164
            SOME U => Same.commit norm U
wenzelm@32018
   165
          | NONE => raise Same.SAME);
wenzelm@32018
   166
  in norm end;
clasohm@0
   167
wenzelm@32031
   168
fun norm_term1 tenv : term Same.operation =
wenzelm@32018
   169
  let
wenzelm@32018
   170
    fun norm (Var v) =
wenzelm@51700
   171
          (case lookup1 tenv v of
wenzelm@32018
   172
            SOME u => Same.commit norm u
wenzelm@32018
   173
          | NONE => raise Same.SAME)
wenzelm@32031
   174
      | norm (Abs (a, T, body)) = Abs (a, T, norm body)
wenzelm@32018
   175
      | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
wenzelm@32018
   176
      | norm (f $ t) =
wenzelm@32018
   177
          ((case norm f of
wenzelm@32018
   178
             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
wenzelm@32018
   179
           | nf => nf $ Same.commit norm t)
wenzelm@32018
   180
          handle Same.SAME => f $ norm t)
wenzelm@32018
   181
      | norm _ = raise Same.SAME;
wenzelm@32018
   182
  in norm end;
clasohm@0
   183
wenzelm@58945
   184
fun norm_term2 (envir as Envir {tenv, tyenv, ...}) : term Same.operation =
wenzelm@32018
   185
  let
wenzelm@32031
   186
    val normT = norm_type0 tyenv;
wenzelm@32018
   187
    fun norm (Const (a, T)) = Const (a, normT T)
wenzelm@32018
   188
      | norm (Free (a, T)) = Free (a, normT T)
wenzelm@32018
   189
      | norm (Var (xi, T)) =
wenzelm@58945
   190
          (case lookup envir (xi, T) of
wenzelm@32018
   191
            SOME u => Same.commit norm u
wenzelm@32018
   192
          | NONE => Var (xi, normT T))
wenzelm@32018
   193
      | norm (Abs (a, T, body)) =
wenzelm@32018
   194
          (Abs (a, normT T, Same.commit norm body)
wenzelm@32018
   195
            handle Same.SAME => Abs (a, T, norm body))
wenzelm@32018
   196
      | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
wenzelm@32018
   197
      | norm (f $ t) =
wenzelm@32018
   198
          ((case norm f of
wenzelm@32018
   199
             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
wenzelm@32018
   200
           | nf => nf $ Same.commit norm t)
wenzelm@32018
   201
          handle Same.SAME => f $ norm t)
wenzelm@32018
   202
      | norm _ = raise Same.SAME;
wenzelm@32018
   203
  in norm end;
berghofe@11513
   204
wenzelm@32018
   205
in
wenzelm@32018
   206
wenzelm@32031
   207
fun norm_type_same tyenv T =
wenzelm@32031
   208
  if Vartab.is_empty tyenv then raise Same.SAME
wenzelm@32031
   209
  else norm_type0 tyenv T;
clasohm@0
   210
wenzelm@32031
   211
fun norm_types_same tyenv Ts =
wenzelm@32031
   212
  if Vartab.is_empty tyenv then raise Same.SAME
wenzelm@32031
   213
  else Same.map (norm_type0 tyenv) Ts;
wenzelm@32018
   214
wenzelm@32031
   215
fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T;
berghofe@11513
   216
wenzelm@58945
   217
fun norm_term_same (envir as Envir {tenv, tyenv, ...}) =
wenzelm@32031
   218
  if Vartab.is_empty tyenv then norm_term1 tenv
wenzelm@58945
   219
  else norm_term2 envir;
wenzelm@10485
   220
wenzelm@32018
   221
fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
berghofe@25471
   222
fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
lcp@719
   223
wenzelm@32018
   224
end;
berghofe@11513
   225
berghofe@11513
   226
wenzelm@52131
   227
(* head normal form for unification *)
berghofe@12231
   228
wenzelm@32018
   229
fun head_norm env =
berghofe@12231
   230
  let
wenzelm@32018
   231
    fun norm (Var v) =
wenzelm@51700
   232
        (case lookup env v of
skalberg@15531
   233
          SOME u => head_norm env u
wenzelm@32018
   234
        | NONE => raise Same.SAME)
wenzelm@32018
   235
      | norm (Abs (a, T, body)) = Abs (a, T, norm body)
wenzelm@32018
   236
      | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
wenzelm@32018
   237
      | norm (f $ t) =
wenzelm@32018
   238
          (case norm f of
wenzelm@32018
   239
            Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
wenzelm@32018
   240
          | nf => nf $ t)
wenzelm@32018
   241
      | norm _ = raise Same.SAME;
wenzelm@32018
   242
  in Same.commit norm end;
berghofe@12231
   243
berghofe@12231
   244
wenzelm@52131
   245
(* eta-long beta-normal form *)
wenzelm@52131
   246
wenzelm@52131
   247
fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
wenzelm@52131
   248
  | eta_long Ts t =
wenzelm@52131
   249
      (case strip_comb t of
wenzelm@52131
   250
        (Abs _, _) => eta_long Ts (beta_norm t)
wenzelm@52131
   251
      | (u, ts) =>
wenzelm@52131
   252
          let
wenzelm@52131
   253
            val Us = binder_types (fastype_of1 (Ts, t));
wenzelm@52131
   254
            val i = length Us;
wenzelm@52132
   255
            val long = eta_long (rev Us @ Ts);
wenzelm@52131
   256
          in
wenzelm@52131
   257
            fold_rev (Term.abs o pair "x") Us
wenzelm@52132
   258
              (list_comb (incr_boundvars i u,
wenzelm@52132
   259
                map (long o incr_boundvars i) ts @ map (long o Bound) (i - 1 downto 0)))
wenzelm@52131
   260
          end);
wenzelm@52131
   261
wenzelm@52131
   262
wenzelm@52131
   263
(* full eta contraction *)
wenzelm@18937
   264
wenzelm@22174
   265
local
wenzelm@22174
   266
wenzelm@32018
   267
fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
wenzelm@22174
   268
  | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
wenzelm@32018
   269
  | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
wenzelm@32018
   270
  | decr _ _ = raise Same.SAME
wenzelm@32018
   271
and decrh lev t = (decr lev t handle Same.SAME => t);
wenzelm@20670
   272
wenzelm@22174
   273
fun eta (Abs (a, T, body)) =
wenzelm@22174
   274
    ((case eta body of
wenzelm@22174
   275
        body' as (f $ Bound 0) =>
wenzelm@42083
   276
          if Term.is_dependent f then Abs (a, T, body')
wenzelm@22174
   277
          else decrh 0 f
wenzelm@32018
   278
     | body' => Abs (a, T, body')) handle Same.SAME =>
wenzelm@22174
   279
        (case body of
wenzelm@22174
   280
          f $ Bound 0 =>
wenzelm@42083
   281
            if Term.is_dependent f then raise Same.SAME
wenzelm@22174
   282
            else decrh 0 f
wenzelm@32018
   283
        | _ => raise Same.SAME))
wenzelm@32018
   284
  | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
wenzelm@32018
   285
  | eta _ = raise Same.SAME;
wenzelm@22174
   286
wenzelm@22174
   287
in
wenzelm@22174
   288
wenzelm@22174
   289
fun eta_contract t =
wenzelm@32018
   290
  if Term.has_abs t then Same.commit eta t else t;
wenzelm@18937
   291
wenzelm@52131
   292
end;
wenzelm@52131
   293
wenzelm@18937
   294
val beta_eta_contract = eta_contract o beta_norm;
wenzelm@18937
   295
wenzelm@52131
   296
fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
wenzelm@22174
   297
wenzelm@18937
   298
wenzelm@52221
   299
fun body_type env (Type ("fun", [_, T])) = body_type env T
wenzelm@52221
   300
  | body_type env (T as TVar v) =
wenzelm@52128
   301
      (case Type.lookup (type_env env) v of
wenzelm@52128
   302
        NONE => T
wenzelm@52221
   303
      | SOME T' => body_type env T')
wenzelm@52221
   304
  | body_type _ T = T;
wenzelm@52128
   305
wenzelm@52221
   306
fun binder_types env (Type ("fun", [T, U])) = T :: binder_types env U
wenzelm@52221
   307
  | binder_types env (TVar v) =
wenzelm@52128
   308
      (case Type.lookup (type_env env) v of
wenzelm@52128
   309
        NONE => []
wenzelm@52221
   310
      | SOME T' => binder_types env T')
wenzelm@52221
   311
  | binder_types _ _ = [];
wenzelm@52128
   312
wenzelm@52221
   313
fun strip_type env T = (binder_types env T, body_type env T);
wenzelm@52128
   314
berghofe@12231
   315
(*finds type of term without checking that combinations are consistent
berghofe@12231
   316
  Ts holds types of bound variables*)
wenzelm@32031
   317
fun fastype (Envir {tyenv, ...}) =
wenzelm@32031
   318
  let
wenzelm@32031
   319
    val funerr = "fastype: expected function type";
berghofe@12231
   320
    fun fast Ts (f $ u) =
paulson@32648
   321
          (case Type.devar tyenv (fast Ts f) of
wenzelm@32031
   322
            Type ("fun", [_, T]) => T
paulson@32648
   323
          | TVar v => raise TERM (funerr, [f $ u])
wenzelm@32031
   324
          | _ => raise TERM (funerr, [f $ u]))
berghofe@12231
   325
      | fast Ts (Const (_, T)) = T
berghofe@12231
   326
      | fast Ts (Free (_, T)) = T
berghofe@12231
   327
      | fast Ts (Bound i) =
wenzelm@43278
   328
          (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i]))
wenzelm@20670
   329
      | fast Ts (Var (_, T)) = T
wenzelm@32031
   330
      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
wenzelm@32031
   331
  in fast end;
berghofe@12231
   332
berghofe@15797
   333
wenzelm@32034
   334
(** plain substitution -- without variable chasing **)
wenzelm@32034
   335
wenzelm@32034
   336
local
berghofe@15797
   337
wenzelm@32034
   338
fun subst_type0 tyenv = Term_Subst.map_atypsT_same
wenzelm@32034
   339
  (fn TVar v =>
wenzelm@32034
   340
        (case Type.lookup tyenv v of
wenzelm@32034
   341
          SOME U => U
wenzelm@32034
   342
        | NONE => raise Same.SAME)
wenzelm@32034
   343
    | _ => raise Same.SAME);
wenzelm@32034
   344
wenzelm@32034
   345
fun subst_term1 tenv = Term_Subst.map_aterms_same
wenzelm@32034
   346
  (fn Var v =>
wenzelm@51700
   347
        (case lookup1 tenv v of
wenzelm@32034
   348
          SOME u => u
wenzelm@32034
   349
        | NONE => raise Same.SAME)
wenzelm@32034
   350
    | _ => raise Same.SAME);
berghofe@15797
   351
wenzelm@32034
   352
fun subst_term2 tenv tyenv : term Same.operation =
wenzelm@32034
   353
  let
wenzelm@32034
   354
    val substT = subst_type0 tyenv;
wenzelm@32034
   355
    fun subst (Const (a, T)) = Const (a, substT T)
wenzelm@32034
   356
      | subst (Free (a, T)) = Free (a, substT T)
wenzelm@32034
   357
      | subst (Var (xi, T)) =
wenzelm@51700
   358
          (case lookup1 tenv (xi, T) of
wenzelm@32034
   359
            SOME u => u
wenzelm@32034
   360
          | NONE => Var (xi, substT T))
wenzelm@32034
   361
      | subst (Bound _) = raise Same.SAME
wenzelm@32034
   362
      | subst (Abs (a, T, t)) =
wenzelm@32034
   363
          (Abs (a, substT T, Same.commit subst t)
wenzelm@32034
   364
            handle Same.SAME => Abs (a, T, subst t))
wenzelm@32034
   365
      | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
wenzelm@32034
   366
  in subst end;
wenzelm@32034
   367
wenzelm@32034
   368
in
berghofe@15797
   369
wenzelm@32034
   370
fun subst_type_same tyenv T =
wenzelm@32034
   371
  if Vartab.is_empty tyenv then raise Same.SAME
wenzelm@32034
   372
  else subst_type0 tyenv T;
wenzelm@32034
   373
wenzelm@32034
   374
fun subst_term_types_same tyenv t =
wenzelm@32034
   375
  if Vartab.is_empty tyenv then raise Same.SAME
wenzelm@32034
   376
  else Term_Subst.map_types_same (subst_type0 tyenv) t;
wenzelm@32034
   377
wenzelm@32034
   378
fun subst_term_same (tyenv, tenv) =
wenzelm@32034
   379
  if Vartab.is_empty tenv then subst_term_types_same tyenv
wenzelm@32034
   380
  else if Vartab.is_empty tyenv then subst_term1 tenv
wenzelm@32034
   381
  else subst_term2 tenv tyenv;
wenzelm@32034
   382
wenzelm@32034
   383
fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
wenzelm@32034
   384
fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
wenzelm@32034
   385
fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
wenzelm@32034
   386
wenzelm@32034
   387
end;
berghofe@15797
   388
wenzelm@18937
   389
wenzelm@32034
   390
wenzelm@32034
   391
(** expand defined atoms -- with local beta reduction **)
wenzelm@18937
   392
wenzelm@19422
   393
fun expand_atom T (U, u) =
wenzelm@32034
   394
  subst_term_types (Type.raw_match (U, T) Vartab.empty) u
wenzelm@32031
   395
    handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
wenzelm@18937
   396
wenzelm@21795
   397
fun expand_term get =
wenzelm@21695
   398
  let
wenzelm@21695
   399
    fun expand tm =
wenzelm@21695
   400
      let
wenzelm@21695
   401
        val (head, args) = Term.strip_comb tm;
wenzelm@21695
   402
        val args' = map expand args;
wenzelm@21695
   403
        fun comb head' = Term.list_comb (head', args');
wenzelm@21695
   404
      in
wenzelm@21695
   405
        (case head of
wenzelm@21695
   406
          Abs (x, T, t) => comb (Abs (x, T, expand t))
wenzelm@21695
   407
        | _ =>
wenzelm@32031
   408
          (case get head of
wenzelm@32031
   409
            SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
wenzelm@32031
   410
          | NONE => comb head))
wenzelm@21695
   411
      end;
wenzelm@21695
   412
  in expand end;
wenzelm@21695
   413
wenzelm@21795
   414
fun expand_term_frees defs =
wenzelm@21795
   415
  let
wenzelm@21795
   416
    val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
wenzelm@21795
   417
    val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
wenzelm@21795
   418
  in expand_term get end;
wenzelm@21795
   419
clasohm@0
   420
end;