Avoid eta-contraction in the simplifier.
authornipkow
Fri Mar 14 10:35:30 1997 +0100 (1997-03-14)
changeset 27926c17c5ec3d8b
parent 2791 b65da0c53d94
child 2793 b30c41754c86
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.
src/Pure/net.ML
src/Pure/pattern.ML
src/Pure/term.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/net.ML	Tue Mar 11 17:20:59 1997 +0100
     1.2 +++ b/src/Pure/net.ML	Fri Mar 14 10:35:30 1997 +0100
     1.3 @@ -198,8 +198,11 @@
     1.4  			else var::nets	   	(*only matches Var in net*)
     1.5  (*If "unif" then a var instantiation in the abstraction could allow
     1.6    an eta-reduction, so regard the abstraction as a wildcard.*)
     1.7 -	     | Abs _ => if unif then net_skip (net,nets)
     1.8 -			else var::nets		(*only a Var can match*)
     1.9 +	     | Abs(_,_,u) => (case u of
    1.10 +                   f $ Bound 0 => if loose_bvar1(f,0) then var::nets
    1.11 +                                  else matching unif f (net,nets)
    1.12 +                 | _ => if unif then net_skip (net,nets)
    1.13 +			else var::nets)		(*only a Var can match*)
    1.14  	     | _ => rands t (net, var::nets)	(*var could match also*)
    1.15    end;
    1.16  
     2.1 --- a/src/Pure/pattern.ML	Tue Mar 11 17:20:59 1997 +0100
     2.2 +++ b/src/Pure/pattern.ML	Fri Mar 14 10:35:30 1997 +0100
     2.3 @@ -226,21 +226,51 @@
     2.4  
     2.5  
     2.6  (*Eta-contract a term (fully)*)
     2.7 +
     2.8 +(* copying: *)
     2.9  fun eta_contract (Abs(a,T,body)) = 
    2.10        (case  eta_contract body  of
    2.11          body' as (f $ Bound 0) => 
    2.12 -	  if (0 mem_int loose_bnos f) then Abs(a,T,body')
    2.13 +	  if loose_bvar1(f,0) then Abs(a,T,body')
    2.14  	  else incr_boundvars ~1 f 
    2.15        | body' => Abs(a,T,body'))
    2.16    | eta_contract(f$t) = eta_contract f $ eta_contract t
    2.17    | eta_contract t = t;
    2.18  
    2.19  
    2.20 +(* sharing:
    2.21 +local
    2.22 +
    2.23 +fun eta(Abs(x,T,t)) =
    2.24 +     (case eta t of
    2.25 +        None => (case t of
    2.26 +                   f $ Bound 0 => if loose_bvar1(f,0)
    2.27 +                                  then None
    2.28 +                                  else Some(incr_boundvars ~1 f)
    2.29 +                 | _ => None)
    2.30 +      | Some(t') => (case t' of
    2.31 +                       f $ Bound 0 => if loose_bvar1(f,0)
    2.32 +                                      then Some(Abs(x,T,t'))
    2.33 +                                      else Some(incr_boundvars ~1 f)
    2.34 +                     | _ => Some(Abs(x,T,t'))))
    2.35 +  | eta(s$t) = (case (eta s,eta t) of
    2.36 +                  (None,   None)    => None
    2.37 +                | (None,   Some t') => Some(s  $ t')
    2.38 +                | (Some s',None)    => Some(s' $ t)
    2.39 +                | (Some s',Some t') => Some(s' $ t'))
    2.40 +  | eta _ = None
    2.41 +
    2.42 +in
    2.43 +
    2.44 +fun eta_contract t = case eta t of None => t | Some(t') => t';
    2.45 +
    2.46 +end; *)
    2.47 +
    2.48  (*Eta-contract a term from outside: just enough to reduce it to an atom*)
    2.49  fun eta_contract_atom (t0 as Abs(a, T, body)) = 
    2.50        (case  eta_contract2 body  of
    2.51          body' as (f $ Bound 0) => 
    2.52 -	    if (0 mem_int loose_bnos f) then Abs(a,T,body')
    2.53 +	    if loose_bvar1(f,0) then Abs(a,T,body')
    2.54  	    else eta_contract_atom (incr_boundvars ~1 f)
    2.55        | _ => t0)
    2.56    | eta_contract_atom t = t
     3.1 --- a/src/Pure/term.ML	Tue Mar 11 17:20:59 1997 +0100
     3.2 +++ b/src/Pure/term.ML	Fri Mar 14 10:35:30 1997 +0100
     3.3 @@ -283,6 +283,10 @@
     3.4    | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
     3.5    | loose_bvar _ = false;
     3.6  
     3.7 +fun loose_bvar1(Bound i,k) = i = k
     3.8 +  | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
     3.9 +  | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
    3.10 +  | loose_bvar1 _ = false;
    3.11  
    3.12  (*Substitute arguments for loose bound variables.
    3.13    Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
     4.1 --- a/src/Pure/thm.ML	Tue Mar 11 17:20:59 1997 +0100
     4.2 +++ b/src/Pure/thm.ML	Fri Mar 14 10:35:30 1997 +0100
     4.3 @@ -1495,7 +1495,7 @@
     4.4  
     4.5  (*simple test for looping rewrite*)
     4.6  fun loops sign prems (lhs, rhs) =
     4.7 -   is_Var lhs
     4.8 +   is_Var (head_of lhs)
     4.9    orelse
    4.10     (exists (apl (lhs, Logic.occs)) (rhs :: prems))
    4.11    orelse
    4.12 @@ -1712,8 +1712,7 @@
    4.13  
    4.14  fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, ...}) 
    4.15               (shypst,hypst,maxt,t,ders) =
    4.16 -  let val etat = Pattern.eta_contract t;
    4.17 -      fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
    4.18 +  let fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
    4.19          let val unit = if Sign.subsig(sign,signt) then ()
    4.20                    else (trace_thm_warning "rewrite rule from different theory"
    4.21                            thm;
    4.22 @@ -1722,7 +1721,7 @@
    4.23                          else Logic.incr_indexes([],maxt+1) prop;
    4.24              val rlhs = if maxt = ~1 then lhs
    4.25                         else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
    4.26 -            val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,etat)
    4.27 +            val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,t)
    4.28              val prop' = ren_inst(insts,rprop,rlhs,t);
    4.29              val hyps' = union_term(hyps,hypst);
    4.30              val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
    4.31 @@ -1766,7 +1765,7 @@
    4.32  
    4.33        fun proc_rews [] = None
    4.34          | proc_rews ((f, _) :: fs) =
    4.35 -            (case f signt etat of
    4.36 +            (case f signt t of
    4.37                None => proc_rews fs
    4.38              | Some raw_thm =>
    4.39                  (trace_thm "Proved rewrite rule: " raw_thm;
    4.40 @@ -1774,12 +1773,12 @@
    4.41                     None => proc_rews fs
    4.42                   | some => some)));
    4.43    in
    4.44 -    (case etat of
    4.45 +    (case t of
    4.46        Abs (_, _, body) $ u =>		(* FIXME bug!? (because of beta/eta overlap) *)
    4.47          Some (shypst, hypst, maxt, subst_bound (u, body), ders)
    4.48       | _ =>
    4.49 -      (case rews (sort_rrules (Net.match_term rules etat)) of
    4.50 -        None => proc_rews (Net.match_term procs etat)
    4.51 +      (case rews (sort_rrules (Net.match_term rules t)) of
    4.52 +        None => proc_rews (Net.match_term procs t)
    4.53        | some => some))
    4.54    end;
    4.55