walther@59967
|
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@60317
|
53 |
(** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"( *TODOO*)
|
wenzelm@60217
|
54 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
|
wenzelm@60217
|
55 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
|
wenzelm@60217
|
56 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
|
wenzelm@60217
|
57 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
|
wenzelm@60217
|
58 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
|
walther@60317
|
59 |
(** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"( *TODOO*)
|
wenzelm@60217
|
60 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
|
wenzelm@60217
|
61 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
|
wenzelm@60217
|
62 |
(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
|
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 |
( **)
|
wneuper@59553
|
84 |
|
wneuper@59553
|
85 |
begin
|
wneuper@59553
|
86 |
|
wenzelm@60240
|
87 |
declare [[ML_print_depth = 20]]
|
wenzelm@60240
|
88 |
|
walther@59628
|
89 |
ML \<open>open ML_System\<close>
|
wneuper@59553
|
90 |
ML \<open>
|
wneuper@59553
|
91 |
open Kernel;
|
walther@59814
|
92 |
open Math_Engine;
|
walther@59814
|
93 |
open Test_Code; CalcTreeTEST;
|
walther@59848
|
94 |
open LItool; arguments_from_model;
|
walther@59817
|
95 |
open Sub_Problem;
|
walther@59823
|
96 |
open Fetch_Tacs;
|
walther@59814
|
97 |
open Step
|
walther@59659
|
98 |
open Env;
|
walther@59814
|
99 |
open LI; scan_dn;
|
walther@59617
|
100 |
open Istate;
|
walther@59909
|
101 |
open Error_Pattern;
|
walther@59909
|
102 |
open Error_Pattern_Def;
|
walther@59977
|
103 |
open Specification;
|
wneuper@59553
|
104 |
open Ctree; append_problem;
|
walther@59696
|
105 |
open Pos;
|
walther@59618
|
106 |
open Program;
|
wneuper@59601
|
107 |
open Prog_Tac;
|
walther@59603
|
108 |
open Tactical;
|
walther@59603
|
109 |
open Prog_Expr;
|
walther@59618
|
110 |
open Auto_Prog; rule2stac;
|
wneuper@59600
|
111 |
open Input_Descript;
|
walther@59971
|
112 |
open Specify;
|
walther@59976
|
113 |
open Specify;
|
walther@59763
|
114 |
open Step_Specify;
|
walther@59749
|
115 |
open Step_Solve;
|
walther@59763
|
116 |
open Step;
|
wneuper@59553
|
117 |
open Solve; (* NONE *)
|
wneuper@59577
|
118 |
open ContextC; transfer_asms_from_to;
|
walther@59814
|
119 |
open Tactic; (* NONE *)
|
walther@60126
|
120 |
open I_Model;
|
walther@60126
|
121 |
open O_Model;
|
walther@60126
|
122 |
open P_Model; (* NONE *)
|
walther@59872
|
123 |
open Rewrite;
|
walther@59878
|
124 |
open Eval; get_pair;
|
wneuper@59553
|
125 |
open TermC; atomt;
|
walther@59858
|
126 |
open Rule;
|
walther@59878
|
127 |
open Rule_Set; Sequence;
|
walther@59919
|
128 |
open Eval_Def
|
walther@59854
|
129 |
open ThyC
|
walther@59865
|
130 |
open ThmC_Def
|
walther@59858
|
131 |
open ThmC
|
walther@59857
|
132 |
open Rewrite_Ord
|
walther@59861
|
133 |
open UnparseC
|
wenzelm@60223
|
134 |
\<close>
|
wneuper@59553
|
135 |
|
wneuper@59553
|
136 |
ML \<open>
|
walther@59659
|
137 |
"~~~~~ fun xxx , args:"; val () = ();
|
walther@59659
|
138 |
"~~~~~ and xxx , args:"; val () = ();
|
walther@59814
|
139 |
"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
|
walther@60262
|
140 |
(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
|
walther@59659
|
141 |
"xx"
|
walther@59814
|
142 |
^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
|
walther@59723
|
143 |
\<close> ML \<open>
|
walther@59723
|
144 |
\<close>
|
walther@59723
|
145 |
ML \<open>
|
walther@59723
|
146 |
\<close> ML \<open>
|
wneuper@59553
|
147 |
\<close> ML \<open>
|
walther@59851
|
148 |
\<close> ML \<open>
|
walther@59851
|
149 |
\<close> ML \<open>
|
walther@59892
|
150 |
\<close> ML \<open>
|
walther@59892
|
151 |
\<close> ML \<open>
|
walther@59851
|
152 |
\<close> ML \<open>
|
walther@59851
|
153 |
\<close> ML \<open>
|
walther@59851
|
154 |
\<close> ML \<open>
|
walther@59851
|
155 |
\<close> ML \<open>
|
wneuper@59553
|
156 |
\<close>
|
wneuper@59553
|
157 |
|
wneuper@59553
|
158 |
ML \<open>
|
wneuper@59553
|
159 |
KEStore_Elems.set_ref_thy @{theory};
|
wneuper@59553
|
160 |
(*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
|
wneuper@59553
|
161 |
\<close>
|
wneuper@59553
|
162 |
|
wneuper@59553
|
163 |
(*---------------------- check test file by testfile -------------------------------------------
|
wneuper@59553
|
164 |
---------------------- check test file by testfile -------------------------------------------*)
|
wneuper@59553
|
165 |
section \<open>trials with Isabelle's functions\<close>
|
wneuper@59553
|
166 |
ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wenzelm@60217
|
167 |
ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
|
wenzelm@60217
|
168 |
ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
|
wenzelm@60217
|
169 |
ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
|
wenzelm@60217
|
170 |
ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
|
wneuper@59553
|
171 |
ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59553
|
172 |
|
wneuper@59553
|
173 |
section \<open>test ML Code of isac\<close>
|
wneuper@59600
|
174 |
subsection \<open>basic code first\<close>
|
wneuper@59553
|
175 |
ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
|
walther@59866
|
176 |
ML_file "BaseDefinitions/libraryC.sml"
|
walther@59866
|
177 |
ML_file "BaseDefinitions/rule-def.sml"
|
walther@59919
|
178 |
ML_file "BaseDefinitions/eval-def.sml"
|
walther@59866
|
179 |
ML_file "BaseDefinitions/rewrite-order.sml"
|
walther@59866
|
180 |
ML_file "BaseDefinitions/theoryC.sml"
|
walther@59866
|
181 |
ML_file "BaseDefinitions/rule.sml"
|
walther@59866
|
182 |
ML_file "BaseDefinitions/thmC-def.sml"
|
walther@59866
|
183 |
ML_file "BaseDefinitions/error-fill-def.sml"
|
walther@59866
|
184 |
ML_file "BaseDefinitions/rule-set.sml"
|
walther@59892
|
185 |
ML_file "BaseDefinitions/check-unique.sml"
|
walther@59932
|
186 |
(*called by Know_Store..*)
|
walther@59866
|
187 |
ML_file "BaseDefinitions/calcelems.sml"
|
walther@59866
|
188 |
ML_file "BaseDefinitions/termC.sml"
|
walther@59912
|
189 |
ML_file "BaseDefinitions/substitution.sml"
|
walther@60317
|
190 |
(** )ML_file "BaseDefinitions/contextC.sml"( *loops with eliminate ThmC.numerals_to_Free*)
|
walther@59866
|
191 |
ML_file "BaseDefinitions/environment.sml"
|
walther@60317
|
192 |
(** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
|
wneuper@59553
|
193 |
(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
|
wneuper@59553
|
194 |
---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
|
walther@59932
|
195 |
|
walther@60317
|
196 |
ML_file "ProgLang/calculate.sml"
|
walther@59964
|
197 |
ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
|
walther@59633
|
198 |
ML_file "ProgLang/listC.sml"
|
walther@59633
|
199 |
ML_file "ProgLang/prog_expr.sml"
|
walther@59633
|
200 |
ML_file "ProgLang/program.sml"
|
walther@59633
|
201 |
ML_file "ProgLang/prog_tac.sml"
|
walther@59763
|
202 |
ML_file "ProgLang/tactical.sml"
|
walther@60317
|
203 |
(** )ML_file "ProgLang/auto_prog.sml"( *loops with eliminate ThmC.numerals_to_Free*)
|
wneuper@59553
|
204 |
(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
|
wneuper@59553
|
205 |
---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
|
wneuper@59600
|
206 |
|
wneuper@59600
|
207 |
subsection \<open>basic functionality on simple example first\<close>
|
wneuper@59553
|
208 |
ML_file "Minisubpbl/000-comments.sml"
|
wneuper@59553
|
209 |
ML_file "Minisubpbl/100-init-rootpbl.sml"
|
wneuper@59553
|
210 |
ML_file "Minisubpbl/150-add-given.sml"
|
walther@59781
|
211 |
ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
|
wneuper@59553
|
212 |
ML_file "Minisubpbl/200-start-method.sml"
|
wneuper@59553
|
213 |
ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
|
walther@59722
|
214 |
ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
|
wneuper@59553
|
215 |
ML_file "Minisubpbl/300-init-subpbl.sml"
|
wneuper@59553
|
216 |
ML_file "Minisubpbl/400-start-meth-subpbl.sml"
|
wneuper@59553
|
217 |
ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
|
walther@59722
|
218 |
ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
|
wneuper@59553
|
219 |
ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
|
wneuper@59553
|
220 |
ML_file "Minisubpbl/500-met-sub-to-root.sml"
|
wneuper@59553
|
221 |
ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
|
walther@59781
|
222 |
ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"
|
wneuper@59553
|
223 |
ML_file "Minisubpbl/600-postcond.sml"
|
wneuper@59553
|
224 |
ML_file "Minisubpbl/700-interSteps.sml"
|
walther@59820
|
225 |
ML_file "Minisubpbl/710-interSteps-short.sml"
|
walther@59836
|
226 |
ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
|
walther@59686
|
227 |
ML_file "Minisubpbl/790-complete.sml"
|
walther@59813
|
228 |
ML_file "Minisubpbl/800-append-on-Frm.sml"
|
wneuper@59600
|
229 |
|
wneuper@59600
|
230 |
subsection \<open>further functionality alongside batch build sequence\<close>
|
walther@59865
|
231 |
ML_file "MathEngBasic/thmC.sml"
|
walther@59865
|
232 |
ML_file "MathEngBasic/rewrite.sml"
|
walther@59728
|
233 |
ML_file "MathEngBasic/tactic.sml"
|
walther@60324
|
234 |
(*ML_file "MathEngBasic/ctree.sml" TOODOO Isa hangs ?!?*)
|
walther@59774
|
235 |
ML_file "MathEngBasic/calculation.sml"
|
walther@59763
|
236 |
|
walther@59996
|
237 |
ML_file "Specify/formalise.sml"
|
walther@59952
|
238 |
ML_file "Specify/o-model.sml"
|
walther@59957
|
239 |
ML_file "Specify/i-model.sml"
|
walther@59996
|
240 |
ML_file "Specify/pre-conditions.sml"
|
walther@59996
|
241 |
ML_file "Specify/p-model.sml"
|
walther@59985
|
242 |
ML_file "Specify/m-match.sml"
|
walther@59967
|
243 |
ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
|
walther@59996
|
244 |
ML_file "Specify/test-out.sml"
|
walther@59996
|
245 |
ML_file "Specify/specify-step.sml"
|
walther@59996
|
246 |
ML_file "Specify/specification.sml"
|
walther@59996
|
247 |
ML_file "Specify/cas-command.sml"
|
walther@59996
|
248 |
ML_file "Specify/p-spec.sml"
|
walther@59996
|
249 |
ML_file "Specify/specify.sml"
|
walther@59800
|
250 |
ML_file "Specify/step-specify.sml"
|
walther@59813
|
251 |
|
walther@59860
|
252 |
ML_file "Interpret/istate.sml"
|
walther@59817
|
253 |
ML_file "Interpret/sub-problem.sml"
|
walther@59909
|
254 |
ML_file "Interpret/error-pattern.sml"
|
walther@59790
|
255 |
ML_file "Interpret/li-tool.sml"
|
wneuper@59561
|
256 |
ML_file "Interpret/lucas-interpreter.sml"
|
walther@60324
|
257 |
ML \<open>
|
walther@60324
|
258 |
\<close> ML \<open>
|
walther@60324
|
259 |
(* Title: "Interpret/lucas-interpreter.sml"
|
walther@60324
|
260 |
Author: Walther Neuper
|
walther@60324
|
261 |
(c) due to copyright terms
|
walther@60324
|
262 |
*)
|
walther@60324
|
263 |
|
walther@60324
|
264 |
"-----------------------------------------------------------------------------------------------";
|
walther@60324
|
265 |
"table of contents -----------------------------------------------------------------------------";
|
walther@60324
|
266 |
"-----------------------------------------------------------------------------------------------";
|
walther@60324
|
267 |
"----------- Take as 1st stac in program -------------------------------------------------------";
|
walther@60324
|
268 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@60324
|
269 |
"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
|
walther@60324
|
270 |
"----------- re-build: fun find_next_step, mini ------------------------------------------------";
|
walther@60324
|
271 |
"----------- re-build: fun locate_input_term ---------------------------------------------------";
|
walther@60324
|
272 |
"-----------------------------------------------------------------------------------------------";
|
walther@60324
|
273 |
"-----------------------------------------------------------------------------------------------";
|
walther@60324
|
274 |
"-----------------------------------------------------------------------------------------------";
|
walther@60324
|
275 |
|
walther@60324
|
276 |
"----------- Take as 1st stac in program -------------------------------------------------------";
|
walther@60324
|
277 |
"----------- Take as 1st stac in program -------------------------------------------------------";
|
walther@60324
|
278 |
"----------- Take as 1st stac in program -------------------------------------------------------";
|
walther@60324
|
279 |
"compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
|
walther@60324
|
280 |
val p = e_pos'; val c = [];
|
walther@60324
|
281 |
val (p,_,f,nxt,_,pt) =
|
walther@60324
|
282 |
CalcTreeTEST
|
walther@60324
|
283 |
[(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
|
walther@60324
|
284 |
("Integrate", ["integrate", "function"], ["diff", "integration"]))];
|
walther@60324
|
285 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
|
walther@60324
|
286 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60324
|
287 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60324
|
288 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60324
|
289 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60324
|
290 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60324
|
291 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60324
|
292 |
case nxt of (Apply_Method ["diff", "integration"]) => ()
|
walther@60324
|
293 |
| _ => error "integrate.sml -- me method [diff,integration] -- spec";
|
walther@60324
|
294 |
"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
|
walther@60324
|
295 |
|
walther@60324
|
296 |
"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
|
walther@60324
|
297 |
"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
|
walther@60324
|
298 |
val Applicable.Yes m = Step.check tac (pt, p);
|
walther@60324
|
299 |
(*if*) Tactic.for_specify' m; (*false*)
|
walther@60324
|
300 |
"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
|
walther@60324
|
301 |
|
walther@60324
|
302 |
"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
|
walther@60324
|
303 |
= (m, (pt, pos));
|
walther@60324
|
304 |
val {srls, ...} = MethodC.from_store mI;
|
walther@60324
|
305 |
val itms = case get_obj I pt p of
|
walther@60324
|
306 |
PblObj {meth=itms, ...} => itms
|
walther@60324
|
307 |
| _ => error "solve Apply_Method: uncovered case get_obj"
|
walther@60324
|
308 |
val thy' = get_obj g_domID pt p;
|
walther@60324
|
309 |
val thy = ThyC.get_theory thy';
|
walther@60324
|
310 |
val srls = LItool.get_simplifier (pt, pos)
|
walther@60324
|
311 |
val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
|
walther@60324
|
312 |
(is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
|
walther@60324
|
313 |
| _ => error "solve Apply_Method: uncovered case init_pstate";
|
walther@60324
|
314 |
(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
|
walther@60324
|
315 |
val ini = LItool.implicit_take sc env;
|
walther@60324
|
316 |
val p = lev_dn p;
|
walther@60324
|
317 |
|
walther@60324
|
318 |
val NONE = (*case*) ini (*of*);
|
walther@60324
|
319 |
val Next_Step (is', ctxt', m') =
|
walther@60324
|
320 |
LI.find_next_step sc (pt, (p, Res)) is ctxt;
|
walther@60324
|
321 |
(*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";
|
walther@60324
|
322 |
val Safe_Step (_, _, Take' _) = (*case*)
|
walther@60324
|
323 |
locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
|
walther@60324
|
324 |
"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
|
walther@60324
|
325 |
= (sc, (pt, (p, Res)), is', ctxt', m');
|
walther@60324
|
326 |
|
walther@60324
|
327 |
(*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
|
walther@60324
|
328 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
|
walther@60324
|
329 |
= ((prog, (cstate, ctxt, tac)), istate);
|
walther@60324
|
330 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
|
walther@60324
|
331 |
|
walther@60324
|
332 |
val Accept_Tac1 (_, _, Take' _) =
|
walther@60324
|
333 |
scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
|
walther@60324
|
334 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
|
walther@60324
|
335 |
= (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
|
walther@60324
|
336 |
|
walther@60324
|
337 |
(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
|
walther@60324
|
338 |
|
walther@60324
|
339 |
(*case*)
|
walther@60324
|
340 |
scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
|
walther@60324
|
341 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@60324
|
342 |
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
|
walther@60324
|
343 |
= (xxx, (ist |> path_down [L, R]), e);
|
walther@60324
|
344 |
val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
|
walther@60324
|
345 |
|
walther@60324
|
346 |
|
walther@60324
|
347 |
|
walther@60324
|
348 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@60324
|
349 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@60324
|
350 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@60324
|
351 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
walther@60324
|
352 |
val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
|
walther@60324
|
353 |
["Test", "squ-equ-test-subpbl1"]);
|
walther@60324
|
354 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@60324
|
355 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
356 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
357 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
358 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
359 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
360 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
361 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
|
walther@60324
|
362 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
|
walther@60324
|
363 |
|
walther@60324
|
364 |
(*//------------------ begin step into ------------------------------------------------------\\*)
|
walther@60324
|
365 |
(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
|
walther@60324
|
366 |
|
walther@60324
|
367 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
|
walther@60324
|
368 |
|
walther@60324
|
369 |
(** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
|
walther@60324
|
370 |
Step.by_tactic tac (pt,p) (*of*);
|
walther@60324
|
371 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
|
walther@60324
|
372 |
val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
|
walther@60324
|
373 |
(*if*) Tactic.for_specify' m; (*false*)
|
walther@60324
|
374 |
|
walther@60324
|
375 |
(** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
|
walther@60324
|
376 |
Step_Solve.by_tactic m ptp;
|
walther@60324
|
377 |
"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
|
walther@60324
|
378 |
(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
|
walther@60324
|
379 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
|
walther@60324
|
380 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@60324
|
381 |
val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
|
walther@60324
|
382 |
|
walther@60324
|
383 |
locate_input_tactic sc (pt, po) (fst is) (snd is) m;
|
walther@60324
|
384 |
"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
|
walther@60324
|
385 |
= (sc, (pt, po), (fst is), (snd is), m);
|
walther@60324
|
386 |
val srls = get_simplifier cstate;
|
walther@60324
|
387 |
|
walther@60324
|
388 |
(** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
|
walther@60324
|
389 |
(*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
|
walther@60324
|
390 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
|
walther@60324
|
391 |
= ((prog, (cstate, ctxt, tac)), istate);
|
walther@60324
|
392 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
|
walther@60324
|
393 |
|
walther@60324
|
394 |
(** )val xxxxx_xx = ( **)
|
walther@60324
|
395 |
scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
|
walther@60324
|
396 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
|
walther@60324
|
397 |
= (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
|
walther@60324
|
398 |
|
walther@60324
|
399 |
(*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
|
walther@60324
|
400 |
"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
|
walther@60324
|
401 |
= (xxx, (ist |> path_down [L, R]), e);
|
walther@60324
|
402 |
|
walther@60324
|
403 |
(*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
|
walther@60324
|
404 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
|
walther@60324
|
405 |
= (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
|
walther@60324
|
406 |
|
walther@60324
|
407 |
(*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
|
walther@60324
|
408 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@60324
|
409 |
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
|
walther@60324
|
410 |
= (xxx, (ist |> path_down [R]), e);
|
walther@60324
|
411 |
val (Program.Tac stac, a') =
|
walther@60324
|
412 |
(*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
|
walther@60324
|
413 |
val LItool.Associated (m, v', ctxt) =
|
walther@60324
|
414 |
(*case*) associate pt ctxt (m, stac) (*of*);
|
walther@60324
|
415 |
|
walther@60324
|
416 |
Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
|
walther@60324
|
417 |
"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
|
walther@60324
|
418 |
= (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
|
walther@60324
|
419 |
|
walther@60324
|
420 |
"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
|
walther@60324
|
421 |
= (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
|
walther@60324
|
422 |
(*if*) LibraryC.assoc (*then*);
|
walther@60324
|
423 |
|
walther@60324
|
424 |
Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
|
walther@60324
|
425 |
"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
|
walther@60324
|
426 |
= (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
|
walther@60324
|
427 |
|
walther@60324
|
428 |
(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
|
walther@60324
|
429 |
val (p'', _, _,pt') =
|
walther@60324
|
430 |
Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
|
walther@60324
|
431 |
(*in*)
|
walther@60324
|
432 |
|
walther@60324
|
433 |
("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
|
walther@60324
|
434 |
[(*ctree NOT cut*)], (pt', p''))) (*return value*);
|
walther@60324
|
435 |
"~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
|
walther@60324
|
436 |
= ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],
|
walther@60324
|
437 |
[(*ctree NOT cut*)], (pt', p'')));
|
walther@60324
|
438 |
|
walther@60324
|
439 |
"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
|
walther@60324
|
440 |
val (_, ts) =
|
walther@60324
|
441 |
(case Step.do_next p ((pt, Pos.e_pos'), []) of
|
walther@60324
|
442 |
("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
|
walther@60324
|
443 |
| ("helpless", _) => ("helpless: cannot propose tac", [])
|
walther@60324
|
444 |
| ("no-fmz-spec", _) => error "no-fmz-spec"
|
walther@60324
|
445 |
| ("end-of-calculation", (ts, _, _)) => ("", ts)
|
walther@60324
|
446 |
| _ => error "me: uncovered case")
|
walther@60324
|
447 |
handle ERROR msg => raise ERROR msg
|
walther@60324
|
448 |
val tac =
|
walther@60324
|
449 |
case ts of
|
walther@60324
|
450 |
tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
|
walther@60324
|
451 |
| _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
|
walther@60324
|
452 |
|
walther@60324
|
453 |
(p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
|
walther@60324
|
454 |
"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
|
walther@60324
|
455 |
= (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
|
walther@60324
|
456 |
|
walther@60324
|
457 |
(*//--------------------- check results from modified me ----------------------------------\\*)
|
walther@60324
|
458 |
if p = ([2], Res) andalso
|
walther@60324
|
459 |
pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
|
walther@60324
|
460 |
then
|
walther@60324
|
461 |
(case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
|
walther@60324
|
462 |
| _ => error "")
|
walther@60324
|
463 |
else error "check results from modified me CHANGED";
|
walther@60324
|
464 |
(*\\--------------------- check results from modified me ----------------------------------//*)
|
walther@60324
|
465 |
|
walther@60324
|
466 |
"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
|
walther@60324
|
467 |
(*\\------------------ end step into --------------------------------------------------------//*)
|
walther@60324
|
468 |
|
walther@60324
|
469 |
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
|
walther@60324
|
470 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
|
walther@60324
|
471 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
|
walther@60324
|
472 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
|
walther@60324
|
473 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
|
walther@60324
|
474 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
|
walther@60324
|
475 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
|
walther@60324
|
476 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
|
walther@60324
|
477 |
(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
|
walther@60324
|
478 |
(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
|
walther@60324
|
479 |
(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
|
walther@60324
|
480 |
(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
|
walther@60324
|
481 |
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
|
walther@60324
|
482 |
(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
|
walther@60324
|
483 |
(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
|
walther@60324
|
484 |
|
walther@60324
|
485 |
(*/--------------------- final test ----------------------------------\\*)
|
walther@60324
|
486 |
if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
|
walther@60324
|
487 |
". ----- pblobj -----\n" ^
|
walther@60324
|
488 |
"1. x + 1 = 2\n" ^
|
walther@60324
|
489 |
"2. x + 1 + - 1 * 2 = 0\n" ^
|
walther@60324
|
490 |
"3. ----- pblobj -----\n" ^
|
walther@60324
|
491 |
"3.1. - 1 + x = 0\n" ^
|
walther@60324
|
492 |
"3.2. x = 0 + - 1 * - 1\n" ^
|
walther@60324
|
493 |
"4. [x = 1]\n"
|
walther@60324
|
494 |
then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
|
walther@60324
|
495 |
else error "re-build: fun locate_input_tactic changed 2";
|
walther@60324
|
496 |
|
walther@60324
|
497 |
|
walther@60324
|
498 |
\<close> ML \<open>
|
walther@60324
|
499 |
"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
|
walther@60324
|
500 |
"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
|
walther@60324
|
501 |
"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
|
walther@60324
|
502 |
(*cp from -- try fun applyTactics ------- *)
|
walther@60324
|
503 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
|
walther@60324
|
504 |
"normalform N"],
|
walther@60324
|
505 |
("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
|
walther@60324
|
506 |
["simplification", "for_polynomials", "with_minus"]))];
|
walther@60324
|
507 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
508 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
509 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
510 |
\<close> ML \<open>
|
walther@60324
|
511 |
f
|
walther@60324
|
512 |
\<close> ML \<open>
|
walther@60324
|
513 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
|
walther@60324
|
514 |
\<close> ML \<open>
|
walther@60325
|
515 |
(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
|
walther@60324
|
516 |
\<close> ML \<open>
|
walther@60324
|
517 |
(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
|
walther@60324
|
518 |
|
walther@60324
|
519 |
\<close> ML \<open>
|
walther@60325
|
520 |
(*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f
|
walther@60324
|
521 |
\<close> ML \<open>
|
walther@60325
|
522 |
\<close> ML \<open> (*GOON*)
|
walther@60324
|
523 |
map Tactic.input_to_string (specific_from_prog pt p)
|
walther@60324
|
524 |
\<close> ML \<open>
|
walther@60324
|
525 |
(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
|
walther@60324
|
526 |
["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
|
walther@60324
|
527 |
"Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
|
walther@60324
|
528 |
then () else error "specific_from_prog ([1], Res) CHANGED";
|
walther@60324
|
529 |
(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
|
walther@60324
|
530 |
|
walther@60324
|
531 |
\<close> ML \<open>
|
walther@60324
|
532 |
(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
|
walther@60324
|
533 |
["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
|
walther@60324
|
534 |
"Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
|
walther@60324
|
535 |
"Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
|
walther@60324
|
536 |
then () else error "specific_from_prog ([1], Res) CHANGED";
|
walther@60324
|
537 |
(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
|
walther@60324
|
538 |
|
walther@60324
|
539 |
\<close> ML \<open>
|
walther@60324
|
540 |
(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
|
walther@60324
|
541 |
(** )val ("ok", (_, _, ptp as (pt, p))) =( **)
|
walther@60324
|
542 |
Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
|
walther@60324
|
543 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
|
walther@60324
|
544 |
val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
|
walther@60324
|
545 |
(*if*) Tactic.for_specify' m; (*false*)
|
walther@60324
|
546 |
|
walther@60324
|
547 |
Step_Solve.by_tactic m (pt, p);
|
walther@60324
|
548 |
"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
|
walther@60324
|
549 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@60324
|
550 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@60324
|
551 |
val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
|
walther@60324
|
552 |
|
walther@60324
|
553 |
(*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
|
walther@60324
|
554 |
"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
|
walther@60324
|
555 |
= (sc, (pt, po), (fst is), (snd is), m);
|
walther@60324
|
556 |
val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
|
walther@60324
|
557 |
|
walther@60324
|
558 |
(*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
|
walther@60324
|
559 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
|
walther@60324
|
560 |
= ((prog, (cstate, ctxt, tac)), istate);
|
walther@60324
|
561 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
|
walther@60324
|
562 |
|
walther@60324
|
563 |
go_scan_up1 (prog, cctt) ist;
|
walther@60324
|
564 |
"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
|
walther@60324
|
565 |
= ((prog, cctt), ist);
|
walther@60324
|
566 |
(*if*) 1 < length path (*then*);
|
walther@60324
|
567 |
|
walther@60324
|
568 |
scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
|
walther@60324
|
569 |
"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Try"(*2*), _) $ _))
|
walther@60324
|
570 |
= (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
|
walther@60324
|
571 |
|
walther@60324
|
572 |
go_scan_up1 pcct ist;
|
walther@60324
|
573 |
"~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
|
walther@60324
|
574 |
= (pcct, ist);
|
walther@60324
|
575 |
(*if*) 1 < length path (*then*);
|
walther@60324
|
576 |
|
walther@60324
|
577 |
scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
|
walther@60324
|
578 |
"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
|
walther@60324
|
579 |
(Const ("Tactical.Chain"(*3*), _) $ _ ))
|
walther@60324
|
580 |
= (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
|
walther@60324
|
581 |
val e2 = check_Seq_up ist prog
|
walther@60324
|
582 |
;
|
walther@60324
|
583 |
(*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
|
walther@60324
|
584 |
"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2))
|
walther@60324
|
585 |
= (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
|
walther@60324
|
586 |
|
walther@60324
|
587 |
(*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
|
walther@60324
|
588 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
|
walther@60324
|
589 |
= (cct, (ist |> path_down [L, R]), e1);
|
walther@60324
|
590 |
|
walther@60324
|
591 |
(*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
|
walther@60324
|
592 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@60324
|
593 |
"~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
|
walther@60324
|
594 |
= (cct, (ist |> path_down [R]), e);
|
walther@60324
|
595 |
(*if*) Tactical.contained_in t (*else*);
|
walther@60324
|
596 |
val (Program.Tac prog_tac, form_arg) = (*case*)
|
walther@60324
|
597 |
LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
|
walther@60324
|
598 |
|
walther@60324
|
599 |
check_tac1 cct ist (prog_tac, form_arg);
|
walther@60324
|
600 |
"~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
|
walther@60324
|
601 |
(cct, ist, (prog_tac, form_arg));
|
walther@60324
|
602 |
val LItool.Not_Associated = (*case*)
|
walther@60324
|
603 |
LItool.associate pt ctxt (tac, prog_tac) (*of*);
|
walther@60324
|
604 |
val _(*ORundef*) = (*case*) or (*of*);
|
walther@60324
|
605 |
val Applicable.Yes m' =
|
walther@60324
|
606 |
(*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
|
walther@60324
|
607 |
|
walther@60324
|
608 |
Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
|
walther@60324
|
609 |
(*return from check_tac1*);
|
walther@60324
|
610 |
"~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
|
walther@60324
|
611 |
(Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
|
walther@60324
|
612 |
|
walther@60324
|
613 |
(*/----- original before child of 7e314dd233fd -------------------------------------------------\* )
|
walther@60324
|
614 |
val (Program.Tac prog_tac, form_arg) = (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
|
walther@60324
|
615 |
val Not_Associated = (*case*) associate pt ctxt (tac, stac) (*of*);
|
walther@60324
|
616 |
val ORundef = (*case*) or (*of*);
|
walther@60324
|
617 |
val Applicable.No "norm_equation not applicable" =
|
walther@60324
|
618 |
(*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") stac) (pt, p) (*of*);
|
walther@60324
|
619 |
|
walther@60324
|
620 |
(Term_Val1 act_arg) (* return value *);
|
walther@60324
|
621 |
|
walther@60324
|
622 |
val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
|
walther@60324
|
623 |
t, (res, asm)) = m;
|
walther@60324
|
624 |
|
walther@60324
|
625 |
if pstate2str ist =
|
walther@60324
|
626 |
"([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], empty, SOME t_t, \n" ^
|
walther@60324
|
627 |
"- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, ORundef, true, false)"
|
walther@60324
|
628 |
andalso
|
walther@60324
|
629 |
UnparseC.term t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
|
walther@60324
|
630 |
andalso
|
walther@60324
|
631 |
UnparseC.term res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
|
walther@60324
|
632 |
andalso
|
walther@60324
|
633 |
UnparseC.terms asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
|
walther@60324
|
634 |
then () else error "locate_input_tactic Helpless, but applicable CHANGED";
|
walther@60324
|
635 |
( *\----- original before child of 7e314dd233fd -------------------------------------------------/*)
|
walther@60324
|
636 |
|
walther@60324
|
637 |
|
walther@60324
|
638 |
\<close> ML \<open>
|
walther@60324
|
639 |
"----------- re-build: fun find_next_step, mini ------------------------------------------------";
|
walther@60324
|
640 |
"----------- re-build: fun find_next_step, mini ------------------------------------------------";
|
walther@60324
|
641 |
"----------- re-build: fun find_next_step, mini ------------------------------------------------";
|
walther@60324
|
642 |
val fmz = ["Term (a + a ::real)", "normalform n_n"];
|
walther@60324
|
643 |
val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
|
walther@60324
|
644 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@60324
|
645 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
|
walther@60324
|
646 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
|
walther@60324
|
647 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
|
walther@60324
|
648 |
(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
|
walther@60324
|
649 |
(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
|
walther@60324
|
650 |
(*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
|
walther@60324
|
651 |
|
walther@60324
|
652 |
Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
|
walther@60324
|
653 |
\<close> ML \<open>
|
walther@60324
|
654 |
(*//------------------ go into 1 ------------------------------------------------------------\\*)
|
walther@60324
|
655 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
|
walther@60324
|
656 |
= (p, ((pt, e_pos'), []));
|
walther@60324
|
657 |
val pIopt = Ctree.get_pblID (pt, ip);
|
walther@60324
|
658 |
(*if*) ip = ([], Res) (*else*);
|
walther@60324
|
659 |
val _ = (*case*) tacis (*of*);
|
walther@60324
|
660 |
val SOME _ = (*case*) pIopt (*of*);
|
walther@60324
|
661 |
(*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
|
walther@60324
|
662 |
|
walther@60324
|
663 |
val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
|
walther@60324
|
664 |
Step_Solve.do_next (pt, ip);
|
walther@60324
|
665 |
"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
walther@60324
|
666 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@60324
|
667 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@60324
|
668 |
val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
|
walther@60324
|
669 |
|
walther@60324
|
670 |
val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
|
walther@60324
|
671 |
LI.find_next_step sc (pt, pos) ist ctxt (*of*);
|
walther@60324
|
672 |
"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
|
walther@60324
|
673 |
= (sc, (pt, pos), ist, ctxt);
|
walther@60324
|
674 |
|
walther@60324
|
675 |
val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
|
walther@60324
|
676 |
(*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
|
walther@60324
|
677 |
"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
|
walther@60324
|
678 |
= ((prog, (ptp, ctxt)), (Pstate ist));
|
walther@60324
|
679 |
(*if*) path = [] (*then*);
|
walther@60324
|
680 |
|
walther@60324
|
681 |
val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
|
walther@60324
|
682 |
scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
|
walther@60324
|
683 |
"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
|
walther@60324
|
684 |
= (cc, (trans_scan_dn ist), (Program.body_of prog));
|
walther@60324
|
685 |
(*if*) Tactical.contained_in t (*else*);
|
walther@60324
|
686 |
val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
|
walther@60324
|
687 |
|
walther@60324
|
688 |
val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
|
walther@60324
|
689 |
check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
|
walther@60324
|
690 |
"~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
|
walther@60324
|
691 |
= (check_tac cc ist (prog_tac, form_arg));
|
walther@60324
|
692 |
|
walther@60324
|
693 |
Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
|
walther@60324
|
694 |
"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
|
walther@60324
|
695 |
= (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
|
walther@60324
|
696 |
|
walther@60324
|
697 |
LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
|
walther@60324
|
698 |
"~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
|
walther@60324
|
699 |
= (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
|
walther@60324
|
700 |
(*\\------------------ end of go into 1 -----------------------------------------------------//*)
|
walther@60324
|
701 |
|
walther@60324
|
702 |
(*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
|
walther@60324
|
703 |
|
walther@60324
|
704 |
Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
|
walther@60324
|
705 |
(*//------------------ go into 2 ------------------------------------------------------------\\*)
|
walther@60324
|
706 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
|
walther@60324
|
707 |
= (p''''', ((pt''''', e_pos'), []));
|
walther@60324
|
708 |
val pIopt = Ctree.get_pblID (pt, ip);
|
walther@60324
|
709 |
(*if*) ip = ([], Res) (*else*);
|
walther@60324
|
710 |
val _ = (*case*) tacis (*of*);
|
walther@60324
|
711 |
val SOME _ = (*case*) pIopt (*of*);
|
walther@60324
|
712 |
(*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
|
walther@60324
|
713 |
|
walther@60324
|
714 |
val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
|
walther@60324
|
715 |
Step_Solve.do_next (pt, ip);
|
walther@60324
|
716 |
"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
walther@60324
|
717 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@60324
|
718 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@60324
|
719 |
val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
|
walther@60324
|
720 |
|
walther@60324
|
721 |
(** )val End_Program (ist, tac) =
|
walther@60324
|
722 |
( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
|
walther@60324
|
723 |
"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
|
walther@60324
|
724 |
= (sc, (pt, pos), ist, ctxt);
|
walther@60324
|
725 |
|
walther@60324
|
726 |
(* val Term_Val (Const ("Groups.times_class.times", _) $ Free ("2", _) $ Free ("a", _))*)
|
walther@60324
|
727 |
(** )val Term_Val prog_result =
|
walther@60324
|
728 |
( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
|
walther@60324
|
729 |
"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
|
walther@60324
|
730 |
= ((prog, (ptp, ctxt)), (Pstate ist));
|
walther@60324
|
731 |
(*if*) path = [] (*else*);
|
walther@60324
|
732 |
|
walther@60324
|
733 |
go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
|
walther@60324
|
734 |
"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
|
walther@60324
|
735 |
= ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
|
walther@60324
|
736 |
(*if*) path = [R] (*then*);
|
walther@60324
|
737 |
(*if*) found_accept = true (*then*);
|
walther@60324
|
738 |
|
walther@60324
|
739 |
Term_Val act_arg (*return from go_scan_up*);
|
walther@60324
|
740 |
"~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
|
walther@60324
|
741 |
|
walther@60324
|
742 |
Term_Val prog_result (*return from scan_to_tactic*);
|
walther@60324
|
743 |
"~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
|
walther@60324
|
744 |
val (true, p', _) = (*case*) parent_node pt p (*of*);
|
walther@60324
|
745 |
val (_, pblID, _) = get_obj g_spec pt p';
|
walther@60324
|
746 |
|
walther@60324
|
747 |
End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
|
walther@60324
|
748 |
(*return from find_next_step*);
|
walther@60324
|
749 |
"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
|
walther@60324
|
750 |
= (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
|
walther@60324
|
751 |
val _ = (*case*) tac (*of*);
|
walther@60324
|
752 |
|
walther@60324
|
753 |
val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
|
walther@60324
|
754 |
= LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
|
walther@60324
|
755 |
"~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
|
walther@60324
|
756 |
= (LI.by_tactic tac (ist, ctxt) ptp);
|
walther@60324
|
757 |
(*\\------------------ end of go into 2 -----------------------------------------------------//*)
|
walther@60324
|
758 |
|
walther@60324
|
759 |
(*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
|
walther@60324
|
760 |
|
walther@60324
|
761 |
Test_Tool.show_pt_tac pt; (*[
|
walther@60324
|
762 |
([], Frm), Simplify (a + a)
|
walther@60324
|
763 |
. . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
|
walther@60324
|
764 |
([1], Frm), a + a
|
walther@60324
|
765 |
. . . . . . . . . . Rewrite_Set "norm_Poly",
|
walther@60324
|
766 |
([1], Res), 2 * a
|
walther@60324
|
767 |
. . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
|
walther@60324
|
768 |
([], Res), 2 * a]*)
|
walther@60324
|
769 |
|
walther@60324
|
770 |
(*/--- final test ---------------------------------------------------------------------------\\*)
|
walther@60324
|
771 |
val (res, asm) = (get_obj g_result pt (fst p));
|
walther@60324
|
772 |
if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
|
walther@60324
|
773 |
andalso p = ([], Und) andalso msg = "end-of-calculation"
|
walther@60324
|
774 |
andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
|
walther@60324
|
775 |
then
|
walther@60324
|
776 |
case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
|
walther@60324
|
777 |
| _ => error "re-build: fun find_next_step, mini 1"
|
walther@60324
|
778 |
else error "re-build: fun find_next_step, mini 2"
|
walther@60324
|
779 |
|
walther@60324
|
780 |
|
walther@60324
|
781 |
\<close> ML \<open>
|
walther@60324
|
782 |
"----------- re-build: fun locate_input_term ---------------------------------------------------";
|
walther@60324
|
783 |
"----------- re-build: fun locate_input_term ---------------------------------------------------";
|
walther@60324
|
784 |
"----------- re-build: fun locate_input_term ---------------------------------------------------";
|
walther@60324
|
785 |
(*cp from inform.sml
|
walther@60324
|
786 |
----------- appendFormula: on Res + late deriv ------------------------------------------------*)
|
walther@60324
|
787 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
walther@60324
|
788 |
val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
|
walther@60324
|
789 |
["Test", "squ-equ-test-subpbl1"]);
|
walther@60324
|
790 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@60324
|
791 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
792 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
793 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
794 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
795 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
796 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60324
|
797 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
|
walther@60324
|
798 |
|
walther@60324
|
799 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
|
walther@60324
|
800 |
(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
|
walther@60324
|
801 |
|
walther@60324
|
802 |
(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
|
walther@60324
|
803 |
(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
|
walther@60324
|
804 |
|
walther@60324
|
805 |
Test_Tool.show_pt_tac pt; (*[
|
walther@60324
|
806 |
([], Frm), solve (x + 1 = 2, x)
|
walther@60324
|
807 |
. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
|
walther@60324
|
808 |
([1], Frm), x + 1 = 2
|
walther@60324
|
809 |
. . . . . . . . . . Rewrite_Set "norm_equation",
|
walther@60324
|
810 |
([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
|
walther@60324
|
811 |
|
walther@60324
|
812 |
(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
|
walther@60324
|
813 |
"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
|
walther@60324
|
814 |
val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
|
walther@60324
|
815 |
val pos = (*get_pos cI 1*) p
|
walther@60324
|
816 |
|
walther@60324
|
817 |
(*+*)val ptp''''' = (pt, p);
|
walther@60324
|
818 |
(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
|
walther@60324
|
819 |
(*+*)Test_Tool.show_pt_tac pt; (*[
|
walther@60324
|
820 |
(*+*)([], Frm), solve (x + 1 = 2, x)
|
walther@60324
|
821 |
(*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
|
walther@60324
|
822 |
(*+*)([1], Frm), x + 1 = 2
|
walther@60324
|
823 |
(*+*). . . . . . . . . . Rewrite_Set "norm_equation",
|
walther@60324
|
824 |
(*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
|
walther@60324
|
825 |
|
walther@60324
|
826 |
val ("ok", cs' as (_, _, ptp')) =
|
walther@60324
|
827 |
(*case*) Step.do_next pos cs (*of*);
|
walther@60324
|
828 |
|
walther@60324
|
829 |
val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
|
walther@60324
|
830 |
Step_Solve.by_term ptp' (encode ifo) (*of*);
|
walther@60324
|
831 |
"~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
|
walther@60324
|
832 |
= (ptp', (encode ifo));
|
walther@60324
|
833 |
val SOME f_in =
|
walther@60324
|
834 |
(*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
|
walther@60324
|
835 |
val f_in = Thm.term_of f_in
|
walther@60324
|
836 |
val pos_pred = lev_back(*'*) pos
|
walther@60324
|
837 |
val f_pred = Ctree.get_curr_formula (pt, pos_pred);
|
walther@60324
|
838 |
val f_succ = Ctree.get_curr_formula (pt, pos);
|
walther@60324
|
839 |
(*if*) f_succ = f_in (*else*);
|
walther@60324
|
840 |
val NONE =
|
walther@60324
|
841 |
(*case*) CAS_Cmd.input f_in (*of*);
|
walther@60324
|
842 |
|
walther@60324
|
843 |
(*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
|
walther@60324
|
844 |
(*old*) val {scr = prog, ...} = MethodC.from_store metID
|
walther@60324
|
845 |
(*old*) val istate = get_istate_LI pt pos
|
walther@60324
|
846 |
(*old*) val ctxt = get_ctxt pt pos
|
walther@60324
|
847 |
val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
|
walther@60324
|
848 |
LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
|
walther@60324
|
849 |
"~~~~~ fun locate_input_term , args:"; val ((Rule.Prog _), ((pt, pos) : Calc.T), (_ : Istate.T), (_ : Proof.context), tm)
|
walther@60324
|
850 |
= (prog, (pt, pos), istate, ctxt, f_in);
|
walther@60324
|
851 |
( *old*)
|
walther@60324
|
852 |
|
walther@60324
|
853 |
(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
|
walther@60324
|
854 |
"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
|
walther@60324
|
855 |
val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
|
walther@60324
|
856 |
|
walther@60324
|
857 |
val ("ok", (_, _, cstate as (pt', pos'))) =
|
walther@60324
|
858 |
(*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
|
walther@60324
|
859 |
|
walther@60324
|
860 |
(*old* )
|
walther@60324
|
861 |
Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
|
walther@60324
|
862 |
( *old*)
|
walther@60324
|
863 |
(*NEW*) Found_Step cstate (*return from locate_input_term*);
|
walther@60324
|
864 |
(*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
|
walther@60324
|
865 |
"~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
|
walther@60324
|
866 |
= (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
|
walther@60324
|
867 |
|
walther@60324
|
868 |
("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
|
walther@60324
|
869 |
"~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
|
walther@60324
|
870 |
= ("ok", ([], [], ptp));
|
walther@60324
|
871 |
|
walther@60324
|
872 |
(*fun me requires nxt...*)
|
walther@60324
|
873 |
Step.do_next p''''' (ptp''''', []);
|
walther@60324
|
874 |
val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
|
walther@60324
|
875 |
(pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
|
walther@60324
|
876 |
(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
|
walther@60324
|
877 |
|
walther@60324
|
878 |
(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
|
walther@60324
|
879 |
(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
|
walther@60324
|
880 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
|
walther@60324
|
881 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
|
walther@60324
|
882 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
|
walther@60324
|
883 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
|
walther@60324
|
884 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
|
walther@60324
|
885 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
|
walther@60324
|
886 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
|
walther@60324
|
887 |
(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
|
walther@60324
|
888 |
(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
|
walther@60324
|
889 |
(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
|
walther@60324
|
890 |
(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
|
walther@60324
|
891 |
( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
|
walther@60324
|
892 |
|
walther@60324
|
893 |
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
|
walther@60324
|
894 |
(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
|
walther@60324
|
895 |
(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
|
walther@60324
|
896 |
|
walther@60324
|
897 |
(*/--- final test ---------------------------------------------------------------------------\\*)
|
walther@60324
|
898 |
if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
|
walther@60324
|
899 |
". ----- pblobj -----\n" ^
|
walther@60324
|
900 |
"1. x + 1 = 2\n" ^
|
walther@60324
|
901 |
"2. x + 1 + - 1 * 2 = 0\n" ^
|
walther@60324
|
902 |
"3. ----- pblobj -----\n" ^
|
walther@60324
|
903 |
"3.1. - 1 + x = 0\n" ^
|
walther@60324
|
904 |
"3.2. x = 0 + - 1 * - 1\n" ^
|
walther@60324
|
905 |
"3.2.1. x = 0 + - 1 * - 1\n" ^
|
walther@60324
|
906 |
"3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
|
walther@60324
|
907 |
then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
|
walther@60324
|
908 |
else error "re-build: fun locate_input_term CHANGED 2";
|
walther@60324
|
909 |
|
walther@60324
|
910 |
Test_Tool.show_pt_tac pt; (*[
|
walther@60324
|
911 |
([], Frm), solve (x + 1 = 2, x)
|
walther@60324
|
912 |
. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
|
walther@60324
|
913 |
([1], Frm), x + 1 = 2
|
walther@60324
|
914 |
. . . . . . . . . . Rewrite_Set "norm_equation",
|
walther@60324
|
915 |
([1], Res), x + 1 + - 1 * 2 = 0
|
walther@60324
|
916 |
. . . . . . . . . . Rewrite_Set "Test_simplify",
|
walther@60324
|
917 |
([2], Res), - 1 + x = 0
|
walther@60324
|
918 |
. . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
|
walther@60324
|
919 |
([3], Pbl), solve (- 1 + x = 0, x)
|
walther@60324
|
920 |
. . . . . . . . . . Apply_Method ["Test", "solve_linear"],
|
walther@60324
|
921 |
([3,1], Frm), - 1 + x = 0
|
walther@60324
|
922 |
. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
|
walther@60324
|
923 |
([3,1], Res), x = 0 + - 1 * - 1
|
walther@60324
|
924 |
. . . . . . . . . . Derive Test_simplify,
|
walther@60324
|
925 |
([3,2,1], Frm), x = 0 + - 1 * - 1
|
walther@60324
|
926 |
. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
|
walther@60324
|
927 |
([3,2,1], Res), x = 0 + 1
|
walther@60324
|
928 |
. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
|
walther@60324
|
929 |
([3,2,2], Res), x = 1
|
walther@60324
|
930 |
. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
|
walther@60324
|
931 |
([3,2], Res), x = 1
|
walther@60324
|
932 |
. . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
|
walther@60324
|
933 |
([3], Res), [x = 1]
|
walther@60324
|
934 |
. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
|
walther@60324
|
935 |
([], Res), [x = 1]]*)
|
walther@60324
|
936 |
|
walther@60324
|
937 |
\<close> ML \<open>
|
walther@60324
|
938 |
\<close> ML \<open>
|
walther@60324
|
939 |
\<close> ML \<open>
|
walther@60324
|
940 |
\<close> ML \<open>
|
walther@60324
|
941 |
\<close> ML \<open>
|
walther@60324
|
942 |
\<close> ML \<open>
|
walther@60324
|
943 |
\<close> ML \<open>
|
walther@60324
|
944 |
\<close> ML \<open>
|
walther@60324
|
945 |
\<close> ML \<open>
|
walther@60324
|
946 |
\<close>
|
walther@59751
|
947 |
ML_file "Interpret/step-solve.sml"
|
walther@59751
|
948 |
|
walther@60317
|
949 |
ML_file "MathEngine/me-misc.sml"
|
walther@59823
|
950 |
ML_file "MathEngine/fetch-tactics.sml"
|
walther@60317
|
951 |
(** )ML_file "MathEngine/solve.sml"( *loops with eliminate ThmC.numerals_to_Free*)
|
walther@59763
|
952 |
ML_file "MathEngine/step.sml"
|
walther@60317
|
953 |
(** )
|
wneuper@59600
|
954 |
ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
|
walther@60317
|
955 |
( *loops with eliminate ThmC.numerals_to_Free*)
|
walther@60317
|
956 |
ML_file "MathEngine/messages.sml"
|
wneuper@59600
|
957 |
ML_file "MathEngine/states.sml"
|
wneuper@59600
|
958 |
|
walther@59917
|
959 |
ML_file "BridgeLibisabelle/thy-present.sml"
|
wneuper@59600
|
960 |
ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
|
walther@60277
|
961 |
ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
|
wneuper@59600
|
962 |
ML_file "BridgeLibisabelle/thy-hierarchy.sml"
|
wneuper@59600
|
963 |
ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
|
walther@60317
|
964 |
(** )ML_file "BridgeLibisabelle/interface.sml"( *loops with eliminate ThmC.numerals_to_Free*)
|
wneuper@59553
|
965 |
(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
|
wneuper@59553
|
966 |
... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
|
wneuper@59600
|
967 |
|
walther@60044
|
968 |
ML_file "BridgeJEdit/parseC.sml"
|
walther@60146
|
969 |
ML_file "BridgeJEdit/preliminary.sml"
|
walther@60044
|
970 |
|
wneuper@59553
|
971 |
ML_file "Knowledge/delete.sml"
|
wneuper@59553
|
972 |
ML_file "Knowledge/descript.sml"
|
wneuper@59553
|
973 |
ML_file "Knowledge/simplify.sml"
|
walther@60248
|
974 |
ML_file "Knowledge/poly.sml"
|
walther@60325
|
975 |
ML \<open>
|
walther@60325
|
976 |
\<close> ML \<open>
|
walther@60325
|
977 |
\<close> ML \<open>
|
walther@60325
|
978 |
\<close> ML \<open>
|
walther@60325
|
979 |
\<close> ML \<open>
|
walther@60325
|
980 |
\<close> ML \<open>
|
walther@60325
|
981 |
\<close> ML \<open>
|
walther@60325
|
982 |
\<close> ML \<open>
|
walther@60325
|
983 |
\<close> ML \<open>
|
walther@60325
|
984 |
\<close> ML \<open>
|
walther@60325
|
985 |
\<close> ML \<open>
|
walther@60325
|
986 |
\<close>
|
wneuper@59553
|
987 |
ML_file "Knowledge/gcd_poly_ml.sml"
|
wneuper@59553
|
988 |
ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
|
walther@60318
|
989 |
ML_file "Knowledge/rational.sml" (*Test_Isac_Short*)
|
wneuper@59553
|
990 |
ML_file "Knowledge/equation.sml"
|
wneuper@59553
|
991 |
ML_file "Knowledge/root.sml"
|
wneuper@59553
|
992 |
ML_file "Knowledge/lineq.sml"
|
walther@60318
|
993 |
|
wneuper@59553
|
994 |
(*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
|
walther@59628
|
995 |
(*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*)
|
walther@60318
|
996 |
ML_file "Knowledge/r/ootrat.sml"
|
wneuper@59553
|
997 |
ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
|
walther@59628
|
998 |
(*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
|
walther@59628
|
999 |
ML_file "Knowledge/polyeq-1.sml"
|
walther@59636
|
1000 |
(*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*)
|
wneuper@59553
|
1001 |
(*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
|
wneuper@59553
|
1002 |
ML_file "Knowledge/calculus.sml"
|
wneuper@59553
|
1003 |
ML_file "Knowledge/trig.sml"
|
wneuper@59553
|
1004 |
(*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
|
wneuper@59553
|
1005 |
ML_file "Knowledge/diff.sml"
|
wneuper@59553
|
1006 |
ML_file "Knowledge/integrate.sml"
|
wneuper@59553
|
1007 |
ML_file "Knowledge/eqsystem.sml"
|
walther@59996
|
1008 |
ML_file "Knowledge/test.sml"
|
wneuper@59553
|
1009 |
ML_file "Knowledge/polyminus.sml"
|
wneuper@59553
|
1010 |
ML_file "Knowledge/vect.sml"
|
wneuper@59553
|
1011 |
ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
|
walther@60090
|
1012 |
ML_file "Knowledge/biegelinie-1.sml"
|
walther@59628
|
1013 |
(*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*)
|
walther@59628
|
1014 |
(*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*)
|
walther@60317
|
1015 |
(** )ML_file "Knowledge/biegelinie-4.sml"( *loops with eliminate ThmC.numerals_to_Free*)
|
walther@60317
|
1016 |
(** )ML_file "Knowledge/algein.sml"( *loops with eliminate ThmC.numerals_to_Free*)
|
wneuper@59553
|
1017 |
ML_file "Knowledge/diophanteq.sml"
|
walther@59628
|
1018 |
(*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
|
wneuper@59553
|
1019 |
ML_file "Knowledge/inssort.sml"
|
wneuper@59553
|
1020 |
ML_file "Knowledge/isac.sml"
|
wneuper@59553
|
1021 |
ML_file "Knowledge/build_thydata.sml"
|
wneuper@59600
|
1022 |
|
walther@59814
|
1023 |
ML_file "Test_Code/test-code.sml"
|
walther@59814
|
1024 |
|
walther@59617
|
1025 |
section \<open>further tests additional to src/.. files\<close>
|
wneuper@59600
|
1026 |
ML_file "BridgeLibisabelle/use-cases.sml"
|
wneuper@59600
|
1027 |
|
wneuper@59553
|
1028 |
ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59553
|
1029 |
ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59553
|
1030 |
ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
walther@60262
|
1031 |
ML \<open>
|
walther@60262
|
1032 |
\<close> ML \<open>
|
wneuper@59561
|
1033 |
\<close> ML \<open>
|
walther@59804
|
1034 |
\<close> ML \<open>
|
walther@59804
|
1035 |
\<close> ML \<open>
|
walther@59804
|
1036 |
\<close> ML \<open>
|
walther@59804
|
1037 |
\<close> ML \<open>
|
walther@59804
|
1038 |
\<close> ML \<open>
|
walther@59804
|
1039 |
\<close> ML \<open>
|
walther@59804
|
1040 |
\<close> ML \<open>
|
walther@59804
|
1041 |
\<close> ML \<open>
|
wneuper@59561
|
1042 |
\<close>
|
wneuper@59553
|
1043 |
|
wneuper@59553
|
1044 |
section \<open>history of tests\<close>
|
wneuper@59553
|
1045 |
text \<open>
|
wneuper@59553
|
1046 |
Systematic regression tests have been introduced to isac development in 2003.
|
wneuper@59553
|
1047 |
Sanity of the regression tests suffers from updates following Isabelle development,
|
wneuper@59553
|
1048 |
which mostly exceeded the resources available in isac's development.
|
wneuper@59553
|
1049 |
|
wneuper@59553
|
1050 |
The survey below shall support to efficiently use the tests for isac
|
wneuper@59553
|
1051 |
on different Isabelle versions. Conclusion in most cases will be:
|
wneuper@59553
|
1052 |
|
wneuper@59553
|
1053 |
!!! Use most recent tests or go back to the old notebook
|
wneuper@59553
|
1054 |
with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
wneuper@59553
|
1055 |
\<close>
|
wneuper@59553
|
1056 |
|
wneuper@59553
|
1057 |
|
wneuper@59553
|
1058 |
subsection \<open>isac on Isabelle2017\<close>
|
wneuper@59553
|
1059 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1060 |
text \<open>
|
wneuper@59553
|
1061 |
* Add further signatures, separate structures and cleanup respective files.
|
wneuper@59553
|
1062 |
* Show feasibility of moving Isac programs to partial_function, i.e. to the function package.
|
wneuper@59553
|
1063 |
* Clean theory dependencies.
|
wneuper@59553
|
1064 |
* Start preparing shift from isac-java to Isabelle/jEdit.
|
wneuper@59553
|
1065 |
\<close>
|
wneuper@59553
|
1066 |
subsubsection \<open>State of tests: unchanged\<close>
|
wneuper@59553
|
1067 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
1068 |
text \<open>
|
wneuper@59553
|
1069 |
last changeset with Test_Isac 925fef0f4c81
|
wneuper@59553
|
1070 |
first changeset with Test_Isac bbb414976dfe
|
wneuper@59553
|
1071 |
\<close>
|
wneuper@59553
|
1072 |
|
wneuper@59553
|
1073 |
subsection \<open>isac on Isabelle2015\<close>
|
wneuper@59553
|
1074 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1075 |
text \<open>
|
wneuper@59553
|
1076 |
* Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
|
wneuper@59553
|
1077 |
This complicates Test_Isac, see "Prepare running tests" above.
|
wneuper@59553
|
1078 |
* Remove TTY interface.
|
wneuper@59553
|
1079 |
* Re-activate insertion sort.
|
wneuper@59553
|
1080 |
\<close>
|
wneuper@59553
|
1081 |
subsubsection \<open>State of tests: unchanged\<close>
|
wneuper@59553
|
1082 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
1083 |
text \<open>
|
wneuper@59553
|
1084 |
last changeset with Test_Isac 2f1b2854927a
|
wneuper@59553
|
1085 |
first changeset with Test_Isac ???
|
wneuper@59553
|
1086 |
\<close>
|
wneuper@59553
|
1087 |
|
wneuper@59553
|
1088 |
subsection \<open>isac on Isabelle2014\<close>
|
wneuper@59553
|
1089 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1090 |
text \<open>
|
wneuper@59553
|
1091 |
migration from "isabelle tty" --> libisabelle
|
wneuper@59553
|
1092 |
\<close>
|
wneuper@59553
|
1093 |
|
wneuper@59553
|
1094 |
subsection \<open>isac on Isabelle2013-2\<close>
|
wneuper@59553
|
1095 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1096 |
text \<open>
|
wneuper@59553
|
1097 |
reactivated context_thy
|
wneuper@59553
|
1098 |
\<close>
|
wneuper@59553
|
1099 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
1100 |
text \<open>
|
wneuper@59553
|
1101 |
TODO
|
wneuper@59553
|
1102 |
\<close>
|
wneuper@59553
|
1103 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
1104 |
text \<open>
|
wneuper@59553
|
1105 |
TODO
|
wneuper@59553
|
1106 |
:
|
wneuper@59553
|
1107 |
: isac on Isablle2013-2
|
wneuper@59553
|
1108 |
:
|
wneuper@59553
|
1109 |
Changeset: 55318 (03826ceb24da) merged
|
wneuper@59553
|
1110 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1111 |
Date: 2013-12-12 14:27:37 +0100 (7 minutes)
|
wneuper@59553
|
1112 |
\<close>
|
wneuper@59553
|
1113 |
|
wneuper@59553
|
1114 |
subsection \<open>isac on Isabelle2013-1\<close>
|
wneuper@59553
|
1115 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1116 |
text \<open>
|
wneuper@59553
|
1117 |
Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
|
wneuper@59553
|
1118 |
no significant development steps for ISAC.
|
wneuper@59553
|
1119 |
\<close>
|
wneuper@59553
|
1120 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
1121 |
text \<open>
|
wneuper@59553
|
1122 |
See points in subsection "isac on Isabelle2011", "State of tests".
|
wneuper@59553
|
1123 |
\<close>
|
wneuper@59553
|
1124 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
1125 |
text \<open>
|
wneuper@59553
|
1126 |
Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
|
wneuper@59553
|
1127 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1128 |
Date: 2013-12-03 18:13:31 +0100 (8 days)
|
wneuper@59553
|
1129 |
:
|
wneuper@59553
|
1130 |
: isac on Isablle2013-1
|
wneuper@59553
|
1131 |
:
|
wneuper@59553
|
1132 |
Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
|
wneuper@59553
|
1133 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1134 |
Date: 2013-11-21 18:12:17 +0100 (2 weeks)
|
wneuper@59553
|
1135 |
|
wneuper@59553
|
1136 |
\<close>
|
wneuper@59553
|
1137 |
|
wneuper@59553
|
1138 |
subsection \<open>isac on Isabelle2013\<close>
|
wneuper@59553
|
1139 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1140 |
text \<open>
|
wneuper@59553
|
1141 |
# Oct.13: replaced "axioms" by "axiomatization"
|
wneuper@59553
|
1142 |
# Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
|
wneuper@59553
|
1143 |
# Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
|
wneuper@59553
|
1144 |
simplification of multivariate rationals (without improving the rulesets involved).
|
wneuper@59553
|
1145 |
\<close>
|
wneuper@59553
|
1146 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
1147 |
text \<open>
|
wneuper@59553
|
1148 |
Is standard now; this subsection will be discontinued under Isabelle2013-1
|
wneuper@59553
|
1149 |
\<close>
|
wneuper@59553
|
1150 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
1151 |
text \<open>
|
wneuper@59553
|
1152 |
See points in subsection "isac on Isabelle2011", "State of tests".
|
wneuper@59553
|
1153 |
# re-activated listC.sml
|
wneuper@59553
|
1154 |
\<close>
|
wneuper@59553
|
1155 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
1156 |
text \<open>
|
wneuper@59553
|
1157 |
changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
|
wneuper@59553
|
1158 |
User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
|
wneuper@59553
|
1159 |
Date: Tue Nov 19 22:23:30 2013 +0000
|
wneuper@59553
|
1160 |
:
|
wneuper@59553
|
1161 |
: isac on Isablle2013
|
wneuper@59553
|
1162 |
:
|
wneuper@59553
|
1163 |
Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
|
wneuper@59553
|
1164 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1165 |
Date: 2013-07-15 08:28:50 +0200 (4 weeks)
|
wneuper@59553
|
1166 |
\<close>
|
wneuper@59553
|
1167 |
|
wneuper@59553
|
1168 |
subsection \<open>isac on Isabelle2012\<close>
|
wneuper@59553
|
1169 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1170 |
text \<open>
|
wneuper@59553
|
1171 |
isac on Isabelle2012 is considered just a transitional stage
|
wneuper@59553
|
1172 |
within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
|
wneuper@59553
|
1173 |
For considerations on the transition see
|
wenzelm@60192
|
1174 |
$ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..".
|
wneuper@59553
|
1175 |
\<close>
|
wneuper@59553
|
1176 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
1177 |
text \<open>
|
wneuper@59553
|
1178 |
$ cd /usr/local/isabisac12/
|
wneuper@59553
|
1179 |
$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
|
wneuper@59553
|
1180 |
$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
|
wneuper@59553
|
1181 |
\<close>
|
wneuper@59553
|
1182 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
1183 |
text \<open>
|
wneuper@59553
|
1184 |
At least the tests from isac on Isabelle2011 run again.
|
wneuper@59553
|
1185 |
However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
|
wneuper@59553
|
1186 |
in parallel with evaluation.
|
wneuper@59553
|
1187 |
|
wneuper@59553
|
1188 |
Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
|
wneuper@59553
|
1189 |
yields 69 hits, some of which were already present before Isabelle2002-->2009-2
|
wneuper@59553
|
1190 |
(i.e. on the old notebook from 2002).
|
wneuper@59553
|
1191 |
|
wneuper@59553
|
1192 |
Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
|
wneuper@59553
|
1193 |
# === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
|
wneuper@59553
|
1194 |
# === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
|
wneuper@59553
|
1195 |
# === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
|
wneuper@59553
|
1196 |
Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
|
wneuper@59553
|
1197 |
|
wneuper@59553
|
1198 |
Some tests have been re-activated (e.g. error patterns, fill patterns).
|
wneuper@59553
|
1199 |
\<close>
|
wneuper@59553
|
1200 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
1201 |
text \<open>
|
wneuper@59553
|
1202 |
Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
|
wneuper@59553
|
1203 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1204 |
Date: 2013-07-11 16:58:31 +0200 (4 weeks)
|
wneuper@59553
|
1205 |
:
|
wneuper@59553
|
1206 |
: isac on Isablle2012
|
wneuper@59553
|
1207 |
:
|
wneuper@59553
|
1208 |
Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
|
wneuper@59553
|
1209 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1210 |
Date: 2012-09-24 18:35:13 +0200 (8 months)
|
wneuper@59553
|
1211 |
------------------------------------------------------------------------------
|
wneuper@59553
|
1212 |
Changeset: 48756 (7443906996a8) merged
|
wneuper@59553
|
1213 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1214 |
Date: 2012-09-24 18:15:49 +0200 (8 months)
|
wneuper@59553
|
1215 |
\<close>
|
wneuper@59553
|
1216 |
|
wneuper@59553
|
1217 |
subsection \<open>isac on Isabelle2011\<close>
|
wneuper@59553
|
1218 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1219 |
text \<open>
|
wneuper@59553
|
1220 |
isac's mathematics engine has been extended by two developments:
|
wneuper@59553
|
1221 |
(1) Isabelle's contexts were introduced by Mathias Lehnfeld
|
wneuper@59553
|
1222 |
(2) Z_Transform was introduced by Jan Rocnik, which revealed
|
wneuper@59553
|
1223 |
further errors introduced by (1).
|
wneuper@59553
|
1224 |
(3) "error patterns" were introduced by Gabriella Daroczy
|
wneuper@59553
|
1225 |
Regressions tests have been added for all of these.
|
wneuper@59553
|
1226 |
\<close>
|
wneuper@59553
|
1227 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
1228 |
text \<open>
|
wneuper@59553
|
1229 |
$ cd /usr/local/isabisac11/
|
wneuper@59553
|
1230 |
$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
|
wneuper@59553
|
1231 |
$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
|
wneuper@59553
|
1232 |
\<close>
|
wneuper@59553
|
1233 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
1234 |
text \<open>
|
wneuper@59553
|
1235 |
Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
|
wneuper@59553
|
1236 |
and sometimes give reasons for failing tests.
|
wneuper@59553
|
1237 |
(*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
|
wneuper@59553
|
1238 |
work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
|
wneuper@59553
|
1239 |
|
wneuper@59553
|
1240 |
The most signification tests (in particular Frontend/interface.sml) run,
|
wneuper@59553
|
1241 |
however, many "error in kernel" are not caught by an exception.
|
wneuper@59553
|
1242 |
------------------------------------------------------------------------------
|
wneuper@59553
|
1243 |
After the changeset below Test_Isac worked with check_unsynchronized_ref ():
|
wneuper@59553
|
1244 |
------------------------------------------------------------------------------
|
wneuper@59553
|
1245 |
Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
|
wneuper@59553
|
1246 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1247 |
Date: 2012-08-06 10:38:11 +0200 (11 months)
|
wneuper@59553
|
1248 |
|
wneuper@59553
|
1249 |
|
wneuper@59553
|
1250 |
The list below records TODOs while producing an ISAC kernel for
|
wneuper@59553
|
1251 |
gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
|
wneuper@59553
|
1252 |
(so to be resumed with Isabelle2013-1):
|
wneuper@59553
|
1253 |
############## WNxxxxxx.TODO can be found in sources ##############
|
wneuper@59553
|
1254 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1255 |
WN111013.TODO: lots of cleanup/removal in test/../Test.thy
|
wneuper@59553
|
1256 |
--------------------------------------------------------------------------------
|
walther@59845
|
1257 |
WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with
|
wneuper@59553
|
1258 |
this special case (see) --- why not nxt = Model_Problem here ? ---
|
wneuper@59553
|
1259 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1260 |
WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
|
wneuper@59553
|
1261 |
... FIRST redesign
|
wneuper@59553
|
1262 |
# simplify_* , *_simp_*
|
wneuper@59553
|
1263 |
# norm_*
|
wneuper@59553
|
1264 |
# calc_* , calculate_* ... require iteration over all rls ...
|
wneuper@59553
|
1265 |
... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
|
wneuper@59553
|
1266 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1267 |
WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
|
wneuper@59553
|
1268 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1269 |
WN120314 changeset a393bb9f5e9f drops root equations.
|
wneuper@59553
|
1270 |
see test/Tools/isac/Knowledge/rootrateq.sml
|
wneuper@59553
|
1271 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1272 |
WN120317.TODO changeset 977788dfed26 dropped rateq:
|
wneuper@59553
|
1273 |
# test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
|
walther@60242
|
1274 |
# test --- solve (1/x = 5, x) by me --- and --- x / (x \<up> 2 - 6 * x + 9) - ...:
|
wneuper@59553
|
1275 |
investigation Check_elementwise stopped due to too much effort finding out,
|
wneuper@59553
|
1276 |
why Check_elementwise worked in 2002 in spite of the error.
|
wneuper@59553
|
1277 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1278 |
WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
|
wneuper@59553
|
1279 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1280 |
WN120317.TODO found by test --- interSteps for Schalk 299a --- that
|
wneuper@59553
|
1281 |
NO test with 'interSteps' is checked properly (with exn on changed behaviour)
|
wneuper@59553
|
1282 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1283 |
WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
|
wneuper@59553
|
1284 |
a newly outcommented test where rewrite_set_ make_polynomial --> NONE
|
wneuper@59553
|
1285 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1286 |
WN120320.TODO check-improve rlsthmsNOTisac:
|
wneuper@59553
|
1287 |
DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
|
wneuper@59553
|
1288 |
DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
|
wneuper@59553
|
1289 |
FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
|
wneuper@59553
|
1290 |
# mark twice thms (in isac + (later) in Isabelle) in Isac.thy
|
wneuper@59553
|
1291 |
--------------------------------------------------------------------------------
|
walther@60242
|
1292 |
WN120320.TODO rlsthmsNOTisac: replace twice thms \<up>
|
wneuper@59553
|
1293 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1294 |
WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
|
wneuper@59553
|
1295 |
--- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
|
wneuper@59553
|
1296 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1297 |
WN120321.TODO rearrange theories:
|
wneuper@59553
|
1298 |
Knowledge
|
wneuper@59553
|
1299 |
:
|
walther@59603
|
1300 |
Prog_Expr.thy
|
walther@60125
|
1301 |
///Input_Descript.thy --> ProgLang
|
walther@59603
|
1302 |
Delete.thy <--- first_Knowledge_thy (*mv to Prog_Expr.thy*)
|
wneuper@59553
|
1303 |
ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
|
wneuper@59553
|
1304 |
Interpret.thy are generated (simplifies xml structure for theories)
|
wneuper@59585
|
1305 |
Program.thy
|
wneuper@59553
|
1306 |
Tools.thy
|
wneuper@59553
|
1307 |
ListC.thy <--- first_Proglang_thy
|
wneuper@59553
|
1308 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1309 |
WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
|
wneuper@59553
|
1310 |
EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
|
wneuper@59553
|
1311 |
broken during work on thy-hierarchy
|
wneuper@59553
|
1312 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1313 |
WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
|
wneuper@59553
|
1314 |
test --- the_hier (get_thes ()) (collect_thydata ())---
|
wneuper@59553
|
1315 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1316 |
WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
|
wneuper@59553
|
1317 |
!!add mutual crossreferences to ?fun headline??? where the same has to be done:
|
wneuper@59553
|
1318 |
!!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
|
wneuper@59553
|
1319 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1320 |
WN120411 scanning html representation of newly generated knowledge:
|
wneuper@59553
|
1321 |
* thy:
|
wneuper@59553
|
1322 |
** Theorems: only "Proof of the theorem" (correct!)
|
wneuper@59553
|
1323 |
and "(c) isac-team (math-autor)"
|
wneuper@59553
|
1324 |
** Rulesets: only "Identifier:///"
|
wneuper@59553
|
1325 |
and "(c) isac-team (math-autor)"
|
wneuper@59553
|
1326 |
** IsacKnowledge: link to dependency graph (which needs to be created first)
|
wneuper@59553
|
1327 |
** IsacScripts --> ProgramLanguage
|
wneuper@59553
|
1328 |
*** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
|
wneuper@59553
|
1329 |
|
wneuper@59553
|
1330 |
* pbl: OK !?!
|
wneuper@59553
|
1331 |
* met: OK !?!
|
wneuper@59553
|
1332 |
* exp:
|
wneuper@59553
|
1333 |
** Z-Transform is missing !!!
|
wneuper@59553
|
1334 |
** type-constraints !!!
|
wneuper@59553
|
1335 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1336 |
WN120417: merging xmldata revealed:
|
wneuper@59553
|
1337 |
..............NEWLY generated:........................................
|
wneuper@59553
|
1338 |
<THEOREMDATA>
|
wneuper@59553
|
1339 |
<GUH> thy_isab_Fun-thm-o_apply </GUH>
|
wneuper@59553
|
1340 |
<STRINGLIST>
|
wneuper@59553
|
1341 |
<STRING> Isabelle </STRING>
|
wneuper@59553
|
1342 |
<STRING> Fun </STRING>
|
wneuper@59553
|
1343 |
<STRING> Theorems </STRING>
|
wneuper@59553
|
1344 |
<STRING> o_apply </STRING>
|
wneuper@59553
|
1345 |
</STRINGLIST>
|
wneuper@59553
|
1346 |
<MATHML>
|
wneuper@59553
|
1347 |
<ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
|
wneuper@59553
|
1348 |
</MATHML> <PROOF>
|
wneuper@59553
|
1349 |
<EXTREF>
|
wneuper@59553
|
1350 |
<TEXT> Proof of the theorem </TEXT>
|
wneuper@59553
|
1351 |
<URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
|
wneuper@59553
|
1352 |
</EXTREF>
|
wneuper@59553
|
1353 |
</PROOF>
|
wneuper@59553
|
1354 |
<EXPLANATIONS> </EXPLANATIONS>
|
wneuper@59553
|
1355 |
<MATHAUTHORS>
|
wneuper@59553
|
1356 |
<STRING> Isabelle team, TU Munich </STRING>
|
wneuper@59553
|
1357 |
</MATHAUTHORS>
|
wneuper@59553
|
1358 |
<COURSEDESIGNS>
|
wneuper@59553
|
1359 |
</COURSEDESIGNS>
|
wneuper@59553
|
1360 |
</THEOREMDATA>
|
wneuper@59553
|
1361 |
..............OLD FORMAT:.............................................
|
wneuper@59553
|
1362 |
<THEOREMDATA>
|
wneuper@59553
|
1363 |
<GUH> thy_isab_Fun-thm-o_apply </GUH>
|
wneuper@59553
|
1364 |
<STRINGLIST>
|
wneuper@59553
|
1365 |
<STRING> Isabelle </STRING>
|
wneuper@59553
|
1366 |
<STRING> Fun </STRING>
|
wneuper@59553
|
1367 |
<STRING> Theorems </STRING>
|
wneuper@59553
|
1368 |
<STRING> o_apply </STRING>
|
wneuper@59553
|
1369 |
</STRINGLIST>
|
wneuper@59553
|
1370 |
<THEOREM>
|
wneuper@59553
|
1371 |
<ID> o_apply </ID>
|
wneuper@59553
|
1372 |
<MATHML>
|
wneuper@59553
|
1373 |
<ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
|
wneuper@59553
|
1374 |
</MATHML>
|
wneuper@59553
|
1375 |
</THEOREM>
|
wneuper@59553
|
1376 |
<PROOF>
|
wneuper@59553
|
1377 |
<EXTREF>
|
wneuper@59553
|
1378 |
<TEXT> Proof of the theorem </TEXT>
|
wneuper@59553
|
1379 |
<URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
|
wneuper@59553
|
1380 |
</EXTREF>
|
wneuper@59553
|
1381 |
</PROOF>
|
wneuper@59553
|
1382 |
<EXPLANATIONS> </EXPLANATIONS>
|
wneuper@59553
|
1383 |
<MATHAUTHORS>
|
wneuper@59553
|
1384 |
<STRING> Isabelle team, TU Munich </STRING>
|
wneuper@59553
|
1385 |
</MATHAUTHORS>
|
wneuper@59553
|
1386 |
<COURSEDESIGNS>
|
wneuper@59553
|
1387 |
</COURSEDESIGNS>
|
wneuper@59553
|
1388 |
</THEOREMDATA>
|
wneuper@59553
|
1389 |
--------------------------------------------------------------------------------
|
wneuper@59553
|
1390 |
\<close>
|
wneuper@59553
|
1391 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
1392 |
text \<open>
|
wneuper@59553
|
1393 |
isac development was done between these changesets:
|
wneuper@59553
|
1394 |
------------------------------------------------------------------------------
|
wneuper@59553
|
1395 |
Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
|
wneuper@59553
|
1396 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1397 |
Date: 2012-09-24 16:39:30 +0200 (8 months)
|
wneuper@59553
|
1398 |
:
|
wneuper@59553
|
1399 |
: isac on Isablle2011
|
wneuper@59553
|
1400 |
:
|
wneuper@59553
|
1401 |
Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
|
wneuper@59553
|
1402 |
Branch: decompose-isar
|
wneuper@59553
|
1403 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1404 |
Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
|
wneuper@59553
|
1405 |
------------------------------------------------------------------------------
|
wneuper@59553
|
1406 |
\<close>
|
wneuper@59553
|
1407 |
|
wneuper@59553
|
1408 |
subsection \<open>isac on Isabelle2009-2\<close>
|
wneuper@59553
|
1409 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1410 |
text \<open>
|
wneuper@59553
|
1411 |
In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
|
wneuper@59553
|
1412 |
The update was painful (bridging 7 years of Isabelle development) and cut short
|
wneuper@59553
|
1413 |
due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
|
wneuper@59553
|
1414 |
going on to Isabelle2011 although most of the tests did not run.
|
wneuper@59553
|
1415 |
\<close>
|
wneuper@59553
|
1416 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
1417 |
text \<open>
|
wneuper@59553
|
1418 |
WN131021 this is broken by installation of Isabelle2011/12/13,
|
wneuper@59553
|
1419 |
because all these write their binaries to ~/.isabelle/heaps/..
|
wneuper@59553
|
1420 |
|
wneuper@59553
|
1421 |
$ cd /usr/local/isabisac09-2/
|
wneuper@59553
|
1422 |
$ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
|
wneuper@59553
|
1423 |
$ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
|
wneuper@59553
|
1424 |
NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
|
wneuper@59553
|
1425 |
\<close>
|
wneuper@59553
|
1426 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
1427 |
text \<open>
|
wneuper@59553
|
1428 |
Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
|
wneuper@59553
|
1429 |
\<close>
|
wneuper@59553
|
1430 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
1431 |
text \<open>
|
wneuper@59553
|
1432 |
isac development was done between these changesets:
|
wneuper@59553
|
1433 |
------------------------------------------------------------------------------
|
wneuper@59553
|
1434 |
Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
|
wneuper@59553
|
1435 |
Branch: decompose-isar
|
wneuper@59553
|
1436 |
User: Marco Steger <m.steger@student.tugraz.at>
|
wneuper@59553
|
1437 |
Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
|
wneuper@59553
|
1438 |
:
|
wneuper@59553
|
1439 |
: isac on Isablle2009-2
|
wneuper@59553
|
1440 |
:
|
wneuper@59553
|
1441 |
Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
|
wneuper@59553
|
1442 |
Branch: isac-from-Isabelle2009-2
|
wneuper@59553
|
1443 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
wneuper@59553
|
1444 |
Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
|
wneuper@59553
|
1445 |
------------------------------------------------------------------------------
|
wneuper@59553
|
1446 |
\<close>
|
wneuper@59553
|
1447 |
|
wneuper@59553
|
1448 |
subsection \<open>isac on Isabelle2002\<close>
|
wneuper@59553
|
1449 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59553
|
1450 |
text \<open>
|
wneuper@59553
|
1451 |
From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
|
wneuper@59553
|
1452 |
of isac's mathematics engine has been implemented.
|
wneuper@59553
|
1453 |
\<close>
|
wneuper@59553
|
1454 |
subsubsection \<open>Run tests\<close>
|
wneuper@59553
|
1455 |
subsubsection \<open>State of tests\<close>
|
wneuper@59553
|
1456 |
text \<open>
|
wneuper@59553
|
1457 |
All tests work on an old notebook (the right PolyML coudn't be upgraded to more
|
wneuper@59553
|
1458 |
recent Linux versions)
|
wneuper@59553
|
1459 |
\<close>
|
wneuper@59553
|
1460 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59553
|
1461 |
text \<open>
|
wneuper@59553
|
1462 |
Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
|
wneuper@59553
|
1463 |
see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
|
wneuper@59553
|
1464 |
\<close>
|
wneuper@59553
|
1465 |
|
wneuper@59553
|
1466 |
end
|
wneuper@59553
|
1467 |
(*========== inhibit exn 130719 Isabelle2013 ===================================
|
wneuper@59553
|
1468 |
============ inhibit exn 130719 Isabelle2013 =================================*)
|
wneuper@59553
|
1469 |
|
wneuper@59553
|
1470 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
wneuper@59553
|
1471 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|
wneuper@59553
|
1472 |
|