slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
authorwenzelm
Sat May 14 21:42:17 2011 +0200 (2011-05-14)
changeset 428102425068fe13a
parent 42808 30870aee8a3f
child 42811 c5146d5fc54c
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/Provers/classical.ML
src/Pure/item_net.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat May 14 18:29:06 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat May 14 21:42:17 2011 +0200
     1.3 @@ -799,8 +799,8 @@
     1.4  fun clasimpset_rules_of ctxt =
     1.5    let
     1.6      val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
     1.7 -    val intros = safeIs @ hazIs
     1.8 -    val elims = map Classical.classical_rule (safeEs @ hazEs)
     1.9 +    val intros = Item_Net.content safeIs @ Item_Net.content hazIs
    1.10 +    val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs)
    1.11      val simps = ctxt |> simpset_of |> dest_ss |> #simps
    1.12    in
    1.13      (mk_fact_table I I intros,
     2.1 --- a/src/Provers/classical.ML	Sat May 14 18:29:06 2011 +0200
     2.2 +++ b/src/Provers/classical.ML	Sat May 14 21:42:17 2011 +0200
     2.3 @@ -37,11 +37,12 @@
     2.4  sig
     2.5    type claset
     2.6    val empty_cs: claset
     2.7 +  val merge_cs: claset * claset -> claset
     2.8    val rep_cs: claset ->
     2.9 -   {safeIs: thm list,
    2.10 -    safeEs: thm list,
    2.11 -    hazIs: thm list,
    2.12 -    hazEs: thm list,
    2.13 +   {safeIs: thm Item_Net.T,
    2.14 +    safeEs: thm Item_Net.T,
    2.15 +    hazIs: thm Item_Net.T,
    2.16 +    hazEs: thm Item_Net.T,
    2.17      swrappers: (string * (Proof.context -> wrapper)) list,
    2.18      uwrappers: (string * (Proof.context -> wrapper)) list,
    2.19      safe0_netpair: netpair,
    2.20 @@ -214,10 +215,10 @@
    2.21  
    2.22  datatype claset =
    2.23    CS of
    2.24 -   {safeIs         : thm list,                (*safe introduction rules*)
    2.25 -    safeEs         : thm list,                (*safe elimination rules*)
    2.26 -    hazIs          : thm list,                (*unsafe introduction rules*)
    2.27 -    hazEs          : thm list,                (*unsafe elimination rules*)
    2.28 +   {safeIs         : thm Item_Net.T,          (*safe introduction rules*)
    2.29 +    safeEs         : thm Item_Net.T,          (*safe elimination rules*)
    2.30 +    hazIs          : thm Item_Net.T,          (*unsafe introduction rules*)
    2.31 +    hazEs          : thm Item_Net.T,          (*unsafe elimination rules*)
    2.32      swrappers      : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*)
    2.33      uwrappers      : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*)
    2.34      safe0_netpair  : netpair,                 (*nets for trivial cases*)
    2.35 @@ -244,10 +245,10 @@
    2.36  
    2.37  val empty_cs =
    2.38    CS
    2.39 -   {safeIs = [],
    2.40 -    safeEs = [],
    2.41 -    hazIs = [],
    2.42 -    hazEs = [],
    2.43 +   {safeIs = Thm.full_rules,
    2.44 +    safeEs = Thm.full_rules,
    2.45 +    hazIs = Thm.full_rules,
    2.46 +    hazEs = Thm.full_rules,
    2.47      swrappers = [],
    2.48      uwrappers = [],
    2.49      safe0_netpair = empty_netpair,
    2.50 @@ -294,9 +295,6 @@
    2.51  fun delete x = delete_tagged_list (joinrules x);
    2.52  fun delete' x = delete_tagged_list (joinrules' x);
    2.53  
    2.54 -val mem_thm = member Thm.eq_thm_prop
    2.55 -and rem_thm = remove Thm.eq_thm_prop;
    2.56 -
    2.57  fun string_of_thm NONE = Display.string_of_thm_without_context
    2.58    | string_of_thm (SOME context) =
    2.59        Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
    2.60 @@ -312,7 +310,7 @@
    2.61    else ();
    2.62  
    2.63  fun warn_rules context msg rules th =
    2.64 -  mem_thm rules th andalso (warn_thm context msg th; true);
    2.65 +  Item_Net.member rules th andalso (warn_thm context msg th; true);
    2.66  
    2.67  fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
    2.68    warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
    2.69 @@ -332,12 +330,12 @@
    2.70        val th' = flat_rule th;
    2.71        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    2.72          List.partition Thm.no_prems [th'];
    2.73 -      val nI = length safeIs + 1;
    2.74 -      val nE = length safeEs;
    2.75 +      val nI = Item_Net.length safeIs + 1;
    2.76 +      val nE = Item_Net.length safeEs;
    2.77        val _ = warn_claset context th cs;
    2.78      in
    2.79        CS
    2.80 -       {safeIs  = th::safeIs,
    2.81 +       {safeIs = Item_Net.update th safeIs,
    2.82          safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
    2.83          safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
    2.84          safeEs = safeEs,
    2.85 @@ -361,12 +359,12 @@
    2.86        val th' = classical_rule (flat_rule th);
    2.87        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    2.88          List.partition (fn rl => nprems_of rl=1) [th'];
    2.89 -      val nI = length safeIs;
    2.90 -      val nE = length safeEs + 1;
    2.91 +      val nI = Item_Net.length safeIs;
    2.92 +      val nE = Item_Net.length safeEs + 1;
    2.93        val _ = warn_claset context th cs;
    2.94      in
    2.95        CS
    2.96 -       {safeEs  = th::safeEs,
    2.97 +       {safeEs = Item_Net.update th safeEs,
    2.98          safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
    2.99          safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   2.100          safeIs = safeIs,
   2.101 @@ -391,12 +389,12 @@
   2.102    else
   2.103      let
   2.104        val th' = flat_rule th;
   2.105 -      val nI = length hazIs + 1;
   2.106 -      val nE = length hazEs;
   2.107 +      val nI = Item_Net.length hazIs + 1;
   2.108 +      val nE = Item_Net.length hazEs;
   2.109        val _ = warn_claset context th cs;
   2.110      in
   2.111        CS
   2.112 -       {hazIs = th :: hazIs,
   2.113 +       {hazIs = Item_Net.update th hazIs,
   2.114          haz_netpair = insert (nI, nE) ([th'], []) haz_netpair,
   2.115          dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair,
   2.116          safeIs = safeIs,
   2.117 @@ -420,12 +418,12 @@
   2.118    else
   2.119      let
   2.120        val th' = classical_rule (flat_rule th);
   2.121 -      val nI = length hazIs;
   2.122 -      val nE = length hazEs + 1;
   2.123 +      val nI = Item_Net.length hazIs;
   2.124 +      val nE = Item_Net.length hazEs + 1;
   2.125        val _ = warn_claset context th cs;
   2.126      in
   2.127        CS
   2.128 -       {hazEs = th :: hazEs,
   2.129 +       {hazEs = Item_Net.update th hazEs,
   2.130          haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
   2.131          dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair,
   2.132          safeIs = safeIs,
   2.133 @@ -450,7 +448,7 @@
   2.134  fun delSI th
   2.135      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   2.136        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   2.137 -  if mem_thm safeIs th then
   2.138 +  if Item_Net.member safeIs th then
   2.139      let
   2.140        val th' = flat_rule th;
   2.141        val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
   2.142 @@ -458,7 +456,7 @@
   2.143        CS
   2.144         {safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   2.145          safep_netpair = delete (safep_rls, []) safep_netpair,
   2.146 -        safeIs = rem_thm th safeIs,
   2.147 +        safeIs = Item_Net.remove th safeIs,
   2.148          safeEs = safeEs,
   2.149          hazIs = hazIs,
   2.150          hazEs = hazEs,
   2.151 @@ -473,7 +471,7 @@
   2.152  fun delSE th
   2.153      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   2.154        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   2.155 -  if mem_thm safeEs th then
   2.156 +  if Item_Net.member safeEs th then
   2.157      let
   2.158        val th' = classical_rule (flat_rule th);
   2.159        val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
   2.160 @@ -482,7 +480,7 @@
   2.161         {safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   2.162          safep_netpair = delete ([], safep_rls) safep_netpair,
   2.163          safeIs = safeIs,
   2.164 -        safeEs = rem_thm th safeEs,
   2.165 +        safeEs = Item_Net.remove th safeEs,
   2.166          hazIs = hazIs,
   2.167          hazEs = hazEs,
   2.168          swrappers = swrappers,
   2.169 @@ -496,14 +494,14 @@
   2.170  fun delI context th
   2.171      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   2.172        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   2.173 -  if mem_thm hazIs th then
   2.174 +  if Item_Net.member hazIs th then
   2.175      let val th' = flat_rule th in
   2.176        CS
   2.177         {haz_netpair = delete ([th'], []) haz_netpair,
   2.178          dup_netpair = delete ([dup_intr th'], []) dup_netpair,
   2.179          safeIs = safeIs,
   2.180          safeEs = safeEs,
   2.181 -        hazIs = rem_thm th hazIs,
   2.182 +        hazIs = Item_Net.remove th hazIs,
   2.183          hazEs = hazEs,
   2.184          swrappers = swrappers,
   2.185          uwrappers = uwrappers,
   2.186 @@ -518,7 +516,7 @@
   2.187  fun delE th
   2.188      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   2.189        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   2.190 -  if mem_thm hazEs th then
   2.191 +  if Item_Net.member hazEs th then
   2.192      let val th' = classical_rule (flat_rule th) in
   2.193        CS
   2.194         {haz_netpair = delete ([], [th']) haz_netpair,
   2.195 @@ -526,7 +524,7 @@
   2.196          safeIs = safeIs,
   2.197          safeEs = safeEs,
   2.198          hazIs = hazIs,
   2.199 -        hazEs = rem_thm th hazEs,
   2.200 +        hazEs = Item_Net.remove th hazEs,
   2.201          swrappers = swrappers,
   2.202          uwrappers = uwrappers,
   2.203          safe0_netpair = safe0_netpair,
   2.204 @@ -538,9 +536,9 @@
   2.205  (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   2.206  fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   2.207    let val th' = Tactic.make_elim th in
   2.208 -    if mem_thm safeIs th orelse mem_thm safeEs th orelse
   2.209 -      mem_thm hazIs th orelse mem_thm hazEs th orelse
   2.210 -      mem_thm safeEs th' orelse mem_thm hazEs th'
   2.211 +    if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
   2.212 +      Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
   2.213 +      Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
   2.214      then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
   2.215      else (warn_thm context "Undeclared classical rule\n" th; cs)
   2.216    end;
   2.217 @@ -570,28 +568,24 @@
   2.218  
   2.219  (* merge_cs *)
   2.220  
   2.221 -(*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   2.222 -  Merging the term nets may look more efficient, but the rather delicate
   2.223 -  treatment of priority might get muddled up.*)
   2.224 +(*Merge works by adding all new rules of the 2nd claset into the 1st claset,
   2.225 +  in order to preserve priorities reliably.*)
   2.226 +
   2.227 +fun merge_thms add thms1 thms2 =
   2.228 +  fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2);
   2.229 +
   2.230  fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
   2.231      cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
   2.232        swrappers, uwrappers, ...}) =
   2.233    if pointer_eq (cs, cs') then cs
   2.234    else
   2.235 -    let
   2.236 -      val safeIs' = fold rem_thm safeIs safeIs2;
   2.237 -      val safeEs' = fold rem_thm safeEs safeEs2;
   2.238 -      val hazIs' = fold rem_thm hazIs hazIs2;
   2.239 -      val hazEs' = fold rem_thm hazEs hazEs2;
   2.240 -    in
   2.241 -      cs
   2.242 -      |> fold_rev (addSI NONE NONE) safeIs'
   2.243 -      |> fold_rev (addSE NONE NONE) safeEs'
   2.244 -      |> fold_rev (addI NONE NONE) hazIs'
   2.245 -      |> fold_rev (addE NONE NONE) hazEs'
   2.246 -      |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
   2.247 -      |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers))
   2.248 -    end;
   2.249 +    cs
   2.250 +    |> merge_thms (addSI NONE NONE) safeIs safeIs2
   2.251 +    |> merge_thms (addSE NONE NONE) safeEs safeEs2
   2.252 +    |> merge_thms (addI NONE NONE) hazIs hazIs2
   2.253 +    |> merge_thms (addE NONE NONE) hazEs hazEs2
   2.254 +    |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
   2.255 +    |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers));
   2.256  
   2.257  
   2.258  (* data *)
   2.259 @@ -617,7 +611,7 @@
   2.260  fun print_claset ctxt =
   2.261    let
   2.262      val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
   2.263 -    val pretty_thms = map (Display.pretty_thm ctxt);
   2.264 +    val pretty_thms = map (Display.pretty_thm ctxt) o Item_Net.content;
   2.265    in
   2.266      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   2.267        Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
     3.1 --- a/src/Pure/item_net.ML	Sat May 14 18:29:06 2011 +0200
     3.2 +++ b/src/Pure/item_net.ML	Sat May 14 21:42:17 2011 +0200
     3.3 @@ -10,6 +10,7 @@
     3.4    type 'a T
     3.5    val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
     3.6    val content: 'a T -> 'a list
     3.7 +  val length: 'a T -> int
     3.8    val retrieve: 'a T -> term -> 'a list
     3.9    val member: 'a T -> 'a -> bool
    3.10    val merge: 'a T * 'a T -> 'a T
    3.11 @@ -36,6 +37,7 @@
    3.12  fun init eq index = mk_items eq index [] ~1 Net.empty;
    3.13  
    3.14  fun content (Items {content, ...}) = content;
    3.15 +fun length items = List.length (content items);
    3.16  fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
    3.17  
    3.18