1 (* Title: todo's for isac core
2 Author: Walther Neuper 111013
3 (c) copyright due to lincense terms.
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
9 Situation at the beginning of this TODO list:
10 Mathias Lehnfeld was required to start his introduction of context,
11 allthough the migration from Isabelle2002 to Isabelle2011 was not finished,
12 in particular very few tests were running. So ctxt have introduced a lot of
13 errors found much later, for instance during work with
14 Jan Rocnik on SignalProcessing. Presently a majority of tests is still sleeping.
16 This list is started to record TODOs wich can NOT be done
17 before all tests are RUNNING.
19 ############## WNxxxxxx.TODO can be found in sources ##############
21 --------------------------------------------------------------------------------
22 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
23 --------------------------------------------------------------------------------
24 WN111013.TODO: remove concept around "fun init_form", lots of troubles with
25 this special case (see) --- why not nxt = Model_Problem here ? ---
27 the following methods need init_form,
28 because they DONT start with Take or SubProblem:
33 ["Biegelinien","setzeRandbedingungenEin"] ?!? ScrExpr .. SubProblem
38 ["DiffApp","max_by_calculus"] ?!? ScrExpr .. SubProblem
39 ["DiffApp","make_fun_by_new_variable"] ?!? ScrExpr .. SubProblem
40 ["DiffApp","make_fun_by_explicit"] ?!? ScrExpr .. SubProblem
43 ["EqSystem","normalize","2x2"]
44 ["EqSystem","normalize","4x4"]
45 ["EqSystem","top_down_substitution","4x4"] ?!? ScrExpr .. Take
50 Inverse_Z_Transform //
53 ["LinEq","solve_lineq_equation"]
55 ["Equation","solve_log"]
57 ["simplification","for_polynomials"]
59 ["simplification","for_polynomials","with_minus"]
60 ["simplification","for_polynomials","with_parentheses"]
61 ["simplification","for_polynomials","with_parentheses_mult"]
63 ["RatEq","solve_rat_equation"]
65 ["simplification","of_rationals"]
68 ["RootEq","norm_sq_root_equation"]
69 ["RootEq","solve_sq_root_equation"]
70 ["RootEq","solve_right_sq_root_equation"]
71 ["RootEq","solve_left_sq_root_equation"]
74 ["RootRatEq","elim_rootrat_equation"]
77 ["Test","solve_linear"]
78 ["Test","sqrt-equ-test"]
79 ["Test","squ-equ-test2"]
80 ["Test","squ-equ-test-subpbl1"]
81 ["Test","squ-equ-test-subpbl2"]
82 ["Test","square_equation...notTerminating"] ?!? tactical While
83 ["Test","square_equation1"] ?!? tactical While
84 ["Test","square_equation2"] ?!? tactical While
85 ["Test","square_equation"] ?!? tactical While
86 ["Test","solve_plain_square"] //..
87 ["Test","norm_univar_equation"]
91 --------------------------------------------------------------------------------
92 WN111013.TODO: these scripts start with Take or Sub_Problem, i.e. NO init_form
95 ["Berechnung","erstNumerisch"]
96 ["Berechnung","erstSymbolisch"]
99 ["IntegrierenUndKonstanteBestimmen"]
100 ["IntegrierenUndKonstanteBestimmen2"]
101 ["Biegelinien","ausBelastung"]
102 ["Biegelinien","setzeRandbedingungenEin"]
103 ["Equation","fromFunction"]
107 ["diff","differentiate_on_R"]
108 ["diff","diff_simpl"]
109 ["diff","differentiate_equality"]
110 ["diff","after_simplification"]
112 ["DiffApp","max_by_calculus"]
113 ["DiffApp","make_fun_by_new_variable"]
114 ["DiffApp","make_fun_by_explicit"]
116 ["Test","solve_diophant"]
118 ["EqSystem","top_down_substitution","2x2"]
119 ["EqSystem","top_down_substitution","4x4"]
123 ["diff","integration"]
124 ["diff","integration","named"]
126 ["SignalProcessing", "Z_Transform", "Inverse"]
133 ["probe","fuer_polynom"]
144 --------------------------------------------------------------------------------
145 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
147 # simplify_* , *_simp_*
149 # calc_* , calculate_* ... require iteration over all rls ...
150 ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
151 --------------------------------------------------------------------------------
152 WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
153 --------------------------------------------------------------------------------
154 WN120314 changeset a393bb9f5e9f drops root equations.
155 see test/Tools/isac/Knowledge/rootrateq.sml
156 --------------------------------------------------------------------------------
157 WN120317.TODO changeset 977788dfed26 dropped rateq:
158 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
159 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
160 investigation Check_elementwise stopped due to too much effort finding out,
161 why Check_elementwise worked in 2002 in spite of the error.
162 --------------------------------------------------------------------------------
163 WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
164 --------------------------------------------------------------------------------
165 WN120317.TODO found by test --- interSteps for Schalk 299a --- that
166 NO test with 'interSteps' is checked properly (with exn on changed behaviour)
167 --------------------------------------------------------------------------------
168 WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
169 a newly outcommented test where rewrite_set_ make_polynomial --> NONE
170 --------------------------------------------------------------------------------
171 WN120320.TODO check-improve rlsthmsNOTisac:
172 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
173 DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
174 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
175 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
176 --------------------------------------------------------------------------------
177 WN120320.TODO rlsthmsNOTisac: replace twice thms ^
178 --------------------------------------------------------------------------------
179 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
180 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
181 --------------------------------------------------------------------------------
182 WN120321.TODO rearrange theories:
186 ///Descript.thy --> ProgLang
187 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*)
188 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
189 Interpret.thy are generated (simplifies xml structure for theories)
192 ListC.thy <--- first_Proglang_thy
193 --------------------------------------------------------------------------------
194 WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
195 EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
196 broken during work on thy-hierarchy
197 --------------------------------------------------------------------------------
198 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
199 test --- the_hier (! thehier) (collect_thydata ())---
200 --------------------------------------------------------------------------------
201 WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
202 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
203 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
204 --------------------------------------------------------------------------------
205 --------------------------------------------------------------------------------
206 --------------------------------------------------------------------------------
208 --------------------------------------------------------------------------------
209 --------------------------------------------------------------------------------
211 --------------------------------------------------------------------------------
212 --------------------------------------------------------------------------------