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