1 (* Title: test/Tools/isac/build_thydata.sml
2 Author: Walther Neuper, TU Graz, 2010
3 (c) due to copyright terms
5 theory Test_Some imports Isac.Build_Isac begin
6 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
7 ML_file "Knowledge/build_thydata.sml"
10 "-----------------------------------------------------------------";
11 "-----------------------------------------------------------------";
12 "table of contents -----------------------------------------------";
13 "-----------------------------------------------------------------";
14 "----------- retrieve errpats ------------------------------------";
15 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
16 "-----------------------------------------------------------------";
17 "-----------------------------------------------------------------";
18 "-----------------------------------------------------------------";
20 "----------- retrieve errpats ------------------------------------";
21 "----------- retrieve errpats ------------------------------------";
22 "----------- retrieve errpats ------------------------------------";
23 val {errpats, nrls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
24 case errpats of [("chain-rule-diff-both", _, _)] => ()
25 | _ => error "errpats chain-rule-diff-both changed"
27 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
28 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
29 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
30 (* "declare [[ML_print_depth = 999]]" *before* opening structure Applicable
31 slows down KEStore_Elems.get_rlss in collect_part in Build_Thydata.thy
32 such, that it hangs (probably due to some full buffer)
33 test below compiled with
35 imports "~~/src/Tools/isac/Knowledge/Isac" "~~/src/Tools/isac/Interpret/Interpret"
36 "~~/src/Tools/isac/Knowledge/Test_Build_Thydata"
39 (*/----- cp from Build_Thydata.thy -----------------------------------------------------------\*)
40 val knowledge_parent = @{theory} (* should be Build_Thydata.thy, replaced by above imports;
41 original = {Pure, .., Inverse_Z_Transform, Isac, Test_Build_Thydata, Build_Thydata:12}
42 here = {Pure, .., Inverse_Z_Transform, Isac, Test_Build_Thydata, Test_Theory:111} *)
43 val proglang_parent = @{theory ProgLang}
44 val allthys = Theory.ancestors_of @{theory};
45 val allthys = filter_out (Library.member Context.eq_thy (* thys for isac bootstrap *)
46 [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory MathEngine},
47 @{theory BridgeLibisabelle}, knowledge_parent]) allthys (*["Isac_Knowledge", ..., "Pure"]*)
48 val isabthys' = (*["Complex_Main", "Taylor", .., "Pure"]*)
49 drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
50 val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "Know_Store"]*)
51 take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
52 val knowthys' = (*["Isac_Knowledge", .., "Descript", "Delete"]*)
53 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
54 val progthys' = (*["Program", "Tools", "ListC", "Know_Store"]*)
55 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
56 val isacrlsthms = (*length = 460*)
57 thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.id * thm) list
58 val rlsthmsNOTisac = isacrlsthms (*length = 36*)
59 |> filter (fn (deriv, _) =>
60 Library.member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
61 : (ThmC.id * thm) list
63 (*\----- cp from Build_Thydata.thy -----------------------------------------------------------/*)
64 (*val thydata_list = ...*)
65 (map (collect_isab "Isabelle") rlsthmsNOTisac); (* OK *)
66 collect_part "IsacScripts" proglang_parent progthys'; (* OK *)
67 (*collect_part "IsacKnowledge" knowledge_parent knowthys' (* NOT terminating *)*)
69 "~~~~~ fun collect_part , args:"; val (part, parent, thys) =
70 ("IsacKnowledge", knowledge_parent, knowthys');
71 (map (collect_thms part) thys); (* OK *)
72 (*(collect_rlss part (KEStore_Elems.get_rlss parent) thys)(* NOT terminating *)*)
73 (*KEStore_Elems.get_rlss parent (* NOT terminating *)*)
75 "~~~~~ fun get_rlss , args:"; val () = ();
76 parent; (* = {Pure, .., Inverse_Z_Transform, Isac, Test_Build_Thydata, Test_Theory:111}*)
78 (*/----- save time in Test_Isac.thy ----------------------------------------------------------
79 (* rls are stored cumulatively vvv we try them by bisection *)
80 (*KEStore_Elems.get_rlss @{theory Isac_Knowledge} (* NOT terminating *)*)
81 (*KEStore_Elems.get_rlss @{theory Inverse_Z_Transform} (* NOT terminating *)*)
82 KEStore_Elems.get_rlss @{theory Biegelinie}; (* very very very slow *)
83 KEStore_Elems.get_rlss @{theory PolyEq}; (* OK, very very slow *)
84 KEStore_Elems.get_rlss @{theory RootRatEq}; (* OK, very slow *)
85 KEStore_Elems.get_rlss @{theory RootRat}; (* OK, slow *)
86 KEStore_Elems.get_rlss @{theory RootEq}; (* OK *)
87 \----- save time in Test_Isac.thy ----------------------------------------------------------/*)