src/Pure/envir.ML
author berghofe
Fri Mar 10 14:58:25 2000 +0100 (2000-03-10)
changeset 8407 d522ad1809e9
parent 5289 41b949f3b8ac
child 10485 f1576723371f
permissions -rw-r--r--
Envir now uses Vartab instead of association lists.
     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 
     7 (*Environments.  They don't take account that typ is part of variable name.
     8                  Therefore we check elsewhere that  two variables with same
     9 		 names and different types cannot occur.
    10 *)
    11 
    12 
    13 signature ENVIR =
    14 sig
    15   datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
    16   val alist_of		: env -> (indexname * term) list
    17   val empty		: int->env
    18   val is_empty		: env -> bool
    19   val above		: int * env -> bool
    20   val genvar		: string -> env * typ -> env * term
    21   val genvars		: string -> env * typ list -> env * term list
    22   val lookup		: env * indexname -> term option
    23   val norm_term		: env -> term -> term
    24   val update		: (indexname * term) * env -> env
    25   val vupdate		: (indexname * term) * env -> env
    26 end;
    27 
    28 structure Envir : ENVIR =
    29 struct
    30 
    31 (*updating can destroy environment in 2 ways!!
    32    (1) variables out of range   (2) circular assignments
    33 *)
    34 datatype env = Envir of
    35     {maxidx: int,               (*maximum index of vars*)
    36      asol: term Vartab.table,   (*table of assignments to Vars*)
    37      iTs: typ Vartab.table}     (*table of assignments to TVars*)
    38 
    39 
    40 (*Generate a list of distinct variables.
    41   Increments index to make them distinct from ALL present variables. *)
    42 fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
    43   let fun genvs (_, [] : typ list) : term list = []
    44         | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
    45         | genvs (n, T::Ts) =
    46             Var((name ^ radixstring(26,"a",n), maxidx+1), T)
    47             :: genvs(n+1,Ts)
    48   in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
    49 
    50 (*Generate a variable.*)
    51 fun genvar name (env,T) : env * term =
    52   let val (env',[v]) = genvars name (env,[T])
    53   in  (env',v)  end;
    54 
    55 fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
    56 
    57 fun update ((xname, t), Envir{maxidx, asol, iTs}) =
    58   Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
    59 
    60 (*The empty environment.  New variables will start with the given index+1.*)
    61 fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
    62 
    63 (*Test for empty environment*)
    64 fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
    65 
    66 (*Determine if the least index updated exceeds lim*)
    67 fun above (lim, Envir {asol, iTs, ...}) =
    68   (case (Vartab.min_key asol, Vartab.min_key iTs) of
    69      (None, None) => true
    70    | (Some (_, i), None) => i > lim
    71    | (None, Some (_, i')) => i' > lim
    72    | (Some (_, i), Some (_, i')) => i > lim andalso i' > lim);
    73 
    74 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
    75 fun vupdate((a,t), env) = case t of
    76       Var(name',T) =>
    77         if a=name' then env     (*cycle!*)
    78         else if xless(a, name')  then
    79            (case lookup(env,name') of  (*if already assigned, chase*)
    80                 None => update((name', Var(a,T)), env)
    81               | Some u => vupdate((a,u), env))
    82         else update((a,t), env)
    83     | _ => update((a,t), env);
    84 
    85 
    86 (*Convert environment to alist*)
    87 fun alist_of (Envir{asol,...}) = Vartab.dest asol;
    88 
    89 
    90 (*** Beta normal form for terms (not eta normal form).
    91      Chases variables in env;  Does not exploit sharing of variable bindings
    92      Does not check types, so could loop. ***)
    93 
    94 (*raised when norm has no effect on a term, to do sharing instead of copying*)
    95 exception SAME;
    96 
    97 fun norm_term1 (asol,t) : term =
    98   let fun norm (Var (w,T)) =
    99 	    (case Vartab.lookup (asol, w) of
   100 		Some u => (norm u handle SAME => u)
   101 	      | None   => raise SAME)
   102 	| norm (Abs(a,T,body)) =  Abs(a, T, norm body)
   103 	| norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
   104 	| norm (f $ t) =
   105 	    ((case norm f of
   106 	       Abs(_,_,body) => normh(subst_bound (t, body))
   107 	     | nf => nf $ (norm t handle SAME => t))
   108 	    handle SAME => f $ norm t)
   109 	| norm _ =  raise SAME
   110       and normh t = norm t handle SAME => t
   111   in normh t end
   112 
   113 and norm_term2(asol,iTs,t) : term =
   114   let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
   115 	| normT(TFree _) = raise SAME
   116 	| normT(TVar(v,_)) = (case Vartab.lookup (iTs, v) of
   117 		Some(U) => normTh U
   118 	      | None => raise SAME)
   119       and normTh T = ((normT T) handle SAME => T)
   120       and normTs([]) = raise SAME
   121 	| normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts))
   122 			   handle SAME => T :: normTs Ts)
   123       and norm(Const(a,T)) = Const(a, normT T)
   124 	| norm(Free(a,T)) = Free(a, normT T)
   125 	| norm(Var (w,T)) =
   126 	    (case Vartab.lookup (asol, w) of
   127 		Some u => normh u
   128 	      | None   => Var(w,normT T))
   129 	| norm(Abs(a,T,body)) =
   130 	      (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
   131 	| norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body))
   132 	| norm(f $ t) =
   133 	    ((case norm f of
   134 	       Abs(_,_,body) => normh(subst_bound (t, body))
   135 	     | nf => nf $ normh t)
   136 	    handle SAME => f $ norm t)
   137 	| norm _ =  raise SAME
   138       and normh t = (norm t) handle SAME => t
   139   in normh t end;
   140 
   141 (*curried version might be slower in recursive calls*)
   142 fun norm_term (env as Envir{asol,iTs,...}) t : term =
   143         if Vartab.is_empty iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
   144 
   145 end;
   146