export eq_rrule;
authorwenzelm
Wed Jul 13 16:07:28 2005 +0200 (2005-07-13)
changeset 16807730cace0ae48
parent 16806 916387f7afd2
child 16808 644fc45c7292
export eq_rrule;
improved Net interface;
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Wed Jul 13 16:07:27 2005 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Wed Jul 13 16:07:28 2005 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val simp_depth_limit: int ref
     1.5    val trace_simp_depth_limit: int ref
     1.6    type rrule
     1.7 +  val eq_rrule: rrule * rrule -> bool
     1.8    type cong
     1.9    type solver
    1.10    val mk_solver: string -> (thm list -> int -> tactic) -> solver
    1.11 @@ -274,10 +275,10 @@
    1.12        Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
    1.13  
    1.14      val Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = ss;
    1.15 -    val smps = map (#thm o #2) (Net.dest rules);
    1.16 +    val smps = map #thm (Net.entries rules);
    1.17      val cngs = map (fn (name, {thm, ...}) => (name, thm)) (#1 congs);
    1.18 -    val prcs = Net.dest procs |>
    1.19 -      map (fn (_, Proc {name, lhs, id, ...}) => ((name, lhs), id))
    1.20 +    val prcs = Net.entries procs |>
    1.21 +      map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
    1.22        |> partition_eq eq_snd
    1.23        |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
    1.24        |> Library.sort_wrt #1;
    1.25 @@ -327,12 +328,12 @@
    1.26       {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
    1.27        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
    1.28  
    1.29 -    val rules' = Net.merge (rules1, rules2, eq_rrule);
    1.30 +    val rules' = Net.merge eq_rrule (rules1, rules2);
    1.31      val prems' = gen_merge_lists Drule.eq_thm_prop prems1 prems2;
    1.32      val bounds' = Int.max (bounds1, bounds2);
    1.33      val congs' = gen_merge_lists (eq_cong o pairself #2) congs1 congs2;
    1.34      val weak' = merge_lists weak1 weak2;
    1.35 -    val procs' = Net.merge (procs1, procs2, eq_proc);
    1.36 +    val procs' = Net.merge eq_proc (procs1, procs2);
    1.37      val loop_tacs' = merge_alists loop_tacs1 loop_tacs2;
    1.38      val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2;
    1.39      val solvers' = merge_solvers solvers1 solvers2;
    1.40 @@ -355,7 +356,7 @@
    1.41    end;
    1.42  
    1.43  fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
    1.44 -fun simproc thy name = simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
    1.45 +fun simproc thy name = simproc_i thy name o map (Sign.read_term thy);
    1.46  
    1.47  
    1.48  
    1.49 @@ -384,7 +385,7 @@
    1.50    ss |> map_simpset1 (fn (rules, prems, bounds) =>
    1.51      let
    1.52        val rrule2 as {elhs, ...} = mk_rrule2 rrule;
    1.53 -      val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule);
    1.54 +      val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
    1.55      in (rules', prems, bounds) end)
    1.56    handle Net.INSERT =>
    1.57      (if quiet then () else warn_thm "Ignoring duplicate rewrite rule:" thm; ss));
    1.58 @@ -513,7 +514,7 @@
    1.59  
    1.60  fun del_rrule (ss, rrule as {thm, elhs, ...}) =
    1.61    ss |> map_simpset1 (fn (rules, prems, bounds) =>
    1.62 -    (Net.delete_term ((term_of elhs, rrule), rules, eq_rrule), prems, bounds))
    1.63 +    (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds))
    1.64    handle Net.DELETE => (warn_thm "Rewrite rule not in simpset:" thm; ss);
    1.65  
    1.66  fun ss delsimps thms =
    1.67 @@ -599,14 +600,14 @@
    1.68  fun add_proc (ss, proc as Proc {name, lhs, ...}) =
    1.69   (trace_cterm false ("Adding simplification procedure " ^ quote name ^ " for") lhs;
    1.70    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.71 -    (congs, Net.insert_term ((term_of lhs, proc), procs, eq_proc),
    1.72 +    (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
    1.73        mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
    1.74    handle Net.INSERT =>
    1.75      (warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
    1.76  
    1.77  fun del_proc (ss, proc as Proc {name, lhs, ...}) =
    1.78    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.79 -    (congs, Net.delete_term ((term_of lhs, proc), procs, eq_proc),
    1.80 +    (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
    1.81        mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
    1.82    handle Net.DELETE =>
    1.83      (warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);