Replaced devar by Envir.head_norm
authorberghofe
Mon Nov 19 17:34:02 2001 +0100 (2001-11-19)
changeset 12232ff75ed08b3fb
parent 12231 4a25f04bea61
child 12233 3348aa8061d1
Replaced devar by Envir.head_norm
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Mon Nov 19 17:32:49 2001 +0100
     1.2 +++ b/src/Pure/pattern.ML	Mon Nov 19 17:34:02 2001 +0100
     1.3 @@ -82,6 +82,8 @@
     1.4        in if i mem_int is then raise Pattern else i::is end
     1.5    | ints_of _              = raise Pattern;
     1.6  
     1.7 +fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts);
     1.8 +
     1.9  
    1.10  fun app (s,(i::is)) = app (s$Bound(i),is)
    1.11    | app (s,[])      = s;
    1.12 @@ -106,14 +108,6 @@
    1.13    in Envir.update((F,mkhnf(binders,is,G,js)),env') end;
    1.14  
    1.15  
    1.16 -fun devar env t = case strip_comb t of
    1.17 -        (Var(F,_),ys) =>
    1.18 -            (case Envir.lookup(env,F) of
    1.19 -               Some(t) => devar env (red t (ints_of  ys) []) 
    1.20 -             | None    => t)
    1.21 -      |  _            => t;
    1.22 -
    1.23 -
    1.24  (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
    1.25  fun mk_proj_list is =
    1.26      let fun mk(i::is,j) = if i >= 0 then j :: mk(is,j-1) else mk(is,j-1)
    1.27 @@ -122,7 +116,7 @@
    1.28  
    1.29  fun proj(s,env,binders,is) =
    1.30      let fun trans d i = if i<d then i else (idx is (i-d))+d;
    1.31 -        fun pr(s,env,d,binders) = (case devar env s of
    1.32 +        fun pr(s,env,d,binders) = (case Envir.head_norm env s of
    1.33                Abs(a,T,t) => let val (t',env') = pr(t,env,d+1,((a,T)::binders))
    1.34                              in (Abs(a,T,t'),env') end
    1.35              | t => (case strip_comb t of
    1.36 @@ -139,7 +133,7 @@
    1.37                                   in (list_comb(Bound j,ts'),env') end
    1.38                           end
    1.39                   | (Var(F as (a,_),Fty),ts) =>
    1.40 -                      let val js = ints_of ts;
    1.41 +                      let val js = ints_of' env ts;
    1.42                            val js' = map (trans d) js;
    1.43                            val ks = mk_proj_list js';
    1.44                            val ls = filter (fn i => i >= 0) js'
    1.45 @@ -193,7 +187,7 @@
    1.46         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.47         handle Type.TUNIFY => raise Unif;
    1.48  
    1.49 -fun unif binders (env,(s,t)) = case (devar env s,devar env t) of
    1.50 +fun unif binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
    1.51        (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
    1.52           let val name = if ns = "" then nt else ns
    1.53           in unif ((name,Ts)::binders) (env,(ts,tt)) end
    1.54 @@ -203,10 +197,10 @@
    1.55  
    1.56  and cases(binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
    1.57         ((Var(F,Fty),ss),(Var(G,Gty),ts)) => 
    1.58 -         if F = G then flexflex1(env,binders,F,Fty,ints_of ss,ints_of ts)
    1.59 -                  else flexflex2(env,binders,F,Fty,ints_of ss,G,Gty,ints_of ts)
    1.60 -      | ((Var(F,_),ss),_)             => flexrigid(env,binders,F,ints_of ss,t)
    1.61 -      | (_,(Var(F,_),ts))             => flexrigid(env,binders,F,ints_of ts,s)
    1.62 +         if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
    1.63 +                  else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
    1.64 +      | ((Var(F,_),ss),_)             => flexrigid(env,binders,F,ints_of' env ss,t)
    1.65 +      | (_,(Var(F,_),ts))             => flexrigid(env,binders,F,ints_of' env ts,s)
    1.66        | ((Const c,ss),(Const d,ts))   => rigidrigid(env,binders,c,d,ss,ts)
    1.67        | ((Free(f),ss),(Free(g),ts))   => rigidrigid(env,binders,f,g,ss,ts)
    1.68        | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts) 
    1.69 @@ -242,35 +236,6 @@
    1.70    | eta_contract(f$t) = eta_contract f $ eta_contract t
    1.71    | eta_contract t = t;
    1.72  
    1.73 -
    1.74 -(* sharing:
    1.75 -local
    1.76 -
    1.77 -fun eta(Abs(x,T,t)) =
    1.78 -     (case eta t of
    1.79 -        None => (case t of
    1.80 -                   f $ Bound 0 => if loose_bvar1(f,0)
    1.81 -                                  then None
    1.82 -                                  else Some(incr_boundvars ~1 f)
    1.83 -                 | _ => None)
    1.84 -      | Some(t') => (case t' of
    1.85 -                       f $ Bound 0 => if loose_bvar1(f,0)
    1.86 -                                      then Some(Abs(x,T,t'))
    1.87 -                                      else Some(incr_boundvars ~1 f)
    1.88 -                     | _ => Some(Abs(x,T,t'))))
    1.89 -  | eta(s$t) = (case (eta s,eta t) of
    1.90 -                  (None,   None)    => None
    1.91 -                | (None,   Some t') => Some(s  $ t')
    1.92 -                | (Some s',None)    => Some(s' $ t)
    1.93 -                | (Some s',Some t') => Some(s' $ t'))
    1.94 -  | eta _ = None
    1.95 -
    1.96 -in
    1.97 -
    1.98 -fun eta_contract t = case eta t of None => t | Some(t') => t';
    1.99 -
   1.100 -end; *)
   1.101 -
   1.102  (*Eta-contract a term from outside: just enough to reduce it to an atom
   1.103  DOESN'T QUITE WORK!
   1.104  *)