src/Pure/envir.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 2191 58383908f177
child 5289 41b949f3b8ac
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
     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   type 'a xolist
    16   exception ENVIR of string * indexname;
    17   datatype env = Envir of {asol: term xolist, iTs: typ xolist, maxidx: int}
    18   val alist_of		: env -> (indexname * term) list
    19   val alist_of_olist	: 'a xolist -> (indexname * 'a) list
    20   val empty		: int->env
    21   val is_empty		: env -> bool
    22   val above		: int * env -> bool
    23   val genvar		: string -> env * typ -> env * term
    24   val genvars		: string -> env * typ list -> env * term list
    25   val lookup		: env * indexname -> term option
    26   val norm_term		: env -> term -> term
    27   val null_olist	: 'a xolist
    28   val olist_of_alist	: (indexname * 'a) list -> 'a xolist
    29   val update		: (indexname * term) * env -> env
    30   val vupdate		: (indexname * term) * env -> env
    31 end;
    32 
    33 structure Envir : ENVIR =
    34 struct
    35 
    36 (*association lists with keys in ascending order, no repeated keys*)
    37 type 'a xolist = (indexname * 'a) list;
    38 
    39 
    40 exception ENVIR of string * indexname;
    41 
    42 (*look up key in ordered list*)
    43 fun xsearch ([], key) = None
    44   | xsearch (((keyi,xi)::pairs), key) =
    45       if xless(keyi,key) then xsearch (pairs, key)
    46       else if key=keyi then Some xi
    47       else None;
    48 
    49 (*insert pair in ordered list, reject if key already present*)
    50 fun xinsert_new (newpr as (key, x), al) =
    51   let fun insert [] = [newpr]
    52         | insert ((pair as (keyi,xi)) :: pairs) =
    53             if xless(keyi,key) then pair :: insert pairs
    54             else if key=keyi then
    55                 raise ENVIR("xinsert_new: already present",key)
    56             else newpr::pair::pairs
    57   in  (insert al)  end;
    58 
    59 (*insert pair in ordered list, overwrite if key already present*)
    60 fun xinsert (newpr as (key, x), al) =
    61   let fun insert [] = [newpr]
    62         | insert ((pair as (keyi,xi)) :: pairs) =
    63             if xless(keyi,key) then pair :: insert pairs
    64             else if key=keyi then newpr::pairs
    65             else newpr::pair::pairs
    66   in  (insert al)  end;
    67 
    68 (*apply function to the contents part of each pair*)
    69 fun xmap f (pairs) =
    70   let fun xmp [] = []
    71         | xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
    72   in (xmp pairs)  end;
    73 
    74 (*allows redefinition of a key by "join"ing the contents parts*)
    75 fun xmerge_olists join (pairsa, pairsb) =
    76   let fun xmrg ([],pairsb) = pairsb
    77         | xmrg (pairsa,[]) = pairsa
    78         | xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
    79             if xless(keya,keyb) then
    80                 (keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
    81             else if xless(keyb,keya) then
    82                 (keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
    83             else (*equal*)  (keya, join(x,y)) :: xmrg (pairsa, pairsb)
    84   in  (xmrg (pairsa,pairsb))  end;
    85 
    86 val null_olist = [];
    87 
    88 fun alist_of_olist (pairs) = pairs;
    89 
    90 fun olist_of_alist pairs = foldr xinsert (pairs, []);
    91 
    92 
    93 
    94 (*updating can destroy environment in 2 ways!!
    95    (1) variables out of range   (2) circular assignments
    96 *)
    97 datatype env = Envir of
    98     {maxidx: int,               (*maximum index of vars*)
    99      asol: term xolist,         (*table of assignments to Vars*)
   100      iTs:  typ  xolist}         (*table of assignments to TVars*)
   101 
   102 
   103 (*Generate a list of distinct variables.
   104   Increments index to make them distinct from ALL present variables. *)
   105 fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
   106   let fun genvs (_, [] : typ list) : term list = []
   107         | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
   108         | genvs (n, T::Ts) =
   109             Var((name ^ radixstring(26,"a",n), maxidx+1), T)
   110             :: genvs(n+1,Ts)
   111   in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
   112 
   113 (*Generate a variable.*)
   114 fun genvar name (env,T) : env * term =
   115   let val (env',[v]) = genvars name (env,[T])
   116   in  (env',v)  end;
   117 
   118 fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);
   119 
   120 fun update ((xname, t), Envir{maxidx, asol, iTs}) =
   121   Envir{maxidx=maxidx, asol=xinsert_new ((xname,t), asol), iTs=iTs};
   122 
   123 (*The empty environment.  New variables will start with the given index.*)
   124 fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};
   125 
   126 (*Test for empty environment*)
   127 fun is_empty (Envir {asol = [], iTs = [], ...}) = true
   128   | is_empty _ = false;
   129 
   130 (*Determine if the least index updated exceeds lim*)
   131 fun above (lim, Envir {asol, iTs, ...}) = 
   132     let fun upd [] = true
   133 	  | upd (i::is) = i>lim andalso upd is
   134     in  upd (map (#2 o #1) asol @ (map (#2 o #1) iTs))
   135     end;
   136 
   137 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
   138 fun vupdate((a,t), env) = case t of
   139       Var(name',T) =>
   140         if a=name' then env     (*cycle!*)
   141         else if xless(a, name')  then
   142            (case lookup(env,name') of  (*if already assigned, chase*)
   143                 None => update((name', Var(a,T)), env)
   144               | Some u => vupdate((a,u), env))
   145         else update((a,t), env)
   146     | _ => update((a,t), env);
   147 
   148 
   149 (*Convert environment to alist*)
   150 fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;
   151 
   152 
   153 (*** Beta normal form for terms (not eta normal form).
   154      Chases variables in env;  Does not exploit sharing of variable bindings
   155      Does not check types, so could loop. ***)
   156 
   157 (*raised when norm has no effect on a term, to do sharing instead of copying*)
   158 exception SAME;
   159 
   160 fun norm_term1 (asol,t) : term =
   161   let fun norm (Var (w,T)) =
   162 	    (case xsearch(asol,w) of
   163 		Some u => (norm u handle SAME => u)
   164 	      | None   => raise SAME)
   165 	| norm (Abs(a,T,body)) =  Abs(a, T, norm body)
   166 	| norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
   167 	| norm (f $ t) =
   168 	    ((case norm f of
   169 	       Abs(_,_,body) => normh(subst_bound (t, body))
   170 	     | nf => nf $ (norm t handle SAME => t))
   171 	    handle SAME => f $ norm t)
   172 	| norm _ =  raise SAME
   173       and normh t = norm t handle SAME => t
   174   in normh t end
   175 
   176 and norm_term2(asol,iTs,t) : term =
   177   let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
   178 	| normT(TFree _) = raise SAME
   179 	| normT(TVar(v,_)) = (case assoc(iTs,v) of
   180 		Some(U) => normTh U
   181 	      | None => raise SAME)
   182       and normTh T = ((normT T) handle SAME => T)
   183       and normTs([]) = raise SAME
   184 	| normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts))
   185 			   handle SAME => T :: normTs Ts)
   186       and norm(Const(a,T)) = Const(a, normT T)
   187 	| norm(Free(a,T)) = Free(a, normT T)
   188 	| norm(Var (w,T)) =
   189 	    (case xsearch(asol,w) of
   190 		Some u => normh u
   191 	      | None   => Var(w,normT T))
   192 	| norm(Abs(a,T,body)) =
   193 	      (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
   194 	| norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body))
   195 	| norm(f $ t) =
   196 	    ((case norm f of
   197 	       Abs(_,_,body) => normh(subst_bound (t, body))
   198 	     | nf => nf $ normh t)
   199 	    handle SAME => f $ norm t)
   200 	| norm _ =  raise SAME
   201       and normh t = (norm t) handle SAME => t
   202   in normh t end;
   203 
   204 (*curried version might be slower in recursive calls*)
   205 fun norm_term (env as Envir{asol,iTs,...}) t : term =
   206         if null iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
   207 
   208 end;
   209