neuper@42314
|
1 |
(* Title: todo's for isac core
|
neuper@42314
|
2 |
Author: Walther Neuper 111013
|
neuper@42314
|
3 |
(c) copyright due to lincense terms.
|
neuper@42314
|
4 |
*)
|
wneuper@59504
|
5 |
theory TODO
|
wneuper@59504
|
6 |
imports "~~/src/Doc/Prog_Prove/LaTeXsugar"
|
wneuper@59504
|
7 |
begin
|
neuper@42314
|
8 |
|
wneuper@59504
|
9 |
section \<open>TODOs from current development\<close>
|
wneuper@59504
|
10 |
|
wneuper@59504
|
11 |
subsection \<open>Shift programs for Lucas-Interpretation from strings to partial_function\<close>
|
wneuper@59504
|
12 |
text\<open>
|
wneuper@59504
|
13 |
String constants have already bee introduced to old string-programs.
|
wneuper@59504
|
14 |
Shifting this program code into partial_function reveals further issues:
|
wneuper@59504
|
15 |
\begin{itemize}
|
wneuper@59549
|
16 |
\item Biegelinie.thy was already broken after isabisac15, but never noticed.
|
wneuper@59549
|
17 |
Switch from script to partial_function has it broken further,
|
wneuper@59549
|
18 |
mostly due to generalisation of handling of meths which extend the model of a probl.
|
wneuper@59549
|
19 |
!Check if (*CURRENT*) error is due to "switch from Script to partial_function" 4035ec339062 ?
|
wneuper@59549
|
20 |
OR ?due to "failed trial to generalise handling of meths
|
wneuper@59549
|
21 |
which extend the model of a probl " 98298342fb6d
|
wneuper@59549
|
22 |
\item
|
wneuper@59504
|
23 |
\item Diff.thy
|
wneuper@59504
|
24 |
\begin{itemize}
|
wneuper@59504
|
25 |
\item differentiateX --> differentiate after removal of script-constant
|
wneuper@59504
|
26 |
\end{itemize}
|
wneuper@59538
|
27 |
\item Inverse_Z_Transform.thy:
|
wneuper@59538
|
28 |
\begin{itemize}
|
wneuper@59538
|
29 |
\item thm ruleZY introduces a new variable on the rhs of the rewrite-rule.
|
wneuper@59537
|
30 |
The problem is related to the decision of typing for "d_d" and making bound variables free (while
|
wneuper@59538
|
31 |
shifting specific handling in equation solving etc. to the metalogic).
|
wneuper@59538
|
32 |
\item Find "stepResponse (x[n::real]::bool)" not reflected in met ?!
|
wneuper@59538
|
33 |
\item Reconsider whole problem:
|
wneuper@59538
|
34 |
input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
|
wneuper@59538
|
35 |
\end{itemize}
|
wneuper@59504
|
36 |
\item Test.thy: met_test_sqrt2: deleted?!
|
wneuper@59541
|
37 |
\item learn to use unknown tools for investigating Test_Some in child of changeset
|
wneuper@59541
|
38 |
"funpack: failed trial to generalise handling of meths which extend the model of a probl"
|
wneuper@59540
|
39 |
\item re-consideration whole of modelling- + specification-phase
|
wneuper@59540
|
40 |
\begin{itemize}
|
wneuper@59540
|
41 |
\item introduction of y, dy as arguments in IntegrierenUndKonstanteBestimmen2
|
wneuper@59540
|
42 |
caused major problems:
|
wneuper@59540
|
43 |
\begin{itemize}
|
wneuper@59540
|
44 |
\item required "--- hack for funpack: generalise handling of meths which extend problem items"
|
wneuper@59540
|
45 |
in order to make Test_Isac run again.
|
wneuper@59540
|
46 |
\begin{itemize}
|
wneuper@59540
|
47 |
\item see several locations of hack in code
|
wneuper@59540
|
48 |
\item these locations are NOT sufficient, see
|
wneuper@59540
|
49 |
test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
|
wneuper@59540
|
50 |
\item "fun assod" "match_ags ..dI" instead "..pI" breaks many tests, however,
|
wneuper@59540
|
51 |
this would be according to survey Notes (3) in src/../calchead.sml.
|
wneuper@59540
|
52 |
\end{itemize}
|
wneuper@59540
|
53 |
\end{itemize}
|
wneuper@59540
|
54 |
\item decide, whether to start with hack or with general notes
|
wneuper@59540
|
55 |
\begin{itemize}
|
wneuper@59540
|
56 |
\item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
|
wneuper@59540
|
57 |
\item reconsider add_field': where is it used for what? Shift into mk_oris
|
wneuper@59540
|
58 |
\item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
|
wneuper@59540
|
59 |
\item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
|
wneuper@59540
|
60 |
\item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
|
wneuper@59540
|
61 |
(relevant for pre-condition)
|
wneuper@59540
|
62 |
\item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
|
wneuper@59540
|
63 |
\item
|
wneuper@59540
|
64 |
\end{itemize}
|
wneuper@59540
|
65 |
\item other issues
|
wneuper@59540
|
66 |
\begin{itemize}
|
wneuper@59540
|
67 |
\item type model = itm list ?
|
wneuper@59540
|
68 |
\item review survey Notes in src/../calchead.sml: they are questionable
|
wneuper@59540
|
69 |
\item review copy-named, probably two issues commingled
|
wneuper@59540
|
70 |
\begin{itemize}
|
wneuper@59540
|
71 |
\item special handling of "#Find#, because it is not a formal argument of partial_function
|
wneuper@59540
|
72 |
\item special naming for solutions of equation solving: x_1, x_2, ...
|
wneuper@59540
|
73 |
\end{itemize}
|
wneuper@59540
|
74 |
\end{itemize}
|
wneuper@59540
|
75 |
\end{itemize}
|
wneuper@59540
|
76 |
\item \item abstract specify + nxt_specif to common aux-funs;
|
wneuper@59540
|
77 |
see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
|
wneuper@59549
|
78 |
\item
|
wneuper@59549
|
79 |
\item
|
wneuper@59549
|
80 |
\item
|
wneuper@59504
|
81 |
\begin{itemize}
|
wneuper@59504
|
82 |
\item
|
wneuper@59540
|
83 |
\begin{itemize}
|
wneuper@59540
|
84 |
\item
|
wneuper@59540
|
85 |
\begin{itemize}
|
wneuper@59540
|
86 |
\item
|
wneuper@59540
|
87 |
\end{itemize}
|
wneuper@59540
|
88 |
\end{itemize}
|
wneuper@59504
|
89 |
\end{itemize}
|
wneuper@59504
|
90 |
\end{itemize}
|
wneuper@59504
|
91 |
\<close>
|
wneuper@59504
|
92 |
subsubsection \<open>\<close>
|
wneuper@59504
|
93 |
|
wneuper@59504
|
94 |
section \<open>TODOs shifted here from above\<close>
|
wneuper@59504
|
95 |
|
wneuper@59504
|
96 |
subsection \<open>adopt Isabelle's numerals for Isac\<close>
|
wneuper@59504
|
97 |
text \<open>WN131021:
|
neuper@52150
|
98 |
intermediate states:
|
neuper@52150
|
99 |
# replace numerals of type "real" by "nat" in some specific functions from ListC.thy
|
neuper@52150
|
100 |
and have both representations in parallel for "nat".
|
wneuper@59504
|
101 |
\<close>subsection \<open>finetunig required for xmldata\<close>
|
wneuper@59504
|
102 |
text \<open>WN140808:
|
neuper@55496
|
103 |
See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
|
neuper@55496
|
104 |
and in kbase html-representation generated from these xmldata.
|
neuper@55496
|
105 |
Notes in ~~/xmldata/TODO.txt.
|
wneuper@59472
|
106 |
\<close>
|
wneuper@59504
|
107 |
|
wneuper@59472
|
108 |
section \<open>\<close>
|
wneuper@59472
|
109 |
subsection \<open>\<close>
|
wneuper@59504
|
110 |
subsubsection \<open>\<close>
|
wneuper@59513
|
111 |
text\<open>
|
wneuper@59513
|
112 |
\begin{itemize}
|
wneuper@59513
|
113 |
\item
|
wneuper@59513
|
114 |
\end{itemize}
|
wneuper@59513
|
115 |
\<close>
|
neuper@52150
|
116 |
end
|