1 (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
2 Author: Walther Neuper 101001
3 (c) copyright due to license terms.
5 Isac's tests are organised parallel to sources:
6 "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
8 ~~/test/Tools/isac/ADDTESTS
9 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
10 -------------------------------------------------------------------------------
12 Prepare running tests: see below
14 $ cd /usr/local/isabisac/
15 $ export ISABELLE_VERSION=2015 # for libisabelle
16 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
19 section \<open>Prepare running tests\<close>
21 Isac encapsulates code as much as possible in structures without open. TODO ProgLang.
22 This policy conflicts with those tests, which go into functions to details
23 not declared in the signatures.
25 In order to maintain these tests without changes, this has to be done before running tests:
26 (1) Extend signatures for tests by
27 ~~$ ./xcoding-to-test.sh
28 ~~$ ./zcoding-to-test.sh # -"- + go back to Test_Isac.thy
29 Running Test_Isac.thy opens all structures, see code after "begin" below.
30 (2) Clean signatures for coding
31 ~~$ ./xtest-to-coding.sh
32 ~~$ ./xtest-to-coding.sh # -"- + go back to coding (!update thy!)
34 ********************* don't forget (2) BEFORE pushing to repository *********************
36 The above bash files accomplish query replace in src/Tools/isac:
37 \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>
38 \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit> \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>
39 ^^^ in signature outcommented, ^^^ NOT outcommented,
40 this is status for coding this is status for tests
43 section \<open>Run the tests\<close>
45 * say "OK" to the popup asking for theories to be loaded
46 * watch the <Theories> window for errors in the "imports" below
49 theory Test_Isac imports Build_Thydata
50 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
51 "ADDTESTS/accumulate-val/Thy_All"
53 "ADDTESTS/test-depend/Build_Test"
56 "ADDTESTS/course/phst11/T1_Basics"
57 "ADDTESTS/course/phst11/T2_Rewriting"
58 "ADDTESTS/course/phst11/T3_MathEngine"
59 "ADDTESTS/file-depend/BuildC_Test"
60 "ADDTESTS/session-get_theory/Foo"
61 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
62 ADDTESTS/------------------------------------------- see end of tests *)
63 (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
64 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
65 "~~/test/Pure/Isar/Test_Parse_Term"
66 "~~/test/HOL/Library/Test_Polynomial"
67 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
68 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
69 "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
70 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
71 "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
72 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
74 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
75 "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
76 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
81 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
82 (* these vvv test, if funs are intermediately opened in structure
83 in case of errors here consider ~~/./xtest-to-coding.sh *)
85 open Math_Engine; CalcTreeTEST;
87 open Inform; cas_input;
88 open Rtools; trtas2str;
89 open Chead; pt_extract;
90 open Generate; (* NONE *)
91 open Ctree; append_problem;
92 open Specify; show_ptyps;
93 open Applicable; mk_set;
94 open Solve; (* NONE *)
96 open Stool; transfer_asms_from_to;
98 open Model; (* NONE *)
99 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
107 KEStore_Elems.set_ref_thy @{theory};
108 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
111 section {* trials with Isabelle's functions *}
112 ML {*"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";*}
113 ML_file "~~/test/Pure/General/alist.ML"
114 ML_file "~~/test/Pure/General/basics.ML"
115 ML_file "~~/test/Pure/General/scan.ML"
116 ML_file "~~/test/Pure/PIDE/xml.ML"
117 ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*}
119 section {* test ML Code of isac *}
120 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
121 ML_file "library.sml"
122 ML_file "calcelems.sml"
123 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
124 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
125 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
126 ML_file "ProgLang/termC.sml"
130 (* Title: test calculation of values for function constants
131 Author: Walther Neuper 2000
132 (c) copyright due to lincense terms.
134 12345678901234567890123456789012345678901234567890123456789012345678901234567890
135 10 20 30 40 50 60 70 80
138 "--------------------------------------------------------";
139 "table of contents --------------------------------------";
140 "--------------------------------------------------------";
141 "-calculate.thy: provides 'setup' -----------------------";
142 "----------- fun norm -----------------------------------";
143 "----------- check return value of adhoc_thm ----";
144 "----------- fun calculate_ -----------------------------";
145 "----------- calculate from script --requires 'setup'----";
146 "----------- calculate check test-root-equ --------------";
147 "----------- check calcul,ate bottom up -----------------";
148 "----------- Atools.pow Power.power_class.power ---------";
149 " ================= calculate.sml: calculate_ 2002 ======";
150 "----------- get_pair with 3 args -----------------------";
151 "----------- calculate (2 * x is_const) -----------------";
152 "--------------------------------------------------------";
153 "--------------------------------------------------------";
154 "--------------------------------------------------------";
156 "----------- check return value of adhoc_thm ----";
157 "----------- check return value of adhoc_thm ----";
158 "----------- check return value of adhoc_thm ----";
159 val thy = @{theory "Poly"};
160 val cal = snd (assoc_calc' thy "is_polyexp");
161 val t = @{term "(x / x) is_polyexp"};
162 val SOME (thmID, thm) = adhoc_thm thy cal t;
163 (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
165 error "calculate.sml: adhoc_thm must return Trueprop";
167 "----------- fun calculate_ -----------------------------";
168 "----------- fun calculate_ -----------------------------";
169 "----------- fun calculate_ -----------------------------";
170 val thy = @{theory "Test"};
172 val t = (Thm.term_of o the o (parse thy)) "1+2";
173 val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
174 term2str (Thm.prop_of thm) = "1 + 2 = 3";
177 val t = (Thm.term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
178 val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
179 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
180 if term2str t = "(3 * 4 / 3) ^^^ 2" then ()
181 else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2";
183 "===== test 3b -- 2 contiued";
184 val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t;
185 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
187 (*val it = "(#12 // #3) ^^^ #2" : string*)
190 val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
191 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
193 (*it = "#4 ^^^ #2" : string*)
196 val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER")))t;
197 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
198 (*show_types := false;*)
199 if term2str t <> "16" then error "calculate.sml: new behaviour in calculate_"
203 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
205 ("Test",["calculate","test"],["Test","test_calculate"]);
207 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
209 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
211 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
212 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
213 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
214 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
215 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
216 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
217 (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
218 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
219 (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
221 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
222 (*nxt = ("Calculate",Calculate "PLUS")*)
223 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
224 (*nxt = ("Calculate",Calculate "TIMES")*)
225 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
226 (*nxt = ("Calculate",Calculate "DIVIDE")*)
227 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
228 (*nxt = ("Calculate",Calculate "POWER")*)
229 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
230 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
231 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
232 (*nxt = ("End_Proof'",End_Proof')*)
233 case f of FormKF "16" => () | _ =>
234 error "calculate.sml: script test_calculate changed behaviour";
237 "----------- calculate check test-root-equ --------------";
238 "----------- calculate check test-root-equ --------------";
239 "----------- calculate check test-root-equ --------------";
240 (*(1): 2nd Test_simplify didn't work:
242 "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
243 > val rls = ("Test_simplify");
244 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
245 val ct = "sqrt (x ^^^ 2 + -3 * x) =
246 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
247 ie. cancel does not work properly
251 val ct = "sqrt (x ^^^ 2 + -3 * x) =\
252 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
253 val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
256 sqrt (x ^^^ 2 + -3 * x) =\
257 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
258 ............... does not work *)
260 (*--------------(2): does divide work in Test_simplify ?: ------*)
261 val thy = @{theory Test};
262 val t = (Thm.term_of o the o (parse thy)) "6 / 2";
263 val rls = Test_simplify;
264 val (t,_) = the (rewrite_set_ thy false rls t);
265 (*val t = Free ("3","Real.real") : term*)
269 val rls = "Test_simplify";
270 val (t,_) = the (rewrite_set thy false rls t);
271 (*val t = "3" : string
272 ....... works, thus: which rule in SqRoot_simplify works differently ?*)
275 (*--------------(3): is_const works ?: -------------------------------------*)
276 val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const";
278 rewrite_set_ @{theory Test} false tval_rls t;
279 (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
281 val t = str2term "2 * x is_const";
282 val SOME (str,t') = eval_const "" "" t (@{theory "Isac"});
286 "----------- check calculate bottom up ------------------";
287 "----------- check calculate bottom up ------------------";
288 "----------- check calculate bottom up ------------------";
289 (*-------------- eval_cancel works: *)
290 trace_rewrite:=false;
291 val thy = @{theory Test};
292 val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
294 val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
298 (*-------------- but ... *)
299 val ct = "x + (-4) / 2";
301 val thy' = "Test"; (* added AK110727 *)
302 val (ct,_) = the (rewrite_set thy' false rls ct);
305 (*-------------- while ... *)
308 val (ct,_) = the (rewrite_set thy' false rls ct);
313 (*--------------(5): reproduce (1) with simpler term: ------------*)
316 val (t,_) = the (rewrite_set thy false rls t);
317 (*val t = "4" ... works*)
319 val t = "(3+1+2*x)/2";
320 val (t,_) = the (rewrite_set thy false rls t);
321 (*val t = "2 + x" ... works*)
323 trace_rewrite:=false; (*=true3.6.03*)
326 val rls = "Test_simplify";
327 val t = "(3+(1+2*x))/2";
328 val (t,_) = the (rewrite_set thy false rls t);
329 (*val t = "2 + x" ... works: give up----------------------------------------*)
330 trace_rewrite:=false;
332 trace_rewrite:=false; (*=true3.6.03*)
333 val thy = @{theory Test};
334 val rls = Test_simplify;
335 val t = str2term "(3+(1+2*x))/2";
336 val SOME (t',asm) = rewrite_set_ thy false rls t;
338 (*val t = "2 + x" ... works: give up----------------------------------------*)
339 trace_rewrite:=false;
344 (*--- trace_rewrite before correction of ... --------------------
345 val ct = "(-3 + 2 * x + -1) / 2";
346 val (ct,_) = the (rewrite_set thy' false rls ct);
348 ### trying thm 'root_ge0_2'
349 ### rewrite_set_: x + (-1 + -3) / 2
350 ### trying thm 'radd_real_const_eq'
351 ### trying thm 'radd_real_const'
352 ### rewrite_set_: x + (-4) / 2
353 ### trying thm 'rcollect_right'
356 -------------------------------------while before Isabelle20002:
357 val ct = "(#-3 + #2 * x + #-1) // #2";
358 val (ct,_) = the (rewrite_set thy' false rls ct);
360 ### trying thm 'root_ge0_2'
361 ### rewrite_set_: x + (#-1 + #-3) // #2
362 ### trying thm 'radd_real_const_eq'
363 ### trying thm 'radd_real_const'
364 ### rewrite_set_: x + #-4 // #2
365 ### rewrite_set_: x + #-2
366 ### trying thm 'rcollect_right'
369 -----------------------------------------------------------------*)
372 (*===================*)
373 trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
375 val rls = "Test_simplify";
376 val ct = "x + (-1 + -3) / 2";
377 val (ct,_) = the (rewrite_set thy' false rls ct);
380 ### trying calc. 'cancel'
381 @@@ get_pair: binop, t = x + (-4) / 2
383 @@@ get_pair: t else -> NONE
384 @@@ get_pair: binop, t = (-4) / 2
386 @@@ get_pair: t -> NONE
387 @@@ get_pair: t1 -> NONE
389 ### trying calc. 'pow'
393 trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
395 val rls = "Test_simplify";
396 val ct = "x + (-4) / 2";
397 val (ct,_) = the (rewrite_set thy' false rls ct);
400 ### trying calc. 'cancel'
401 @@@ get_pair: binop, t = x + -4 / 2
403 @@@ get_pair: t else -> NONE
404 @@@ get_pair: binop, t = -4 / 2
406 @@@ adhoc_thm': SOME #cancel_-4_2
407 ### calc. to: x + (-2)
408 ### trying calc. 'cancel'
410 trace_rewrite:=false;
412 "----------- Atools.pow Power.power_class.power ---------";
413 "----------- Atools.pow Power.power_class.power ---------";
414 "----------- Atools.pow Power.power_class.power ---------";
415 val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa";
418 *** Const ( Nat.power, ['a, nat] => 'a)
420 *** . Free ( aaa, nat) *)
422 val t = str2term "1 ^^^ aaa";
425 *** Const (Atools.pow, real => real => real)
427 *** . Free (aaa, real)
430 " ================= calculate.sml: calculate_ 2002 =================== ";
431 " ================= calculate.sml: calculate_ 2002 =================== ";
432 " ================= calculate.sml: calculate_ 2002 =================== ";
434 val thy = @{theory Test};
435 val t = (Thm.term_of o the o (parse thy)) "12 / 3";
436 val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
437 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
439 val thy = @{theory Test};
440 val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2";
441 val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER"))) t;
442 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
445 val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
446 val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
448 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
451 val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES")))t;
453 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
456 val SOME (thmID,thm) =adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
458 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
461 val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER")))t;
463 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
466 if it <> "16" then error "calculate.sml: new behaviour in calculate_"
470 (*13.9.02 *** calc: operator = pow not defined*)
471 val t = (Thm.term_of o the o (parse thy)) "3^^^2";
472 val SOME (thmID,thm) =
473 adhoc_thm thy (the(assoc(calclist,"POWER"))) t;
474 (*** calc: operator = pow not defined*)
476 val (op_, eval_fn) = the (assoc(calclist,"POWER"));
478 val op_ = "Atools.pow" : string
479 val eval_fn = fn : string -> term -> theory -> (string * term) option*)
481 val SOME (thmid,t') = get_pair thy op_ eval_fn t;
482 (*** calc: operator = pow not defined*)
484 val SOME (id,t') = eval_fn op_ t thy;
485 (*** calc: operator = pow not defined*)
487 val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
488 val SOME (id,t') = eval_binop thmid op_ t thy;
489 (*** calc: operator = pow not defined*)
492 @{theory EqSystem}; (*.., Isac.EqSystem}*)
499 *} ML {* (*Theory loader: undefined entry for theory "EqSystem"*)
501 "----------- get_pair with 3 args --------------------------------";
502 "----------- get_pair with 3 args --------------------------------";
503 "----------- get_pair with 3 args --------------------------------";
504 val (thy, op_, ef, arg) =
505 (thy, "EqSystem.occur'_exactly'_in",
506 assoc_calc' (Thy_Info_get_theory "EqSystem") "occur_exactly_in" |> snd |> snd,
508 "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
510 val SOME (str, simpl) = get_pair thy op_ ef arg;
518 if str = "2 * x_" then () else writeln "probably WORKS"
521 "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
522 then () else error "calculate.sml get_pair with 3 args:occur_exactly_in";
526 "----------- calculate (2 * x is_const) -----------------";
527 "----------- calculate (2 * x is_const) -----------------";
528 "----------- calculate (2 * x is_const) -----------------";
529 val t = str2term "2 * x is_const";
530 val SOME (str, t') = eval_const "" "" t @{theory Test};
532 "(2 * x is_const) = False";
534 val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
540 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
541 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
542 ML_file "ProgLang/rewrite.sml"
543 ML_file "ProgLang/listC.sml"
544 ML_file "ProgLang/scrtools.sml"
545 ML_file "ProgLang/tools.sml"
546 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
547 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
548 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
549 ML_file "Minisubpbl/000-comments.sml"
550 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
551 ML_file "Minisubpbl/100-init-rootpbl.sml"
552 ML_file "Minisubpbl/150-add-given.sml"
553 ML_file "Minisubpbl/200-start-method.sml"
554 ML_file "Minisubpbl/300-init-subpbl.sml"
555 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
556 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
557 ML_file "Minisubpbl/500-met-sub-to-root.sml"
558 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
559 ML_file "Minisubpbl/600-postcond.sml"
560 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
561 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
562 ML_file "Interpret/mstools.sml"
563 ML_file "Interpret/ctree.sml" (*!...!see(25)*)
564 ML_file "Interpret/ptyps.sml" (* requires setup from ptyps.thy *)
565 ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
566 (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
567 ML_file "Interpret/generate.sml"
568 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
569 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
570 ML_file "Interpret/calchead.sml"
571 ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
572 ML_file "Interpret/rewtools.sml"
573 ML_file "Interpret/script.sml"
574 ML_file "Interpret/solve.sml"
575 ML_file "Interpret/inform.sml"
576 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
577 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
578 ML_file "Interpret/mathengine.sml" (*!part. WN130804: +check Interpret/me.sml*)
579 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
580 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
581 ML_file "xmlsrc/mathml.sml" (*part.*)
582 ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
583 ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
584 ML_file "xmlsrc/thy-hierarchy.sml"
585 ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
586 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
587 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
588 ML_file "Frontend/messages.sml"
589 ML_file "Frontend/states.sml"
590 ML_file "Frontend/interface.sml"
591 ML_file "Frontend/use-cases.sml"
592 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
593 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
594 ML_file "print_exn_G.sml"
595 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
596 ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}
597 ML_file "Knowledge/delete.sml"
598 ML_file "Knowledge/descript.sml"
599 ML_file "Knowledge/atools.sml"
600 ML_file "Knowledge/simplify.sml"
601 ML_file "Knowledge/poly.sml"
602 ML_file "Knowledge/gcd_poly_ml.sml"
603 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
604 ML_file "Knowledge/rational.sml"
605 ML_file "Knowledge/equation.sml"
606 ML_file "Knowledge/root.sml"
607 ML_file "Knowledge/lineq.sml"
608 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
609 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
610 ML_file "Knowledge/rootrat.sml"
611 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
612 ML_file "Knowledge/partial_fractions.sml"
613 ML_file "Knowledge/polyeq.sml"
614 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
615 ML_file "Knowledge/calculus.sml"
616 ML_file "Knowledge/trig.sml"
617 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
618 ML_file "Knowledge/diff.sml"
619 ML_file "Knowledge/integrate.sml"
620 ML_file "Knowledge/eqsystem.sml"
621 ML_file "Knowledge/test.sml"
622 ML_file "Knowledge/polyminus.sml"
623 ML_file "Knowledge/vect.sml"
624 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
625 ML_file "Knowledge/biegelinie.sml"
626 ML_file "Knowledge/algein.sml"
627 ML_file "Knowledge/diophanteq.sml"
628 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
629 ML_file "Knowledge/inssort.sml"
630 ML_file "Knowledge/isac.sml"
631 ML_file "Knowledge/build_thydata.sml"
632 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
633 ML {*"%%%%%%%%%%%%%%%%% start ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%";*}
634 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
635 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
636 ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*}
638 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
639 ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*}
640 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
641 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
643 section {* history of tests *}
645 Systematic regression tests have been introduced to isac development in 2003.
646 Sanity of the regression tests suffers from updates following Isabelle development,
647 which mostly exceeded the resources available in isac's development.
649 The survey below shall support to efficiently use the tests for isac
650 on different Isabelle versions. Conclusion in most cases will be:
652 !!! Use most recent tests or go back to the old notebook
653 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
657 subsection {* isac on Isabelle2015 *}
658 subsubsection {* Summary of development *}
660 * Add signatures from top of thy-hierarchy down to Interpret, not ProgLang.
661 This complicates Test_Isac, see "Prepare running tests" above.
662 * Remove TTY interface.
663 * Re-activate insertion sort.
665 subsubsection {* State of tests: unchanged *}
666 subsubsection {* Changesets of begin and end *}
668 last changeset with Test_Isac 2f1b2854927a
669 first changeset with Test_Isac ???
672 subsection {* isac on Isabelle2014 *}
673 subsubsection {* Summary of development *}
675 migration from "isabelle tty" --> libisabelle
678 subsection {* isac on Isabelle2013-2 *}
679 subsubsection {* Summary of development *}
681 reactivated context_thy
683 subsubsection {* State of tests *}
687 subsubsection {* Changesets of begin and end *}
691 : isac on Isablle2013-2
693 Changeset: 55318 (03826ceb24da) merged
694 User: Walther Neuper <neuper@ist.tugraz.at>
695 Date: 2013-12-12 14:27:37 +0100 (7 minutes)
698 subsection {* isac on Isabelle2013-1 *}
699 subsubsection {* Summary of development *}
701 Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
702 no significant development steps for ISAC.
704 subsubsection {* State of tests *}
706 See points in subsection "isac on Isabelle2011", "State of tests".
708 subsubsection {* Changesets of begin and end *}
710 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
711 User: Walther Neuper <neuper@ist.tugraz.at>
712 Date: 2013-12-03 18:13:31 +0100 (8 days)
714 : isac on Isablle2013-1
716 Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
717 User: Walther Neuper <neuper@ist.tugraz.at>
718 Date: 2013-11-21 18:12:17 +0100 (2 weeks)
722 subsection {* isac on Isabelle2013 *}
723 subsubsection {* Summary of development *}
725 # Oct.13: replaced "axioms" by "axiomatization"
726 # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
727 # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
728 simplification of multivariate rationals (without improving the rulesets involved).
730 subsubsection {* Run tests *}
732 Is standard now; this subsection will be discontinued under Isabelle2013-1
734 subsubsection {* State of tests *}
736 See points in subsection "isac on Isabelle2011", "State of tests".
737 # re-activated listC.sml
739 subsubsection {* Changesets of begin and end *}
741 changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
742 User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
743 Date: Tue Nov 19 22:23:30 2013 +0000
745 : isac on Isablle2013
747 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
748 User: Walther Neuper <neuper@ist.tugraz.at>
749 Date: 2013-07-15 08:28:50 +0200 (4 weeks)
752 subsection {* isac on Isabelle2012 *}
753 subsubsection {* Summary of development *}
755 isac on Isabelle2012 is considered just a transitional stage
756 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
757 For considerations on the transition see
758 ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
760 subsubsection {* Run tests *}
762 $ cd /usr/local/isabisac12/
763 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
764 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
766 subsubsection {* State of tests *}
768 At least the tests from isac on Isabelle2011 run again.
769 However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
770 in parallel with evaluation.
772 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
773 yields 69 hits, some of which were already present before Isabelle2002-->2009-2
774 (i.e. on the old notebook from 2002).
776 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
777 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
778 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
779 # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
780 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
782 Some tests have been re-activated (e.g. error patterns, fill patterns).
784 subsubsection {* Changesets of begin and end *}
786 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
787 User: Walther Neuper <neuper@ist.tugraz.at>
788 Date: 2013-07-11 16:58:31 +0200 (4 weeks)
790 : isac on Isablle2012
792 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
793 User: Walther Neuper <neuper@ist.tugraz.at>
794 Date: 2012-09-24 18:35:13 +0200 (8 months)
795 ------------------------------------------------------------------------------
796 Changeset: 48756 (7443906996a8) merged
797 User: Walther Neuper <neuper@ist.tugraz.at>
798 Date: 2012-09-24 18:15:49 +0200 (8 months)
801 subsection {* isac on Isabelle2011 *}
802 subsubsection {* Summary of development *}
804 isac's mathematics engine has been extended by two developments:
805 (1) Isabelle's contexts were introduced by Mathias Lehnfeld
806 (2) Z_Transform was introduced by Jan Rocnik, which revealed
807 further errors introduced by (1).
808 (3) "error patterns" were introduced by Gabriella Daroczy
809 Regressions tests have been added for all of these.
811 subsubsection {* Run tests *}
813 $ cd /usr/local/isabisac11/
814 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
815 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
817 subsubsection {* State of tests *}
819 Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
820 and sometimes give reasons for failing tests.
821 (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
822 work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
824 The most signification tests (in particular Frontend/interface.sml) run,
825 however, many "error in kernel" are not caught by an exception.
826 ------------------------------------------------------------------------------
827 After the changeset below Test_Isac worked with check_unsynchronized_ref ():
828 ------------------------------------------------------------------------------
829 Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
830 User: Walther Neuper <neuper@ist.tugraz.at>
831 Date: 2012-08-06 10:38:11 +0200 (11 months)
834 The list below records TODOs while producing an ISAC kernel for
835 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
836 (so to be resumed with Isabelle2013-1):
837 ############## WNxxxxxx.TODO can be found in sources ##############
838 --------------------------------------------------------------------------------
839 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
840 --------------------------------------------------------------------------------
841 WN111013.TODO: remove concept around "fun init_form", lots of troubles with
842 this special case (see) --- why not nxt = Model_Problem here ? ---
843 --------------------------------------------------------------------------------
844 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
846 # simplify_* , *_simp_*
848 # calc_* , calculate_* ... require iteration over all rls ...
849 ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
850 --------------------------------------------------------------------------------
851 WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
852 --------------------------------------------------------------------------------
853 WN120314 changeset a393bb9f5e9f drops root equations.
854 see test/Tools/isac/Knowledge/rootrateq.sml
855 --------------------------------------------------------------------------------
856 WN120317.TODO changeset 977788dfed26 dropped rateq:
857 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
858 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
859 investigation Check_elementwise stopped due to too much effort finding out,
860 why Check_elementwise worked in 2002 in spite of the error.
861 --------------------------------------------------------------------------------
862 WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
863 --------------------------------------------------------------------------------
864 WN120317.TODO found by test --- interSteps for Schalk 299a --- that
865 NO test with 'interSteps' is checked properly (with exn on changed behaviour)
866 --------------------------------------------------------------------------------
867 WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
868 a newly outcommented test where rewrite_set_ make_polynomial --> NONE
869 --------------------------------------------------------------------------------
870 WN120320.TODO check-improve rlsthmsNOTisac:
871 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
872 DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
873 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
874 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
875 --------------------------------------------------------------------------------
876 WN120320.TODO rlsthmsNOTisac: replace twice thms ^
877 --------------------------------------------------------------------------------
878 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
879 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
880 --------------------------------------------------------------------------------
881 WN120321.TODO rearrange theories:
885 ///Descript.thy --> ProgLang
886 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*)
887 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
888 Interpret.thy are generated (simplifies xml structure for theories)
891 ListC.thy <--- first_Proglang_thy
892 --------------------------------------------------------------------------------
893 WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
894 EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
895 broken during work on thy-hierarchy
896 --------------------------------------------------------------------------------
897 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
898 test --- the_hier (get_thes ()) (collect_thydata ())---
899 --------------------------------------------------------------------------------
900 WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
901 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
902 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
903 --------------------------------------------------------------------------------
904 WN120409.TODO replace "op mem" (2002) with member (2011) ...
905 ... an exercise interesting for beginners !
906 --------------------------------------------------------------------------------
907 WN120411 scanning html representation of newly generated knowledge:
909 ** Theorems: only "Proof of the theorem" (correct!)
910 and "(c) isac-team (math-autor)"
911 ** Rulesets: only "Identifier:///"
912 and "(c) isac-team (math-autor)"
913 ** IsacKnowledge: link to dependency graph (which needs to be created first)
914 ** IsacScripts --> ProgramLanguage
915 *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
920 ** Z-Transform is missing !!!
921 ** type-constraints !!!
922 --------------------------------------------------------------------------------
923 WN120417: merging xmldata revealed:
924 ..............NEWLY generated:........................................
926 <GUH> thy_isab_Fun-thm-o_apply </GUH>
928 <STRING> Isabelle </STRING>
929 <STRING> Fun </STRING>
930 <STRING> Theorems </STRING>
931 <STRING> o_apply </STRING>
934 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
937 <TEXT> Proof of the theorem </TEXT>
938 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
941 <EXPLANATIONS> </EXPLANATIONS>
943 <STRING> Isabelle team, TU Munich </STRING>
948 ..............OLD FORMAT:.............................................
950 <GUH> thy_isab_Fun-thm-o_apply </GUH>
952 <STRING> Isabelle </STRING>
953 <STRING> Fun </STRING>
954 <STRING> Theorems </STRING>
955 <STRING> o_apply </STRING>
960 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
965 <TEXT> Proof of the theorem </TEXT>
966 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
969 <EXPLANATIONS> </EXPLANATIONS>
971 <STRING> Isabelle team, TU Munich </STRING>
976 --------------------------------------------------------------------------------
978 subsubsection {* Changesets of begin and end *}
980 isac development was done between these changesets:
981 ------------------------------------------------------------------------------
982 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
983 User: Walther Neuper <neuper@ist.tugraz.at>
984 Date: 2012-09-24 16:39:30 +0200 (8 months)
986 : isac on Isablle2011
988 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
989 Branch: decompose-isar
990 User: Walther Neuper <neuper@ist.tugraz.at>
991 Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
992 ------------------------------------------------------------------------------
995 subsection {* isac on Isabelle2009-2 *}
996 subsubsection {* Summary of development *}
998 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
999 The update was painful (bridging 7 years of Isabelle development) and cut short
1000 due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
1001 going on to Isabelle2011 although most of the tests did not run.
1003 subsubsection {* Run tests *}
1005 WN131021 this is broken by installation of Isabelle2011/12/13,
1006 because all these write their binaries to ~/.isabelle/heaps/..
1008 $ cd /usr/local/isabisac09-2/
1009 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
1010 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
1011 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
1013 subsubsection {* State of tests *}
1015 Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
1017 subsubsection {* Changesets of begin and end *}
1019 isac development was done between these changesets:
1020 ------------------------------------------------------------------------------
1021 Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
1022 Branch: decompose-isar
1023 User: Marco Steger <m.steger@student.tugraz.at>
1024 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
1026 : isac on Isablle2009-2
1028 Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
1029 Branch: isac-from-Isabelle2009-2
1030 User: Walther Neuper <neuper@ist.tugraz.at>
1031 Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
1032 ------------------------------------------------------------------------------
1035 subsection {* isac on Isabelle2002 *}
1036 subsubsection {* Summary of development *}
1038 From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
1039 of isac's mathematics engine has been implemented.
1041 subsubsection {* Run tests *}
1042 subsubsection {* State of tests *}
1044 All tests work on an old notebook (the right PolyML coudn't be upgraded to more
1045 recent Linux versions)
1047 subsubsection {* Changesets of begin and end *}
1049 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
1050 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
1054 (*========== inhibit exn 130719 Isabelle2013 ===================================
1055 ============ inhibit exn 130719 Isabelle2013 =================================*)
1057 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1058 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)