src/Pure/envir.ML
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15570 8d8c70b41bab
child 16652 4ecf94235ec7
permissions -rw-r--r--
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
wenzelm@247
     1
(*  Title:      Pure/envir.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@247
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1988  University of Cambridge
wenzelm@10485
     5
berghofe@15797
     6
Environments.  The type of a term variable / sort of a type variable is
berghofe@15797
     7
part of its name. The lookup function must apply type substitutions,
berghofe@15797
     8
since they may change the identity of a variable.
clasohm@0
     9
*)
clasohm@0
    10
wenzelm@247
    11
signature ENVIR =
clasohm@0
    12
sig
berghofe@15797
    13
  type tenv
berghofe@15797
    14
  datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
berghofe@15797
    15
  val type_env: env -> Type.tyenv
berghofe@11513
    16
  exception SAME
wenzelm@10485
    17
  val genvars: string -> env * typ list -> env * term list
wenzelm@10485
    18
  val genvar: string -> env * typ -> env * term
berghofe@15797
    19
  val lookup: env * (indexname * typ) -> term option
berghofe@15797
    20
  val lookup': (Type.tyenv * tenv) * (indexname * typ) -> term option
berghofe@15797
    21
  val update: ((indexname * typ) * term) * env -> env
wenzelm@10485
    22
  val empty: int -> env
wenzelm@10485
    23
  val is_empty: env -> bool
wenzelm@10485
    24
  val above: int * env -> bool
berghofe@15797
    25
  val vupdate: ((indexname * typ) * term) * env -> env
berghofe@15797
    26
  val alist_of: env -> (indexname * (typ * term)) list
wenzelm@10485
    27
  val norm_term: env -> term -> term
berghofe@11513
    28
  val norm_term_same: env -> term -> term
berghofe@15797
    29
  val norm_type: Type.tyenv -> typ -> typ
berghofe@15797
    30
  val norm_type_same: Type.tyenv -> typ -> typ
berghofe@15797
    31
  val norm_types_same: Type.tyenv -> typ list -> typ list
wenzelm@10485
    32
  val beta_norm: term -> term
berghofe@12231
    33
  val head_norm: env -> 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
clasohm@0
    39
end;
clasohm@0
    40
paulson@1500
    41
structure Envir : ENVIR =
clasohm@0
    42
struct
clasohm@0
    43
clasohm@0
    44
(*updating can destroy environment in 2 ways!!
clasohm@0
    45
   (1) variables out of range   (2) circular assignments
clasohm@0
    46
*)
berghofe@15797
    47
type tenv = (typ * term) Vartab.table
berghofe@15797
    48
clasohm@0
    49
datatype env = Envir of
berghofe@15797
    50
    {maxidx: int,      (*maximum index of vars*)
berghofe@15797
    51
     asol: tenv,       (*table of assignments to Vars*)
berghofe@15797
    52
     iTs: Type.tyenv}  (*table of assignments to TVars*)
clasohm@0
    53
wenzelm@12496
    54
fun type_env (Envir {iTs, ...}) = iTs;
clasohm@0
    55
clasohm@0
    56
(*Generate a list of distinct variables.
clasohm@0
    57
  Increments index to make them distinct from ALL present variables. *)
clasohm@0
    58
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
clasohm@0
    59
  let fun genvs (_, [] : typ list) : term list = []
clasohm@0
    60
        | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
clasohm@0
    61
        | genvs (n, T::Ts) =
wenzelm@247
    62
            Var((name ^ radixstring(26,"a",n), maxidx+1), T)
wenzelm@247
    63
            :: genvs(n+1,Ts)
clasohm@0
    64
  in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
clasohm@0
    65
clasohm@0
    66
(*Generate a variable.*)
clasohm@0
    67
fun genvar name (env,T) : env * term =
wenzelm@247
    68
  let val (env',[v]) = genvars name (env,[T])
clasohm@0
    69
  in  (env',v)  end;
clasohm@0
    70
berghofe@15797
    71
(* de-reference TVars. When dealing with environments produced by *)
berghofe@15797
    72
(* matching instead of unification, there is no need to chase     *)
berghofe@15797
    73
(* assigned TVars. In this case, set b to false.                  *)
berghofe@15797
    74
fun devar b iTs (T as TVar vT) = (case Type.lookup (iTs, vT) of
berghofe@15797
    75
      NONE => T
berghofe@15797
    76
    | SOME T' => if b then devar true iTs T' else T')
berghofe@15797
    77
  | devar b iTs T = T;
berghofe@15797
    78
berghofe@15797
    79
fun eq_type b iTs (T, T') =
berghofe@15797
    80
  (case (devar b iTs T, devar b iTs T') of
berghofe@15797
    81
     (Type (s, Ts), Type (s', Ts')) =>
berghofe@15797
    82
       s = s' andalso ListPair.all (eq_type b iTs) (Ts, Ts')
berghofe@15797
    83
   | (U, U') => U = U');
berghofe@15797
    84
berghofe@15797
    85
fun var_clash ixn T T' = raise TYPE ("Variable " ^
berghofe@15797
    86
  quote (Syntax.string_of_vname ixn) ^ " has two distinct types",
berghofe@15797
    87
  [T', T], []);
clasohm@0
    88
berghofe@15797
    89
fun gen_lookup f asol (xname, T) =
berghofe@15797
    90
  (case Vartab.lookup (asol, xname) of
berghofe@15797
    91
     NONE => NONE
berghofe@15797
    92
   | SOME (U, t) => if f (T, U) then SOME t
berghofe@15797
    93
       else var_clash xname T U);
berghofe@15797
    94
berghofe@15797
    95
(* version ignoring type substitutions *)
berghofe@15797
    96
fun lookup1 asol = gen_lookup op = asol;
berghofe@15797
    97
berghofe@15797
    98
fun gen_lookup2 b (iTs, asol) =
berghofe@15797
    99
  if Vartab.is_empty iTs then lookup1 asol
berghofe@15797
   100
  else gen_lookup (eq_type b iTs) asol;
berghofe@15797
   101
berghofe@15797
   102
fun lookup2 env = gen_lookup2 true env;
berghofe@15797
   103
berghofe@15797
   104
fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
berghofe@15797
   105
berghofe@15797
   106
(* version for matching algorithms, does not chase TVars *)
berghofe@15797
   107
fun lookup' (env, p) = gen_lookup2 false env p;
berghofe@15797
   108
berghofe@15797
   109
fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
berghofe@15797
   110
  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname, (T, t)), asol), iTs=iTs};
clasohm@0
   111
wenzelm@5289
   112
(*The empty environment.  New variables will start with the given index+1.*)
berghofe@8407
   113
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
clasohm@0
   114
paulson@2142
   115
(*Test for empty environment*)
berghofe@8407
   116
fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
wenzelm@247
   117
paulson@2142
   118
(*Determine if the least index updated exceeds lim*)
berghofe@8407
   119
fun above (lim, Envir {asol, iTs, ...}) =
berghofe@8407
   120
  (case (Vartab.min_key asol, Vartab.min_key iTs) of
skalberg@15531
   121
     (NONE, NONE) => true
skalberg@15531
   122
   | (SOME (_, i), NONE) => i > lim
skalberg@15531
   123
   | (NONE, SOME (_, i')) => i' > lim
skalberg@15531
   124
   | (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim);
wenzelm@247
   125
clasohm@0
   126
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
berghofe@15797
   127
fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
berghofe@15797
   128
      Var (nT as (name', T)) =>
berghofe@15797
   129
        if a = name' then env     (*cycle!*)
wenzelm@247
   130
        else if xless(a, name')  then
berghofe@15797
   131
           (case lookup (env, nT) of  (*if already assigned, chase*)
berghofe@15797
   132
                NONE => update ((nT, Var (a, T)), env)
berghofe@15797
   133
              | SOME u => vupdate ((aU, u), env))
berghofe@15797
   134
        else update ((aU, t), env)
berghofe@15797
   135
    | _ => update ((aU, t), env);
clasohm@0
   136
clasohm@0
   137
clasohm@0
   138
(*Convert environment to alist*)
berghofe@8407
   139
fun alist_of (Envir{asol,...}) = Vartab.dest asol;
clasohm@0
   140
clasohm@0
   141
paulson@1500
   142
(*** Beta normal form for terms (not eta normal form).
paulson@1500
   143
     Chases variables in env;  Does not exploit sharing of variable bindings
paulson@1500
   144
     Does not check types, so could loop. ***)
paulson@1500
   145
paulson@1500
   146
(*raised when norm has no effect on a term, to do sharing instead of copying*)
paulson@1500
   147
exception SAME;
clasohm@0
   148
berghofe@11513
   149
fun norm_term1 same (asol,t) : term =
berghofe@15797
   150
  let fun norm (Var wT) =
berghofe@15797
   151
            (case lookup1 asol wT of
skalberg@15531
   152
                SOME u => (norm u handle SAME => u)
skalberg@15531
   153
              | NONE   => raise SAME)
wenzelm@10485
   154
        | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
wenzelm@10485
   155
        | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
wenzelm@10485
   156
        | norm (f $ t) =
wenzelm@10485
   157
            ((case norm f of
wenzelm@10485
   158
               Abs(_,_,body) => normh(subst_bound (t, body))
wenzelm@10485
   159
             | nf => nf $ (norm t handle SAME => t))
wenzelm@10485
   160
            handle SAME => f $ norm t)
wenzelm@10485
   161
        | norm _ =  raise SAME
paulson@2191
   162
      and normh t = norm t handle SAME => t
berghofe@11513
   163
  in (if same then norm else normh) t end
clasohm@0
   164
berghofe@11513
   165
fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
berghofe@11513
   166
  | normT iTs (TFree _) = raise SAME
berghofe@15797
   167
  | normT iTs (TVar vS) = (case Type.lookup (iTs, vS) of
skalberg@15531
   168
          SOME U => normTh iTs U
skalberg@15531
   169
        | NONE => raise SAME)
berghofe@11513
   170
and normTh iTs T = ((normT iTs T) handle SAME => T)
berghofe@11513
   171
and normTs iTs [] = raise SAME
berghofe@11513
   172
  | normTs iTs (T :: Ts) =
berghofe@11513
   173
      ((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
berghofe@11513
   174
       handle SAME => T :: normTs iTs Ts);
berghofe@11513
   175
berghofe@11513
   176
fun norm_term2 same (asol, iTs, t) : term =
berghofe@11513
   177
  let fun norm (Const (a, T)) = Const(a, normT iTs T)
berghofe@11513
   178
        | norm (Free (a, T)) = Free(a, normT iTs T)
berghofe@11513
   179
        | norm (Var (w, T)) =
berghofe@15797
   180
            (case lookup2 (iTs, asol) (w, T) of
skalberg@15531
   181
                SOME u => normh u
skalberg@15531
   182
              | NONE   => Var(w, normT iTs T))
berghofe@11513
   183
        | norm (Abs (a, T, body)) =
berghofe@11513
   184
               (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
berghofe@11513
   185
        | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
berghofe@11513
   186
        | norm (f $ t) =
wenzelm@10485
   187
            ((case norm f of
berghofe@11513
   188
               Abs(_, _, body) => normh (subst_bound (t, body))
wenzelm@10485
   189
             | nf => nf $ normh t)
wenzelm@10485
   190
            handle SAME => f $ norm t)
wenzelm@10485
   191
        | norm _ =  raise SAME
paulson@1500
   192
      and normh t = (norm t) handle SAME => t
berghofe@11513
   193
  in (if same then norm else normh) t end;
clasohm@0
   194
berghofe@11513
   195
fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
berghofe@11513
   196
  if Vartab.is_empty iTs then norm_term1 same (asol, t)
berghofe@11513
   197
  else norm_term2 same (asol, iTs, t);
berghofe@11513
   198
berghofe@11513
   199
val norm_term = gen_norm_term false;
berghofe@11513
   200
val norm_term_same = gen_norm_term true;
wenzelm@10485
   201
wenzelm@10485
   202
val beta_norm = norm_term (empty 0);
lcp@719
   203
wenzelm@12496
   204
fun norm_type iTs = normTh iTs;
wenzelm@12496
   205
fun norm_type_same iTs =
berghofe@11513
   206
  if Vartab.is_empty iTs then raise SAME else normT iTs;
berghofe@11513
   207
wenzelm@12496
   208
fun norm_types_same iTs =
berghofe@11513
   209
  if Vartab.is_empty iTs then raise SAME else normTs iTs;
berghofe@11513
   210
berghofe@11513
   211
berghofe@12231
   212
(*Put a term into head normal form for unification.*)
berghofe@12231
   213
berghofe@12231
   214
fun head_norm env t =
berghofe@12231
   215
  let
berghofe@15797
   216
    fun hnorm (Var vT) = (case lookup (env, vT) of
skalberg@15531
   217
          SOME u => head_norm env u
skalberg@15531
   218
        | NONE => raise SAME)
berghofe@12231
   219
      | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
berghofe@12231
   220
      | hnorm (Abs (_, _, body) $ t) =
berghofe@12231
   221
          head_norm env (subst_bound (t, body))
berghofe@12231
   222
      | hnorm (f $ t) = (case hnorm f of
berghofe@12231
   223
          Abs (_, _, body) => head_norm env (subst_bound (t, body))
berghofe@12231
   224
        | nf => nf $ t)
berghofe@12231
   225
	  | hnorm _ =  raise SAME
berghofe@12231
   226
  in hnorm t handle SAME => t end;
berghofe@12231
   227
berghofe@12231
   228
berghofe@12231
   229
(*finds type of term without checking that combinations are consistent
berghofe@12231
   230
  Ts holds types of bound variables*)
berghofe@12231
   231
fun fastype (Envir {iTs, ...}) =
berghofe@12231
   232
let val funerr = "fastype: expected function type";
berghofe@12231
   233
    fun fast Ts (f $ u) =
berghofe@12231
   234
	(case fast Ts f of
berghofe@12231
   235
	   Type ("fun", [_, T]) => T
berghofe@15797
   236
	 | TVar ixnS =>
berghofe@15797
   237
		(case Type.lookup (iTs, ixnS) of
skalberg@15531
   238
		   SOME (Type ("fun", [_, T])) => T
berghofe@12231
   239
		 | _ => raise TERM (funerr, [f $ u]))
berghofe@12231
   240
	 | _ => raise TERM (funerr, [f $ u]))
berghofe@12231
   241
      | fast Ts (Const (_, T)) = T
berghofe@12231
   242
      | fast Ts (Free (_, T)) = T
berghofe@12231
   243
      | fast Ts (Bound i) =
skalberg@15570
   244
	(List.nth (Ts, i)
skalberg@15570
   245
  	 handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
berghofe@12231
   246
      | fast Ts (Var (_, T)) = T 
berghofe@12231
   247
      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
berghofe@12231
   248
in fast end;
berghofe@12231
   249
berghofe@15797
   250
berghofe@15797
   251
(*Substitute for type Vars in a type*)
berghofe@15797
   252
fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else
berghofe@15797
   253
  let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
berghofe@15797
   254
        | subst(T as TFree _) = T
berghofe@15797
   255
        | subst(T as TVar ixnS) =
berghofe@15797
   256
            (case Type.lookup (iTs, ixnS) of NONE => T | SOME(U) => U)
berghofe@15797
   257
  in subst T end;
berghofe@15797
   258
berghofe@15797
   259
(*Substitute for type Vars in a term*)
berghofe@15797
   260
val subst_TVars = map_term_types o typ_subst_TVars;
berghofe@15797
   261
berghofe@15797
   262
(*Substitute for Vars in a term *)
berghofe@15797
   263
fun subst_Vars itms t = if Vartab.is_empty itms then t else
berghofe@15797
   264
  let fun subst (v as Var ixnT) = getOpt (lookup1 itms ixnT, v)
berghofe@15797
   265
        | subst (Abs (a, T, t)) = Abs (a, T, subst t)
berghofe@15797
   266
        | subst (f $ t) = subst f $ subst t
berghofe@15797
   267
        | subst t = t
berghofe@15797
   268
  in subst t end;
berghofe@15797
   269
berghofe@15797
   270
(*Substitute for type/term Vars in a term *)
berghofe@15797
   271
fun subst_vars (env as (iTs, itms)) =
berghofe@15797
   272
  if Vartab.is_empty iTs then subst_Vars itms else
berghofe@15797
   273
  let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
berghofe@15797
   274
        | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
berghofe@15797
   275
        | subst (Var (ixn, T)) = (case lookup' (env, (ixn, T)) of
berghofe@15797
   276
            NONE   => Var (ixn, typ_subst_TVars iTs T)
berghofe@15797
   277
          | SOME t => t)
berghofe@15797
   278
        | subst (b as Bound _) = b
berghofe@15797
   279
        | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
berghofe@15797
   280
        | subst (f $ t) = subst f $ subst t
berghofe@15797
   281
  in subst end;
berghofe@15797
   282
clasohm@0
   283
end;