src/Pure/pattern.ML
changeset 12784 bab3b002cbbb
parent 12781 f76180d14819
child 12797 4de06a8f67ef
     1.1 --- a/src/Pure/pattern.ML	Wed Jan 16 23:17:44 2002 +0100
     1.2 +++ b/src/Pure/pattern.ML	Wed Jan 16 23:18:20 2002 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4 -(*  Title: 	pattern
     1.5 +(*  Title:      Pure/pattern.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Tobias Nipkow and Christine Heinzelmann, TU Muenchen
     1.8 -    Copyright   1993  TU Muenchen
     1.9 +    Author:     Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer
    1.10 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.11  
    1.12  Unification of Higher-Order Patterns.
    1.13  
    1.14 @@ -32,6 +32,7 @@
    1.15    val unify             : sg * env * (term * term)list -> env
    1.16    val first_order       : term -> bool
    1.17    val pattern           : term -> bool
    1.18 +  val rewrite_term      : type_sig -> (term * term) list -> term -> term
    1.19    exception Unif
    1.20    exception MATCH
    1.21    exception Pattern
    1.22 @@ -47,7 +48,7 @@
    1.23  exception Unif;
    1.24  exception Pattern;
    1.25  
    1.26 -fun occurs(F,t,env) = 
    1.27 +fun occurs(F,t,env) =
    1.28      let fun occ(Var(G,_))   = (case Envir.lookup(env,G) of
    1.29                                   Some(t) => occ t
    1.30                                 | None    => F=G)
    1.31 @@ -71,14 +72,14 @@
    1.32  
    1.33  fun mkabs (binders,is,t)  =
    1.34      let fun mk(i::is) = let val (x,T) = nth_elem(i,binders)
    1.35 -                        in Abs(x,T,mk is) end 
    1.36 +                        in Abs(x,T,mk is) end
    1.37            | mk []     = t
    1.38      in mk is end;
    1.39  
    1.40  val incr = mapbnd (fn i => i+1);
    1.41  
    1.42  fun ints_of []             = []
    1.43 -  | ints_of (Bound i ::bs) = 
    1.44 +  | ints_of (Bound i ::bs) =
    1.45        let val is = ints_of bs
    1.46        in if i mem_int is then raise Pattern else i::is end
    1.47    | ints_of _              = raise Pattern;
    1.48 @@ -155,8 +156,8 @@
    1.49  
    1.50  
    1.51  (* mk_ff_list(is,js) = [ length(is) - k | 1 <= k <= |is| and is[k] = js[k] ] *)
    1.52 -fun mk_ff_list(is,js) = 
    1.53 -    let fun mk([],[],_)        = [] 
    1.54 +fun mk_ff_list(is,js) =
    1.55 +    let fun mk([],[],_)        = []
    1.56            | mk(i::is,j::js, k) = if i=j then k :: mk(is,js,k-1)
    1.57                                          else mk(is,js,k-1)
    1.58            | mk _               = error"mk_ff_list"
    1.59 @@ -197,14 +198,14 @@
    1.60      | p => cases(binders,env,p)
    1.61  
    1.62  and cases(binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
    1.63 -       ((Var(F,Fty),ss),(Var(G,Gty),ts)) => 
    1.64 +       ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
    1.65           if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
    1.66                    else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
    1.67        | ((Var(F,_),ss),_)             => flexrigid(env,binders,F,ints_of' env ss,t)
    1.68        | (_,(Var(F,_),ts))             => flexrigid(env,binders,F,ints_of' env ts,s)
    1.69        | ((Const c,ss),(Const d,ts))   => rigidrigid(env,binders,c,d,ss,ts)
    1.70        | ((Free(f),ss),(Free(g),ts))   => rigidrigid(env,binders,f,g,ss,ts)
    1.71 -      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts) 
    1.72 +      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts)
    1.73        | ((Abs(_),_),_)                => raise Pattern
    1.74        | (_,(Abs(_),_))                => raise Pattern
    1.75        | _                             => raise Unif
    1.76 @@ -228,11 +229,11 @@
    1.77  (*Eta-contract a term (fully)*)
    1.78  
    1.79  (* copying: *)
    1.80 -fun eta_contract (Abs(a,T,body)) = 
    1.81 +fun eta_contract (Abs(a,T,body)) =
    1.82        (case  eta_contract body  of
    1.83 -        body' as (f $ Bound 0) => 
    1.84 -	  if loose_bvar1(f,0) then Abs(a,T,body')
    1.85 -	  else incr_boundvars ~1 f 
    1.86 +        body' as (f $ Bound 0) =>
    1.87 +          if loose_bvar1(f,0) then Abs(a,T,body')
    1.88 +          else incr_boundvars ~1 f
    1.89        | body' => Abs(a,T,body'))
    1.90    | eta_contract(f$t) = eta_contract f $ eta_contract t
    1.91    | eta_contract t = t;
    1.92 @@ -242,11 +243,11 @@
    1.93  (*Eta-contract a term from outside: just enough to reduce it to an atom
    1.94  DOESN'T QUITE WORK!
    1.95  *)
    1.96 -fun eta_contract_atom (t0 as Abs(a, T, body)) = 
    1.97 +fun eta_contract_atom (t0 as Abs(a, T, body)) =
    1.98        (case  eta_contract2 body  of
    1.99 -        body' as (f $ Bound 0) => 
   1.100 -	    if loose_bvar1(f,0) then Abs(a,T,body')
   1.101 -	    else eta_contract_atom (incr_boundvars ~1 f)
   1.102 +        body' as (f $ Bound 0) =>
   1.103 +            if loose_bvar1(f,0) then Abs(a,T,body')
   1.104 +            else eta_contract_atom (incr_boundvars ~1 f)
   1.105        | _ => t0)
   1.106    | eta_contract_atom t = t
   1.107  and eta_contract2 (f$t) = f $ eta_contract_atom t
   1.108 @@ -259,9 +260,9 @@
   1.109  and aconv_aux (Const(a,T), Const(b,U)) = a=b  andalso  T=U
   1.110    | aconv_aux (Free(a,T),  Free(b,U))  = a=b  andalso  T=U
   1.111    | aconv_aux (Var(v,T),   Var(w,U))   = eq_ix(v,w) andalso  T=U
   1.112 -  | aconv_aux (Bound i,	   Bound j)    = i=j
   1.113 +  | aconv_aux (Bound i,    Bound j)    = i=j
   1.114    | aconv_aux (Abs(_,T,t), Abs(_,U,u)) = (t aeconv u)  andalso  T=U
   1.115 -  | aconv_aux (f$t,	   g$u)        = (f aeconv g)  andalso (t aeconv u)
   1.116 +  | aconv_aux (f$t,        g$u)        = (f aeconv g)  andalso (t aeconv u)
   1.117    | aconv_aux _ =  false;
   1.118  
   1.119  
   1.120 @@ -283,18 +284,18 @@
   1.121    let
   1.122      fun mtch (instsp as (tyinsts,insts)) = fn
   1.123          (Var(ixn,T), t)  =>
   1.124 -	  if loose_bvar(t,0) then raise MATCH
   1.125 -	  else (case assoc_string_int(insts,ixn) of
   1.126 -		  None => (typ_match tsig (tyinsts, (T, fastype_of t)), 
   1.127 -			   (ixn,t)::insts)
   1.128 -		| Some u => if t aeconv u then instsp else raise MATCH)
   1.129 +          if loose_bvar(t,0) then raise MATCH
   1.130 +          else (case assoc_string_int(insts,ixn) of
   1.131 +                  None => (typ_match tsig (tyinsts, (T, fastype_of t)),
   1.132 +                           (ixn,t)::insts)
   1.133 +                | Some u => if t aeconv u then instsp else raise MATCH)
   1.134        | (Free (a,T), Free (b,U)) =>
   1.135 -	  if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
   1.136 +          if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
   1.137        | (Const (a,T), Const (b,U))  =>
   1.138 -	  if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
   1.139 +          if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
   1.140        | (Bound i, Bound j)  =>  if  i=j  then  instsp  else raise MATCH
   1.141        | (Abs(_,T,t), Abs(_,U,u))  =>
   1.142 -	  mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u)
   1.143 +          mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u)
   1.144        | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u)
   1.145        | (t, Abs(_,U,u))  =>  mtch instsp ((incr t)$(Bound 0), u)
   1.146        | _ => raise MATCH
   1.147 @@ -394,4 +395,48 @@
   1.148                      else forall pattern args
   1.149                   end;
   1.150  
   1.151 +
   1.152 +(* rewriting -- simple but fast *)
   1.153 +
   1.154 +fun rewrite_term tsig rules tm =
   1.155 +  let
   1.156 +    fun match_rew tm (tm1, tm2) =
   1.157 +      Some (subst_vars (match tsig (tm1, tm)) tm2) handle MATCH => None;
   1.158 +
   1.159 +    fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body))
   1.160 +      | rew tm = get_first (match_rew tm) rules;
   1.161 +
   1.162 +    fun rew0 (tm as Abs (_, _, tm' $ Bound 0)) =
   1.163 +          if loose_bvar1 (tm', 0) then rew tm
   1.164 +          else
   1.165 +            let val tm'' = incr_boundvars ~1 tm'
   1.166 +            in Some (if_none (rew tm'') tm'') end
   1.167 +      | rew0 tm = rew tm;
   1.168 +
   1.169 +    fun rew1 tm = (case rew2 tm of
   1.170 +          Some tm1 => (case rew0 tm1 of
   1.171 +              Some tm2 => Some (if_none (rew1 tm2) tm2)
   1.172 +            | None => Some tm1)
   1.173 +        | None => (case rew0 tm of
   1.174 +              Some tm1 => Some (if_none (rew1 tm1) tm1)
   1.175 +            | None => None))
   1.176 +
   1.177 +    and rew2 (tm1 $ tm2) = (case tm1 of
   1.178 +            Abs (_, _, body) =>
   1.179 +              let val tm' = subst_bound (tm2, body)
   1.180 +              in Some (if_none (rew2 tm') tm') end
   1.181 +          | _ => (case rew1 tm1 of
   1.182 +              Some tm1' => (case rew1 tm2 of
   1.183 +                  Some tm2' => Some (tm1' $ tm2')
   1.184 +                | None => Some (tm1' $ tm2))
   1.185 +            | None => (case rew1 tm2 of
   1.186 +                  Some tm2' => Some (tm1 $ tm2')
   1.187 +                | None => None)))
   1.188 +      | rew2 (Abs (x, T, tm)) = (case rew1 tm of
   1.189 +            Some tm' => Some (Abs (x, T, tm'))
   1.190 +          | None => None)
   1.191 +      | rew2 _ = None
   1.192 +
   1.193 +  in if_none (rew1 tm) tm end;
   1.194 +
   1.195  end;