src/Pure/envir.ML
author wenzelm
Wed Nov 28 00:46:26 2001 +0100 (2001-11-28)
changeset 12311 ce5f9e61c037
parent 12231 4a25f04bea61
child 12496 0a9bd5034e05
permissions -rw-r--r--
theory data: removed obsolete finish method;
     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.  They don't take account that typ is part of variable
     7 name.  Therefore we check elsewhere that two variables with same names
     8 and different types cannot occur.
     9 *)
    10 
    11 signature ENVIR =
    12 sig
    13   datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
    14   exception SAME
    15   val genvars: string -> env * typ list -> env * term list
    16   val genvar: string -> env * typ -> env * term
    17   val lookup: env * indexname -> term option
    18   val update: (indexname * term) * env -> env
    19   val empty: int -> env
    20   val is_empty: env -> bool
    21   val above: int * env -> bool
    22   val vupdate: (indexname * term) * env -> env
    23   val alist_of: env -> (indexname * term) list
    24   val norm_term: env -> term -> term
    25   val norm_term_same: env -> term -> term
    26   val norm_type: env -> typ -> typ
    27   val norm_type_same: env -> typ -> typ
    28   val norm_types_same: env -> typ list -> typ list
    29   val beta_norm: term -> term
    30   val head_norm: env -> term -> term
    31   val fastype: env -> typ list -> term -> typ
    32 end;
    33 
    34 structure Envir : ENVIR =
    35 struct
    36 
    37 (*updating can destroy environment in 2 ways!!
    38    (1) variables out of range   (2) circular assignments
    39 *)
    40 datatype env = Envir of
    41     {maxidx: int,               (*maximum index of vars*)
    42      asol: term Vartab.table,   (*table of assignments to Vars*)
    43      iTs: typ Vartab.table}     (*table of assignments to TVars*)
    44 
    45 
    46 (*Generate a list of distinct variables.
    47   Increments index to make them distinct from ALL present variables. *)
    48 fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
    49   let fun genvs (_, [] : typ list) : term list = []
    50         | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
    51         | genvs (n, T::Ts) =
    52             Var((name ^ radixstring(26,"a",n), maxidx+1), T)
    53             :: genvs(n+1,Ts)
    54   in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
    55 
    56 (*Generate a variable.*)
    57 fun genvar name (env,T) : env * term =
    58   let val (env',[v]) = genvars name (env,[T])
    59   in  (env',v)  end;
    60 
    61 fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
    62 
    63 fun update ((xname, t), Envir{maxidx, asol, iTs}) =
    64   Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
    65 
    66 (*The empty environment.  New variables will start with the given index+1.*)
    67 fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
    68 
    69 (*Test for empty environment*)
    70 fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
    71 
    72 (*Determine if the least index updated exceeds lim*)
    73 fun above (lim, Envir {asol, iTs, ...}) =
    74   (case (Vartab.min_key asol, Vartab.min_key iTs) of
    75      (None, None) => true
    76    | (Some (_, i), None) => i > lim
    77    | (None, Some (_, i')) => i' > lim
    78    | (Some (_, i), Some (_, i')) => i > lim andalso i' > lim);
    79 
    80 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
    81 fun vupdate((a,t), env) = case t of
    82       Var(name',T) =>
    83         if a=name' then env     (*cycle!*)
    84         else if xless(a, name')  then
    85            (case lookup(env,name') of  (*if already assigned, chase*)
    86                 None => update((name', Var(a,T)), env)
    87               | Some u => vupdate((a,u), env))
    88         else update((a,t), env)
    89     | _ => update((a,t), env);
    90 
    91 
    92 (*Convert environment to alist*)
    93 fun alist_of (Envir{asol,...}) = Vartab.dest asol;
    94 
    95 
    96 (*** Beta normal form for terms (not eta normal form).
    97      Chases variables in env;  Does not exploit sharing of variable bindings
    98      Does not check types, so could loop. ***)
    99 
   100 (*raised when norm has no effect on a term, to do sharing instead of copying*)
   101 exception SAME;
   102 
   103 fun norm_term1 same (asol,t) : term =
   104   let fun norm (Var (w,T)) =
   105             (case Vartab.lookup (asol, w) of
   106                 Some u => (norm u handle SAME => u)
   107               | None   => raise SAME)
   108         | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
   109         | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
   110         | norm (f $ t) =
   111             ((case norm f of
   112                Abs(_,_,body) => normh(subst_bound (t, body))
   113              | nf => nf $ (norm t handle SAME => t))
   114             handle SAME => f $ norm t)
   115         | norm _ =  raise SAME
   116       and normh t = norm t handle SAME => t
   117   in (if same then norm else normh) t end
   118 
   119 fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
   120   | normT iTs (TFree _) = raise SAME
   121   | normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of
   122           Some U => normTh iTs U
   123         | None => raise SAME)
   124 and normTh iTs T = ((normT iTs T) handle SAME => T)
   125 and normTs iTs [] = raise SAME
   126   | normTs iTs (T :: Ts) =
   127       ((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
   128        handle SAME => T :: normTs iTs Ts);
   129 
   130 fun norm_term2 same (asol, iTs, t) : term =
   131   let fun norm (Const (a, T)) = Const(a, normT iTs T)
   132         | norm (Free (a, T)) = Free(a, normT iTs T)
   133         | norm (Var (w, T)) =
   134             (case Vartab.lookup (asol, w) of
   135                 Some u => normh u
   136               | None   => Var(w, normT iTs T))
   137         | norm (Abs (a, T, body)) =
   138                (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
   139         | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
   140         | norm (f $ t) =
   141             ((case norm f of
   142                Abs(_, _, body) => normh (subst_bound (t, body))
   143              | nf => nf $ normh t)
   144             handle SAME => f $ norm t)
   145         | norm _ =  raise SAME
   146       and normh t = (norm t) handle SAME => t
   147   in (if same then norm else normh) t end;
   148 
   149 fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
   150   if Vartab.is_empty iTs then norm_term1 same (asol, t)
   151   else norm_term2 same (asol, iTs, t);
   152 
   153 val norm_term = gen_norm_term false;
   154 val norm_term_same = gen_norm_term true;
   155 
   156 val beta_norm = norm_term (empty 0);
   157 
   158 fun norm_type (Envir {iTs, ...}) = normTh iTs;
   159 fun norm_type_same (Envir {iTs, ...}) =
   160   if Vartab.is_empty iTs then raise SAME else normT iTs;
   161 
   162 fun norm_types_same (Envir {iTs, ...}) =
   163   if Vartab.is_empty iTs then raise SAME else normTs iTs;
   164 
   165 
   166 (*Put a term into head normal form for unification.*)
   167 
   168 fun head_norm env t =
   169   let
   170     fun hnorm (Var (v, T)) = (case lookup (env, v) of
   171           Some u => head_norm env u
   172         | None => raise SAME)
   173       | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
   174       | hnorm (Abs (_, _, body) $ t) =
   175           head_norm env (subst_bound (t, body))
   176       | hnorm (f $ t) = (case hnorm f of
   177           Abs (_, _, body) => head_norm env (subst_bound (t, body))
   178         | nf => nf $ t)
   179 	  | hnorm _ =  raise SAME
   180   in hnorm t handle SAME => t end;
   181 
   182 
   183 (*finds type of term without checking that combinations are consistent
   184   Ts holds types of bound variables*)
   185 fun fastype (Envir {iTs, ...}) =
   186 let val funerr = "fastype: expected function type";
   187     fun fast Ts (f $ u) =
   188 	(case fast Ts f of
   189 	   Type ("fun", [_, T]) => T
   190 	 | TVar(ixn, _) =>
   191 		(case Vartab.lookup (iTs, ixn) of
   192 		   Some (Type ("fun", [_, T])) => T
   193 		 | _ => raise TERM (funerr, [f $ u]))
   194 	 | _ => raise TERM (funerr, [f $ u]))
   195       | fast Ts (Const (_, T)) = T
   196       | fast Ts (Free (_, T)) = T
   197       | fast Ts (Bound i) =
   198 	(nth_elem (i, Ts)
   199   	 handle LIST _=> raise TERM ("fastype: Bound", [Bound i]))
   200       | fast Ts (Var (_, T)) = T 
   201       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
   202 in fast end;
   203 
   204 end;