1.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Oct 24 15:00:44 2013 +0200
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Oct 24 17:24:47 2013 +0200
1.3 @@ -24,7 +24,7 @@
1.4 then
1.5 let
1.6 val thy' = get_obj g_domID pt p'
1.7 - val {rew_ord', erls, ...} = et_met (get_obj g_metID pt p')
1.8 + val {rew_ord', erls, ...} = get_met (get_obj g_metID pt p')
1.9 in ("OK", thy', rew_ord', erls, false) end
1.10 else
1.11 let
2.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Thu Oct 24 15:00:44 2013 +0200
2.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Thu Oct 24 17:24:47 2013 +0200
2.3 @@ -4,6 +4,6 @@
2.4
2.5 ML_file "lucas_interpreter.sml"
2.6 ML {*
2.7 -val test_ruleset' = Unsynchronized.ref ([] : (rls' * (theory' * rls)) list)
2.8 +(*val test_ruleset' = Unsynchronized.ref ([] : (rls' * (theory' * rls)) list)*)
2.9 *}
2.10 end
3.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Thu Oct 24 15:00:44 2013 +0200
3.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Thu Oct 24 17:24:47 2013 +0200
3.3 @@ -4,14 +4,15 @@
3.4 (* CHECK length (KEStore_Elems.get_rlss @{theory}) = length (! ruleset')
3.5 AT THE BOTTOM OF A THEORY:*)
3.6 length (KEStore_Elems.get_rlss @{theory}) = 0;
3.7 - length (! test_ruleset') = 1 (* if you have clicked somewhere below *)
3.8 +(*length (! test_ruleset') = 1 (* if you have clicked somewhere below *)*)
3.9 *}
3.10 setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
3.11 ML {*
3.12 - test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)])
3.13 +(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)])
3.14 ;
3.15 if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
3.16 - else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*}
3.17 + else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*)
3.18 +*}
3.19
3.20 setup {* KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
3.21
4.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy Thu Oct 24 15:00:44 2013 +0200
4.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy Thu Oct 24 17:24:47 2013 +0200
4.3 @@ -7,7 +7,8 @@
4.4 [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*)
4.5 test_list_rls))] *}
4.6
4.7 -ML {* test_ruleset' := overwritelthy @{theory} (! test_ruleset',
4.8 - [("test_list_rls", test_list_rls)]) *}
4.9 +ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset',
4.10 + [("test_list_rls", test_list_rls)])*)
4.11 +*}
4.12
4.13 end
5.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy Thu Oct 24 15:00:44 2013 +0200
5.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy Thu Oct 24 17:24:47 2013 +0200
5.3 @@ -5,7 +5,8 @@
5.4
5.5 setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory},
5.6 test_list_rls))] *}
5.7 -ML {* test_ruleset' := overwritelthy @{theory} (! test_ruleset',
5.8 - [("test_list_rls", test_list_rls)]) *}
5.9 +ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset',
5.10 + [("test_list_rls", test_list_rls)])*)
5.11 +*}
5.12
5.13 end
6.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Thu Oct 24 15:00:44 2013 +0200
6.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Thu Oct 24 17:24:47 2013 +0200
6.3 @@ -10,11 +10,11 @@
6.4 if length (KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*)
6.5 then () else error "rls identified by string-identifier, not by theory: changed"
6.6
6.7 - test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls",
6.8 - append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])])
6.9 +(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls",
6.10 + append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])])*)
6.11 ;
6.12 - if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
6.13 - then () else error "KEStore_Elems.get_rlss = test_ruleset': changed"
6.14 +(*if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
6.15 + then () else error "KEStore_Elems.get_rlss = test_ruleset': changed"*)
6.16 ;
6.17 val SOME (_, Rls {rules, ...}) =
6.18 AList.lookup op= (KEStore_Elems.get_rlss @{theory}) "test_list_rls"
7.1 --- a/test/Tools/isac/Interpret/rewtools.sml Thu Oct 24 15:00:44 2013 +0200
7.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Thu Oct 24 17:24:47 2013 +0200
7.3 @@ -72,11 +72,13 @@
7.4 val ancestors = Theory.ancestors_of @{theory "Complex_Main"};
7.5 val isabthms = (flat o (map Theory.axioms_of)) ancestors;
7.6
7.7 -val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (! ruleset');
7.8 +val isacrules = (flat o (map (thms_of_rls o #2 o #2)))
7.9 + (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
7.10 (*thms from rulesets*)
7.11 (*=== inhibit exn AK110725 =============================================================
7.12 val isacrlsthms = ((map rep_thm_G') o flat o
7.13 - (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset');
7.14 + (map (PureThy.all_thms_of_rls o #2 o #2)))
7.15 + (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
7.16 length isacrlsthms;
7.17 (*takes a few seconds...
7.18 val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
7.19 @@ -157,14 +159,14 @@
7.20 curry ((op mem) o swap) dropthys' "Isac";
7.21 val ancestors_rls =
7.22 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
7.23 - (rev (!ruleset'));
7.24 + (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
7.25
7.26 take (10, map #1 ancestors_rls) =
7.27 ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation",
7.28 "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*)
7.29
7.30 (* WN120523 popped up again ?!?!?
7.31 -if length (!ruleset') <> length ancestors_rls then ()
7.32 +if length (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then ()
7.33 else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?";
7.34 *)
7.35
7.36 @@ -189,7 +191,7 @@
7.37 val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
7.38 val ancestors_rls =
7.39 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
7.40 - (rev (!ruleset'));
7.41 + (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
7.42
7.43 case assoc (ancestors_rls, rls') of
7.44 SOME ("Poly", Seq {id = "norm_Poly", ...}) => ()
8.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Thu Oct 24 15:00:44 2013 +0200
8.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Thu Oct 24 17:24:47 2013 +0200
8.3 @@ -30,14 +30,15 @@
8.4
8.5 local
8.6 val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o
8.7 - (map (thms_of_rls o #2 o #2))) (!ruleset');
8.8 + (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
8.9 val isacthms = (flat o (map (thms_of o #2))) (!theory');
8.10 in
8.11 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
8.12 end;
8.13 *)
8.14 val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o
8.15 - (map (thms_of_rls o #2 o #2))) (!ruleset'): (thmID * thm) list;
8.16 + (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
8.17 + : (thmID * thm) list;
8.18 (* THIS IS TOO EXPENSIVE:
8.19 val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"});
8.20 length all_ListC_thms = 19860 <<<<<-----*)
8.21 @@ -136,7 +137,7 @@
8.22 "-------- prop_of thm .. Theory.axioms_of ---------------";
8.23 "-------- prop_of thm .. Theory.axioms_of ---------------";
8.24 "-------- prop_of thm .. Theory.axioms_of ---------------";
8.25 -val isacrlsthms''''' = ! ruleset'
8.26 +val isacrlsthms''''' = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
8.27 |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
8.28 |> flat
8.29 |> map thm_of_thm
8.30 @@ -246,7 +247,7 @@
8.31 "----- so we cannot get isacthms as thm, only as term ---";
8.32 "----- but we can retain isacrlsthms as thm ---";
8.33 *)
8.34 -val isacrlsthms = ! ruleset'
8.35 +val isacrlsthms = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
8.36 |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
8.37 |> flat
8.38 |> map thm_of_thm
9.1 --- a/test/Tools/isac/Knowledge/diff.sml Thu Oct 24 15:00:44 2013 +0200
9.2 +++ b/test/Tools/isac/Knowledge/diff.sml Thu Oct 24 17:24:47 2013 +0200
9.3 @@ -45,42 +45,6 @@
9.4 get_pbt ["derivative_of","function"];
9.5 get_met ["diff","differentiate_on_R"];
9.6
9.7 -(*erls should not be in ruleset'! Here only for tests*)
9.8 -ruleset' :=
9.9 -overwritelthy thy
9.10 - (!ruleset',
9.11 - [("erls",
9.12 - Rls {id = "erls",preconds = [], rew_ord = ("termlessI",termlessI),
9.13 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
9.14 - rules = [Thm ("refl",num_str @{thm refl}),
9.15 - Thm ("order_refl",num_str @{thm order_refl}),
9.16 - Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
9.17 - Thm ("not_true",num_str @{thm not_true}),
9.18 - Thm ("not_false",num_str @{thm not_false}),
9.19 - Thm ("and_true",num_str @{thm and_true}),
9.20 - Thm ("and_false",num_str @{thm and_false}),
9.21 - Thm ("or_true",num_str @{thm or_true}),
9.22 - Thm ("or_false",num_str @{thm or_false}),
9.23 - Thm ("and_commute",num_str @{thm and_commute}),
9.24 - Thm ("or_commute",num_str @{thm or_commute}),
9.25 -
9.26 - Calc ("Atools.is'_const",eval_const "#is_const_"),
9.27 - Calc ("Atools.occurs'_in", eval_occurs_in ""),
9.28 - Calc ("Tools.matches",eval_matches ""),
9.29 -
9.30 - Calc ("Groups.plus_class.plus",eval_binop "#add_"),
9.31 - Calc ("Groups.times_class.times",eval_binop "#mult_"),
9.32 - Calc ("Atools.pow" ,eval_binop "#power_"),
9.33 -
9.34 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
9.35 - Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
9.36 -
9.37 - Calc ("Atools.ident",eval_ident "#ident_")],
9.38 - scr = Prog ((term_of o the o (parse thy))
9.39 - "empty_script")
9.40 - }:rls
9.41 - )]);
9.42 -
9.43 "----------- for correction of diff_const ---------------";
9.44 "----------- for correction of diff_const ---------------";
9.45 "----------- for correction of diff_const ---------------";
10.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Oct 24 15:00:44 2013 +0200
10.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Oct 24 17:24:47 2013 +0200
10.3 @@ -38,9 +38,9 @@
10.4 overwrite (al, b);
10.5 overwritelthy thy (al, bl);
10.6
10.7 -case assoc' (! ruleset',"e_rls") of
10.8 +case assoc' ((KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of
10.9 SOME ("Tools", Rls _) => ()
10.10 -| _ => error "e_rls not in ! ruleset'"
10.11 +| _ => error "e_rls not in Theory_Data"
10.12
10.13 assoc_rls "e_rls";
10.14
10.15 @@ -80,7 +80,7 @@
10.16 val thy' = "Test";
10.17 val rlss = filter ((curry op= thy') o
10.18 ((#1 o #2):(rls' * (theory' * rls)) -> theory'))
10.19 - (!ruleset');
10.20 + (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
10.21 collect_rlss ("IsacKnowledge",thy');
10.22
10.23 "collect_thy thy-------------------------------------------------";
10.24 @@ -388,7 +388,7 @@
10.25 val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
10.26 val ancestors_rls =
10.27 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
10.28 - (rev (!ruleset'));
10.29 + (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
10.30
10.31 case assoc (ancestors_rls, rls') of
10.32 SOME ("Poly", Rls {id = "discard_minus", ...}) => ()