1.1 --- a/test/Tools/isac/Test_Isac.thy Tue Apr 03 17:29:54 2018 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Apr 04 12:41:03 2018 +0200
1.3 @@ -183,7 +183,113 @@
1.4 ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
1.5 ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
1.6 ML_file "xmlsrc/thy-hierarchy.sml"
1.7 - ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
1.8 +
1.9 +ML {*
1.10 +"~~~~~ fun xxx, args:"; val () = ();
1.11 +*} ML {*
1.12 +"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
1.13 +"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
1.14 +"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
1.15 + val isacrlsthms = KEStore_Elems.get_rlss @{theory Test_Build_Thydata}
1.16 +(* CHANGE FOR CODE ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.17 + |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "list_rls" (*unpleasant in test*)
1.18 + |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rrls" (*unpleasant in test*)
1.19 + |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rls" (*unpleasant in test*)
1.20 + |> thms_of_rlss @{theory} (*length = 4*)
1.21 +
1.22 + val rlsthmsNOTisac = isacrlsthms (*length = 2*)
1.23 + |> filter (fn (deriv, _) =>
1.24 + member op= (map Context.theory_name isabthys') (thyID_of_derivation_name deriv))
1.25 +;
1.26 +val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])
1.27 +;
1.28 +val thydata_list =
1.29 + collect_part "IsacKnowledge" knowledge_parent knowthys' @
1.30 + (map (collect_isab "Isabelle") rlsthmsNOTisac) @
1.31 + collect_part "IsacScripts" proglang_parent progthys' (* only the thms, no rls *)
1.32 +;
1.33 +*} ML {*
1.34 +thydata_list
1.35 +(*
1.36 + [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
1.37 + Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111",
1.38 + mathauthors = ["isac-team"], thm = "?thm111.0 = ?thm111.0 + 111"}),
1.39 + (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],
1.40 + Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222",
1.41 + mathauthors = ["isac-team"], thm = "?thm222.0 = ?thm222.0 + 222"}),
1.42 + (["Isabelle", "HOL", "Theorems", "refl"],
1.43 + Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl", mathauthors =
1.44 + ["Isabelle team, TU Munich"], thm = "?t = ?t"}),
1.45 + (["Isabelle", "Fun", "Theorems", "o_def"],
1.46 + Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_Fun-thm-o_def", mathauthors =
1.47 + ["Isabelle team, TU Munich"], thm = "?f \<circ> ?g = (\<lambda>x. ?f (?g x))"}),
1.48 + (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],
1.49 + Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111",
1.50 + mathauthors = ["isac-team"], thm = "?thm111.0 = ?thm111.0 + 111"}),
1.51 + (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],
1.52 + Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222",
1.53 + mathauthors = ["isac-team"], thm = "?thm222.0 = ?thm222.0 + 222"})]
1.54 +*)
1.55 +*} ML {*
1.56 +*} ML {*
1.57 +case thydata_list of (*length = 8*)
1.58 + [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
1.59 + Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111",
1.60 + mathauthors = ["isac-team"], thm = _}),
1.61 + (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],
1.62 + Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222",
1.63 + mathauthors = ["isac-team"], thm = _}),
1.64 + (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls111"],
1.65 + Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111",
1.66 + mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
1.67 + (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls222"],
1.68 + Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222",
1.69 + mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
1.70 + (["Isabelle", "HOL", "Theorems", "refl"],
1.71 + Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl",
1.72 + mathauthors = ["Isabelle team, TU Munich"], thm = _}),
1.73 + (["Isabelle", "Fun", "Theorems", "o_def"], Hthm {coursedesign = [], fillpats = [],
1.74 + guh = "thy_isab_Fun-thm-o_def", mathauthors = ["Isabelle team, TU Munich"], thm = _}),
1.75 + (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],
1.76 + Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111",
1.77 + mathauthors = ["isac-team"], thm = _}),
1.78 + (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],
1.79 + Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222",
1.80 + mathauthors = ["isac-team"], thm = _})] => ()
1.81 +| _ => error "collect thydata from Test_Build_Thydata changed";
1.82 +;
1.83 +(* we store locally on MINIthehier instead on KEStore, see KEStore: *)
1.84 + fun add_the (thydata, theID) = add_thydata ([], theID) thydata;
1.85 +val thes = map (fn (a, b) => (b, a)) thydata_list
1.86 +val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata});
1.87 +*} ML {*
1.88 +"~~~~~ fun xxx, args:"; val () = ();
1.89 +*} ML {*
1.90 +*} ML {*
1.91 +*} ML {*
1.92 +*} ML {*
1.93 +*} ML {*
1.94 +*} ML {*
1.95 +*} ML {*
1.96 +*} ML {*
1.97 +*} ML {*
1.98 +*} ML {*
1.99 +*} ML {*
1.100 +*} ML {*
1.101 +*} ML {*
1.102 +*} ML {*
1.103 +*} ML {*
1.104 +"~~~~~ fun xxx, args:"; val () = ();
1.105 +*}
1.106 +
1.107 +
1.108 +
1.109 +
1.110 +
1.111 +
1.112 +
1.113 +
1.114 +ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
1.115 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
1.116 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
1.117 ML_file "Frontend/messages.sml"