Tried to speed up the rewriter by eta-contracting all patterns beforehand and
authornipkow
Wed Apr 22 14:04:35 1998 +0200 (1998-04-22)
changeset 48208f6dbbd8d497
parent 4819 ef2e8e2a10e1
child 4821 bfbaea156f43
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
by classifying each pattern as to whether it allows first-order matching.
src/Pure/pattern.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/pattern.ML	Tue Apr 21 17:25:19 1998 +0200
     1.2 +++ b/src/Pure/pattern.ML	Wed Apr 22 14:04:35 1998 +0200
     1.3 @@ -24,9 +24,13 @@
     1.4    val eta_contract_atom : term -> term
     1.5    val match             : type_sig -> term * term
     1.6                            -> (indexname*typ)list * (indexname*term)list
     1.7 +  val first_order_match : type_sig -> term * term
     1.8 +                          -> (indexname*typ)list * (indexname*term)list
     1.9    val matches           : type_sig -> term * term -> bool
    1.10    val matches_subterm   : type_sig -> term * term -> bool
    1.11    val unify             : sg * env * (term * term)list -> env
    1.12 +  val first_order       : term -> bool
    1.13 +  val pattern           : term -> bool
    1.14    exception Unif
    1.15    exception MATCH
    1.16    exception Pattern
    1.17 @@ -279,48 +283,6 @@
    1.18    | eta_contract2 t     = eta_contract_atom t;
    1.19  
    1.20  
    1.21 -(* Pattern matching *)
    1.22 -exception MATCH;
    1.23 -
    1.24 -(*First-order matching;  term_match tsig (pattern, object)
    1.25 -    returns a (tyvar,typ)list and (var,term)list.
    1.26 -  The pattern and object may have variables in common.
    1.27 -  Instantiation does not affect the object, so matching ?a with ?a+1 works.
    1.28 -  A Const does not match a Free of the same name! *)
    1.29 -fun fomatch tsig (pat,obj) =
    1.30 -  let fun typ_match args = (Type.typ_match tsig args)
    1.31 -			   handle Type.TYPE_MATCH => raise MATCH;
    1.32 -      fun mtch (tyinsts,insts) = fn
    1.33 -	(Var(ixn,T), t)  =>
    1.34 -	  if loose_bvar(t,0) then raise MATCH
    1.35 -	  else (case assoc_string_int(insts,ixn) of
    1.36 -		  None => (typ_match (tyinsts, (T, fastype_of t)), 
    1.37 -			   (ixn,t)::insts)
    1.38 -		| Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
    1.39 -      | (Free (a,T), Free (b,U)) =>
    1.40 -	  if  a=b  then (typ_match (tyinsts,(T,U)), insts)  else raise MATCH
    1.41 -      | (Const (a,T), Const (b,U))  =>
    1.42 -	  if  a=b  then (typ_match (tyinsts,(T,U)), insts)  else raise MATCH
    1.43 -      | (Bound i, Bound j)  =>
    1.44 -          if  i=j  then  (tyinsts,insts)  else raise MATCH
    1.45 -      | (Abs(_,T,t), Abs(_,U,u))  =>
    1.46 -	  mtch (typ_match (tyinsts,(T,U)),insts) (t,u)
    1.47 -      | (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u)
    1.48 -      | _ => raise MATCH
    1.49 -  in mtch([],[]) (eta_contract pat, eta_contract obj) end;
    1.50 -
    1.51 -
    1.52 -fun match_bind(itms,binders,ixn,is,t) =
    1.53 -  let val js = loose_bnos t
    1.54 -  in if null is
    1.55 -     then if null js then (ixn,t)::itms else raise MATCH
    1.56 -     else if js subset_int is
    1.57 -          then let val t' = if downto0(is,length binders - 1) then t
    1.58 -                            else mapbnd (idx is) t
    1.59 -               in (ixn, mkabs(binders,is,t')) :: itms end
    1.60 -          else raise MATCH
    1.61 -  end;
    1.62 -
    1.63  (*Tests whether 2 terms are alpha/eta-convertible and have same type.
    1.64    Note that Consts and Vars may have more than one type.*)
    1.65  fun t aeconv u = aconv_aux (eta_contract_atom t, eta_contract_atom u)
    1.66 @@ -333,59 +295,106 @@
    1.67    | aconv_aux _ =  false;
    1.68  
    1.69  
    1.70 +(*** Matching ***)
    1.71 +
    1.72 +exception MATCH;
    1.73 +
    1.74 +fun typ_match tsig args = (Type.typ_match tsig args)
    1.75 +                          handle Type.TYPE_MATCH => raise MATCH;
    1.76 +
    1.77 +(*First-order matching;
    1.78 +  fomatch tsig (pattern, object) returns a (tyvar,typ)list and (var,term)list.
    1.79 +  The pattern and object may have variables in common.
    1.80 +  Instantiation does not affect the object, so matching ?a with ?a+1 works.
    1.81 +  Object is eta-contracted on the fly (by eta-expanding the pattern).
    1.82 +  Precondition: the pattern is already eta-contracted!
    1.83 +  Note: types are matched on the fly *)
    1.84 +fun fomatch tsig =
    1.85 +  let
    1.86 +    fun mtch (instsp as (tyinsts,insts)) = fn
    1.87 +        (Var(ixn,T), t)  =>
    1.88 +	  if loose_bvar(t,0) then raise MATCH
    1.89 +	  else (case assoc_string_int(insts,ixn) of
    1.90 +		  None => (typ_match tsig (tyinsts, (T, fastype_of t)), 
    1.91 +			   (ixn,t)::insts)
    1.92 +		| Some u => if t aeconv u then instsp else raise MATCH)
    1.93 +      | (Free (a,T), Free (b,U)) =>
    1.94 +	  if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
    1.95 +      | (Const (a,T), Const (b,U))  =>
    1.96 +	  if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
    1.97 +      | (Bound i, Bound j)  =>  if  i=j  then  instsp  else raise MATCH
    1.98 +      | (Abs(_,T,t), Abs(_,U,u))  =>
    1.99 +	  mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u)
   1.100 +      | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u)
   1.101 +      | (t, Abs(_,U,u))  =>  mtch instsp ((incr t)$(Bound 0), u)
   1.102 +      | _ => raise MATCH
   1.103 +  in mtch end;
   1.104 +
   1.105 +fun first_order_match tsig = fomatch tsig ([],[]);
   1.106 + 
   1.107 +(* Matching of higher-order patterns *)
   1.108 +
   1.109 +fun match_bind(itms,binders,ixn,is,t) =
   1.110 +  let val js = loose_bnos t
   1.111 +  in if null is
   1.112 +     then if null js then (ixn,t)::itms else raise MATCH
   1.113 +     else if js subset_int is
   1.114 +          then let val t' = if downto0(is,length binders - 1) then t
   1.115 +                            else mapbnd (idx is) t
   1.116 +               in (ixn, mkabs(binders,is,t')) :: itms end
   1.117 +          else raise MATCH
   1.118 +  end;
   1.119 +
   1.120  fun match tsg (po as (pat,obj)) =
   1.121  let
   1.122 -
   1.123 -fun typ_match args = Type.typ_match tsg args
   1.124 -                     handle Type.TYPE_MATCH => raise MATCH;
   1.125 -
   1.126 -(* Pre: pat and obj have same type *)
   1.127 -fun mtch binders (env as (iTs,itms),(pat,obj)) =
   1.128 -      case pat of
   1.129 -        Abs(ns,Ts,ts) =>
   1.130 -          (case obj of
   1.131 -             Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
   1.132 -           | _ => let val Tt = typ_subst_TVars iTs Ts
   1.133 -                  in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
   1.134 -      | _ => (case obj of
   1.135 -                Abs(nt,Tt,tt) =>
   1.136 -                  mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt))
   1.137 -              | _ => cases(binders,env,pat,obj))
   1.138 +  (* Pre: pat and obj have same type *)
   1.139 +  fun mtch binders (env as (iTs,itms),(pat,obj)) =
   1.140 +    case pat of
   1.141 +      Abs(ns,Ts,ts) =>
   1.142 +        (case obj of
   1.143 +           Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
   1.144 +         | _ => let val Tt = typ_subst_TVars iTs Ts
   1.145 +                in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
   1.146 +    | _ => (case obj of
   1.147 +              Abs(nt,Tt,tt) =>
   1.148 +                mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt))
   1.149 +            | _ => cases(binders,env,pat,obj))
   1.150  
   1.151 -and cases(binders,env as (iTs,itms),pat,obj) =
   1.152 -      let val (ph,pargs) = strip_comb pat
   1.153 -          fun rigrig1(iTs,oargs) =
   1.154 -                foldl (mtch binders) ((iTs,itms), pargs~~oargs)
   1.155 -          fun rigrig2((a,Ta),(b,Tb),oargs) =
   1.156 -                if a<> b then raise MATCH
   1.157 -                else rigrig1(typ_match(iTs,(Ta,Tb)), oargs)
   1.158 -      in case ph of
   1.159 -           Var(ixn,_) =>
   1.160 -             let val is = ints_of pargs
   1.161 -             in case assoc_string_int(itms,ixn) of
   1.162 -                  None => (iTs,match_bind(itms,binders,ixn,is,obj))
   1.163 -                | Some u => if obj aeconv (red u is []) then env
   1.164 -                            else raise MATCH
   1.165 -             end
   1.166 -         | _ =>
   1.167 -             let val (oh,oargs) = strip_comb obj
   1.168 -             in case (ph,oh) of
   1.169 -                  (Const c,Const d) => rigrig2(c,d,oargs)
   1.170 -                | (Free f,Free g)   => rigrig2(f,g,oargs)
   1.171 -                | (Bound i,Bound j) => if i<>j then raise MATCH
   1.172 -                                       else rigrig1(iTs,oargs)
   1.173 -                | (Abs _, _)        => raise Pattern
   1.174 -                | (_, Abs _)        => raise Pattern
   1.175 -                | _                 => raise MATCH
   1.176 -             end
   1.177 -      end;
   1.178 +  and cases(binders,env as (iTs,itms),pat,obj) =
   1.179 +    let val (ph,pargs) = strip_comb pat
   1.180 +        fun rigrig1(iTs,oargs) =
   1.181 +              foldl (mtch binders) ((iTs,itms), pargs~~oargs)
   1.182 +        fun rigrig2((a,Ta),(b,Tb),oargs) =
   1.183 +              if a<> b then raise MATCH
   1.184 +              else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
   1.185 +    in case ph of
   1.186 +         Var(ixn,_) =>
   1.187 +           let val is = ints_of pargs
   1.188 +           in case assoc_string_int(itms,ixn) of
   1.189 +                None => (iTs,match_bind(itms,binders,ixn,is,obj))
   1.190 +              | Some u => if obj aeconv (red u is []) then env
   1.191 +                          else raise MATCH
   1.192 +           end
   1.193 +       | _ =>
   1.194 +           let val (oh,oargs) = strip_comb obj
   1.195 +           in case (ph,oh) of
   1.196 +                (Const c,Const d) => rigrig2(c,d,oargs)
   1.197 +              | (Free f,Free g)   => rigrig2(f,g,oargs)
   1.198 +              | (Bound i,Bound j) => if i<>j then raise MATCH
   1.199 +                                     else rigrig1(iTs,oargs)
   1.200 +              | (Abs _, _)        => raise Pattern
   1.201 +              | (_, Abs _)        => raise Pattern
   1.202 +              | _                 => raise MATCH
   1.203 +           end
   1.204 +    end;
   1.205  
   1.206 -val pT = fastype_of pat
   1.207 -and oT = fastype_of obj
   1.208 -val iTs = typ_match ([],(pT,oT))
   1.209 +  val pT = fastype_of pat
   1.210 +  and oT = fastype_of obj
   1.211 +  val iTs = typ_match tsg ([],(pT,oT))
   1.212 +  val insts2 = (iTs,[])
   1.213  
   1.214 -in mtch [] ((iTs,[]), po)
   1.215 -   handle Pattern => fomatch tsg po
   1.216 +in mtch [] (insts2, po)
   1.217 +   handle Pattern => fomatch tsg insts2 po
   1.218  end;
   1.219  
   1.220  (*Predicate: does the pattern match the object?*)
   1.221 @@ -402,4 +411,17 @@
   1.222              | _ => false
   1.223    in msub([],obj) end;
   1.224  
   1.225 +fun first_order(Abs(_,_,t)) = first_order t
   1.226 +  | first_order(t $ u) = first_order t andalso first_order u andalso
   1.227 +                         not(is_Var t)
   1.228 +  | first_order _ = true;
   1.229 +
   1.230 +fun pattern(Abs(_,_,t)) = pattern t
   1.231 +  | pattern(t) = let val (head,args) = strip_comb t
   1.232 +                 in if is_Var head
   1.233 +                    then let val _ = ints_of args in true end
   1.234 +                         handle Pattern => false
   1.235 +                    else forall pattern args
   1.236 +                 end;
   1.237 +
   1.238  end;
     2.1 --- a/src/Pure/thm.ML	Tue Apr 21 17:25:19 1998 +0200
     2.2 +++ b/src/Pure/thm.ML	Wed Apr 22 14:04:35 1998 +0200
     2.3 @@ -1479,7 +1479,7 @@
     2.4  
     2.5  (* basic components *)
     2.6  
     2.7 -type rrule = {thm: thm, lhs: term, perm: bool};
     2.8 +type rrule = {thm: thm, lhs: term, elhs: term, fo: bool, perm: bool};
     2.9  type cong = {thm: thm, lhs: term};
    2.10  type simproc =
    2.11   {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
    2.12 @@ -1570,10 +1570,16 @@
    2.13  
    2.14  (* add_simps *)
    2.15  
    2.16 +fun mk_rrule2{thm,lhs,perm} =
    2.17 +  let val elhs = Pattern.eta_contract lhs
    2.18 +      val fo = Pattern.first_order elhs orelse not(Pattern.pattern elhs)
    2.19 +  in {thm=thm,lhs=lhs,elhs=elhs,fo=fo,perm=perm} end
    2.20 +
    2.21  fun insert_rrule(mss as Mss {rules,...},
    2.22 -                 rrule as {thm = thm, lhs = lhs, perm = perm}) =
    2.23 +                 rrule as {thm,lhs,perm}) =
    2.24    (trace_thm false "Adding rewrite rule:" thm;
    2.25 -   let val rules' = Net.insert_term ((lhs, rrule), rules, eq_rrule)
    2.26 +   let val rrule2 as {elhs,...} = mk_rrule2 rrule
    2.27 +       val rules' = Net.insert_term ((elhs, rrule2), rules, eq_rrule)
    2.28     in upd_rules(mss,rules') end
    2.29     handle Net.INSERT =>
    2.30       (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
    2.31 @@ -1660,7 +1666,9 @@
    2.32                 else let val Mss{mk_rews={mk_sym,...},...} = mss
    2.33                      in case mk_sym thm of
    2.34                           None => []
    2.35 -                       | Some thm' => rrule_eq_True(thm',rhs,lhs,mss,thm)
    2.36 +                       | Some thm' =>
    2.37 +                           let val (_,_,lhs',rhs',_) = decomp_simp thm'
    2.38 +                           in rrule_eq_True(thm',lhs',rhs',mss,thm) end
    2.39                      end
    2.40            else rrule_eq_True(thm,lhs,rhs,mss,thm)
    2.41    end;
    2.42 @@ -1688,13 +1696,13 @@
    2.43  (* del_simps *)
    2.44  
    2.45  fun del_rrule(mss as Mss {rules,...},
    2.46 -              rrule as {thm = thm, lhs = lhs, perm = perm}) =
    2.47 -  (upd_rules(mss, Net.delete_term ((lhs, rrule), rules, eq_rrule))
    2.48 +              rrule as {thm, elhs, ...}) =
    2.49 +  (upd_rules(mss, Net.delete_term ((elhs, rrule), rules, eq_rrule))
    2.50     handle Net.DELETE =>
    2.51       (prthm true "Rewrite rule not in simpset:" thm; mss));
    2.52  
    2.53  fun del_simps(mss,thms) =
    2.54 -  orient_comb_simps del_rrule (mk_rrule mss) (mss,thms);
    2.55 +  orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule mss) (mss,thms);
    2.56  
    2.57  
    2.58  (* add_congs *)
    2.59 @@ -1834,6 +1842,10 @@
    2.60          | renAbs(t) = t
    2.61    in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
    2.62  
    2.63 +fun incr_insts i (in1:(indexname*typ)list,in2:(indexname*term)list) =
    2.64 +  let fun incr ((a,n),x) = ((a,n+i),x)
    2.65 +  in (map incr in1, map incr in2) end;
    2.66 +
    2.67  fun add_insts_sorts ((iTs, is), Ss) =
    2.68    add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));
    2.69  
    2.70 @@ -1844,7 +1856,7 @@
    2.71    let val (_,prems,lhs,rhs,_) = decomp_simp thm
    2.72    in if rewrite_rule_extra_vars prems lhs rhs
    2.73       then (prthm true "Extra vars on rhs:" thm; [])
    2.74 -     else [{thm = thm, lhs = lhs, perm = false}]
    2.75 +     else [mk_rrule2{thm = thm, lhs = lhs, perm = false}]
    2.76    end;
    2.77  
    2.78  
    2.79 @@ -1867,17 +1879,18 @@
    2.80    let
    2.81      val signt = Sign.deref sign_reft;
    2.82      val tsigt = Sign.tsig_of signt;
    2.83 -    fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...}, lhs, perm} =
    2.84 +    fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...},
    2.85 +            lhs, elhs, fo, perm} =
    2.86        let
    2.87          val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
    2.88                  else (trace_thm true "Rewrite rule from different theory:" thm;
    2.89                        raise Pattern.MATCH);
    2.90          val rprop = if maxt = ~1 then prop
    2.91                      else Logic.incr_indexes([],maxt+1) prop;
    2.92 -        val rlhs = if maxt = ~1 then lhs
    2.93 -                   else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
    2.94 -        val insts = Pattern.match tsigt (rlhs,t);
    2.95 -        val prop' = ren_inst(insts,rprop,rlhs,t);
    2.96 +        val insts = if fo then Pattern.first_order_match tsigt (elhs,t)
    2.97 +                          else Pattern.match             tsigt (elhs,t);
    2.98 +        val insts = if maxt = ~1 then insts else incr_insts (maxt+1) insts
    2.99 +        val prop' = ren_inst(insts,rprop,lhs,t);
   2.100          val hyps' = union_term(hyps,hypst);
   2.101          val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
   2.102          val unconditional = (Logic.count_prems(prop',0) = 0);
   2.103 @@ -1906,7 +1919,7 @@
   2.104            in case opt of None => rews rrules | some => some end;
   2.105  
   2.106      fun sort_rrules rrs = let
   2.107 -      fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of 
   2.108 +      fun is_simple({thm as Thm{prop,...}, ...}:rrule) = case prop of 
   2.109                                        Const("==",_) $ _ $ _ => true
   2.110                                        | _                   => false 
   2.111        fun sort []        (re1,re2) = re1 @ re2
   2.112 @@ -1928,8 +1941,7 @@
   2.113                    | some => some)))
   2.114            else proc_rews eta_t ps;
   2.115    in case t of
   2.116 -       Abs (_, _, body) $ u =>
   2.117 -         Some (subst_bound (u, body), etc)
   2.118 +       Abs (_, _, body) $ u => Some (subst_bound (u, body), etc)
   2.119       | _ => (case rews (sort_rrules (Net.match_term rules t)) of
   2.120                 None => proc_rews (Pattern.eta_contract t)
   2.121                                   (Net.match_term procs t)
   2.122 @@ -2045,7 +2057,7 @@
   2.123  
   2.124      and mut_impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) =
   2.125        let
   2.126 -        fun uncond({thm,lhs,...}:rrule) =
   2.127 +        fun uncond({thm,lhs,perm}) =
   2.128            if nprems_of thm = 0 then Some lhs else None
   2.129  
   2.130          val (lhss1,mss1) =