1.1 --- a/test/Tools/isac/Test_Isac.thy Wed Aug 28 07:08:25 2019 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Aug 28 11:21:26 2019 +0200
1.3 @@ -94,12 +94,13 @@
1.4 open Math_Engine; CalcTreeTEST;
1.5 open Lucin; itms2args;
1.6 open LucinNEW; appy;
1.7 - open Istate;
1.8 + open Istate;
1.9 open Inform; cas_input;
1.10 open Rtools; trtas2str;
1.11 open Chead; pt_extract;
1.12 open Generate; (* NONE *)
1.13 open Ctree; append_problem;
1.14 + open Input_Descript;
1.15 open Specify; show_ptyps;
1.16 open Applicable; mk_set;
1.17 open Solve; (* NONE *)
1.18 @@ -140,6 +141,7 @@
1.19 ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.20
1.21 section \<open>test ML Code of isac\<close>
1.22 +subsection \<open>basic code first\<close>
1.23 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
1.24 ML_file "CalcElements/libraryC.sml"
1.25 ML_file "CalcElements/calcelems.sml"
1.26 @@ -155,8 +157,8 @@
1.27 ML_file "ProgLang/tools.sml"
1.28 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.29 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
1.30 - ML \<open>"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";\<close>
1.31 - ML \<open>"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";\<close>
1.32 +
1.33 +subsection \<open>basic functionality on simple example first\<close>
1.34 ML_file "Minisubpbl/000-comments.sml"
1.35 ML_file "Minisubpbl/100-init-rootpbl.sml"
1.36 ML_file "Minisubpbl/150-add-given.sml"
1.37 @@ -171,8 +173,8 @@
1.38 ML_file "Minisubpbl/600-postcond.sml"
1.39 ML_file "Minisubpbl/700-interSteps.sml"
1.40 ML_file "Minisubpbl/799-complete.sml"
1.41 - ML \<open>"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.42 - ML \<open>"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";\<close>
1.43 +
1.44 +subsection \<open>further functionality alongside batch build sequence\<close>
1.45 ML_file "Specify/mstools.sml"
1.46 ML_file "Specify/specification-elems.sml"
1.47 ML_file "Specify/ctree.sml" (*!...!see(25)*)
1.48 @@ -181,30 +183,26 @@
1.49 ML_file "Specify/generate.sml"
1.50 ML_file "Specify/calchead.sml"
1.51 ML_file "Specify/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
1.52 +
1.53 ML_file "Interpret/rewtools.sml"
1.54 ML_file "Interpret/script.sml"
1.55 ML_file "Interpret/inform.sml"
1.56 ML_file "Interpret/lucas-interpreter.sml"
1.57 - ML_file "Interpret/solve.sml"
1.58 - ML_file "Interpret/mathengine.sml" (*!part. WN130804: +check Interpret/me.sml*)
1.59 - ML \<open>"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";\<close>
1.60 - ML \<open>"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";\<close>
1.61 - ML_file "xmlsrc/mathml.sml" (*part.*)
1.62 - ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
1.63 - ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
1.64 - ML_file "xmlsrc/thy-hierarchy.sml"
1.65 - ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
1.66 - ML \<open>"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.67 - ML \<open>"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";\<close>
1.68 - ML_file "Frontend/messages.sml"
1.69 - ML_file "Frontend/states.sml"
1.70 - ML_file "Frontend/interface.sml"
1.71 - ML_file "Frontend/use-cases.sml"
1.72 +
1.73 + ML_file "MathEngine/solve.sml"
1.74 + ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
1.75 + ML_file "MathEngine/messages.sml"
1.76 + ML_file "MathEngine/states.sml"
1.77 +
1.78 + ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
1.79 + ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*)
1.80 + ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
1.81 + ML_file "BridgeLibisabelle/thy-hierarchy.sml"
1.82 + ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
1.83 + ML_file "BridgeLibisabelle/interface.sml"
1.84 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
1.85 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
1.86 - ML_file "print_exn_G.sml"
1.87 - ML \<open>"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";\<close>
1.88 - ML \<open>"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";\<close>
1.89 +
1.90 ML_file "Knowledge/delete.sml"
1.91 ML_file "Knowledge/descript.sml"
1.92 ML_file "Knowledge/atools.sml"
1.93 @@ -242,11 +240,12 @@
1.94 ML_file "Knowledge/inssort.sml"
1.95 ML_file "Knowledge/isac.sml"
1.96 ML_file "Knowledge/build_thydata.sml"
1.97 - ML \<open>"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.98 - ML \<open>"%%%%%%%%%%%%%%%%% start ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.99 +
1.100 +section \<open>tests additional to src/.. files\<close>
1.101 + ML_file "BridgeLibisabelle/use-cases.sml"
1.102 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
1.103 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
1.104 - ML \<open>"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.105 +
1.106 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.107 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.108 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>