src/Pure/pattern.ML
changeset 12784 bab3b002cbbb
parent 12781 f76180d14819
child 12797 4de06a8f67ef
--- a/src/Pure/pattern.ML	Wed Jan 16 23:17:44 2002 +0100
+++ b/src/Pure/pattern.ML	Wed Jan 16 23:18:20 2002 +0100
@@ -1,7 +1,7 @@
-(*  Title: 	pattern
+(*  Title:      Pure/pattern.ML
     ID:         $Id$
-    Author: 	Tobias Nipkow and Christine Heinzelmann, TU Muenchen
-    Copyright   1993  TU Muenchen
+    Author:     Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Unification of Higher-Order Patterns.
 
@@ -32,6 +32,7 @@
   val unify             : sg * env * (term * term)list -> env
   val first_order       : term -> bool
   val pattern           : term -> bool
+  val rewrite_term      : type_sig -> (term * term) list -> term -> term
   exception Unif
   exception MATCH
   exception Pattern
@@ -47,7 +48,7 @@
 exception Unif;
 exception Pattern;
 
-fun occurs(F,t,env) = 
+fun occurs(F,t,env) =
     let fun occ(Var(G,_))   = (case Envir.lookup(env,G) of
                                  Some(t) => occ t
                                | None    => F=G)
@@ -71,14 +72,14 @@
 
 fun mkabs (binders,is,t)  =
     let fun mk(i::is) = let val (x,T) = nth_elem(i,binders)
-                        in Abs(x,T,mk is) end 
+                        in Abs(x,T,mk is) end
           | mk []     = t
     in mk is end;
 
 val incr = mapbnd (fn i => i+1);
 
 fun ints_of []             = []
-  | ints_of (Bound i ::bs) = 
+  | ints_of (Bound i ::bs) =
       let val is = ints_of bs
       in if i mem_int is then raise Pattern else i::is end
   | ints_of _              = raise Pattern;
@@ -155,8 +156,8 @@
 
 
 (* mk_ff_list(is,js) = [ length(is) - k | 1 <= k <= |is| and is[k] = js[k] ] *)
-fun mk_ff_list(is,js) = 
-    let fun mk([],[],_)        = [] 
+fun mk_ff_list(is,js) =
+    let fun mk([],[],_)        = []
           | mk(i::is,j::js, k) = if i=j then k :: mk(is,js,k-1)
                                         else mk(is,js,k-1)
           | mk _               = error"mk_ff_list"
@@ -197,14 +198,14 @@
     | p => cases(binders,env,p)
 
 and cases(binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
-       ((Var(F,Fty),ss),(Var(G,Gty),ts)) => 
+       ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
          if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
                   else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
       | ((Var(F,_),ss),_)             => flexrigid(env,binders,F,ints_of' env ss,t)
       | (_,(Var(F,_),ts))             => flexrigid(env,binders,F,ints_of' env ts,s)
       | ((Const c,ss),(Const d,ts))   => rigidrigid(env,binders,c,d,ss,ts)
       | ((Free(f),ss),(Free(g),ts))   => rigidrigid(env,binders,f,g,ss,ts)
-      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts) 
+      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts)
       | ((Abs(_),_),_)                => raise Pattern
       | (_,(Abs(_),_))                => raise Pattern
       | _                             => raise Unif
@@ -228,11 +229,11 @@
 (*Eta-contract a term (fully)*)
 
 (* copying: *)
-fun eta_contract (Abs(a,T,body)) = 
+fun eta_contract (Abs(a,T,body)) =
       (case  eta_contract body  of
-        body' as (f $ Bound 0) => 
-	  if loose_bvar1(f,0) then Abs(a,T,body')
-	  else incr_boundvars ~1 f 
+        body' as (f $ Bound 0) =>
+          if loose_bvar1(f,0) then Abs(a,T,body')
+          else incr_boundvars ~1 f
       | body' => Abs(a,T,body'))
   | eta_contract(f$t) = eta_contract f $ eta_contract t
   | eta_contract t = t;
@@ -242,11 +243,11 @@
 (*Eta-contract a term from outside: just enough to reduce it to an atom
 DOESN'T QUITE WORK!
 *)
-fun eta_contract_atom (t0 as Abs(a, T, body)) = 
+fun eta_contract_atom (t0 as Abs(a, T, body)) =
       (case  eta_contract2 body  of
-        body' as (f $ Bound 0) => 
-	    if loose_bvar1(f,0) then Abs(a,T,body')
-	    else eta_contract_atom (incr_boundvars ~1 f)
+        body' as (f $ Bound 0) =>
+            if loose_bvar1(f,0) then Abs(a,T,body')
+            else eta_contract_atom (incr_boundvars ~1 f)
       | _ => t0)
   | eta_contract_atom t = t
 and eta_contract2 (f$t) = f $ eta_contract_atom t
@@ -259,9 +260,9 @@
 and aconv_aux (Const(a,T), Const(b,U)) = a=b  andalso  T=U
   | aconv_aux (Free(a,T),  Free(b,U))  = a=b  andalso  T=U
   | aconv_aux (Var(v,T),   Var(w,U))   = eq_ix(v,w) andalso  T=U
-  | aconv_aux (Bound i,	   Bound j)    = i=j
+  | aconv_aux (Bound i,    Bound j)    = i=j
   | aconv_aux (Abs(_,T,t), Abs(_,U,u)) = (t aeconv u)  andalso  T=U
-  | aconv_aux (f$t,	   g$u)        = (f aeconv g)  andalso (t aeconv u)
+  | aconv_aux (f$t,        g$u)        = (f aeconv g)  andalso (t aeconv u)
   | aconv_aux _ =  false;
 
 
@@ -283,18 +284,18 @@
   let
     fun mtch (instsp as (tyinsts,insts)) = fn
         (Var(ixn,T), t)  =>
-	  if loose_bvar(t,0) then raise MATCH
-	  else (case assoc_string_int(insts,ixn) of
-		  None => (typ_match tsig (tyinsts, (T, fastype_of t)), 
-			   (ixn,t)::insts)
-		| Some u => if t aeconv u then instsp else raise MATCH)
+          if loose_bvar(t,0) then raise MATCH
+          else (case assoc_string_int(insts,ixn) of
+                  None => (typ_match tsig (tyinsts, (T, fastype_of t)),
+                           (ixn,t)::insts)
+                | Some u => if t aeconv u then instsp else raise MATCH)
       | (Free (a,T), Free (b,U)) =>
-	  if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
+          if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
       | (Const (a,T), Const (b,U))  =>
-	  if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
+          if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
       | (Bound i, Bound j)  =>  if  i=j  then  instsp  else raise MATCH
       | (Abs(_,T,t), Abs(_,U,u))  =>
-	  mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u)
+          mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u)
       | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u)
       | (t, Abs(_,U,u))  =>  mtch instsp ((incr t)$(Bound 0), u)
       | _ => raise MATCH
@@ -394,4 +395,48 @@
                     else forall pattern args
                  end;
 
+
+(* rewriting -- simple but fast *)
+
+fun rewrite_term tsig rules tm =
+  let
+    fun match_rew tm (tm1, tm2) =
+      Some (subst_vars (match tsig (tm1, tm)) tm2) handle MATCH => None;
+
+    fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body))
+      | rew tm = get_first (match_rew tm) rules;
+
+    fun rew0 (tm as Abs (_, _, tm' $ Bound 0)) =
+          if loose_bvar1 (tm', 0) then rew tm
+          else
+            let val tm'' = incr_boundvars ~1 tm'
+            in Some (if_none (rew tm'') tm'') end
+      | rew0 tm = rew tm;
+
+    fun rew1 tm = (case rew2 tm of
+          Some tm1 => (case rew0 tm1 of
+              Some tm2 => Some (if_none (rew1 tm2) tm2)
+            | None => Some tm1)
+        | None => (case rew0 tm of
+              Some tm1 => Some (if_none (rew1 tm1) tm1)
+            | None => None))
+
+    and rew2 (tm1 $ tm2) = (case tm1 of
+            Abs (_, _, body) =>
+              let val tm' = subst_bound (tm2, body)
+              in Some (if_none (rew2 tm') tm') end
+          | _ => (case rew1 tm1 of
+              Some tm1' => (case rew1 tm2 of
+                  Some tm2' => Some (tm1' $ tm2')
+                | None => Some (tm1' $ tm2))
+            | None => (case rew1 tm2 of
+                  Some tm2' => Some (tm1 $ tm2')
+                | None => None)))
+      | rew2 (Abs (x, T, tm)) = (case rew1 tm of
+            Some tm' => Some (Abs (x, T, tm'))
+          | None => None)
+      | rew2 _ = None
+
+  in if_none (rew1 tm) tm end;
+
 end;