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