Walther@60424
|
1 |
(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
|
wneuper@59553
|
2 |
Author: Walther Neuper 101001
|
wneuper@59553
|
3 |
(c) copyright due to license terms.
|
wneuper@59553
|
4 |
|
wneuper@59553
|
5 |
Isac's tests are organised parallel to sources:
|
wenzelm@60192
|
6 |
$ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
|
wneuper@59553
|
7 |
plus
|
wenzelm@60217
|
8 |
$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS
|
wenzelm@60217
|
9 |
$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
|
walther@59935
|
10 |
|
walther@59935
|
11 |
Note, that only the first error in a file is shown here.
|
wneuper@59553
|
12 |
*)
|
wneuper@59553
|
13 |
|
walther@59623
|
14 |
section \<open>Notes on running tests\<close>
|
walther@59623
|
15 |
subsection \<open>Switch between running tests and updating code\<close>
|
wneuper@59553
|
16 |
text \<open>
|
walther@59623
|
17 |
Isac encapsulates code as much as possible in structures without open.
|
walther@59623
|
18 |
This policy conflicts with those tests, which go into functions to details
|
walther@59623
|
19 |
not declared in the signatures.
|
walther@59623
|
20 |
\<close>
|
walther@59623
|
21 |
subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
|
walther@59623
|
22 |
text \<open>
|
walther@59623
|
23 |
Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")
|
walther@59623
|
24 |
if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).
|
walther@59626
|
25 |
This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
|
walther@59626
|
26 |
A model is in the repository at ~~/etc/preferences.
|
walther@59623
|
27 |
These preferences have drawbacks, however:
|
walther@59623
|
28 |
* they claim more memory such that Isabelle instances canNOT run in parallel.
|
walther@59623
|
29 |
* they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.
|
wneuper@59553
|
30 |
|
walther@59623
|
31 |
So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.
|
walther@59623
|
32 |
From time to time full testing in Test_Isac.thy is recommended. For that purpose
|
walther@59626
|
33 |
* set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
|
wneuper@59553
|
34 |
|
walther@59964
|
35 |
\\******************* don't forget to re-set defaults BEFORE updating code *******************//
|
walther@59623
|
36 |
|
walther@59626
|
37 |
Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use
|
walther@59626
|
38 |
***************** $ gedit ~/.isabelle/isabisac/etc/preferences &
|
wneuper@59553
|
39 |
\<close>
|
wneuper@59553
|
40 |
|
wneuper@59553
|
41 |
section \<open>Run the tests\<close>
|
wneuper@59553
|
42 |
text \<open>
|
wneuper@59553
|
43 |
* say "OK" to the popup asking for theories to be loaded
|
wneuper@59553
|
44 |
* watch the <Theories> window for errors in the "imports" below
|
wneuper@59553
|
45 |
\<close>
|
wneuper@59553
|
46 |
|
walther@59623
|
47 |
theory Test_Isac_Short
|
walther@59603
|
48 |
imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
|
walther@59997
|
49 |
(* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one
|
walther@59997
|
50 |
and find out, which ML_file or *.thy causes an error (might be ONLY one).
|
walther@59997
|
51 |
Also backup files (#* ) recognised by jEdit cause this trouble *)
|
wneuper@59553
|
52 |
(*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
|
Walther@60519
|
53 |
(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
|
walther@60387
|
54 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
|
wenzelm@60217
|
55 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
|
wenzelm@60217
|
56 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
|
wenzelm@60217
|
57 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
|
wenzelm@60217
|
58 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
|
wenzelm@60217
|
59 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
|
Walther@60519
|
60 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
|
wenzelm@60217
|
61 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
|
wenzelm@60217
|
62 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
|
wneuper@59553
|
63 |
(*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
|
wneuper@59553
|
64 |
ADDTESTS/------------------------------------------- see end of tests *)
|
walther@60317
|
65 |
(*/~~~ these work directly from Pure, but create problems here ..
|
wenzelm@60217
|
66 |
"$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
|
wenzelm@60217
|
67 |
"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
|
wenzelm@60217
|
68 |
"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
|
wenzelm@60217
|
69 |
"$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
|
wenzelm@60217
|
70 |
"$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
|
walther@60317
|
71 |
\~~~ .. these work independently, but create problems here *)
|
wenzelm@60217
|
72 |
(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
|
wenzelm@60217
|
73 |
(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
|
wneuper@59553
|
74 |
(*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
|
wenzelm@60217
|
75 |
"$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
|
wenzelm@60217
|
76 |
"$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
|
wenzelm@60217
|
77 |
"$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
|
walther@60317
|
78 |
(** )
|
wneuper@59553
|
79 |
(*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
|
wenzelm@60192
|
80 |
(*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
|
wenzelm@60192
|
81 |
(*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*)
|
wneuper@59556
|
82 |
(*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
|
walther@60317
|
83 |
( **)
|
Walther@60491
|
84 |
"$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
|
wneuper@59553
|
85 |
|
wneuper@59553
|
86 |
begin
|
wneuper@59553
|
87 |
|
Walther@60640
|
88 |
declare [[ML_print_depth = 20]] (*otherwise buffer overflow*)
|
wenzelm@60240
|
89 |
|
walther@59628
|
90 |
ML \<open>open ML_System\<close>
|
wneuper@59553
|
91 |
ML \<open>
|
wneuper@59553
|
92 |
open Kernel;
|
walther@59814
|
93 |
open Math_Engine;
|
Walther@60571
|
94 |
open Test_Code; Test_Code.init_calc @{context};
|
walther@59848
|
95 |
open LItool; arguments_from_model;
|
walther@59817
|
96 |
open Sub_Problem;
|
walther@59823
|
97 |
open Fetch_Tacs;
|
walther@59814
|
98 |
open Step
|
walther@59659
|
99 |
open Env;
|
walther@59814
|
100 |
open LI; scan_dn;
|
walther@59617
|
101 |
open Istate;
|
walther@59909
|
102 |
open Error_Pattern;
|
walther@59909
|
103 |
open Error_Pattern_Def;
|
walther@59977
|
104 |
open Specification;
|
wneuper@59553
|
105 |
open Ctree; append_problem;
|
walther@59696
|
106 |
open Pos;
|
walther@59618
|
107 |
open Program;
|
wneuper@59601
|
108 |
open Prog_Tac;
|
walther@59603
|
109 |
open Tactical;
|
walther@59603
|
110 |
open Prog_Expr;
|
walther@59618
|
111 |
open Auto_Prog; rule2stac;
|
wneuper@59600
|
112 |
open Input_Descript;
|
walther@59971
|
113 |
open Specify;
|
walther@59976
|
114 |
open Specify;
|
walther@59763
|
115 |
open Step_Specify;
|
walther@59749
|
116 |
open Step_Solve;
|
walther@59763
|
117 |
open Step;
|
wneuper@59553
|
118 |
open Solve; (* NONE *)
|
wneuper@59577
|
119 |
open ContextC; transfer_asms_from_to;
|
walther@59814
|
120 |
open Tactic; (* NONE *)
|
walther@60126
|
121 |
open I_Model;
|
walther@60126
|
122 |
open O_Model;
|
walther@60126
|
123 |
open P_Model; (* NONE *)
|
walther@59872
|
124 |
open Rewrite;
|
walther@59878
|
125 |
open Eval; get_pair;
|
Walther@60650
|
126 |
open TermC;
|
walther@59858
|
127 |
open Rule;
|
walther@59878
|
128 |
open Rule_Set; Sequence;
|
walther@59919
|
129 |
open Eval_Def
|
walther@59854
|
130 |
open ThyC
|
walther@59865
|
131 |
open ThmC_Def
|
walther@59858
|
132 |
open ThmC
|
walther@59857
|
133 |
open Rewrite_Ord
|
Walther@60608
|
134 |
open UnparseC;
|
Walther@60608
|
135 |
|
Walther@60608
|
136 |
Know_Store.set_ref_last_thy @{theory};
|
Walther@60608
|
137 |
(*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)
|
wenzelm@60223
|
138 |
\<close>
|
wneuper@59553
|
139 |
|
Walther@60737
|
140 |
section \<open>code for copy & paste ===============================================================\<close>
|
Walther@60737
|
141 |
text \<open>
|
Walther@60737
|
142 |
declare [[show_types]]
|
Walther@60737
|
143 |
declare [[show_sorts]]
|
Walther@60737
|
144 |
find_theorems "?a <= ?a"
|
Walther@60737
|
145 |
|
Walther@60737
|
146 |
print_theorems
|
Walther@60737
|
147 |
print_facts
|
Walther@60737
|
148 |
print_statement ""
|
Walther@60737
|
149 |
print_theory
|
Walther@60737
|
150 |
ML_command \<open>Pretty.writeln prt\<close>
|
Walther@60737
|
151 |
declare [[ML_print_depth = 999]]
|
Walther@60737
|
152 |
declare [[ML_exception_trace]]
|
Walther@60737
|
153 |
\<close>
|
wneuper@59553
|
154 |
ML \<open>
|
Walther@60737
|
155 |
\<close> ML \<open>
|
walther@59659
|
156 |
"~~~~~ fun xxx , args:"; val () = ();
|
walther@59659
|
157 |
"~~~~~ and xxx , args:"; val () = ();
|
walther@59814
|
158 |
"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
|
Walther@60578
|
159 |
"~~~~~ continue fun xxx"; val () = ();
|
Walther@60729
|
160 |
(*if*) (*then*); (*else*); (*andalso*) (*case*) (*of*); (*return value*); (*in*) (*end*);
|
walther@59659
|
161 |
"xx"
|
Walther@60629
|
162 |
^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
|
Walther@60729
|
163 |
\<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)
|
Walther@60729
|
164 |
(*//------------------ build fun XXXXX -----------------------------------------------------\\*)
|
Walther@60729
|
165 |
(*\\------------------ build fun XXXXX -----------------------------------------------------//*)
|
Walther@60729
|
166 |
\<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
|
Walther@60729
|
167 |
val return_XXXXX = "XXXXX"
|
Walther@60578
|
168 |
\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
|
Walther@60578
|
169 |
(*//------------------ step into XXXXX -----------------------------------------------------\\*)
|
Walther@60756
|
170 |
\<close> ML \<open> (*||----------- contine-- XXXXX -------------------------------------------------------*)
|
Walther@60756
|
171 |
(*||------------------ contine-- XXXXX -------------------------------------------------------*)
|
Walther@60578
|
172 |
(*\\------------------ step into XXXXX -----------------------------------------------------//*)
|
Walther@60578
|
173 |
\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
|
Walther@60729
|
174 |
val "XXXXX" = return_XXXXX;
|
Walther@60578
|
175 |
|
Walther@60578
|
176 |
(* final test ... ----------------------------------------------------------------------------*)
|
Walther@60578
|
177 |
|
Walther@60578
|
178 |
\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
|
Walther@60578
|
179 |
(*//------------------ inserted hidden code ------------------------------------------------\\*)
|
Walther@60578
|
180 |
(*\\------------------ inserted hidden code ------------------------------------------------//*)
|
Walther@60578
|
181 |
\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
|
walther@59723
|
182 |
\<close>
|
walther@59723
|
183 |
ML \<open>
|
walther@59723
|
184 |
\<close> ML \<open>
|
Walther@60733
|
185 |
|
walther@59851
|
186 |
\<close> ML \<open>
|
wneuper@59553
|
187 |
\<close>
|
wneuper@59553
|
188 |
|
wneuper@59553
|
189 |
section \<open>trials with Isabelle's functions\<close>
|
wneuper@59553
|
190 |
ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
Walther@60424
|
191 |
ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
|
wenzelm@60217
|
192 |
ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
|
wenzelm@60217
|
193 |
ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
|
wenzelm@60217
|
194 |
ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
|
wneuper@59553
|
195 |
ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59553
|
196 |
|
wneuper@59553
|
197 |
section \<open>test ML Code of isac\<close>
|
wneuper@59600
|
198 |
subsection \<open>basic code first\<close>
|
wneuper@59553
|
199 |
ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
|
walther@60413
|
200 |
ML_file "BaseDefinitions/base-definitions.sml"
|
walther@59866
|
201 |
ML_file "BaseDefinitions/libraryC.sml"
|
walther@59866
|
202 |
ML_file "BaseDefinitions/rule-def.sml"
|
walther@59919
|
203 |
ML_file "BaseDefinitions/eval-def.sml"
|
Walther@60624
|
204 |
ML_file "BaseDefinitions/rewrite-order.sml"
|
walther@59866
|
205 |
ML_file "BaseDefinitions/theoryC.sml"
|
walther@59866
|
206 |
ML_file "BaseDefinitions/rule.sml"
|
walther@59866
|
207 |
ML_file "BaseDefinitions/thmC-def.sml"
|
Walther@60624
|
208 |
ML_file "BaseDefinitions/model-pattern.sml"
|
walther@59866
|
209 |
ML_file "BaseDefinitions/error-fill-def.sml"
|
walther@59866
|
210 |
ML_file "BaseDefinitions/rule-set.sml"
|
walther@59892
|
211 |
ML_file "BaseDefinitions/check-unique.sml"
|
walther@59932
|
212 |
(*called by Know_Store..*)
|
walther@59866
|
213 |
ML_file "BaseDefinitions/calcelems.sml"
|
walther@59866
|
214 |
ML_file "BaseDefinitions/termC.sml"
|
walther@59912
|
215 |
ML_file "BaseDefinitions/substitution.sml"
|
Walther@60558
|
216 |
ML_file "BaseDefinitions/contextC.sml"(*sometimes needs separation into ML blocks for evaluation*)
|
walther@59866
|
217 |
ML_file "BaseDefinitions/environment.sml"
|
Walther@60424
|
218 |
(**)ML_file "BaseDefinitions/kestore.sml"(*setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
|
wneuper@59553
|
219 |
(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
|
wneuper@59553
|
220 |
---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
|
walther@59932
|
221 |
|
walther@60317
|
222 |
ML_file "ProgLang/calculate.sml"
|
walther@59964
|
223 |
ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
|
walther@59633
|
224 |
ML_file "ProgLang/listC.sml"
|
walther@59633
|
225 |
ML_file "ProgLang/prog_expr.sml"
|
walther@59633
|
226 |
ML_file "ProgLang/program.sml"
|
walther@59633
|
227 |
ML_file "ProgLang/prog_tac.sml"
|
walther@59763
|
228 |
ML_file "ProgLang/tactical.sml"
|
walther@60326
|
229 |
ML_file "ProgLang/auto_prog.sml"
|
wneuper@59553
|
230 |
(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
|
wneuper@59553
|
231 |
---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
|
wneuper@59600
|
232 |
|
wneuper@59600
|
233 |
subsection \<open>basic functionality on simple example first\<close>
|
wneuper@59553
|
234 |
ML_file "Minisubpbl/000-comments.sml"
|
wneuper@59553
|
235 |
ML_file "Minisubpbl/100-init-rootpbl.sml"
|
Walther@60578
|
236 |
ML_file "Minisubpbl/150a-add-given-Maximum.sml"
|
Walther@60590
|
237 |
ML_file "Minisubpbl/150-add-given-Equation.sml"
|
walther@59781
|
238 |
ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
|
Walther@60755
|
239 |
ML_file "Minisubpbl/200-start-method.sml"
|
wneuper@59553
|
240 |
ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
|
walther@59722
|
241 |
ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
|
wneuper@59553
|
242 |
ML_file "Minisubpbl/300-init-subpbl.sml"
|
wneuper@59553
|
243 |
ML_file "Minisubpbl/400-start-meth-subpbl.sml"
|
wneuper@59553
|
244 |
ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
|
walther@59722
|
245 |
ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
|
wneuper@59553
|
246 |
ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
|
wneuper@59553
|
247 |
ML_file "Minisubpbl/500-met-sub-to-root.sml"
|
wneuper@59553
|
248 |
ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
|
walther@59781
|
249 |
ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"
|
wneuper@59553
|
250 |
ML_file "Minisubpbl/600-postcond.sml"
|
wneuper@59553
|
251 |
ML_file "Minisubpbl/700-interSteps.sml"
|
walther@59820
|
252 |
ML_file "Minisubpbl/710-interSteps-short.sml"
|
walther@59836
|
253 |
ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
|
walther@59686
|
254 |
ML_file "Minisubpbl/790-complete.sml"
|
walther@60340
|
255 |
ML_file "Minisubpbl/800-append-on-Frm.sml"
|
wneuper@59600
|
256 |
|
wneuper@59600
|
257 |
subsection \<open>further functionality alongside batch build sequence\<close>
|
walther@59865
|
258 |
ML_file "MathEngBasic/thmC.sml"
|
Walther@60624
|
259 |
ML_file "MathEngBasic/problem.sml"
|
walther@60389
|
260 |
ML_file "MathEngBasic/rewrite.sml"
|
walther@59728
|
261 |
ML_file "MathEngBasic/tactic.sml"
|
Walther@60519
|
262 |
ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
|
Walther@60697
|
263 |
ML_file "MathEngBasic/references.sml"
|
walther@59774
|
264 |
ML_file "MathEngBasic/calculation.sml"
|
walther@59763
|
265 |
|
walther@59996
|
266 |
ML_file "Specify/formalise.sml"
|
walther@59952
|
267 |
ML_file "Specify/o-model.sml"
|
Walther@60729
|
268 |
ML_file "Specify/i-model.sml" (* (BROKEN!) test on elementwise input to lists*)
|
Walther@60757
|
269 |
ML \<open>
|
Walther@60757
|
270 |
\<close> ML \<open>
|
Walther@60757
|
271 |
"----------- build I_Model.s_make_complete -----------------------------------------------------";
|
Walther@60757
|
272 |
"----------- build I_Model.s_make_complete -----------------------------------------------------";
|
Walther@60757
|
273 |
"----------- build I_Model.s_make_complete -----------------------------------------------------";
|
Walther@60757
|
274 |
val (_(*example text*),
|
Walther@60757
|
275 |
(model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
|
Walther@60757
|
276 |
"Extremum (A = 2 * u * v - u \<up> 2)" ::
|
Walther@60757
|
277 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60757
|
278 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60757
|
279 |
"SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
|
Walther@60757
|
280 |
(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
|
Walther@60757
|
281 |
"FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
|
Walther@60757
|
282 |
"Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
|
Walther@60757
|
283 |
"ErrorBound (\<epsilon> = (0::real))" :: []),
|
Walther@60757
|
284 |
refs as ("Diff_App",
|
Walther@60757
|
285 |
["univariate_calculus", "Optimisation"],
|
Walther@60757
|
286 |
["Optimisation", "by_univariate_calculus"])))
|
Walther@60757
|
287 |
= Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
|
Walther@60757
|
288 |
|
Walther@60757
|
289 |
val c = [];
|
Walther@60757
|
290 |
val (p,_,f,nxt,_,pt) =
|
Walther@60757
|
291 |
Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
|
Walther@60757
|
292 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
Walther@60757
|
293 |
|
Walther@60757
|
294 |
(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
|
Walther@60757
|
295 |
val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of
|
Walther@60757
|
296 |
PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}
|
Walther@60757
|
297 |
=> (o_model, (pbl_imod, met_imod), (pI, mI))
|
Walther@60757
|
298 |
| _ => raise ERROR ""
|
Walther@60757
|
299 |
|
Walther@60757
|
300 |
val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
|
Walther@60757
|
301 |
(1, [1, 2, 3], true, "#undef", (Cor_TEST (@{term Constants},
|
Walther@60757
|
302 |
[@{term "[r = (7::real)]"}]), Position.none)),
|
Walther@60757
|
303 |
(1, [1, 2], true, "#undef", (Cor_TEST (@{term SideConditions},
|
Walther@60757
|
304 |
[@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]
|
Walther@60757
|
305 |
|
Walther@60757
|
306 |
val met_imod = [ (*1 item for creating code*)
|
Walther@60757
|
307 |
(8, [2], true, "#undef", (Cor_TEST (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]
|
Walther@60757
|
308 |
;
|
Walther@60757
|
309 |
(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
|
Walther@60757
|
310 |
(*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
|
Walther@60757
|
311 |
(*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
|
Walther@60757
|
312 |
(*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
|
Walther@60757
|
313 |
(*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
|
Walther@60757
|
314 |
(*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
|
Walther@60757
|
315 |
(*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
|
Walther@60757
|
316 |
(*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
|
Walther@60757
|
317 |
(*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
|
Walther@60757
|
318 |
(*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
|
Walther@60757
|
319 |
(*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
|
Walther@60757
|
320 |
(*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
|
Walther@60757
|
321 |
(*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
|
Walther@60757
|
322 |
then () else error "setup test data for I_Model.s_make_complete CHANGED";
|
Walther@60757
|
323 |
(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
|
Walther@60757
|
324 |
|
Walther@60757
|
325 |
val return_s_make_complete =
|
Walther@60757
|
326 |
s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);
|
Walther@60757
|
327 |
(*/------------------- step into s_make_complete -------------------------------------------\\*)
|
Walther@60757
|
328 |
"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pI, mI)) =
|
Walther@60757
|
329 |
(o_model, (pbl_imod, met_imod), (pI, mI));
|
Walther@60757
|
330 |
val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id;
|
Walther@60757
|
331 |
val {model = met_patt, ...} = MethodC.from_store ctxt met_id;
|
Walther@60757
|
332 |
val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
|
Walther@60757
|
333 |
val i_from_pbl = map (fn (_, (descr, _)) =>
|
Walther@60757
|
334 |
Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
|
Walther@60757
|
335 |
\<close> ML \<open>
|
Walther@60757
|
336 |
val [] = i_from_pbl
|
Walther@60757
|
337 |
\<close> ML \<open>
|
Walther@60757
|
338 |
|
Walther@60757
|
339 |
(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
|
Walther@60757
|
340 |
"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
|
Walther@60757
|
341 |
(@{term Constants}, pbl_max_vnts, pbl_imod);
|
Walther@60757
|
342 |
val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
|
Walther@60757
|
343 |
| SOME descr' => if descr = descr' then true else false) i_model
|
Walther@60757
|
344 |
;
|
Walther@60757
|
345 |
(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr: I_Model.T_TEST
|
Walther@60757
|
346 |
;
|
Walther@60757
|
347 |
val return_get_descr_vnt_1 =
|
Walther@60757
|
348 |
case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
|
Walther@60757
|
349 |
[] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
|
Walther@60757
|
350 |
| items => Library.the_single items (*only applied to model_patt, which has each descr once*)
|
Walther@60757
|
351 |
(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
|
Walther@60757
|
352 |
\<close> ML \<open>
|
Walther@60757
|
353 |
\<close> ML \<open>
|
Walther@60757
|
354 |
|
Walther@60757
|
355 |
(*|------------------- continue s_make_complete ----------------------------------------------*)
|
Walther@60757
|
356 |
val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
|
Walther@60757
|
357 |
if is_empty_single_TEST i_single
|
Walther@60757
|
358 |
then
|
Walther@60757
|
359 |
case get_descr_vnt' feedb pbl_max_vnts o_model of
|
Walther@60757
|
360 |
(*-----------^^^^^^^^^^^^^^-----------------------------*)
|
Walther@60757
|
361 |
[] => raise ERROR (msg pbl_max_vnts feedb)
|
Walther@60757
|
362 |
| o_singles => map transfer_terms o_singles
|
Walther@60757
|
363 |
else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
|
Walther@60757
|
364 |
|
Walther@60757
|
365 |
\<close> ML \<open>
|
Walther@60757
|
366 |
(*+*)val [2, 1] = vnts;
|
Walther@60757
|
367 |
\<close> ML \<open>
|
Walther@60757
|
368 |
val "[]" = (pbl_from_o_model |> I_Model.to_string_TEST @{context})
|
Walther@60757
|
369 |
\<close> ML \<open>
|
Walther@60757
|
370 |
(*+*)if (pbl_from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
|
Walther@60757
|
371 |
"(1, [1, 2, 3], true ,#undef, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
|
Walther@60757
|
372 |
"(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
|
Walther@60757
|
373 |
"(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
|
Walther@60757
|
374 |
"(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
|
Walther@60757
|
375 |
"(1, [1, 2], true ,#undef, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
|
Walther@60757
|
376 |
then () else error "pbl_from_o_model CHANGED 1"
|
Walther@60757
|
377 |
|
Walther@60757
|
378 |
\<close> ML \<open>
|
Walther@60757
|
379 |
(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
|
Walther@60757
|
380 |
"~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
|
Walther@60757
|
381 |
(*if*) is_empty_single_TEST i_single (*else*);
|
Walther@60757
|
382 |
get_descr_vnt' feedb pbl_max_vnts o_model;
|
Walther@60757
|
383 |
|
Walther@60757
|
384 |
val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
|
Walther@60757
|
385 |
if is_empty_single_TEST i_single
|
Walther@60757
|
386 |
then
|
Walther@60757
|
387 |
case get_descr_vnt' feedb pbl_max_vnts o_model of
|
Walther@60757
|
388 |
(*---------- ^^^^^^^^^^^^^^ ----------------------------*)
|
Walther@60757
|
389 |
[] => raise ERROR (msg pbl_max_vnts feedb)
|
Walther@60757
|
390 |
| o_singles => map transfer_terms o_singles
|
Walther@60757
|
391 |
else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
|
Walther@60757
|
392 |
(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
|
Walther@60757
|
393 |
|
Walther@60757
|
394 |
(*|------------------- continue s_make_complete ----------------------------------------------*)
|
Walther@60757
|
395 |
val i_from_met = map (fn (_, (descr, _)) =>
|
Walther@60757
|
396 |
Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
|
Walther@60757
|
397 |
;
|
Walther@60757
|
398 |
(*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
|
Walther@60757
|
399 |
"(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
|
Walther@60757
|
400 |
"(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
|
Walther@60757
|
401 |
"(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
|
Walther@60757
|
402 |
"(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^
|
Walther@60757
|
403 |
"(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
|
Walther@60757
|
404 |
(*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)
|
Walther@60757
|
405 |
"(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
|
Walther@60757
|
406 |
"(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
|
Walther@60757
|
407 |
"(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
|
Walther@60757
|
408 |
(*+*)then () else error "s_make_complete: from_met CHANGED";
|
Walther@60757
|
409 |
;
|
Walther@60757
|
410 |
val met_max_vnts = Model_Def.max_variants o_model i_from_met;
|
Walther@60757
|
411 |
(*+*)val [2] = met_max_vnts
|
Walther@60757
|
412 |
|
Walther@60757
|
413 |
val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
|
Walther@60757
|
414 |
val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
|
Walther@60757
|
415 |
if is_empty_single_TEST i_single
|
Walther@60757
|
416 |
then
|
Walther@60757
|
417 |
case get_descr_vnt' feedb [met_max_vnt] o_model of
|
Walther@60757
|
418 |
[] => raise ERROR (msg [met_max_vnt] feedb)
|
Walther@60757
|
419 |
| o_singles => map transfer_terms o_singles
|
Walther@60757
|
420 |
else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
|
Walther@60757
|
421 |
;
|
Walther@60757
|
422 |
(*+*)if (met_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
|
Walther@60757
|
423 |
"(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
|
Walther@60757
|
424 |
"(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
|
Walther@60757
|
425 |
"(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
|
Walther@60757
|
426 |
"(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
|
Walther@60757
|
427 |
"(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
|
Walther@60757
|
428 |
"(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
|
Walther@60757
|
429 |
"(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
|
Walther@60757
|
430 |
"(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
|
Walther@60757
|
431 |
(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
|
Walther@60757
|
432 |
;
|
Walther@60757
|
433 |
val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)
|
Walther@60757
|
434 |
(*\------------------- step into s_make_complete -------------------------------------------//*)
|
Walther@60757
|
435 |
;
|
Walther@60757
|
436 |
if return_s_make_complete = return_s_make_complete_step
|
Walther@60757
|
437 |
then () else error "s_make_complete: stewise construction <> value of fun"
|
Walther@60757
|
438 |
|
Walther@60757
|
439 |
|
Walther@60757
|
440 |
|
Walther@60757
|
441 |
\<close> ML \<open>
|
Walther@60757
|
442 |
\<close>
|
walther@59996
|
443 |
ML_file "Specify/pre-conditions.sml"
|
walther@59996
|
444 |
ML_file "Specify/p-model.sml"
|
walther@59985
|
445 |
ML_file "Specify/m-match.sml"
|
walther@59967
|
446 |
ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
|
Walther@60757
|
447 |
ML \<open>
|
Walther@60757
|
448 |
\<close> ML \<open>
|
Walther@60757
|
449 |
|
Walther@60757
|
450 |
\<close> ML \<open>
|
Walther@60757
|
451 |
\<close>
|
walther@59996
|
452 |
ML_file "Specify/test-out.sml"
|
walther@59996
|
453 |
ML_file "Specify/specify-step.sml"
|
walther@59996
|
454 |
ML_file "Specify/specification.sml"
|
walther@59996
|
455 |
ML_file "Specify/cas-command.sml"
|
walther@59996
|
456 |
ML_file "Specify/p-spec.sml"
|
walther@59996
|
457 |
ML_file "Specify/specify.sml"
|
Walther@60610
|
458 |
ML_file "Specify/sub-problem.sml"
|
walther@59800
|
459 |
ML_file "Specify/step-specify.sml"
|
walther@59813
|
460 |
|
walther@59860
|
461 |
ML_file "Interpret/istate.sml"
|
walther@60389
|
462 |
ML_file "Interpret/error-pattern.sml"
|
walther@59790
|
463 |
ML_file "Interpret/li-tool.sml"
|
walther@60340
|
464 |
ML_file "Interpret/lucas-interpreter.sml"
|
walther@59751
|
465 |
ML_file "Interpret/step-solve.sml"
|
walther@59751
|
466 |
|
walther@60326
|
467 |
ML_file "MathEngine/me-misc.sml"
|
walther@59823
|
468 |
ML_file "MathEngine/fetch-tactics.sml"
|
walther@60326
|
469 |
ML_file "MathEngine/solve.sml"
|
walther@59763
|
470 |
ML_file "MathEngine/step.sml"
|
Walther@60624
|
471 |
ML_file "MathEngine/mathengine-stateless.sml"
|
walther@60326
|
472 |
ML_file "MathEngine/messages.sml"
|
wneuper@59600
|
473 |
ML_file "MathEngine/states.sml"
|
wneuper@59600
|
474 |
|
wneuper@59600
|
475 |
ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
|
walther@60277
|
476 |
ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
|
Walther@60424
|
477 |
ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
|
walther@60389
|
478 |
ML_file "BridgeLibisabelle/interface.sml"
|
Walther@60603
|
479 |
|
Walther@60730
|
480 |
(**) (* evaluated in Build_Isac.thy already *)
|
Walther@60692
|
481 |
ML_file "BridgeJEdit/e-collect.sml"
|
Walther@60692
|
482 |
ML_file "BridgeJEdit/user-model.sml"
|
Walther@60696
|
483 |
ML_file "BridgeJEdit/template.sml"
|
walther@60146
|
484 |
ML_file "BridgeJEdit/preliminary.sml"
|
Walther@60697
|
485 |
ML_file "BridgeJEdit/calculation.sml"
|
Walther@60465
|
486 |
ML_file "BridgeJEdit/vscode-example.sml"
|
Walther@60730
|
487 |
(**)
|
walther@60044
|
488 |
|
wneuper@59553
|
489 |
ML_file "Knowledge/delete.sml"
|
wneuper@59553
|
490 |
ML_file "Knowledge/descript.sml"
|
wneuper@59553
|
491 |
ML_file "Knowledge/simplify.sml"
|
walther@60340
|
492 |
ML_file "Knowledge/poly-1.sml"
|
walther@60329
|
493 |
(*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*)
|
wneuper@59553
|
494 |
ML_file "Knowledge/gcd_poly_ml.sml"
|
walther@60329
|
495 |
ML_file "Knowledge/rational-1.sml"
|
walther@60329
|
496 |
(*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*)
|
Walther@60519
|
497 |
ML_file "Knowledge/equation.sml"
|
walther@60384
|
498 |
ML_file "Knowledge/root.sml"
|
wneuper@59553
|
499 |
ML_file "Knowledge/lineq.sml"
|
wneuper@59553
|
500 |
(*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
|
walther@59628
|
501 |
(*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*)
|
walther@60389
|
502 |
ML_file "Knowledge/rootrat.sml"
|
Walther@60729
|
503 |
ML_file "Knowledge/rootrateq.sml"(*one complicated equations not recovered from 2002 *)
|
walther@59628
|
504 |
(*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
|
walther@60393
|
505 |
ML_file "Knowledge/polyeq-1.sml"
|
walther@60393
|
506 |
(*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*)
|
wneuper@59553
|
507 |
(*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
|
wneuper@59553
|
508 |
ML_file "Knowledge/calculus.sml"
|
wneuper@59553
|
509 |
ML_file "Knowledge/trig.sml"
|
wneuper@59553
|
510 |
(*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
|
walther@60350
|
511 |
ML_file "Knowledge/diff.sml"
|
walther@60350
|
512 |
ML_file "Knowledge/integrate.sml"
|
Walther@60706
|
513 |
(*see TODO WN230404* )
|
walther@60347
|
514 |
ML_file "Knowledge/eqsystem-1.sml"
|
Walther@60556
|
515 |
ML_file "Knowledge/eqsystem-1a.sml"
|
walther@60395
|
516 |
ML_file "Knowledge/eqsystem-2.sml"
|
Walther@60706
|
517 |
( **)
|
walther@59996
|
518 |
ML_file "Knowledge/test.sml"
|
Walther@60624
|
519 |
ML_file "Knowledge/polyminus.sml"
|
wneuper@59553
|
520 |
ML_file "Knowledge/vect.sml"
|
Walther@60458
|
521 |
ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *)
|
walther@60396
|
522 |
ML_file "Knowledge/biegelinie-1.sml"
|
walther@59628
|
523 |
(*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*)
|
walther@59628
|
524 |
(*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*)
|
walther@60398
|
525 |
ML_file "Knowledge/biegelinie-4.sml"
|
walther@60326
|
526 |
ML_file "Knowledge/algein.sml"
|
wneuper@59553
|
527 |
ML_file "Knowledge/diophanteq.sml"
|
walther@59628
|
528 |
(*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
|
wneuper@59553
|
529 |
ML_file "Knowledge/inssort.sml"
|
wneuper@59553
|
530 |
ML_file "Knowledge/isac.sml"
|
wneuper@59600
|
531 |
|
walther@59814
|
532 |
ML_file "Test_Code/test-code.sml"
|
walther@59814
|
533 |
|
walther@59617
|
534 |
section \<open>further tests additional to src/.. files\<close>
|
walther@60399
|
535 |
ML_file "BridgeLibisabelle/use-cases.sml"
|
wneuper@59600
|
536 |
|
wneuper@59553
|
537 |
ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59553
|
538 |
ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59553
|
539 |
ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
walther@60262
|
540 |
ML \<open>
|
walther@60262
|
541 |
\<close> ML \<open>
|
Walther@60754
|
542 |
|
walther@59804
|
543 |
\<close> ML \<open>
|
wneuper@59561
|
544 |
\<close>
|
wneuper@59553
|
545 |
|
wneuper@59553
|
546 |
section \<open>history of tests\<close>
|
wneuper@59553
|
547 |
text \<open>
|
wneuper@59553
|
548 |
Systematic regression tests have been introduced to isac development in 2003.
|
wneuper@59553
|
549 |
Sanity of the regression tests suffers from updates following Isabelle development,
|
wneuper@59553
|
550 |
which mostly exceeded the resources available in isac's development.
|
wneuper@59553
|
551 |
|
wneuper@59553
|
552 |
The survey below shall support to efficiently use the tests for isac
|
wneuper@59553
|
553 |
on different Isabelle versions. Conclusion in most cases will be:
|
wneuper@59553
|
554 |
|
wneuper@59553
|
555 |
!!! Use most recent tests or go back to the old notebook
|
wneuper@59553
|
556 |
with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
wneuper@59553
|
557 |
\<close>
|
wneuper@59553
|
558 |
|
wneuper@59553
|
559 |
|
wneuper@59553
|
560 |
subsection \<open>isac on Isabelle2017\<close>
|
wneuper@59553
|
561 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
562 |
text \<open>
|
wneuper@59553
|
563 |
* Add further signatures, separate structures and cleanup respective files.
|
wneuper@59553
|
564 |
* Show feasibility of moving Isac programs to partial_function, i.e. to the function package.
|
wneuper@59553
|
565 |
* Clean theory dependencies.
|
wneuper@59553
|
566 |
* Start preparing shift from isac-java to Isabelle/jEdit.
|
wneuper@59553
|
567 |
\<close>
|
wneuper@59553
|
568 |
subsubsection \<open>State of tests: unchanged\<close>
|
wneuper@59553
|
569 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
570 |
text \<open>
|
wneuper@59553
|
571 |
last changeset with Test_Isac 925fef0f4c81
|
wneuper@59553
|
572 |
first changeset with Test_Isac bbb414976dfe
|
wneuper@59553
|
573 |
\<close>
|
wneuper@59553
|
574 |
|
wneuper@59553
|
575 |
subsection \<open>isac on Isabelle2015\<close>
|
wneuper@59553
|
576 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
577 |
text \<open>
|
wneuper@59553
|
578 |
* Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
|
wneuper@59553
|
579 |
This complicates Test_Isac, see "Prepare running tests" above.
|
wneuper@59553
|
580 |
* Remove TTY interface.
|
wneuper@59553
|
581 |
* Re-activate insertion sort.
|
wneuper@59553
|
582 |
\<close>
|
wneuper@59553
|
583 |
subsubsection \<open>State of tests: unchanged\<close>
|
wneuper@59553
|
584 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
585 |
text \<open>
|
wneuper@59553
|
586 |
last changeset with Test_Isac 2f1b2854927a
|
wneuper@59553
|
587 |
first changeset with Test_Isac ???
|
wneuper@59553
|
588 |
\<close>
|
wneuper@59553
|
589 |
|
wneuper@59553
|
590 |
subsection \<open>isac on Isabelle2014\<close>
|
wneuper@59553
|
591 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
592 |
text \<open>
|
wneuper@59553
|
593 |
migration from "isabelle tty" --> libisabelle
|
wneuper@59553
|
594 |
\<close>
|
wneuper@59553
|
595 |
|
Walther@60424
|
596 |
subsection \<open>isac on Isabelle2013-2\<close>
|
wneuper@59553
|
597 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
598 |
text \<open>
|
wneuper@59553
|
599 |
reactivated context_thy
|
wneuper@59553
|
600 |
\<close>
|
wneuper@59553
|
601 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
602 |
text \<open>
|
wneuper@59553
|
603 |
TODO
|
wneuper@59553
|
604 |
\<close>
|
wneuper@59553
|
605 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
606 |
text \<open>
|
wneuper@59553
|
607 |
TODO
|
wneuper@59553
|
608 |
:
|
Walther@60424
|
609 |
: isac on Isablle2013-2
|
wneuper@59553
|
610 |
:
|
wneuper@59553
|
611 |
Changeset: 55318 (03826ceb24da) merged
|
wneuper@59553
|
612 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
613 |
Date: 2013-12-12 14:27:37 +0100 (7 minutes)
|
wneuper@59553
|
614 |
\<close>
|
wneuper@59553
|
615 |
|
Walther@60424
|
616 |
subsection \<open>isac on Isabelle2013-1\<close>
|
wneuper@59553
|
617 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
618 |
text \<open>
|
Walther@60424
|
619 |
Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
|
wneuper@59553
|
620 |
no significant development steps for ISAC.
|
wneuper@59553
|
621 |
\<close>
|
wneuper@59553
|
622 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
623 |
text \<open>
|
wneuper@59553
|
624 |
See points in subsection "isac on Isabelle2011", "State of tests".
|
wneuper@59553
|
625 |
\<close>
|
wneuper@59553
|
626 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
627 |
text \<open>
|
wneuper@59553
|
628 |
Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
|
wneuper@59553
|
629 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
630 |
Date: 2013-12-03 18:13:31 +0100 (8 days)
|
wneuper@59553
|
631 |
:
|
Walther@60424
|
632 |
: isac on Isablle2013-1
|
wneuper@59553
|
633 |
:
|
Walther@60424
|
634 |
Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
|
wneuper@59553
|
635 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
636 |
Date: 2013-11-21 18:12:17 +0100 (2 weeks)
|
wneuper@59553
|
637 |
|
wneuper@59553
|
638 |
\<close>
|
wneuper@59553
|
639 |
|
wneuper@59553
|
640 |
subsection \<open>isac on Isabelle2013\<close>
|
wneuper@59553
|
641 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
642 |
text \<open>
|
wneuper@59553
|
643 |
# Oct.13: replaced "axioms" by "axiomatization"
|
wneuper@59553
|
644 |
# Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
|
wneuper@59553
|
645 |
# Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
|
wneuper@59553
|
646 |
simplification of multivariate rationals (without improving the rulesets involved).
|
wneuper@59553
|
647 |
\<close>
|
wneuper@59553
|
648 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
649 |
text \<open>
|
Walther@60424
|
650 |
Is standard now; this subsection will be discontinued under Isabelle2013-1
|
wneuper@59553
|
651 |
\<close>
|
wneuper@59553
|
652 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
653 |
text \<open>
|
wneuper@59553
|
654 |
See points in subsection "isac on Isabelle2011", "State of tests".
|
wneuper@59553
|
655 |
# re-activated listC.sml
|
wneuper@59553
|
656 |
\<close>
|
wneuper@59553
|
657 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
658 |
text \<open>
|
wneuper@59553
|
659 |
changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
|
wneuper@59553
|
660 |
User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
|
wneuper@59553
|
661 |
Date: Tue Nov 19 22:23:30 2013 +0000
|
wneuper@59553
|
662 |
:
|
wneuper@59553
|
663 |
: isac on Isablle2013
|
wneuper@59553
|
664 |
:
|
wneuper@59553
|
665 |
Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
|
wneuper@59553
|
666 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
667 |
Date: 2013-07-15 08:28:50 +0200 (4 weeks)
|
wneuper@59553
|
668 |
\<close>
|
wneuper@59553
|
669 |
|
wneuper@59553
|
670 |
subsection \<open>isac on Isabelle2012\<close>
|
wneuper@59553
|
671 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
672 |
text \<open>
|
wneuper@59553
|
673 |
isac on Isabelle2012 is considered just a transitional stage
|
wneuper@59553
|
674 |
within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
|
wneuper@59553
|
675 |
For considerations on the transition see
|
wenzelm@60192
|
676 |
$ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..".
|
wneuper@59553
|
677 |
\<close>
|
wneuper@59553
|
678 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
679 |
text \<open>
|
wneuper@59553
|
680 |
$ cd /usr/local/isabisac12/
|
wneuper@59553
|
681 |
$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
|
wneuper@59553
|
682 |
$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
|
wneuper@59553
|
683 |
\<close>
|
wneuper@59553
|
684 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
685 |
text \<open>
|
wneuper@59553
|
686 |
At least the tests from isac on Isabelle2011 run again.
|
wneuper@59553
|
687 |
However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
|
wneuper@59553
|
688 |
in parallel with evaluation.
|
wneuper@59553
|
689 |
|
wneuper@59553
|
690 |
Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
|
Walther@60424
|
691 |
yields 69 hits, some of which were already present before Isabelle2002-->2009-2
|
wneuper@59553
|
692 |
(i.e. on the old notebook from 2002).
|
wneuper@59553
|
693 |
|
wneuper@59553
|
694 |
Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
|
wneuper@59553
|
695 |
# === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
|
wneuper@59553
|
696 |
# === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
|
Walther@60424
|
697 |
# === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
|
wneuper@59553
|
698 |
Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
|
wneuper@59553
|
699 |
|
wneuper@59553
|
700 |
Some tests have been re-activated (e.g. error patterns, fill patterns).
|
wneuper@59553
|
701 |
\<close>
|
wneuper@59553
|
702 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
703 |
text \<open>
|
wneuper@59553
|
704 |
Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
|
wneuper@59553
|
705 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
706 |
Date: 2013-07-11 16:58:31 +0200 (4 weeks)
|
wneuper@59553
|
707 |
:
|
wneuper@59553
|
708 |
: isac on Isablle2012
|
wneuper@59553
|
709 |
:
|
wneuper@59553
|
710 |
Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
|
wneuper@59553
|
711 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
712 |
Date: 2012-09-24 18:35:13 +0200 (8 months)
|
wneuper@59553
|
713 |
------------------------------------------------------------------------------
|
wneuper@59553
|
714 |
Changeset: 48756 (7443906996a8) merged
|
wneuper@59553
|
715 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
716 |
Date: 2012-09-24 18:15:49 +0200 (8 months)
|
wneuper@59553
|
717 |
\<close>
|
wneuper@59553
|
718 |
|
wneuper@59553
|
719 |
subsection \<open>isac on Isabelle2011\<close>
|
wneuper@59553
|
720 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
721 |
text \<open>
|
wneuper@59553
|
722 |
isac's mathematics engine has been extended by two developments:
|
wneuper@59553
|
723 |
(1) Isabelle's contexts were introduced by Mathias Lehnfeld
|
wneuper@59553
|
724 |
(2) Z_Transform was introduced by Jan Rocnik, which revealed
|
wneuper@59553
|
725 |
further errors introduced by (1).
|
wneuper@59553
|
726 |
(3) "error patterns" were introduced by Gabriella Daroczy
|
wneuper@59553
|
727 |
Regressions tests have been added for all of these.
|
wneuper@59553
|
728 |
\<close>
|
wneuper@59553
|
729 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
730 |
text \<open>
|
wneuper@59553
|
731 |
$ cd /usr/local/isabisac11/
|
wneuper@59553
|
732 |
$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
|
wneuper@59553
|
733 |
$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
|
wneuper@59553
|
734 |
\<close>
|
wneuper@59553
|
735 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
736 |
text \<open>
|
wneuper@59553
|
737 |
Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
|
wneuper@59553
|
738 |
and sometimes give reasons for failing tests.
|
wneuper@59553
|
739 |
(*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
|
wneuper@59553
|
740 |
work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
|
wneuper@59553
|
741 |
|
wneuper@59553
|
742 |
The most signification tests (in particular Frontend/interface.sml) run,
|
wneuper@59553
|
743 |
however, many "error in kernel" are not caught by an exception.
|
wneuper@59553
|
744 |
------------------------------------------------------------------------------
|
wneuper@59553
|
745 |
After the changeset below Test_Isac worked with check_unsynchronized_ref ():
|
wneuper@59553
|
746 |
------------------------------------------------------------------------------
|
wneuper@59553
|
747 |
Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
|
wneuper@59553
|
748 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
749 |
Date: 2012-08-06 10:38:11 +0200 (11 months)
|
wneuper@59553
|
750 |
|
wneuper@59553
|
751 |
|
wneuper@59553
|
752 |
The list below records TODOs while producing an ISAC kernel for
|
wneuper@59553
|
753 |
gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
|
Walther@60424
|
754 |
(so to be resumed with Isabelle2013-1):
|
wneuper@59553
|
755 |
############## WNxxxxxx.TODO can be found in sources ##############
|
wneuper@59553
|
756 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
757 |
WN111013.TODO: lots of cleanup/removal in test/../Test.thy
|
wneuper@59553
|
758 |
--------------------------------------------------------------------------------
|
walther@59845
|
759 |
WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with
|
wneuper@59553
|
760 |
this special case (see) --- why not nxt = Model_Problem here ? ---
|
wneuper@59553
|
761 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
762 |
WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
|
wneuper@59553
|
763 |
... FIRST redesign
|
wneuper@59553
|
764 |
# simplify_* , *_simp_*
|
wneuper@59553
|
765 |
# norm_*
|
wneuper@59553
|
766 |
# calc_* , calculate_* ... require iteration over all rls ...
|
wneuper@59553
|
767 |
... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
|
wneuper@59553
|
768 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
769 |
WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
|
wneuper@59553
|
770 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
771 |
WN120314 changeset a393bb9f5e9f drops root equations.
|
wneuper@59553
|
772 |
see test/Tools/isac/Knowledge/rootrateq.sml
|
wneuper@59553
|
773 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
774 |
WN120317.TODO changeset 977788dfed26 dropped rateq:
|
wneuper@59553
|
775 |
# test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
|
Walther@60424
|
776 |
# test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
|
wneuper@59553
|
777 |
investigation Check_elementwise stopped due to too much effort finding out,
|
wneuper@59553
|
778 |
why Check_elementwise worked in 2002 in spite of the error.
|
wneuper@59553
|
779 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
780 |
WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
|
wneuper@59553
|
781 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
782 |
WN120317.TODO found by test --- interSteps for Schalk 299a --- that
|
wneuper@59553
|
783 |
NO test with 'interSteps' is checked properly (with exn on changed behaviour)
|
wneuper@59553
|
784 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
785 |
WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
|
wneuper@59553
|
786 |
a newly outcommented test where rewrite_set_ make_polynomial --> NONE
|
wneuper@59553
|
787 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
788 |
WN120320.TODO check-improve rlsthmsNOTisac:
|
wneuper@59553
|
789 |
DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
|
Walther@60424
|
790 |
DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
|
wneuper@59553
|
791 |
FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
|
wneuper@59553
|
792 |
# mark twice thms (in isac + (later) in Isabelle) in Isac.thy
|
wneuper@59553
|
793 |
--------------------------------------------------------------------------------
|
Walther@60424
|
794 |
WN120320.TODO rlsthmsNOTisac: replace twice thms ^
|
wneuper@59553
|
795 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
796 |
WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
|
wneuper@59553
|
797 |
--- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
|
wneuper@59553
|
798 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
799 |
WN120321.TODO rearrange theories:
|
wneuper@59553
|
800 |
Knowledge
|
wneuper@59553
|
801 |
:
|
walther@59603
|
802 |
Prog_Expr.thy
|
walther@60125
|
803 |
///Input_Descript.thy --> ProgLang
|
walther@59603
|
804 |
Delete.thy <--- first_Knowledge_thy (*mv to Prog_Expr.thy*)
|
wneuper@59553
|
805 |
ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
|
wneuper@59553
|
806 |
Interpret.thy are generated (simplifies xml structure for theories)
|
wneuper@59585
|
807 |
Program.thy
|
wneuper@59553
|
808 |
Tools.thy
|
wneuper@59553
|
809 |
ListC.thy <--- first_Proglang_thy
|
wneuper@59553
|
810 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
811 |
WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
|
wneuper@59553
|
812 |
EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
|
wneuper@59553
|
813 |
broken during work on thy-hierarchy
|
wneuper@59553
|
814 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
815 |
WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
|
wneuper@59553
|
816 |
test --- the_hier (get_thes ()) (collect_thydata ())---
|
wneuper@59553
|
817 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
818 |
WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
|
wneuper@59553
|
819 |
!!add mutual crossreferences to ?fun headline??? where the same has to be done:
|
wneuper@59553
|
820 |
!!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
|
wneuper@59553
|
821 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
822 |
WN120411 scanning html representation of newly generated knowledge:
|
wneuper@59553
|
823 |
* thy:
|
wneuper@59553
|
824 |
** Theorems: only "Proof of the theorem" (correct!)
|
wneuper@59553
|
825 |
and "(c) isac-team (math-autor)"
|
wneuper@59553
|
826 |
** Rulesets: only "Identifier:///"
|
wneuper@59553
|
827 |
and "(c) isac-team (math-autor)"
|
wneuper@59553
|
828 |
** IsacKnowledge: link to dependency graph (which needs to be created first)
|
wneuper@59553
|
829 |
** IsacScripts --> ProgramLanguage
|
wneuper@59553
|
830 |
*** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
|
wneuper@59553
|
831 |
|
wneuper@59553
|
832 |
* pbl: OK !?!
|
wneuper@59553
|
833 |
* met: OK !?!
|
wneuper@59553
|
834 |
* exp:
|
wneuper@59553
|
835 |
** Z-Transform is missing !!!
|
wneuper@59553
|
836 |
** type-constraints !!!
|
wneuper@59553
|
837 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
838 |
WN120417: merging xmldata revealed:
|
wneuper@59553
|
839 |
..............NEWLY generated:........................................
|
wneuper@59553
|
840 |
<THEOREMDATA>
|
wneuper@59553
|
841 |
<GUH> thy_isab_Fun-thm-o_apply </GUH>
|
wneuper@59553
|
842 |
<STRINGLIST>
|
wneuper@59553
|
843 |
<STRING> Isabelle </STRING>
|
wneuper@59553
|
844 |
<STRING> Fun </STRING>
|
wneuper@59553
|
845 |
<STRING> Theorems </STRING>
|
wneuper@59553
|
846 |
<STRING> o_apply </STRING>
|
wneuper@59553
|
847 |
</STRINGLIST>
|
wneuper@59553
|
848 |
<MATHML>
|
wneuper@59553
|
849 |
<ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
|
wneuper@59553
|
850 |
</MATHML> <PROOF>
|
wneuper@59553
|
851 |
<EXTREF>
|
wneuper@59553
|
852 |
<TEXT> Proof of the theorem </TEXT>
|
wneuper@59553
|
853 |
<URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
|
wneuper@59553
|
854 |
</EXTREF>
|
wneuper@59553
|
855 |
</PROOF>
|
wneuper@59553
|
856 |
<EXPLANATIONS> </EXPLANATIONS>
|
wneuper@59553
|
857 |
<MATHAUTHORS>
|
wneuper@59553
|
858 |
<STRING> Isabelle team, TU Munich </STRING>
|
wneuper@59553
|
859 |
</MATHAUTHORS>
|
wneuper@59553
|
860 |
<COURSEDESIGNS>
|
wneuper@59553
|
861 |
</COURSEDESIGNS>
|
wneuper@59553
|
862 |
</THEOREMDATA>
|
wneuper@59553
|
863 |
..............OLD FORMAT:.............................................
|
wneuper@59553
|
864 |
<THEOREMDATA>
|
wneuper@59553
|
865 |
<GUH> thy_isab_Fun-thm-o_apply </GUH>
|
wneuper@59553
|
866 |
<STRINGLIST>
|
wneuper@59553
|
867 |
<STRING> Isabelle </STRING>
|
wneuper@59553
|
868 |
<STRING> Fun </STRING>
|
wneuper@59553
|
869 |
<STRING> Theorems </STRING>
|
wneuper@59553
|
870 |
<STRING> o_apply </STRING>
|
wneuper@59553
|
871 |
</STRINGLIST>
|
wneuper@59553
|
872 |
<THEOREM>
|
wneuper@59553
|
873 |
<ID> o_apply </ID>
|
wneuper@59553
|
874 |
<MATHML>
|
wneuper@59553
|
875 |
<ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
|
wneuper@59553
|
876 |
</MATHML>
|
wneuper@59553
|
877 |
</THEOREM>
|
wneuper@59553
|
878 |
<PROOF>
|
wneuper@59553
|
879 |
<EXTREF>
|
wneuper@59553
|
880 |
<TEXT> Proof of the theorem </TEXT>
|
wneuper@59553
|
881 |
<URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
|
wneuper@59553
|
882 |
</EXTREF>
|
wneuper@59553
|
883 |
</PROOF>
|
wneuper@59553
|
884 |
<EXPLANATIONS> </EXPLANATIONS>
|
wneuper@59553
|
885 |
<MATHAUTHORS>
|
wneuper@59553
|
886 |
<STRING> Isabelle team, TU Munich </STRING>
|
wneuper@59553
|
887 |
</MATHAUTHORS>
|
wneuper@59553
|
888 |
<COURSEDESIGNS>
|
wneuper@59553
|
889 |
</COURSEDESIGNS>
|
wneuper@59553
|
890 |
</THEOREMDATA>
|
wneuper@59553
|
891 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
892 |
\<close>
|
wneuper@59553
|
893 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
894 |
text \<open>
|
wneuper@59553
|
895 |
isac development was done between these changesets:
|
wneuper@59553
|
896 |
------------------------------------------------------------------------------
|
wneuper@59553
|
897 |
Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
|
wneuper@59553
|
898 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
899 |
Date: 2012-09-24 16:39:30 +0200 (8 months)
|
wneuper@59553
|
900 |
:
|
wneuper@59553
|
901 |
: isac on Isablle2011
|
wneuper@59553
|
902 |
:
|
wneuper@59553
|
903 |
Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
|
wneuper@59553
|
904 |
Branch: decompose-isar
|
wneuper@59553
|
905 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
906 |
Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
|
wneuper@59553
|
907 |
------------------------------------------------------------------------------
|
wneuper@59553
|
908 |
\<close>
|
wneuper@59553
|
909 |
|
Walther@60424
|
910 |
subsection \<open>isac on Isabelle2009-2\<close>
|
wneuper@59553
|
911 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
912 |
text \<open>
|
wneuper@59553
|
913 |
In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
|
wneuper@59553
|
914 |
The update was painful (bridging 7 years of Isabelle development) and cut short
|
wneuper@59553
|
915 |
due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
|
wneuper@59553
|
916 |
going on to Isabelle2011 although most of the tests did not run.
|
wneuper@59553
|
917 |
\<close>
|
wneuper@59553
|
918 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
919 |
text \<open>
|
wneuper@59553
|
920 |
WN131021 this is broken by installation of Isabelle2011/12/13,
|
wneuper@59553
|
921 |
because all these write their binaries to ~/.isabelle/heaps/..
|
wneuper@59553
|
922 |
|
Walther@60424
|
923 |
$ cd /usr/local/isabisac09-2/
|
wneuper@59553
|
924 |
$ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
|
wneuper@59553
|
925 |
$ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
|
wneuper@59553
|
926 |
NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
|
wneuper@59553
|
927 |
\<close>
|
wneuper@59553
|
928 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
929 |
text \<open>
|
Walther@60424
|
930 |
Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
|
wneuper@59553
|
931 |
\<close>
|
wneuper@59553
|
932 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
933 |
text \<open>
|
wneuper@59553
|
934 |
isac development was done between these changesets:
|
wneuper@59553
|
935 |
------------------------------------------------------------------------------
|
wneuper@59553
|
936 |
Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
|
wneuper@59553
|
937 |
Branch: decompose-isar
|
wneuper@59553
|
938 |
User: Marco Steger <m.steger@student.tugraz.at>
|
wneuper@59553
|
939 |
Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
|
wneuper@59553
|
940 |
:
|
Walther@60424
|
941 |
: isac on Isablle2009-2
|
wneuper@59553
|
942 |
:
|
Walther@60424
|
943 |
Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
|
Walther@60424
|
944 |
Branch: isac-from-Isabelle2009-2
|
wneuper@59553
|
945 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
Walther@60424
|
946 |
Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
|
wneuper@59553
|
947 |
------------------------------------------------------------------------------
|
wneuper@59553
|
948 |
\<close>
|
wneuper@59553
|
949 |
|
wneuper@59553
|
950 |
subsection \<open>isac on Isabelle2002\<close>
|
wneuper@59553
|
951 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
952 |
text \<open>
|
wneuper@59553
|
953 |
From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
|
wneuper@59553
|
954 |
of isac's mathematics engine has been implemented.
|
wneuper@59553
|
955 |
\<close>
|
wneuper@59553
|
956 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
957 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
958 |
text \<open>
|
wneuper@59553
|
959 |
All tests work on an old notebook (the right PolyML coudn't be upgraded to more
|
wneuper@59553
|
960 |
recent Linux versions)
|
wneuper@59553
|
961 |
\<close>
|
wneuper@59553
|
962 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
963 |
text \<open>
|
wneuper@59553
|
964 |
Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
|
wneuper@59553
|
965 |
see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
|
wneuper@59553
|
966 |
\<close>
|
Walther@60729
|
967 |
ML \<open>
|
Walther@60729
|
968 |
\<close> ML \<open>
|
Walther@60729
|
969 |
\<close> ML \<open>
|
Walther@60729
|
970 |
\<close> ML \<open>
|
Walther@60729
|
971 |
\<close>
|
wneuper@59553
|
972 |
end
|
wneuper@59553
|
973 |
(*========== inhibit exn 130719 Isabelle2013 ===================================
|
wneuper@59553
|
974 |
============ inhibit exn 130719 Isabelle2013 =================================*)
|
wneuper@59553
|
975 |
|
wneuper@59553
|
976 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
wneuper@59553
|
977 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|
wneuper@59553
|
978 |
|