# HG changeset patch # User wenzelm # Date 1439717346 -7200 # Node ID 0af3e522406c4b7a7fe8b3ae3d5dcdd95e6d4a66 # Parent e7c761c63c180e9b33bd8d721ef58a34ff8fe734 tuned; diff -r e7c761c63c18 -r 0af3e522406c src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Aug 15 23:10:13 2015 +0200 +++ b/src/Provers/classical.ML Sun Aug 16 11:29:06 2015 +0200 @@ -109,7 +109,7 @@ safep_netpair: netpair, haz_netpair: netpair, dup_netpair: netpair, - xtra_netpair: Context_Rules.netpair} + extra_netpair: Context_Rules.netpair} val get_cs: Context.generic -> claset val map_cs: (claset -> claset) -> Context.generic -> Context.generic val safe_dest: int option -> attribute @@ -224,7 +224,7 @@ safep_netpair : netpair, (*nets for >0 subgoals*) haz_netpair : netpair, (*nets for unsafe rules*) dup_netpair : netpair, (*nets for duplication*) - xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*) + extra_netpair : Context_Rules.netpair}; (*nets for extra rules*) val empty_netpair = (Net.empty, Net.empty); @@ -240,7 +240,7 @@ safep_netpair = empty_netpair, haz_netpair = empty_netpair, dup_netpair = empty_netpair, - xtra_netpair = empty_netpair}; + extra_netpair = empty_netpair}; fun rep_cs (CS args) = args; @@ -310,7 +310,7 @@ fun addSI w opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = if warn_rules opt_context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs else let @@ -333,12 +333,12 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} + extra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) extra_netpair} end; fun addSE w opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = if warn_rules opt_context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th else @@ -362,7 +362,7 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} + extra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) extra_netpair} end; fun addSD w opt_context th = addSE w opt_context (make_elim opt_context th); @@ -372,7 +372,7 @@ fun addI w opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = if warn_rules opt_context "Ignoring duplicate introduction (intro)\n" hazIs th then cs else let @@ -393,14 +393,14 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair} + extra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) extra_netpair} end handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) bad_thm opt_context "Ill-formed introduction rule" th; fun addE w opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = if warn_rules opt_context "Ignoring duplicate elimination (elim)\n" hazEs th then cs else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th else @@ -422,7 +422,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair} + extra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) extra_netpair} end; fun addD w opt_context th = addE w opt_context (make_elim opt_context th); @@ -436,7 +436,7 @@ fun delSI opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = if Item_Net.member safeIs th then let val ctxt = default_context opt_context th; @@ -454,13 +454,13 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = delete' ([th], []) xtra_netpair} + extra_netpair = delete' ([th], []) extra_netpair} end else cs; fun delSE opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = if Item_Net.member safeEs th then let val ctxt = default_context opt_context th; @@ -478,13 +478,13 @@ uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair, - xtra_netpair = delete' ([], [th]) xtra_netpair} + extra_netpair = delete' ([], [th]) extra_netpair} end else cs; fun delI opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = if Item_Net.member hazIs th then let val ctxt = default_context opt_context th; @@ -501,7 +501,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = delete' ([th], []) xtra_netpair} + extra_netpair = delete' ([th], []) extra_netpair} end else cs handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) @@ -509,7 +509,7 @@ fun delE opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = if Item_Net.member hazEs th then let val ctxt = default_context opt_context th; @@ -526,7 +526,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = delete' ([], [th]) xtra_netpair} + extra_netpair = delete' ([], [th]) extra_netpair} end else cs; @@ -537,10 +537,13 @@ Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse Item_Net.member safeEs th' orelse Item_Net.member hazEs th' then - delSI opt_context th - (delSE opt_context th - (delI opt_context th - (delE opt_context th (delSE opt_context th' (delE opt_context th' cs))))) + cs + |> delE opt_context th' + |> delSE opt_context th' + |> delE opt_context th + |> delI opt_context th + |> delSE opt_context th + |> delSI opt_context th else (warn_thm opt_context "Undeclared classical rule\n" th; cs) end; @@ -552,19 +555,19 @@ fun map_swrappers f (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, swrappers = f swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; + haz_netpair = haz_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; fun map_uwrappers f (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, swrappers = swrappers, uwrappers = f uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; + haz_netpair = haz_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; (* merge_cs *) @@ -902,8 +905,8 @@ fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => let val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt; - val {xtra_netpair, ...} = rep_claset_of ctxt; - val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair; + val {extra_netpair, ...} = rep_claset_of ctxt; + val rules3 = Context_Rules.find_rules_netpair true facts goal extra_netpair; val rules = rules1 @ rules2 @ rules3 @ rules4; val ruleq = Drule.multi_resolves (SOME ctxt) facts rules; val _ = Method.trace ctxt rules;