wneuper/isa: src/Tools/isac/TODO.thy@e0e3d41ef86c

     1 (* Title:  todo's for isac core

     2    Author: Walther Neuper 111013

     3    (c) copyright due to lincense terms.

     4 *)

     5 theory TODO

     6 imports "~~/src/Doc/Prog_Prove/LaTeXsugar"

     7 begin

     9 section \<open>TODOs from current development\<close>

    11 subsection \<open>Shift programs for Lucas-Interpretation from strings to partial_function\<close>

    12 text\<open>

    13 String constants have already bee introduced to old string-programs.

    14 Shifting this program code into partial_function reveals further issues:

    15 \begin{itemize}

    16 \item Biegelinie.thy was already broken after isabisac15, but never noticed.

    17   Switch from script to partial_function has it broken further,

    18   mostly due to generalisation of handling of meths which extend the model of a probl.

    19   !Check if (*CURRENT*) error is due to "switch from Script to partial_function" 4035ec339062 ?

    20                              OR ?due to "failed trial to generalise handling of meths

    21                                  which extend the model of a probl " 98298342fb6d

    22 \item

    23 \item Diff.thy

    24   \begin{itemize}

    25   \item differentiateX --> differentiate after removal of script-constant

    26   \end{itemize}

    27 \item Inverse_Z_Transform.thy:

    28   \begin{itemize}

    29   \item thm ruleZY introduces a new variable on the rhs of the rewrite-rule.

    30   The problem is related to the decision of typing for "d_d" and making bound variables free (while

    31   shifting specific handling in equation solving etc. to the metalogic).

    32   \item Find "stepResponse (x[n::real]::bool)" not reflected in met ?!

    33   \item Reconsider whole problem:

    34     input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?

    35   \end{itemize}

    36 \item Test.thy: met_test_sqrt2: deleted?!

    37 \item learn to use unknown tools for investigating Test_Some in child of changeset

    38   "funpack: failed trial to generalise handling of meths which extend the model of a probl"

    39 \item re-consideration whole of modelling- + specification-phase

    40   \begin{itemize}

    41   \item introduction of y, dy as arguments in IntegrierenUndKonstanteBestimmen2

    42     caused major problems:

    43     \begin{itemize}

    44     \item required "--- hack for funpack: generalise handling of meths which extend problem items"

    45       in order to make Test_Isac run again.

    46       \begin{itemize}

    47       \item see several locations of hack in code

    48       \item these locations are NOT sufficient, see

    49         test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---

    50       \item "fun assod" "match_ags ..dI" instead "..pI" breaks many tests, however,

    51         this would be according to survey Notes (3) in src/../calchead.sml.

    52       \end{itemize}

    53     \end{itemize}

    54   \item decide, whether to start with hack or with general notes

    55     \begin{itemize}

    56     \item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]

    57     \item reconsider add_field': where is it used for what? Shift into mk_oris

    58     \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???

    59     \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey

    60     \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_

    61       (relevant for pre-condition)

    62     \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth

    63     \item

    64     \end{itemize}

    65   \item other issues

    66     \begin{itemize}

    67     \item type model = itm list ?

    68     \item review survey Notes in src/../calchead.sml: they are questionable

    69     \item review copy-named, probably two issues commingled

    70       \begin{itemize}

    71       \item special handling of "#Find#, because it is not a formal argument of partial_function

    72       \item special naming for solutions of equation solving: x_1, x_2, ...

    73       \end{itemize}

    74     \end{itemize}

    75   \end{itemize}

    76 \item \item abstract specify + nxt_specif to common aux-funs;

    77   see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"

    78 \item

    79 \item

    80 \item

    81   \begin{itemize}

    82   \item

    83     \begin{itemize}

    84     \item

    85       \begin{itemize}

    86       \item

    87       \end{itemize}

    88     \end{itemize}

    89   \end{itemize}

    90 \end{itemize}

    91 \<close>

    92 subsubsection \<open>\<close>

    94 section \<open>TODOs shifted here from above\<close>

    96 subsection \<open>adopt Isabelle's numerals for Isac\<close>

    97 text \<open>WN131021:

    98 intermediate states:

    99 # replace numerals of type "real" by "nat" in some specific functions from ListC.thy

   100   and have both representations in parallel for "nat".

   101 \<close>subsection \<open>finetunig required for xmldata\<close>

   102 text \<open>WN140808:

   103 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390

   104 and in kbase html-representation generated from these xmldata.

   105 Notes in ~~/xmldata/TODO.txt.

   106 \<close>

   108 section \<open>\<close>

   109 subsection \<open>\<close>

   110 subsubsection \<open>\<close>

   111 text\<open>

   112 \begin{itemize}

   113 \item

   114 \end{itemize}

   115 \<close>

   116 end

author	Walther Neuper <wneuper@ist.tugraz.at>
	Sat, 01 Jun 2019 11:09:19 +0200
changeset 59549	e0e3d41ef86c
parent 59541	3ba43630359c
child 59550	2e7631381921
permissions	-rw-r--r--