Tried to reorganize rewriter a little. More to be done.
authornipkow
Sat Feb 28 15:40:03 1998 +0100 (1998-02-28)
changeset 46676328d427a339
parent 4666 b7c4e4ade1aa
child 4668 131989b78417
Tried to reorganize rewriter a little. More to be done.
src/Pure/logic.ML
src/Pure/pattern.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/logic.ML	Fri Feb 27 11:21:28 1998 +0100
     1.2 +++ b/src/Pure/logic.ML	Sat Feb 28 15:40:03 1998 +0100
     1.3 @@ -324,11 +324,11 @@
     1.4    orelse
     1.5     (null prems andalso
     1.6      Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
     1.7 -  orelse
     1.8 +(*  orelse
     1.9     (case lhs of
    1.10        (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse
    1.11                                   (null prems andalso f occs rhs)
    1.12 -    | _ => false);
    1.13 +    | _ => false)*);
    1.14  (*the condition "null prems" in the last cases is necessary because
    1.15    conditional rewrites with extra variables in the conditions may terminate
    1.16    although the rhs is an instance of the lhs. Example:
     2.1 --- a/src/Pure/pattern.ML	Fri Feb 27 11:21:28 1998 +0100
     2.2 +++ b/src/Pure/pattern.ML	Sat Feb 28 15:40:03 1998 +0100
     2.3 @@ -25,6 +25,7 @@
     2.4    val match             : type_sig -> term * term
     2.5                            -> (indexname*typ)list * (indexname*term)list
     2.6    val matches           : type_sig -> term * term -> bool
     2.7 +  val matches_subterm   : type_sig -> term * term -> bool
     2.8    val unify             : sg * env * (term * term)list -> env
     2.9    exception Unif
    2.10    exception MATCH
    2.11 @@ -390,4 +391,15 @@
    2.12  (*Predicate: does the pattern match the object?*)
    2.13  fun matches tsig po = (match tsig po; true) handle MATCH => false;
    2.14  
    2.15 +(* Does pat match a subterm of obj? *)
    2.16 +fun matches_subterm tsig (pat,obj) =
    2.17 +  let fun msub(bounds,obj) = matches tsig (pat,obj) orelse
    2.18 +            case obj of
    2.19 +              Abs(x,T,t) => let val y = variant bounds x
    2.20 +                                val f = Free(":" ^ y,T)
    2.21 +                            in msub(x::bounds,subst_bound(f,t)) end
    2.22 +            | s$t => msub(bounds,s) orelse msub(bounds,t)
    2.23 +            | _ => false
    2.24 +  in msub([],obj) end;
    2.25 +
    2.26  end;
     3.1 --- a/src/Pure/thm.ML	Fri Feb 27 11:21:28 1998 +0100
     3.2 +++ b/src/Pure/thm.ML	Sat Feb 28 15:40:03 1998 +0100
     3.3 @@ -164,7 +164,7 @@
     3.4    val add_prems         : meta_simpset * thm list -> meta_simpset
     3.5    val prems_of_mss      : meta_simpset -> thm list
     3.6    val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
     3.7 -  val mk_rews_of_mss    : meta_simpset -> thm -> thm list
     3.8 +(*  val mk_rews_of_mss    : meta_simpset -> thm -> thm list *)
     3.9    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
    3.10    val trace_simp        : bool ref
    3.11    val rewrite_cterm     : bool * bool -> meta_simpset ->
    3.12 @@ -1575,33 +1575,39 @@
    3.13  
    3.14  (* add_simps *)
    3.15  
    3.16 -fun add_simp
    3.17 -  (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
    3.18 -    thm as Thm {sign_ref, prop, ...}) =
    3.19 -  (case mk_rrule thm of
    3.20 +fun add_simp1(mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
    3.21 +              thm as Thm {sign_ref, prop, ...}) =
    3.22 +  case mk_rrule thm of
    3.23      None => mss
    3.24    | Some (rrule as {lhs, ...}) =>
    3.25        (trace_thm false "Adding rewrite rule:" thm;
    3.26 -        mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule) handle Net.INSERT =>
    3.27 -          (prtm true "ignoring duplicate rewrite rule" (Sign.deref sign_ref) prop; rules),
    3.28 -            congs, procs, bounds, prems, mk_rews, termless)));
    3.29 +       mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule),
    3.30 +               congs, procs, bounds, prems, mk_rews, termless)
    3.31 +       handle Net.INSERT =>
    3.32 +       (prtm true "ignoring duplicate rewrite rule" (Sign.deref sign_ref) prop;
    3.33 +        mss));
    3.34 +
    3.35 +fun add_simp(mss as Mss{mk_rews,...},thm) = foldl add_simp1 (mss, mk_rews thm);
    3.36  
    3.37  val add_simps = foldl add_simp;
    3.38  
    3.39 -fun mss_of thms = add_simps (empty_mss, thms);
    3.40 +fun mss_of thms = foldl add_simp1 (empty_mss, thms);
    3.41  
    3.42  
    3.43  (* del_simps *)
    3.44  
    3.45 -fun del_simp
    3.46 -  (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
    3.47 -    thm as Thm {sign_ref, prop, ...}) =
    3.48 -  (case mk_rrule thm of
    3.49 +fun del_simp1(mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
    3.50 +              thm as Thm {sign_ref, prop, ...}) =
    3.51 +  case mk_rrule thm of
    3.52      None => mss
    3.53    | Some (rrule as {lhs, ...}) =>
    3.54 -      mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule) handle Net.DELETE =>
    3.55 -        (prtm true "rewrite rule not in simpset" (Sign.deref sign_ref) prop; rules),
    3.56 -          congs, procs, bounds, prems, mk_rews, termless));
    3.57 +      (mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule),
    3.58 +               congs, procs, bounds, prems, mk_rews, termless)
    3.59 +       handle Net.DELETE =>
    3.60 +       (prtm true "rewrite rule not in simpset" (Sign.deref sign_ref) prop;
    3.61 +        mss));
    3.62 +
    3.63 +fun del_simp(mss as Mss{mk_rews,...},thm) = foldl del_simp1 (mss, mk_rews thm);
    3.64  
    3.65  val del_simps = foldl del_simp;
    3.66  
    3.67 @@ -1951,7 +1957,7 @@
    3.68                 end)
    3.69           | _ => None)
    3.70  
    3.71 -     and impc(shyps, hyps, s, u, mss as Mss{mk_rews,...}, ders) =
    3.72 +     and impc(shyps, hyps, s, u, mss, ders) =
    3.73         let val (shyps1,hyps1,s1,ders1) =
    3.74               if simprem then try_botc mss (shyps,hyps,s,ders)
    3.75                          else (shyps,hyps,s,ders);
    3.76 @@ -1963,7 +1969,7 @@
    3.77                                                    (Sign.deref sign_ref) s1; mss)
    3.78               else let val thm = assume (Cterm{sign_ref=sign_ref, t=s1, 
    3.79                                                T=propT, maxidx= ~1})
    3.80 -                  in add_simps(add_prems(mss,[thm]), mk_rews thm) end
    3.81 +                  in add_simp(add_prems(mss,[thm]), thm) end
    3.82             val (shyps2,hyps2,u1,ders2) = try_botc mss1 (shyps1,hyps1,u,ders1)
    3.83             val hyps3 = if gen_mem (op aconv) (s1, hyps1)
    3.84                         then hyps2 else hyps2\s1