1.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 24 16:47:31 2022 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Thu May 26 12:44:51 2022 +0200
1.3 @@ -50,7 +50,8 @@
1.4 and find out, which ML_file or *.thy causes an error (might be ONLY one).
1.5 Also backup files (#* ) recognised by jEdit cause this trouble *)
1.6 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.7 - "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"
1.8 +(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
1.9 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
1.10 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
1.11 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
1.12 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
1.13 @@ -62,27 +63,30 @@
1.14 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
1.15 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
1.16 ADDTESTS/------------------------------------------- see end of tests *)
1.17 -(*/--- these work directly from Pure, but create problems here ..
1.18 +(*/~~~ these work directly from Pure, but create problems here ..
1.19 "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
1.20 "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
1.21 "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
1.22 "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
1.23 "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
1.24 - \--- .. these work independently, but create problems here *)
1.25 -(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Check_Outer_Syntax"
1.26 + \~~~ .. these work independently, but create problems here *)
1.27 (**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
1.28 -(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Term"
1.29 +(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
1.30 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.31 "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
1.32 "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
1.33 "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
1.34 +(**)
1.35 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
1.36 "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
1.37 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
1.38 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
1.39 +(**)
1.40
1.41 begin
1.42
1.43 +declare [[ML_print_depth = 20]]
1.44 +
1.45 ML \<open>open ML_System\<close>
1.46 ML \<open>
1.47 open Kernel;
1.48 @@ -129,51 +133,22 @@
1.49 open Rewrite_Ord
1.50 open UnparseC
1.51 \<close>
1.52 -ML_file "BaseDefinitions/libraryC.sml"
1.53
1.54 -section \<open>code for copy & paste ===============================================================\<close>
1.55 ML \<open>
1.56 "~~~~~ fun xxx , args:"; val () = ();
1.57 "~~~~~ and xxx , args:"; val () = ();
1.58 -"~~~~~ fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
1.59 -(*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*);
1.60 +"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
1.61 +(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
1.62 "xx"
1.63 -^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
1.64 -(*/------------------- step into XXXXX -----------------------------------------------------\*)
1.65 -(*-------------------- stop step into XXXXX -------------------------------------------------*)
1.66 -(*\------------------- step into XXXXX -----------------------------------------------------/*)
1.67 -(*-------------------- contiue step into XXXXX ----------------------------------------------*)
1.68 -(*/------------------- check entry to XXXXX ------------------------------------------------\*)
1.69 -(*\------------------- check entry to XXXXX ------------------------------------------------/*)
1.70 -(*/------------------- check within XXXXX --------------------------------------------------\*)
1.71 -(*\------------------- check within XXXXX --------------------------------------------------/*)
1.72 -(*/------------------- check result of XXXXX -----------------------------------------------\*)
1.73 -(*\------------------- check result of XXXXX -----------------------------------------------/*)
1.74 -(* final test ...*)
1.75 -(*/------------------- build new fun XXXXX -------------------------------------------------\*)
1.76 -(*\------------------- build new fun XXXXX -------------------------------------------------/*)
1.77 +^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
1.78 +\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
1.79 \<close> ML \<open>
1.80 +\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
1.81 +Rewrite.trace_on := false;
1.82 \<close>
1.83 ML \<open>
1.84 \<close> ML \<open>
1.85 \<close> ML \<open>
1.86 -\<close>
1.87 -text \<open>
1.88 - declare [[show_types]]
1.89 - declare [[show_sorts]]
1.90 - find_theorems "?a <= ?a"
1.91 -
1.92 - print_theorems
1.93 - print_facts
1.94 - print_statement ""
1.95 - print_theory
1.96 - ML_command \<open>Pretty.writeln prt\<close>
1.97 - declare [[ML_print_depth = 999]]
1.98 - declare [[ML_exception_trace]]
1.99 -\<close>
1.100 -
1.101 -section \<open>===================================================================================\<close>
1.102 -ML \<open>
1.103 \<close> ML \<open>
1.104 \<close> ML \<open>
1.105 \<close> ML \<open>
1.106 @@ -189,8 +164,6 @@
1.107 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
1.108 \<close>
1.109
1.110 -(*---------------------- check test file by testfile -------------------------------------------
1.111 - ---------------------- check test file by testfile -------------------------------------------*)
1.112 section \<open>trials with Isabelle's functions\<close>
1.113 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.114 ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
1.115 @@ -202,6 +175,7 @@
1.116 section \<open>test ML Code of isac\<close>
1.117 subsection \<open>basic code first\<close>
1.118 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
1.119 + ML_file "BaseDefinitions/base-definitions.sml"
1.120 ML_file "BaseDefinitions/libraryC.sml"
1.121 ML_file "BaseDefinitions/rule-def.sml"
1.122 ML_file "BaseDefinitions/eval-def.sml"
1.123 @@ -216,9 +190,9 @@
1.124 ML_file "BaseDefinitions/calcelems.sml"
1.125 ML_file "BaseDefinitions/termC.sml"
1.126 ML_file "BaseDefinitions/substitution.sml"
1.127 - ML_file "BaseDefinitions/contextC.sml"
1.128 + ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*)
1.129 ML_file "BaseDefinitions/environment.sml"
1.130 - ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
1.131 +(** )ML_file "BaseDefinitions/kestore.sml"( *setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
1.132 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.133 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
1.134
1.135 @@ -259,7 +233,7 @@
1.136 ML_file "MathEngBasic/thmC.sml"
1.137 ML_file "MathEngBasic/rewrite.sml"
1.138 ML_file "MathEngBasic/tactic.sml"
1.139 - ML_file "MathEngBasic/ctree.sml"
1.140 + ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
1.141 ML_file "MathEngBasic/calculation.sml"
1.142
1.143 ML_file "Specify/formalise.sml"
1.144 @@ -294,7 +268,6 @@
1.145
1.146 ML_file "BridgeLibisabelle/thy-present.sml"
1.147 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
1.148 - ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*)
1.149 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
1.150 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
1.151 ML_file "BridgeLibisabelle/interface.sml"
1.152 @@ -306,9 +279,9 @@
1.153 ML_file "Knowledge/delete.sml"
1.154 ML_file "Knowledge/descript.sml"
1.155 ML_file "Knowledge/simplify.sml"
1.156 - ML_file "Knowledge/poly.sml"
1.157 ML_file "Knowledge/gcd_poly_ml.sml"
1.158 - ML_file "Knowledge/rational.sml" (*Test_Isac_Short*)
1.159 + ML_file "Knowledge/rational-1.sml"
1.160 + ML_file "Knowledge/rational-2.sml" (*Test_Isac_Short*)
1.161 ML_file "Knowledge/equation.sml"
1.162 ML_file "Knowledge/root.sml"
1.163 ML_file "Knowledge/lineq.sml"
1.164 @@ -325,7 +298,8 @@
1.165 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
1.166 ML_file "Knowledge/diff.sml"
1.167 ML_file "Knowledge/integrate.sml"
1.168 - ML_file "Knowledge/eqsystem.sml"
1.169 + ML_file "Knowledge/eqsystem-1.sml"
1.170 + ML_file "Knowledge/eqsystem-2.sml"
1.171 ML_file "Knowledge/test.sml"
1.172 ML_file "Knowledge/polyminus.sml"
1.173 ML_file "Knowledge/vect.sml"