Eta contraction is now performed all the time during rewriting.
authornipkow
Thu Apr 29 18:33:31 1999 +0200 (1999-04-29)
changeset 65392e7d2fba9f6c
parent 6538 d575fb1edabf
child 6540 eaf90f6806df
Eta contraction is now performed all the time during rewriting.
src/Pure/net.ML
src/Pure/pattern.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/net.ML	Thu Apr 29 15:35:40 1999 +0200
     1.2 +++ b/src/Pure/net.ML	Thu Apr 29 18:33:31 1999 +0200
     1.3 @@ -195,16 +195,14 @@
     1.4       case net of
     1.5  	 Leaf _ => nets
     1.6         | Net{var,...} =>
     1.7 -	     let val etat = Pattern.eta_contract_atom t
     1.8 -	     in case (head_of etat) of
     1.9 +	     case head_of t of
    1.10  		 Var _ => if unif then net_skip (net,nets)
    1.11  			  else var::nets	   (*only matches Var in net*)
    1.12    (*If "unif" then a var instantiation in the abstraction could allow
    1.13      an eta-reduction, so regard the abstraction as a wildcard.*)
    1.14  	       | Abs _ => if unif then net_skip (net,nets)
    1.15  			  else var::nets	   (*only a Var can match*)
    1.16 -	       | _ => rands etat (net, var::nets)  (*var could match also*)
    1.17 -	     end
    1.18 +	       | _ => rands t (net, var::nets)  (*var could match also*)
    1.19    end;
    1.20  
    1.21  fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);
     2.1 --- a/src/Pure/pattern.ML	Thu Apr 29 15:35:40 1999 +0200
     2.2 +++ b/src/Pure/pattern.ML	Thu Apr 29 18:33:31 1999 +0200
     2.3 @@ -271,7 +271,9 @@
     2.4  
     2.5  end; *)
     2.6  
     2.7 -(*Eta-contract a term from outside: just enough to reduce it to an atom*)
     2.8 +(*Eta-contract a term from outside: just enough to reduce it to an atom
     2.9 +DOESN'T QUITE WORK!
    2.10 +*)
    2.11  fun eta_contract_atom (t0 as Abs(a, T, body)) = 
    2.12        (case  eta_contract2 body  of
    2.13          body' as (f $ Bound 0) => 
     3.1 --- a/src/Pure/thm.ML	Thu Apr 29 15:35:40 1999 +0200
     3.2 +++ b/src/Pure/thm.ML	Thu Apr 29 18:33:31 1999 +0200
     3.3 @@ -1987,6 +1987,7 @@
     3.4               (mss as Mss{rules, procs, termless, prems, congs, ...}) 
     3.5               (t:term,etc as (shypst,hypst,ders)) =
     3.6    let
     3.7 +    val eta_t = Pattern.eta_contract t;
     3.8      val signt = Sign.deref sign_reft;
     3.9      val tsigt = Sign.tsig_of signt;
    3.10      fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...},
    3.11 @@ -1997,10 +1998,10 @@
    3.12                        raise Pattern.MATCH);
    3.13          val rprop = if maxt = ~1 then prop
    3.14                      else Logic.incr_indexes([],maxt+1) prop;
    3.15 -        val insts = if fo then Pattern.first_order_match tsigt (elhs,t)
    3.16 -                          else Pattern.match             tsigt (elhs,t);
    3.17 +        val insts = if fo then Pattern.first_order_match tsigt (elhs,eta_t)
    3.18 +                          else Pattern.match             tsigt (elhs,eta_t);
    3.19          val insts = if maxt = ~1 then insts else incr_insts (maxt+1) insts
    3.20 -        val prop' = ren_inst(insts,rprop,lhs,t);
    3.21 +        val prop' = ren_inst(insts,rprop,lhs,eta_t);
    3.22          val hyps' = union_term(hyps,hypst);
    3.23          val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
    3.24          val unconditional = (Logic.count_prems(prop',0) = 0);
    3.25 @@ -2049,23 +2050,22 @@
    3.26                                       else sort rrs (re1,rr::re2)
    3.27      in sort rrs ([],[]) end
    3.28  
    3.29 -    fun proc_rews _ ([]:simproc list) = None
    3.30 -      | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
    3.31 +    fun proc_rews ([]:simproc list) = None
    3.32 +      | proc_rews ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
    3.33            if Pattern.matches tsigt (plhs, t) then
    3.34              (trace_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
    3.35               case proc signt prems eta_t of
    3.36 -               None => (trace false "FAILED"; proc_rews eta_t ps)
    3.37 +               None => (trace false "FAILED"; proc_rews ps)
    3.38               | Some raw_thm =>
    3.39                   (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
    3.40                    (case rews (mk_procrule raw_thm) of
    3.41 -                    None => (trace false "IGNORED"; proc_rews eta_t ps)
    3.42 +                    None => (trace false "IGNORED"; proc_rews ps)
    3.43                    | some => some)))
    3.44 -          else proc_rews eta_t ps;
    3.45 -  in case t of
    3.46 +          else proc_rews ps;
    3.47 +  in case eta_t of
    3.48         Abs (_, _, body) $ u => Some ((subst_bound (u, body), etc),skel0)
    3.49 -     | _ => (case rews (sort_rrules (Net.match_term rules t)) of
    3.50 -               None => proc_rews (Pattern.eta_contract t)
    3.51 -                                 (Net.match_term procs t)
    3.52 +     | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
    3.53 +               None => proc_rews (Net.match_term procs eta_t)
    3.54               | some => some)
    3.55    end;
    3.56