1.1 --- a/test/Tools/isac/Interpret/mathengine.sml Sun Jun 22 14:47:36 2014 +0200
1.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Sun Jun 22 14:58:51 2014 +0200
1.3 @@ -238,7 +238,7 @@
1.4 "~~~~~ fun fetchErrorpatterns, args:"; val (tac) = (tac);
1.5 val rlsID = "e_rls"
1.6 val (part, thyID) = thy_containing_rls "Build_Thydata" rlsID;
1.7 -if part = "IsacKnowledge" andalso thyID = "KEStore" then ()
1.8 +if part = "IsacScripts" andalso thyID = "KEStore" then ()
1.9 else error "fetchErrorpatterns .. e_rls changed";
1.10 (* val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]
1.11 ERROR app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
2.1 --- a/test/Tools/isac/Interpret/rewtools.sml Sun Jun 22 14:47:36 2014 +0200
2.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Sun Jun 22 14:58:51 2014 +0200
2.3 @@ -1,8 +1,10 @@
2.4 (* Title: test for rewtools.sml
2.5 authors: Walther Neuper 2000, 2006
2.6
2.7 -theory Test_Some imports Isac begin
2.8 +theory Test_Some imports Build_Thydata begin
2.9 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
2.10 +ML {* KEStore_Elems.set_ref_thy @{theory};
2.11 + fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
2.12 ML_file "Interpret/rewtools.sml"
2.13 *)
2.14
2.15 @@ -10,10 +12,6 @@
2.16 "--------------------------------------------------------";
2.17 "table of contents --------------------------------------";
2.18 "--------------------------------------------------------";
2.19 -(*============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! =================
2.20 -"----------- fun make_isab ------------------------------";
2.21 -"----------- fun collect_isab_thys ----------------------";
2.22 -============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ===============*)
2.23 "----------- fun thy_containing_rls ---------------------";
2.24 "----------- fun thy_containing_cal ---------------------";
2.25 (*============ inhibit exn WN120321 ==============================================
2.26 @@ -36,204 +34,29 @@
2.27 "--------------------------------------------------------";
2.28 "--------------------------------------------------------";
2.29
2.30 -"----------- fun make_isab ------------------------------";
2.31 -"----------- fun make_isab ------------------------------";
2.32 -(*============ inhibit exn WN120321 ==============================================
2.33 -"----------- fun make_isab ------------------------------";
2.34 -(* rlsthmsNOTisac: contains thms in rls requested from Isabelle ---" *)
2.35 -map #1 (rlsthmsNOTisac : (string * term) list) = (*WN101011, Isabelle2009-2*)
2.36 -["refl", "o_apply", "del_base", "del_rec", "LENGTH_CONS", "LENGTH_NIL",
2.37 - "list_diff_def", "take_Nil", "take_Cons", "if_True", "if_False",
2.38 - "sym_real_mult_minus1", "distrib_right", "distrib_left",
2.39 - "sym_realpow_twoI", "sym_realpow_addI", "mult_1_right",
2.40 - "sym_real_mult_2", "mult_1_left", "mult_zero_left", "mult_zero_right",
2.41 - "add_0_left", "add_0_right", "divide_zero_left", "sym_mult_assoc",
2.42 - "order_refl", "minus_minus", "mult_commute", "mult_assoc",
2.43 - "add_commute", "add_left_commute", "add_assoc", "minus_mult_left",
2.44 - "right_minus", "sym_add_assoc", "left_diff_distrib",
2.45 - "right_diff_distrib", "minus_divide_left", "times_divide_eq_right",
2.46 - "times_divide_eq_left", "divide_divide_eq_left",
2.47 - "divide_divide_eq_right", "divide_1", "add_divide_distrib",
2.48 - "sym_rmult_assoc"];
2.49 -if length rlsthmsNOTisac > 34 then ()
2.50 -else error "rewtools.sml: some rlsthmsNOTisac dropped";
2.51 -
2.52 -"----- FIXME.WN11xxxx: rlsthmsNOTisac DOES contain thms from isac ---";
2.53 -map (thmID_of_derivation_name o #1) rlsthmsNOTisac;
2.54 -"----- FIXME.WN11xxxx: sym_* in rlsthmsNOTisac DOES contain thms from isac ---";
2.55 -val symthms = [("real_mult_minus1", @{thm real_mult_minus1}),
2.56 - ("realpow_twoI", @{thm realpow_twoI}),
2.57 - ("realpow_addI", @{thm realpow_addI}),
2.58 - ("real_mult_2", @{thm real_mult_2}),
2.59 - ("mult_assoc", @{thm mult_assoc}),
2.60 - ("add_assoc", @{thm add_assoc}),
2.61 - ("rmult_assoc", @{thm rmult_assoc})];
2.62 -map (Thm.derivation_name o #2) symthms;
2.63 -
2.64 -"----------- fun collect_isab_thys ----------------------";
2.65 -"----------- fun collect_isab_thys ----------------------";
2.66 -"----------- fun collect_isab_thys ----------------------";
2.67 -val ancestors = Theory.ancestors_of @{theory "Complex_Main"};
2.68 -val isabthms = (flat o (map Theory.axioms_of)) ancestors;
2.69 -
2.70 -val isacrules = (flat o (map (thms_of_rls o #2 o #2)))
2.71 - (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
2.72 -(*thms from rulesets*)
2.73 -(*=== inhibit exn AK110725 =============================================================
2.74 -val isacrlsthms = ((map rep_thm_G') o flat o
2.75 - (map (PureThy.all_thms_of_rls o #2 o #2)))
2.76 - (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
2.77 -length isacrlsthms;
2.78 -(*takes a few seconds...
2.79 -val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
2.80 -length isacrlsthms;
2.81 -"----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv";
2.82 -print_depth 99; map #1 isacrlsthms; print_depth 3;
2.83 -"----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^";
2.84 -...*)
2.85 -
2.86 -
2.87 -(!theory');
2.88 -map #2 (!theory');
2.89 -map (PureThy.all_thms_of o #2) (!theory');
2.90 -val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');
2.91 -(*takes a few seconds...
2.92 -val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
2.93 -length rlsthmsNOTisac;
2.94 -"----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv";
2.95 -print_depth 99; map #1 rlsthmsNOTisac; print_depth 3;
2.96 -"----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^";
2.97 -...*)
2.98 -
2.99 -"----- for 'fun make_isab_thm_thy'";
2.100 -inter eq_thmI isacrlsthms (PureThy.all_thms_of (nth 1 ancestors));
2.101 -inter eq_thmI;
2.102 -(inter eq_thmI);
2.103 -(inter eq_thmI) isacrlsthms;
2.104 -(*takes a few seconds...
2.105 -curry (inter eq_thmI) isacrlsthms (PureThy.all_thms_of (nth 9 ancestors));
2.106 -
2.107 -val thy = (nth 52 ancestors);
2.108 -val sec = ((inter eq_thmI) isacrlsthms o PureThy.all_thms_of) (nth 52 ancestors);
2.109 -length (PureThy.all_thms_of (nth 9 ancestors));
2.110 -length sec;
2.111 -...*)
2.112 -(*takes 1 minute...
2.113 -print_depth 99;
2.114 -map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors;
2.115 -print_depth 3;
2.116 -*)
2.117 -
2.118 -(*takes some seconds...
2.119 -val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac)))
2.120 - ((#ancestors o rep_theory) first_isac_thy);
2.121 -print_depth 99; isab_thm_thy; print_depth 3;
2.122 -*)
2.123 -=== inhibit exn AK110725 =============================================================*)
2.124 -============ inhibit exn WN120321 ==============================================*)
2.125 -
2.126 -
2.127 -
2.128 "----------- fun thy_containing_rls ---------------------";
2.129 "----------- fun thy_containing_rls ---------------------";
2.130 "----------- fun thy_containing_rls ---------------------";
2.131 -infix mem; (*from Isabelle2002*)
2.132 -fun x mem [] = false
2.133 - | x mem (y :: ys) = x = y orelse x mem ys;
2.134 -
2.135 -val thy' = "Biegelinie";
2.136 - val dropthys =
2.137 - takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
2.138 - (rev (!theory'));
2.139 -
2.140 -(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
2.141 -if length (!theory') <> length dropthys then ()
2.142 -else error "thy_containing_rls changed 1";
2.143 -
2.144 - val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;
2.145 -
2.146 -if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"](*, "Biegelinie",..,"Test",.*)
2.147 -then () else error "thy_containing_rls changed ancestors_rls";
2.148 -
2.149 -"Isac" mem dropthys';
2.150 -op mem ("Isac", dropthys');
2.151 -(op mem) o swap;
2.152 -((op mem) o swap) (dropthys', "Isac");
2.153 -curry ((op mem) o swap);
2.154 -curry ((op mem) o swap) dropthys' "Isac";
2.155 - val ancestors_rls =
2.156 - filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
2.157 - (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
2.158 -
2.159 -take (10, map #1 ancestors_rls) =
2.160 - ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation",
2.161 - "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*)
2.162 -
2.163 -(* WN120523 popped up again ?!?!?
2.164 -if length (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then ()
2.165 -else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?";
2.166 -*)
2.167 -
2.168 -val rls' = "norm_Poly";
2.169 -case assoc (ancestors_rls, rls') of
2.170 - SOME (thy', _) => thyID2theory' thy'
2.171 - | _ => error ("thy_containing_rls : rls '" ^ rls' ^
2.172 - "' not in !rulset' und thy '" ^ thy' ^ "'");
2.173 -
2.174 -if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly") then ()
2.175 -else error "thy_containing_rls 3: changed with (Biegelinie, norm_Poly)";
2.176 -
2.177 -"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie" ,"norm_Poly");
2.178 - val rls' = strip_thy rls'
2.179 - val thy' = thyID2theory' thy'
2.180 - val dropthys =
2.181 - takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
2.182 - (rev (!theory'));
2.183 -
2.184 -map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"]; (*= true WN120410*)
2.185 -
2.186 - val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
2.187 - val ancestors_rls =
2.188 - filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
2.189 - (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
2.190 -
2.191 -case assoc (ancestors_rls, rls') of
2.192 - SOME ("Poly", Seq {id = "norm_Poly", ...}) => ()
2.193 -| _ => error "thy_containing_rls changed 2";
2.194 -============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
2.195 -
2.196 +if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
2.197 +else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
2.198 +;
2.199 +if thy_containing_rls "Biegelinie" "e_rls" = ("IsacScripts", "KEStore") then ()
2.200 +else error ("thy_containing_rls changed for 'Biegelinie', 'e_rls'")
2.201 +;
2.202 +if thy_containing_rls "Build_Thydata" "list_rls" = (*FIXME: handle redifinition in several thys*)
2.203 + ("IsacScripts", "Tools") then ()
2.204 +else error ("thy_containing_rls changed for 'Biegelinie', 'list_rls'")
2.205 +;
2.206 +if thy_containing_rls "Biegelinie" "list_rls" = (*FIXME: handle redifinition in several thys*)
2.207 + ("IsacKnowledge", "Atools") then ()
2.208 +else error ("thy_containing_rls changed for 'Biegelinie', 'list_rls'")
2.209
2.210 "----------- fun thy_containing_cal ---------------------";
2.211 "----------- fun thy_containing_cal ---------------------";
2.212 "----------- fun thy_containing_cal ---------------------";
2.213 -val thy' = "Atools";
2.214 - val dropthys =
2.215 - takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
2.216 - (rev (!theory'));
2.217 -
2.218 -length dropthys <> length (!theory');
2.219 -
2.220 - val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;
2.221 -
2.222 -(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
2.223 -if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", "Biegelinie",
2.224 - "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate",
2.225 - "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq",
2.226 - "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify"] (*, "Atools", ..*)
2.227 -then () else error "thy_containing_cal changed ancestors_rls for Atools";
2.228 -
2.229 -Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev;
2.230 -Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map #1;
2.231 -Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map (#1 : calc -> string);
2.232 -
2.233 - val ancestors_cal =
2.234 - filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))
2.235 - (Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev);
2.236 -
2.237 -if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "plus")
2.238 - (*WN120410: SHOULD BE = ("IsacKnowledge", "Atools")*)
2.239 -then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed";
2.240 -============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
2.241 +(* ATTENTION: both, "IsacKnowledge" and "Atools" are fixed as results for any input*)
2.242 +if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Atools")
2.243 +then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"
2.244
2.245 "----------- initContext Thy_ Integration-demo ----------";
2.246 "----------- initContext Thy_ Integration-demo ----------";
3.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Sun Jun 22 14:47:36 2014 +0200
3.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Sun Jun 22 14:58:51 2014 +0200
3.3 @@ -363,7 +363,7 @@
3.4 "----------- correct theIDs for e_rls ----------------------------";
3.5 "----------- correct theIDs for e_rls ----------------------------";
3.6 "----------- correct theIDs for e_rls ----------------------------";
3.7 -if thy_containing_rls "Build_Thydata" "e_rls" = ("IsacKnowledge", "KEStore") then ()
3.8 +if thy_containing_rls "Build_Thydata" "e_rls" = ("IsacScripts", "KEStore") then ()
3.9 else error "thy_containing_rls e_rls changed";
3.10 show_thes ();
3.11 (*shows different assignment for "e_rls"...
3.12 @@ -374,7 +374,7 @@
3.13 "----------- correct theIDs for list_rls -------------------------";
3.14 "----------- correct theIDs for list_rls -------------------------";
3.15 "----------- correct theIDs for list_rls -------------------------";
3.16 -if thy_containing_rls "Build_Thydata" "list_rls" = ("IsacKnowledge", "Tools") then ()
3.17 +if thy_containing_rls "Build_Thydata" "list_rls" = ("IsacScripts", "Tools") then ()
3.18 else error "thy_containing_rls list_rls changed";
3.19 show_thes ();
3.20 (*shows different assignment for "list_rls"...