# HG changeset patch
# User nipkow
# Date 858332130 -3600
# Node ID 6c17c5ec3d8b25e404e8e9b550ef6b80cea31975
# Parent  b65da0c53d9430bcf3ccea127ce8912f2d91812b
Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.

diff -r b65da0c53d94 -r 6c17c5ec3d8b src/Pure/net.ML
--- a/src/Pure/net.ML	Tue Mar 11 17:20:59 1997 +0100
+++ b/src/Pure/net.ML	Fri Mar 14 10:35:30 1997 +0100
@@ -198,8 +198,11 @@
 			else var::nets	   	(*only matches Var in net*)
 (*If "unif" then a var instantiation in the abstraction could allow
   an eta-reduction, so regard the abstraction as a wildcard.*)
-	     | Abs _ => if unif then net_skip (net,nets)
-			else var::nets		(*only a Var can match*)
+	     | Abs(_,_,u) => (case u of
+                   f $ Bound 0 => if loose_bvar1(f,0) then var::nets
+                                  else matching unif f (net,nets)
+                 | _ => if unif then net_skip (net,nets)
+			else var::nets)		(*only a Var can match*)
 	     | _ => rands t (net, var::nets)	(*var could match also*)
   end;
 
diff -r b65da0c53d94 -r 6c17c5ec3d8b src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Tue Mar 11 17:20:59 1997 +0100
+++ b/src/Pure/pattern.ML	Fri Mar 14 10:35:30 1997 +0100
@@ -226,21 +226,51 @@
 
 
 (*Eta-contract a term (fully)*)
+
+(* copying: *)
 fun eta_contract (Abs(a,T,body)) = 
       (case  eta_contract body  of
         body' as (f $ Bound 0) => 
-	  if (0 mem_int loose_bnos f) then Abs(a,T,body')
+	  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;
 
 
+(* sharing:
+local
+
+fun eta(Abs(x,T,t)) =
+     (case eta t of
+        None => (case t of
+                   f $ Bound 0 => if loose_bvar1(f,0)
+                                  then None
+                                  else Some(incr_boundvars ~1 f)
+                 | _ => None)
+      | Some(t') => (case t' of
+                       f $ Bound 0 => if loose_bvar1(f,0)
+                                      then Some(Abs(x,T,t'))
+                                      else Some(incr_boundvars ~1 f)
+                     | _ => Some(Abs(x,T,t'))))
+  | eta(s$t) = (case (eta s,eta t) of
+                  (None,   None)    => None
+                | (None,   Some t') => Some(s  $ t')
+                | (Some s',None)    => Some(s' $ t)
+                | (Some s',Some t') => Some(s' $ t'))
+  | eta _ = None
+
+in
+
+fun eta_contract t = case eta t of None => t | Some(t') => t';
+
+end; *)
+
 (*Eta-contract a term from outside: just enough to reduce it to an atom*)
 fun eta_contract_atom (t0 as Abs(a, T, body)) = 
       (case  eta_contract2 body  of
         body' as (f $ Bound 0) => 
-	    if (0 mem_int loose_bnos f) then Abs(a,T,body')
+	    if loose_bvar1(f,0) then Abs(a,T,body')
 	    else eta_contract_atom (incr_boundvars ~1 f)
       | _ => t0)
   | eta_contract_atom t = t
diff -r b65da0c53d94 -r 6c17c5ec3d8b src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Mar 11 17:20:59 1997 +0100
+++ b/src/Pure/term.ML	Fri Mar 14 10:35:30 1997 +0100
@@ -283,6 +283,10 @@
   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   | loose_bvar _ = false;
 
+fun loose_bvar1(Bound i,k) = i = k
+  | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
+  | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
+  | loose_bvar1 _ = false;
 
 (*Substitute arguments for loose bound variables.
   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
diff -r b65da0c53d94 -r 6c17c5ec3d8b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Mar 11 17:20:59 1997 +0100
+++ b/src/Pure/thm.ML	Fri Mar 14 10:35:30 1997 +0100
@@ -1495,7 +1495,7 @@
 
 (*simple test for looping rewrite*)
 fun loops sign prems (lhs, rhs) =
-   is_Var lhs
+   is_Var (head_of lhs)
   orelse
    (exists (apl (lhs, Logic.occs)) (rhs :: prems))
   orelse
@@ -1712,8 +1712,7 @@
 
 fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, ...}) 
              (shypst,hypst,maxt,t,ders) =
-  let val etat = Pattern.eta_contract t;
-      fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
+  let fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
         let val unit = if Sign.subsig(sign,signt) then ()
                   else (trace_thm_warning "rewrite rule from different theory"
                           thm;
@@ -1722,7 +1721,7 @@
                         else Logic.incr_indexes([],maxt+1) prop;
             val rlhs = if maxt = ~1 then lhs
                        else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
-            val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,etat)
+            val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,t)
             val prop' = ren_inst(insts,rprop,rlhs,t);
             val hyps' = union_term(hyps,hypst);
             val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
@@ -1766,7 +1765,7 @@
 
       fun proc_rews [] = None
         | proc_rews ((f, _) :: fs) =
-            (case f signt etat of
+            (case f signt t of
               None => proc_rews fs
             | Some raw_thm =>
                 (trace_thm "Proved rewrite rule: " raw_thm;
@@ -1774,12 +1773,12 @@
                    None => proc_rews fs
                  | some => some)));
   in
-    (case etat of
+    (case t of
       Abs (_, _, body) $ u =>		(* FIXME bug!? (because of beta/eta overlap) *)
         Some (shypst, hypst, maxt, subst_bound (u, body), ders)
      | _ =>
-      (case rews (sort_rrules (Net.match_term rules etat)) of
-        None => proc_rews (Net.match_term procs etat)
+      (case rews (sort_rrules (Net.match_term rules t)) of
+        None => proc_rews (Net.match_term procs t)
       | some => some))
   end;