# HG changeset patch # User lcp # Date 799059460 -7200 # Node ID b3f190995bc9a14384d35cee5b1af0b5e7ea6b2a # Parent 0140ff702b232f48cb4c7414dca663e41acad213 Recoded addSIs, etc., so that nets are built incrementally instead of from scratch each time. The old approach used excessive time (>1 sec for adding a rule to ZF_cs) and probably excessive space. Now rep_claset includes all record fields. joinrules no longer sorts the rules on number of subgoals, since it does not see the full set of them; instead the number of subgoals modifies the priority. diff -r 0140ff702b23 -r b3f190995bc9 src/Provers/classical.ML --- a/src/Provers/classical.ML Tue Apr 25 11:14:03 1995 +0200 +++ b/src/Provers/classical.ML Fri Apr 28 10:57:40 1995 +0200 @@ -33,6 +33,7 @@ signature CLASSICAL = sig type claset + type netpair val empty_cs : claset val addDs : claset * thm list -> claset val addEs : claset * thm list -> claset @@ -46,9 +47,12 @@ val addafter : claset * tactic -> claset val print_cs : claset -> unit - val rep_claset : claset -> {safeIs: thm list, safeEs: thm list, - hazIs: thm list, hazEs: thm list, - wrapper: tactic -> tactic} + val rep_claset : + claset -> {safeIs: thm list, safeEs: thm list, + hazIs: thm list, hazEs: thm list, + wrapper: tactic -> tactic, + safe0_netpair: netpair, safep_netpair: netpair, + haz_netpair: netpair, dup_netpair: netpair} val getwrapper : claset -> tactic -> tactic val THEN_MAYBE : tactic * tactic -> tactic @@ -118,6 +122,7 @@ fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> rule_by_tactic (TRYALL (etac revcut_rl)); + (*** Classical rule sets ***) type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; @@ -133,79 +138,164 @@ haz_netpair : netpair, (*nets for unsafe rules*) dup_netpair : netpair}; (*nets for duplication*) -fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) = - {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper}; - -fun getwrapper (CS{wrapper,...}) = wrapper; - -(*For use with biresolve_tac. Combines intr rules with swap to handle negated - assumptions. Pairs elim rules with true. Sorts the list of pairs by - the number of new subgoals generated. *) -fun joinrules (intrs,elims) = - sort lessb - (map (pair true) (elims @ swapify intrs) @ - map (pair false) intrs); - -val build = build_netpair(Net.empty,Net.empty); - -(*Make a claset from the four kinds of rules*) -fun make_cs {safeIs,safeEs,hazIs,hazEs,wrapper} = - let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) - take_prefix (fn brl => subgoals_of_brl brl=0) - (joinrules(safeIs, safeEs)) - in CS{safeIs = safeIs, - safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, - wrapper = wrapper, +(*Desired invariants are safe0_netpair = build safe0_brls, safep_netpair = build safep_brls, haz_netpair = build (joinrules(hazIs, hazEs)), dup_netpair = build (joinrules(map dup_intr hazIs, map dup_elim hazEs))} - end; + +where build = build_netpair(Net.empty,Net.empty), + safe0_brls contains all brules that solve the subgoal, and + safep_brls contains all brules that generate 1 or more new subgoals. +Nets must be built incrementally, to save space and time. +*) -(*** Manipulation of clasets ***) - -val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[], wrapper=I}; +val empty_cs = + CS{safeIs = [], + safeEs = [], + hazIs = [], + hazEs = [], + wrapper = I, + safe0_netpair = (Net.empty,Net.empty), + safep_netpair = (Net.empty,Net.empty), + haz_netpair = (Net.empty,Net.empty), + dup_netpair = (Net.empty,Net.empty)}; fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) = - (writeln"Introduction rules"; prths hazIs; - writeln"Safe introduction rules"; prths safeIs; - writeln"Elimination rules"; prths hazEs; - writeln"Safe elimination rules"; prths safeEs; + (writeln"Introduction rules"; prths hazIs; + writeln"Safe introduction rules"; prths safeIs; + writeln"Elimination rules"; prths hazEs; + writeln"Safe elimination rules"; prths safeEs; ()); -(** Adding new (un)safe introduction or elimination rules - In case of overlap, new rules are tried BEFORE old ones +fun rep_claset (CS args) = args; + +fun getwrapper (CS{wrapper,...}) = wrapper; + + +(** Adding (un)safe introduction or elimination rules. + + In case of overlap, new rules are tried BEFORE old ones!! **) -fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addSIs ths = - make_cs {safeIs=ths@safeIs, - safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper}; +(*For use with biresolve_tac. Combines intr rules with swap to handle negated + assumptions. Pairs elim rules with true. *) +fun joinrules (intrs,elims) = + (map (pair true) (elims @ swapify intrs) @ + map (pair false) intrs); + +(*Priority: prefer rules with fewest subgoals, + then rules added most recently.*) +fun tag_brls k [] = [] + | tag_brls k (brl::brls) = + (1000000*subgoals_of_brl brl + k, brl) :: + tag_brls (k+1) brls; + +fun insert_tagged_list kbrls np = foldr insert_tagged_brl (kbrls, np); + +(*Insert into netpair that already has nI intr rules and nE elim rules. + Count the intr rules double (to account for swapify). Negate to give the + new insertions the lowest priority.*) +fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; + + +(** Safe rules **) -fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addSEs ths = - make_cs {safeEs=ths@safeEs, - safeIs=safeIs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper}; +fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) + addSIs ths = + let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) + take_prefix (fn rl => nprems_of rl=0) ths + val nI = length safeIs + length ths + and nE = length safeEs + in CS{safeIs = ths@safeIs, + safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, + safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + wrapper = wrapper, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} + end; + +fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) + addSEs ths = + let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) + take_prefix (fn rl => nprems_of rl=1) ths + val nI = length safeIs + and nE = length safeEs + length ths + in + CS{safeEs = ths@safeEs, + safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, + safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, + safeIs = safeIs, + hazIs = hazIs, + hazEs = hazEs, + wrapper = wrapper, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} + end; fun cs addSDs ths = cs addSEs (map make_elim ths); -fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addIs ths = - make_cs {hazIs=ths@hazIs, - safeIs=safeIs, safeEs=safeEs, hazEs=hazEs, wrapper=wrapper}; + +(** Hazardous (unsafe) rules **) -fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addEs ths = - make_cs {hazEs=ths@hazEs, - safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, wrapper=wrapper}; +fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) + addIs ths = + let val nI = length hazIs + length ths + and nE = length hazEs + in + CS{hazIs = ths@hazIs, + haz_netpair = insert (nI,nE) (ths, []) haz_netpair, + dup_netpair = insert (nI,nE) (map dup_intr ths, []) dup_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazEs = hazEs, + wrapper = wrapper, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair} + end; + +fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) + addEs ths = + let val nI = length hazIs + and nE = length hazEs + length ths + in + CS{hazEs = ths@hazEs, + haz_netpair = insert (nI,nE) ([], ths) haz_netpair, + dup_netpair = insert (nI,nE) ([], map dup_elim ths) dup_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + wrapper = wrapper, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair} + end; fun cs addDs ths = cs addEs (map make_elim ths); + (** Setting or modifying the wrapper tactical **) (*Set a new wrapper*) -fun (CS{safeIs,safeEs,hazIs,hazEs,...}) setwrapper wrapper = - make_cs {wrapper=wrapper, - safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; +fun (CS{safeIs, safeEs, hazIs, hazEs, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) + setwrapper new_wrapper = + CS{wrapper = new_wrapper, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair}; (*Compose a tactical with the existing wrapper*) fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs);