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