# HG changeset patch # User Walther Neuper # Date 1382628287 -7200 # Node ID aa0884017d4838bc52852e30c3c3df2eee76b58c # Parent e4ddf21390fd83c07da764d242e8950b1e88f19b removed "rulelist'" also from ~~/test/Tools/isac/* Notes: (1) these changes should have been done before e4ddf21390fd (2) the previous changeset e4ddf21390fd containes a typo in appl.sml, which should not have happened (NO case for a [-Test_Isac] mark) diff -r e4ddf21390fd -r aa0884017d48 src/Tools/isac/Interpret/appl.sml --- a/src/Tools/isac/Interpret/appl.sml Thu Oct 24 15:00:44 2013 +0200 +++ b/src/Tools/isac/Interpret/appl.sml Thu Oct 24 17:24:47 2013 +0200 @@ -24,7 +24,7 @@ then let val thy' = get_obj g_domID pt p' - val {rew_ord', erls, ...} = et_met (get_obj g_metID pt p') + val {rew_ord', erls, ...} = get_met (get_obj g_metID pt p') in ("OK", thy', rew_ord', erls, false) end else let diff -r e4ddf21390fd -r aa0884017d48 test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy --- a/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Thu Oct 24 15:00:44 2013 +0200 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Thu Oct 24 17:24:47 2013 +0200 @@ -4,6 +4,6 @@ ML_file "lucas_interpreter.sml" ML {* -val test_ruleset' = Unsynchronized.ref ([] : (rls' * (theory' * rls)) list) +(*val test_ruleset' = Unsynchronized.ref ([] : (rls' * (theory' * rls)) list)*) *} end diff -r e4ddf21390fd -r aa0884017d48 test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Thu Oct 24 15:00:44 2013 +0200 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Thu Oct 24 17:24:47 2013 +0200 @@ -4,14 +4,15 @@ (* CHECK length (KEStore_Elems.get_rlss @{theory}) = length (! ruleset') AT THE BOTTOM OF A THEORY:*) length (KEStore_Elems.get_rlss @{theory}) = 0; - length (! test_ruleset') = 1 (* if you have clicked somewhere below *) +(*length (! test_ruleset') = 1 (* if you have clicked somewhere below *)*) *} setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *} ML {* - test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)]) +(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)]) ; if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then () - else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*} + else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*) +*} setup {* KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *} diff -r e4ddf21390fd -r aa0884017d48 test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy Thu Oct 24 15:00:44 2013 +0200 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy Thu Oct 24 17:24:47 2013 +0200 @@ -7,7 +7,8 @@ [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*) test_list_rls))] *} -ML {* test_ruleset' := overwritelthy @{theory} (! test_ruleset', - [("test_list_rls", test_list_rls)]) *} +ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', + [("test_list_rls", test_list_rls)])*) +*} end diff -r e4ddf21390fd -r aa0884017d48 test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy Thu Oct 24 15:00:44 2013 +0200 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy Thu Oct 24 17:24:47 2013 +0200 @@ -5,7 +5,8 @@ setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))] *} -ML {* test_ruleset' := overwritelthy @{theory} (! test_ruleset', - [("test_list_rls", test_list_rls)]) *} +ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', + [("test_list_rls", test_list_rls)])*) +*} end diff -r e4ddf21390fd -r aa0884017d48 test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Thu Oct 24 15:00:44 2013 +0200 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Thu Oct 24 17:24:47 2013 +0200 @@ -10,11 +10,11 @@ if length (KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*) then () else error "rls identified by string-identifier, not by theory: changed" - test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", - append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])]) +(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", + append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])])*) ; - if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') - then () else error "KEStore_Elems.get_rlss = test_ruleset': changed" +(*if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') + then () else error "KEStore_Elems.get_rlss = test_ruleset': changed"*) ; val SOME (_, Rls {rules, ...}) = AList.lookup op= (KEStore_Elems.get_rlss @{theory}) "test_list_rls" diff -r e4ddf21390fd -r aa0884017d48 test/Tools/isac/Interpret/rewtools.sml --- a/test/Tools/isac/Interpret/rewtools.sml Thu Oct 24 15:00:44 2013 +0200 +++ b/test/Tools/isac/Interpret/rewtools.sml Thu Oct 24 17:24:47 2013 +0200 @@ -72,11 +72,13 @@ val ancestors = Theory.ancestors_of @{theory "Complex_Main"}; val isabthms = (flat o (map Theory.axioms_of)) ancestors; -val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (! ruleset'); +val isacrules = (flat o (map (thms_of_rls o #2 o #2))) + (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); (*thms from rulesets*) (*=== inhibit exn AK110725 ============================================================= val isacrlsthms = ((map rep_thm_G') o flat o - (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset'); + (map (PureThy.all_thms_of_rls o #2 o #2))) + (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); length isacrlsthms; (*takes a few seconds... val isacrlsthms = gen_distinct eq_thmI isacrlsthms; @@ -157,14 +159,14 @@ curry ((op mem) o swap) dropthys' "Isac"; val ancestors_rls = filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory')) - (rev (!ruleset')); + (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))); take (10, map #1 ancestors_rls) = ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation", "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*) (* WN120523 popped up again ?!?!? -if length (!ruleset') <> length ancestors_rls then () +if length (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then () else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?"; *) @@ -189,7 +191,7 @@ val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list; val ancestors_rls = filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory')) - (rev (!ruleset')); + (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))); case assoc (ancestors_rls, rls') of SOME ("Poly", Seq {id = "norm_Poly", ...}) => () diff -r e4ddf21390fd -r aa0884017d48 test/Tools/isac/Knowledge/build_thydata.sml --- a/test/Tools/isac/Knowledge/build_thydata.sml Thu Oct 24 15:00:44 2013 +0200 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Thu Oct 24 17:24:47 2013 +0200 @@ -30,14 +30,15 @@ local val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o - (map (thms_of_rls o #2 o #2))) (!ruleset'); + (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); val isacthms = (flat o (map (thms_of o #2))) (!theory'); in val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms); end; *) val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o - (map (thms_of_rls o #2 o #2))) (!ruleset'): (thmID * thm) list; + (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) + : (thmID * thm) list; (* THIS IS TOO EXPENSIVE: val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"}); length all_ListC_thms = 19860 <<<<<-----*) @@ -136,7 +137,7 @@ "-------- prop_of thm .. Theory.axioms_of ---------------"; "-------- prop_of thm .. Theory.axioms_of ---------------"; "-------- prop_of thm .. Theory.axioms_of ---------------"; -val isacrlsthms''''' = ! ruleset' +val isacrlsthms''''' = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*) |> flat |> map thm_of_thm @@ -246,7 +247,7 @@ "----- so we cannot get isacthms as thm, only as term ---"; "----- but we can retain isacrlsthms as thm ---"; *) -val isacrlsthms = ! ruleset' +val isacrlsthms = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*) |> flat |> map thm_of_thm diff -r e4ddf21390fd -r aa0884017d48 test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Thu Oct 24 15:00:44 2013 +0200 +++ b/test/Tools/isac/Knowledge/diff.sml Thu Oct 24 17:24:47 2013 +0200 @@ -45,42 +45,6 @@ get_pbt ["derivative_of","function"]; get_met ["diff","differentiate_on_R"]; -(*erls should not be in ruleset'! Here only for tests*) -ruleset' := -overwritelthy thy - (!ruleset', - [("erls", - Rls {id = "erls",preconds = [], rew_ord = ("termlessI",termlessI), - erls = e_rls, srls = Erls, calc = [], errpatts = [], - rules = [Thm ("refl",num_str @{thm refl}), - Thm ("order_refl",num_str @{thm order_refl}), - Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}), - Thm ("not_true",num_str @{thm not_true}), - Thm ("not_false",num_str @{thm not_false}), - Thm ("and_true",num_str @{thm and_true}), - Thm ("and_false",num_str @{thm and_false}), - Thm ("or_true",num_str @{thm or_true}), - Thm ("or_false",num_str @{thm or_false}), - Thm ("and_commute",num_str @{thm and_commute}), - Thm ("or_commute",num_str @{thm or_commute}), - - Calc ("Atools.is'_const",eval_const "#is_const_"), - Calc ("Atools.occurs'_in", eval_occurs_in ""), - Calc ("Tools.matches",eval_matches ""), - - Calc ("Groups.plus_class.plus",eval_binop "#add_"), - Calc ("Groups.times_class.times",eval_binop "#mult_"), - Calc ("Atools.pow" ,eval_binop "#power_"), - - Calc ("Orderings.ord_class.less",eval_equ "#less_"), - Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"), - - Calc ("Atools.ident",eval_ident "#ident_")], - scr = Prog ((term_of o the o (parse thy)) - "empty_script") - }:rls - )]); - "----------- for correction of diff_const ---------------"; "----------- for correction of diff_const ---------------"; "----------- for correction of diff_const ---------------"; diff -r e4ddf21390fd -r aa0884017d48 test/Tools/isac/xmlsrc/thy-hierarchy.sml --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Oct 24 15:00:44 2013 +0200 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Oct 24 17:24:47 2013 +0200 @@ -38,9 +38,9 @@ overwrite (al, b); overwritelthy thy (al, bl); -case assoc' (! ruleset',"e_rls") of +case assoc' ((KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of SOME ("Tools", Rls _) => () -| _ => error "e_rls not in ! ruleset'" +| _ => error "e_rls not in Theory_Data" assoc_rls "e_rls"; @@ -80,7 +80,7 @@ val thy' = "Test"; val rlss = filter ((curry op= thy') o ((#1 o #2):(rls' * (theory' * rls)) -> theory')) - (!ruleset'); + (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); collect_rlss ("IsacKnowledge",thy'); "collect_thy thy-------------------------------------------------"; @@ -388,7 +388,7 @@ val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list; val ancestors_rls = filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory')) - (rev (!ruleset')); + (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))); case assoc (ancestors_rls, rls') of SOME ("Poly", Rls {id = "discard_minus", ...}) => ()