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