src/Pure/envir.ML
author wenzelm
Thu Jul 16 20:32:05 2009 +0200 (2009-07-16)
changeset 32018 3370cea95387
parent 30146 a77fc0209723
child 32031 e2e6b0691264
permissions -rw-r--r--
use structure Same;
tuned signature;
tuned comments;
tuned;
wenzelm@247
     1
(*  Title:      Pure/envir.ML
wenzelm@247
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@10485
     3
berghofe@15797
     4
Environments.  The type of a term variable / sort of a type variable is
berghofe@15797
     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
berghofe@15797
    12
  datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
berghofe@15797
    13
  val type_env: env -> Type.tyenv
wenzelm@26638
    14
  val insert_sorts: env -> sort list -> sort list
wenzelm@10485
    15
  val genvars: string -> env * typ list -> env * term list
wenzelm@10485
    16
  val genvar: string -> env * typ -> env * term
berghofe@15797
    17
  val lookup: env * (indexname * typ) -> term option
berghofe@16652
    18
  val lookup': tenv * (indexname * typ) -> term option
berghofe@15797
    19
  val update: ((indexname * typ) * term) * env -> env
wenzelm@10485
    20
  val empty: int -> env
wenzelm@10485
    21
  val is_empty: env -> bool
wenzelm@19861
    22
  val above: env -> int -> bool
berghofe@15797
    23
  val vupdate: ((indexname * typ) * term) * env -> env
berghofe@15797
    24
  val alist_of: env -> (indexname * (typ * term)) list
wenzelm@32018
    25
  val norm_type_same: Type.tyenv -> typ Same.operation
wenzelm@32018
    26
  val norm_types_same: Type.tyenv -> typ list Same.operation
berghofe@15797
    27
  val norm_type: Type.tyenv -> typ -> typ
wenzelm@32018
    28
  val norm_term_same: env -> term Same.operation
wenzelm@32018
    29
  val norm_term: env -> term -> term
wenzelm@10485
    30
  val beta_norm: term -> term
berghofe@12231
    31
  val head_norm: env -> term -> term
wenzelm@18937
    32
  val eta_contract: term -> term
wenzelm@18937
    33
  val beta_eta_contract: term -> term
berghofe@12231
    34
  val fastype: env -> typ list -> term -> typ
berghofe@15797
    35
  val typ_subst_TVars: Type.tyenv -> typ -> typ
berghofe@15797
    36
  val subst_TVars: Type.tyenv -> term -> term
berghofe@15797
    37
  val subst_Vars: tenv -> term -> term
berghofe@15797
    38
  val subst_vars: Type.tyenv * tenv -> term -> term
wenzelm@19422
    39
  val expand_atom: typ -> typ * term -> term
wenzelm@21695
    40
  val expand_term: (term -> (typ * term) option) -> term -> term
wenzelm@21795
    41
  val expand_term_frees: ((string * typ) * term) list -> term -> term
clasohm@0
    42
end;
clasohm@0
    43
paulson@1500
    44
structure Envir : ENVIR =
clasohm@0
    45
struct
clasohm@0
    46
clasohm@0
    47
(*updating can destroy environment in 2 ways!!
clasohm@0
    48
   (1) variables out of range   (2) circular assignments
clasohm@0
    49
*)
wenzelm@32018
    50
type tenv = (typ * term) Vartab.table;
berghofe@15797
    51
clasohm@0
    52
datatype env = Envir of
wenzelm@32018
    53
 {maxidx: int,      (*maximum index of vars*)
wenzelm@32018
    54
  asol: tenv,       (*assignments to Vars*)
wenzelm@32018
    55
  iTs: Type.tyenv}; (*assignments to TVars*)
clasohm@0
    56
wenzelm@12496
    57
fun type_env (Envir {iTs, ...}) = iTs;
clasohm@0
    58
wenzelm@26638
    59
(*NB: type unification may invent new sorts*)
wenzelm@26638
    60
val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
wenzelm@26638
    61
clasohm@0
    62
(*Generate a list of distinct variables.
clasohm@0
    63
  Increments index to make them distinct from ALL present variables. *)
clasohm@0
    64
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
wenzelm@32018
    65
  let
wenzelm@32018
    66
    fun genvs (_, [] : typ list) : term list = []
wenzelm@32018
    67
      | genvs (n, [T]) = [Var ((name, maxidx + 1), T)]
wenzelm@32018
    68
      | genvs (n, T :: Ts) =
wenzelm@32018
    69
          Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T)
wenzelm@32018
    70
            :: genvs (n + 1, Ts);
wenzelm@32018
    71
  in (Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs}, genvs (0, Ts)) end;
clasohm@0
    72
clasohm@0
    73
(*Generate a variable.*)
wenzelm@32018
    74
fun genvar name (env, T) : env * term =
wenzelm@32018
    75
  let val (env', [v]) = genvars name (env, [T])
wenzelm@32018
    76
  in (env', v) end;
clasohm@0
    77
berghofe@15797
    78
fun var_clash ixn T T' = raise TYPE ("Variable " ^
wenzelm@32018
    79
    quote (Term.string_of_vname ixn) ^ " has two distinct types",
wenzelm@32018
    80
    [T', T], []);
clasohm@0
    81
berghofe@15797
    82
fun gen_lookup f asol (xname, T) =
wenzelm@17412
    83
  (case Vartab.lookup asol xname of
wenzelm@32018
    84
    NONE => NONE
wenzelm@32018
    85
  | SOME (U, t) => if f (T, U) then SOME t else var_clash xname T U);
berghofe@15797
    86
berghofe@16652
    87
(* When dealing with environments produced by matching instead *)
berghofe@16652
    88
(* of unification, there is no need to chase assigned TVars.   *)
berghofe@16652
    89
(* In this case, we can simply ignore the type substitution    *)
berghofe@16652
    90
(* and use = instead of eq_type.                               *)
berghofe@15797
    91
berghofe@16652
    92
fun lookup' (asol, p) = gen_lookup op = asol p;
berghofe@15797
    93
berghofe@16652
    94
fun lookup2 (iTs, asol) p =
berghofe@16652
    95
  if Vartab.is_empty iTs then lookup' (asol, p)
berghofe@16652
    96
  else gen_lookup (Type.eq_type iTs) asol p;
berghofe@15797
    97
berghofe@15797
    98
fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
berghofe@15797
    99
berghofe@15797
   100
fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
wenzelm@32018
   101
  Envir {maxidx = maxidx, asol = Vartab.update_new (xname, (T, t)) asol, iTs = iTs};
clasohm@0
   102
wenzelm@5289
   103
(*The empty environment.  New variables will start with the given index+1.*)
wenzelm@32018
   104
fun empty m = Envir {maxidx = m, asol = Vartab.empty, iTs = Vartab.empty};
clasohm@0
   105
paulson@2142
   106
(*Test for empty environment*)
berghofe@8407
   107
fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
wenzelm@247
   108
paulson@2142
   109
(*Determine if the least index updated exceeds lim*)
wenzelm@19861
   110
fun above (Envir {asol, iTs, ...}) lim =
wenzelm@19861
   111
  (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso
wenzelm@19861
   112
  (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true);
wenzelm@247
   113
clasohm@0
   114
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
berghofe@15797
   115
fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
berghofe@15797
   116
      Var (nT as (name', T)) =>
berghofe@15797
   117
        if a = name' then env     (*cycle!*)
wenzelm@29269
   118
        else if TermOrd.indexname_ord (a, name') = LESS then
berghofe@15797
   119
           (case lookup (env, nT) of  (*if already assigned, chase*)
berghofe@15797
   120
                NONE => update ((nT, Var (a, T)), env)
berghofe@15797
   121
              | SOME u => vupdate ((aU, u), env))
berghofe@15797
   122
        else update ((aU, t), env)
berghofe@15797
   123
    | _ => update ((aU, t), env);
clasohm@0
   124
clasohm@0
   125
clasohm@0
   126
(*Convert environment to alist*)
berghofe@8407
   127
fun alist_of (Envir{asol,...}) = Vartab.dest asol;
clasohm@0
   128
clasohm@0
   129
paulson@1500
   130
(*** Beta normal form for terms (not eta normal form).
paulson@1500
   131
     Chases variables in env;  Does not exploit sharing of variable bindings
paulson@1500
   132
     Does not check types, so could loop. ***)
paulson@1500
   133
wenzelm@32018
   134
local
wenzelm@32018
   135
wenzelm@32018
   136
fun norm_type0 iTs : typ Same.operation =
wenzelm@32018
   137
  let
wenzelm@32018
   138
    fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
wenzelm@32018
   139
      | norm (TFree _) = raise Same.SAME
wenzelm@32018
   140
      | norm (TVar v) =
wenzelm@32018
   141
          (case Type.lookup iTs v of
wenzelm@32018
   142
            SOME U => Same.commit norm U
wenzelm@32018
   143
          | NONE => raise Same.SAME);
wenzelm@32018
   144
  in norm end;
clasohm@0
   145
wenzelm@32018
   146
fun norm_term1 asol : term Same.operation =
wenzelm@32018
   147
  let
wenzelm@32018
   148
    fun norm (Var v) =
wenzelm@32018
   149
          (case lookup' (asol, v) of
wenzelm@32018
   150
            SOME u => Same.commit norm u
wenzelm@32018
   151
          | NONE => raise Same.SAME)
wenzelm@32018
   152
      | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
wenzelm@32018
   153
      | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
wenzelm@32018
   154
      | norm (f $ t) =
wenzelm@32018
   155
          ((case norm f of
wenzelm@32018
   156
             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
wenzelm@32018
   157
           | nf => nf $ Same.commit norm t)
wenzelm@32018
   158
          handle Same.SAME => f $ norm t)
wenzelm@32018
   159
      | norm _ = raise Same.SAME;
wenzelm@32018
   160
  in norm end;
clasohm@0
   161
wenzelm@32018
   162
fun norm_term2 asol iTs : term Same.operation =
wenzelm@32018
   163
  let
wenzelm@32018
   164
    val normT = norm_type0 iTs;
wenzelm@32018
   165
    fun norm (Const (a, T)) = Const (a, normT T)
wenzelm@32018
   166
      | norm (Free (a, T)) = Free (a, normT T)
wenzelm@32018
   167
      | norm (Var (xi, T)) =
wenzelm@32018
   168
          (case lookup2 (iTs, asol) (xi, T) of
wenzelm@32018
   169
            SOME u => Same.commit norm u
wenzelm@32018
   170
          | NONE => Var (xi, normT T))
wenzelm@32018
   171
      | norm (Abs (a, T, body)) =
wenzelm@32018
   172
          (Abs (a, normT T, Same.commit norm body)
wenzelm@32018
   173
            handle Same.SAME => Abs (a, T, norm body))
wenzelm@32018
   174
      | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
wenzelm@32018
   175
      | norm (f $ t) =
wenzelm@32018
   176
          ((case norm f of
wenzelm@32018
   177
             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
wenzelm@32018
   178
           | nf => nf $ Same.commit norm t)
wenzelm@32018
   179
          handle Same.SAME => f $ norm t)
wenzelm@32018
   180
      | norm _ = raise Same.SAME;
wenzelm@32018
   181
  in norm end;
berghofe@11513
   182
wenzelm@32018
   183
in
wenzelm@32018
   184
wenzelm@32018
   185
fun norm_type_same iTs T =
wenzelm@32018
   186
  if Vartab.is_empty iTs then raise Same.SAME
wenzelm@32018
   187
  else norm_type0 iTs T;
clasohm@0
   188
wenzelm@32018
   189
fun norm_types_same iTs Ts =
wenzelm@32018
   190
  if Vartab.is_empty iTs then raise Same.SAME
wenzelm@32018
   191
  else Same.map (norm_type0 iTs) Ts;
wenzelm@32018
   192
wenzelm@32018
   193
fun norm_type iTs T = norm_type_same iTs T handle Same.SAME => T;
berghofe@11513
   194
wenzelm@32018
   195
fun norm_term_same (Envir {asol, iTs, ...}) =
wenzelm@32018
   196
  if Vartab.is_empty iTs then norm_term1 asol
wenzelm@32018
   197
  else norm_term2 asol iTs;
wenzelm@10485
   198
wenzelm@32018
   199
fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
berghofe@25471
   200
fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
lcp@719
   201
wenzelm@32018
   202
end;
berghofe@11513
   203
berghofe@11513
   204
berghofe@12231
   205
(*Put a term into head normal form for unification.*)
berghofe@12231
   206
wenzelm@32018
   207
fun head_norm env =
berghofe@12231
   208
  let
wenzelm@32018
   209
    fun norm (Var v) =
wenzelm@32018
   210
        (case lookup (env, v) of
skalberg@15531
   211
          SOME u => head_norm env u
wenzelm@32018
   212
        | NONE => raise Same.SAME)
wenzelm@32018
   213
      | norm (Abs (a, T, body)) = Abs (a, T, norm body)
wenzelm@32018
   214
      | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
wenzelm@32018
   215
      | norm (f $ t) =
wenzelm@32018
   216
          (case norm f of
wenzelm@32018
   217
            Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
wenzelm@32018
   218
          | nf => nf $ t)
wenzelm@32018
   219
      | norm _ = raise Same.SAME;
wenzelm@32018
   220
  in Same.commit norm end;
berghofe@12231
   221
berghofe@12231
   222
wenzelm@18937
   223
(*Eta-contract a term (fully)*)
wenzelm@18937
   224
wenzelm@22174
   225
local
wenzelm@22174
   226
wenzelm@32018
   227
fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
wenzelm@22174
   228
  | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
wenzelm@32018
   229
  | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
wenzelm@32018
   230
  | decr _ _ = raise Same.SAME
wenzelm@32018
   231
and decrh lev t = (decr lev t handle Same.SAME => t);
wenzelm@20670
   232
wenzelm@22174
   233
fun eta (Abs (a, T, body)) =
wenzelm@22174
   234
    ((case eta body of
wenzelm@22174
   235
        body' as (f $ Bound 0) =>
wenzelm@22174
   236
          if loose_bvar1 (f, 0) then Abs (a, T, body')
wenzelm@22174
   237
          else decrh 0 f
wenzelm@32018
   238
     | body' => Abs (a, T, body')) handle Same.SAME =>
wenzelm@22174
   239
        (case body of
wenzelm@22174
   240
          f $ Bound 0 =>
wenzelm@32018
   241
            if loose_bvar1 (f, 0) then raise Same.SAME
wenzelm@22174
   242
            else decrh 0 f
wenzelm@32018
   243
        | _ => raise Same.SAME))
wenzelm@32018
   244
  | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
wenzelm@32018
   245
  | eta _ = raise Same.SAME;
wenzelm@22174
   246
wenzelm@22174
   247
in
wenzelm@22174
   248
wenzelm@22174
   249
fun eta_contract t =
wenzelm@32018
   250
  if Term.has_abs t then Same.commit eta t else t;
wenzelm@18937
   251
wenzelm@18937
   252
val beta_eta_contract = eta_contract o beta_norm;
wenzelm@18937
   253
wenzelm@22174
   254
end;
wenzelm@22174
   255
wenzelm@18937
   256
berghofe@12231
   257
(*finds type of term without checking that combinations are consistent
berghofe@12231
   258
  Ts holds types of bound variables*)
berghofe@12231
   259
fun fastype (Envir {iTs, ...}) =
berghofe@12231
   260
let val funerr = "fastype: expected function type";
berghofe@12231
   261
    fun fast Ts (f $ u) =
wenzelm@20670
   262
        (case fast Ts f of
wenzelm@20670
   263
           Type ("fun", [_, T]) => T
wenzelm@20670
   264
         | TVar ixnS =>
haftmann@26328
   265
                (case Type.lookup iTs ixnS of
wenzelm@20670
   266
                   SOME (Type ("fun", [_, T])) => T
wenzelm@20670
   267
                 | _ => raise TERM (funerr, [f $ u]))
wenzelm@20670
   268
         | _ => raise TERM (funerr, [f $ u]))
berghofe@12231
   269
      | fast Ts (Const (_, T)) = T
berghofe@12231
   270
      | fast Ts (Free (_, T)) = T
berghofe@12231
   271
      | fast Ts (Bound i) =
wenzelm@30146
   272
        (nth Ts i
wenzelm@20670
   273
         handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
wenzelm@20670
   274
      | fast Ts (Var (_, T)) = T
berghofe@12231
   275
      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
berghofe@12231
   276
in fast end;
berghofe@12231
   277
berghofe@15797
   278
berghofe@15797
   279
(*Substitute for type Vars in a type*)
berghofe@15797
   280
fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else
berghofe@15797
   281
  let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
berghofe@15797
   282
        | subst(T as TFree _) = T
berghofe@15797
   283
        | subst(T as TVar ixnS) =
haftmann@26328
   284
            (case Type.lookup iTs ixnS of NONE => T | SOME(U) => U)
berghofe@15797
   285
  in subst T end;
berghofe@15797
   286
berghofe@15797
   287
(*Substitute for type Vars in a term*)
wenzelm@20548
   288
val subst_TVars = map_types o typ_subst_TVars;
berghofe@15797
   289
berghofe@15797
   290
(*Substitute for Vars in a term *)
berghofe@15797
   291
fun subst_Vars itms t = if Vartab.is_empty itms then t else
wenzelm@18937
   292
  let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT))
berghofe@15797
   293
        | subst (Abs (a, T, t)) = Abs (a, T, subst t)
berghofe@15797
   294
        | subst (f $ t) = subst f $ subst t
berghofe@15797
   295
        | subst t = t
berghofe@15797
   296
  in subst t end;
berghofe@15797
   297
berghofe@15797
   298
(*Substitute for type/term Vars in a term *)
berghofe@16652
   299
fun subst_vars (iTs, itms) =
berghofe@15797
   300
  if Vartab.is_empty iTs then subst_Vars itms else
berghofe@15797
   301
  let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
berghofe@15797
   302
        | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
berghofe@16652
   303
        | subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of
berghofe@15797
   304
            NONE   => Var (ixn, typ_subst_TVars iTs T)
berghofe@15797
   305
          | SOME t => t)
berghofe@15797
   306
        | subst (b as Bound _) = b
berghofe@15797
   307
        | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
berghofe@15797
   308
        | subst (f $ t) = subst f $ subst t
berghofe@15797
   309
  in subst end;
berghofe@15797
   310
wenzelm@18937
   311
wenzelm@21795
   312
(* expand defined atoms -- with local beta reduction *)
wenzelm@18937
   313
wenzelm@19422
   314
fun expand_atom T (U, u) =
wenzelm@19422
   315
  subst_TVars (Type.raw_match (U, T) Vartab.empty) u
wenzelm@18937
   316
  handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
wenzelm@18937
   317
wenzelm@21795
   318
fun expand_term get =
wenzelm@21695
   319
  let
wenzelm@21695
   320
    fun expand tm =
wenzelm@21695
   321
      let
wenzelm@21695
   322
        val (head, args) = Term.strip_comb tm;
wenzelm@21695
   323
        val args' = map expand args;
wenzelm@21695
   324
        fun comb head' = Term.list_comb (head', args');
wenzelm@21695
   325
      in
wenzelm@21695
   326
        (case head of
wenzelm@21695
   327
          Abs (x, T, t) => comb (Abs (x, T, expand t))
wenzelm@21695
   328
        | _ =>
wenzelm@21795
   329
            (case get head of
wenzelm@21695
   330
              SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
wenzelm@21695
   331
            | NONE => comb head)
wenzelm@21695
   332
        | _ => comb head)
wenzelm@21695
   333
      end;
wenzelm@21695
   334
  in expand end;
wenzelm@21695
   335
wenzelm@21795
   336
fun expand_term_frees defs =
wenzelm@21795
   337
  let
wenzelm@21795
   338
    val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
wenzelm@21795
   339
    val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
wenzelm@21795
   340
  in expand_term get end;
wenzelm@21795
   341
clasohm@0
   342
end;