(* Title:  todo's for isac core

    Author: Walther Neuper 111013

    (c) copyright due to lincense terms.

 *)

 theory TODO

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

 begin

 section \<open>TODOs from current changesets\<close>

 text\<open>

   Shift more complicated issues from the next subsection to the next but one!

 \<close>

 subsection \<open>Current changeset\<close>

 text \<open>

   \begin{itemize}

   \item xxx

   \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper

   \item check in states: length ?? > 1 with tracing these cases

   \item xxx

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Postponed from current changeset\<close>

 text \<open>

   \begin{itemize}

   \item language definition: use (f #> g) x = x |> f |> g instead of @

     see implementation.pdf p.16

   \item xxx

   \item xxx

   \item pull update of Ctree.state out of 2 Lucin funs (locate_input_formula is different))

     \begin{itemize}

     \item 1. check if Ctree.state can be updated OUTSIDE determine_next_step

     \item 2. fun locate_input_tactic: pull generate1 out (because it stores ctxt also in cstate)

     \item xxx

     \item xxx

     \end{itemize}

   \item xxx

   \item xxx

   \item inform: TermC.parse (Celem.assoc_thy "Isac") istr --> parseNEW context istr

   \item extract common code from associate.. stac2tac_

   \end{itemize}

 \<close>

 section \<open>Separated tasks\<close>

 text \<open>

 \<close>

 subsection \<open>Simple\<close>

 text \<open>

   \begin{itemize}

   \item Diff.thy: differentiateX --> differentiate after removal of script-constant

   \item Test.thy: met_test_sqrt2: deleted?!

   \item xxx

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Simple but laborous\<close>

 text \<open>

   \begin{itemize}

   \item rename rename field scr in meth

   \item prep_met: check match between args of partial_function and model-pattern of meth;

      provide error message.

   \item xxx

   \item xxx

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Questionable\<close>

 text \<open>

   \begin{itemize}

   \item finish output of trace_script with Check_Postcond (useful for SubProblem)

   \item unify in signature LANGUAGE_TOOLS =\\

     val pblterm: Rule.domID -> Celem.pblID -> term     vvv        vvv\\

     val subpbl: string -> string list -> term          unify with ^^^

   \item xxx

   \item xxx

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 section \<open>Complex, related to --> other tasks\<close>

 text \<open>

 \<close>

 subsection \<open>review all signatures wrt. implementation.pdf canonical argument order\<close>

 text \<open>

 \<close>

 subsection \<open>solve, loc_solve_, ...\<close>

 text \<open>

   unify to calcstate, calcstate'

   \begin{itemize}

   \item ? rename begin_end_prog -> check_switch_prog

   \item adopt the same for specification phase

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Review modelling- + specification-phase\<close>

 text \<open>

   \begin{itemize}

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

     \begin{itemize}

     \item see several locations of hack in code

     \item these locations are NOT sufficient, see

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

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

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

     \end{itemize}

   \item see "failed trial to generalise handling of meths"98298342fb6d

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

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

   \item xxx

   \item type model = itm list ?

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

   \item review copy-named, probably two issues commingled 

     \begin{itemize}

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

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

     \end{itemize}

   \item xxx

   \item this has been written in one go:

     \begin{itemize}

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

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

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

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

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

       (relevant for pre-condition)

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

     \item 

     \end{itemize}

   \end{itemize}

 \<close>

 subsection \<open>taci list, type step\<close>

 text \<open>

   \begin{itemize}

   \item states.sml: check, when "length tacis > 1"

   \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml

   \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Cleanup signatures\<close>

 text \<open>

   \begin{itemize}

   \item there are comments in several signatures

   \item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted

   \item src/../Frontend/: signatures missing

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Ctree\<close>

 text \<open>

   \begin{itemize}

   \item review get_ctxt, update_ctxt, get_istate, upd_istate, upd_ctxt,

     <---> update_loc', repl_loc (remove the latter)

   \item delete field ctxt in PblObj in favour of loc

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>replace theory/thy by context/ctxt\<close>

 text \<open>

   \begin{itemize}

   \item 1. Rewrite.eval_true_, then

     Lucin.handle_leaf, Rewrite.eval_listexpr_, Generate.generate1, Lucin.stac2tac.

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Rfuns, Begin_/End_Detail', Rrls\<close>

 text \<open>

   \begin{itemize}

   \item removing from_pblobj_or_detail' causes many strange errors

   \item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ...

   \item xxx

   \item probably only "normal_form" seems to be needed

   \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"

     but that seems desirable

   \item ?how is the relation to reverse-rewriting ???

   \item "Rfuns" markers in test/../rational

   \item xxx

   \item datatype istate (Istate.T): remove RrlsState, scrstate: use Rrls only for creating results beyond

     rewriting and/or respective intermediate steps (e.g. cancellation of fractions).

     Thus we get a 1-step-action which does NOT require a state beyond istate(?).

     Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.

   \item debug ^^^ related: is there an occurence of Steps with more than 1 element?

   \item xxx

   \item and do_solve_step (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)

   \item xxx

   \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?

   \end{itemize}

 \<close>

 subsection \<open>Inverse_Z_Transform.thy\<close>

 text \<open>

   \begin{itemize}

   \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.

   ? replace rewriting with substitution ?!?

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

   shifting specific handling in equation solving etc. to the meta-logic). 

   \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by

     rewrite-rules; see \ref{new-var-rhs}.

   \item Reconsider whole problem:

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

   \end{itemize}

 \<close>

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

 text \<open>

   \begin{itemize}

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

     and have both representations in parallel for "nat".

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Finetunig required for xmldata\<close>

 text \<open>

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

   and in kbase html-representation generated from these xmldata.

   Notes in ~~/xmldata/TODO.txt.

 \<close>

 section \<open>Hints for further development\<close>

 text \<open>

 \<close>

 subsection \<open>get proof-state\<close>

 text \<open>

   Re: [isabelle] Programatically get "this"

   ----------------------------------------------------

   So here is my (Makarius') version of your initial example, following these principles:

   begin{verbatim}

     notepad

     begin

       assume a: A

       ML_val \<open>

         val ctxt = @{context};

         val this_name =

           Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name

     Auto_Bind.thisN);

         val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));

       \<close>

     end

   end{verbatim}

 \<close>

 subsection \<open>write Specification to jEdit\<close>

 text \<open>

   Re: [isabelle] Printing terms with type annotations

   ----------------------------------------------------

   On 06/02/2019 17:52, Moa Johansson wrote:

   >

   > I’m writing some code that should create a snippet of Isar script.

   This is how Sledgehammer approximates this:

   http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299

   (The module name already shows that the proper terminology is "Isar

   proof" (or "Isar proof text").  Proof scripts are a thing from the past,

   before Isar. You can emulate old-style proof scripts via a sequence of

   'apply' commands, but this is improper Isar.)

   Note that there is no standard function in Isabelle/Pure, because the

   problem to print just the right amount of type information is very

   complex and not fully solved. One day, after 1 or 2 rounds of

   refinements over the above approach, it might become generally available.

 \<close>

 subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>

 text \<open>

   isabelle update -u path_cartouches

   isabelle update -u inner_syntax_cartouches

 \<close>

 section \<open>For copy & paste\<close>

 text \<open>

   \begin{itemize}

   \item xxx

     \begin{itemize}

     \item xxx

       \begin{itemize}

       \item xxx

         \begin{itemize}

         \item xxx

         \end{itemize}

       \end{itemize}

     \end{itemize}

   \end{itemize}

 \end{itemize}

 \<close>

 subsection \<open>xxx\<close>

 subsubsection \<open>xxx\<close>

 end