(* 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 xxx

  \item xxx

  \item lucas-intrpreter.locate_input_tactic: execute_progr_2 srls tac cstate (progr, Rule.e_rls)

                                                                                      ^^^^^^^^^^

  \item xxx

  \item xxx

  \end{itemize}

\<close>

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

text \<open>

  \begin{itemize}

  \item clarify handling of contexts

    \begin{itemize}

    \item Check_Elementwise "Assumptions": prerequisite for ^^goal

    \item xxx

    \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt

    \item rm ctxt from Subproblem' (is separated in associate!))

    \item check Tactic.Subproblem': are 2 terms required?

    \item xxx

    \item Test_Some.--- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts --

      --: wait for deleting Check_Elementwise Assumptions

    \item xxx

    \item lucas-intrpreter.assy: Generate.generate1 (Celem.assoc_thy "Isac") 

    \end{itemize}

  \item xxx

  \item complete mstools.sml (* survey on handling contexts:

  \item xxx

  \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur.

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

  \item xxx

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

  \item xxx

  \item datatype L,R,D --> Istate

  \item xxx

  \item Lucin.Ass_Weak etc \<longrightarrow> NEW structutre ? LItool ?

  \item xxx

  \item istate

    \begin{itemize}

    \item DONE rename srcstate --> pstate

        and after review of Rrls, detail ?-->? istate

    \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)

    \item xxx

    \item xxx

    \item xxx

    \end{itemize}

  \item xxx

  \item ctxt context

    \begin{itemize}

    \item DONE Rewrite.eval_listexpr_ thy ..: can thy be extracted from ctxt ?

    \item xxx

    \item xxx

    \end{itemize}

  \item push srls into srcstate

  \item change Lucin.handle_leaf "locate" "Isac" sr E a v t

        to     Lucin.handle_leaf "locate"  ctxt ( srcstate )        !!srls in scrstate!!^^

        and redesign handle_leaf .. subst_stacexpr .. associate

        to Tactic.from_code : 

        + keep ! trace_script

  \item in locate_input_tactic .. ?assy?; Program.is_eval_expr   .use  Term.exists_Const

  \item trace_script: replace ' by " in writeln

  \item xxx

  \item librarys.ml --> libraryC.sml + text from termC.sml

  \item xxx

  \item rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl

  \item xxx

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

    see implementation.pdf p.16

  \item xxx

  \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 

    \item xxx

    \end{itemize}

  \item concentracte "insert_assumptions" in "associate" ?for determine_next_tactic ?where?

    \begin{itemize}

    \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)

    \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))

    \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"

    \item xxx

    \item xxx

    \item DO DELETIONS AFTER analogous concentrations in determine_next_tactic

    \end{itemize}

  \item xxx

  \item ? what is the difference headline <--> cascmd in

    Subproblem' (spec, oris, headline, fmz_, context, cascmd)

  \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 Applicable.applicable_in --> Applicable.tactic_at

  \item Const ("Program.SubProblem", _) --> Const ("Program.SubProblem", _):rename!  separate?

  \item xxx

  \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc

  \item xxx

  \item TermC.vars_of replace by vars (recognises numerals)

  \item xxx

  \item xxx

  \end{itemize}

\<close>

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

text \<open>

  \begin{itemize}

  \item prep_met

    \begin{itemize}

    \item rename field scr in meth

    \item xxx

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

       provide error message.

    \item xxx

    \item automatically extrac rls from program-code 

      ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?

    \item xxx

    \item xxx

    \item xxx

    \end{itemize}

  \item xxx

  \item drop "init_form" and use "Take" in programs (start with latter!)

  \item xxx

  \item deprive Check_elementwise, but keep it for Minisubpl

    (which checks for Check_Postcond separated by another tactic)

    This seems a prerequisite for appropriate handling of contexts at Check_Postcond.

  \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 ?delete Check_Postcond' in begin_end_prog (already done in solve?)

    in case both are needed, unify !

  \item xxx

  \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 cleaup the many conversions string -- theory

  \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?

  \item 1. Rewrite.eval_true_, then

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

  \item fun associate

    let val thy = Celem.assoc_thy "Isac";(*TODO*)

  \item xxx

  \item xxx

  \item xxx

  \item !!! Tactic.Refine_Problem uses Pattern.match, which takes a theory, NOT a ctxt

    but there is Proof_Context.theory_of !!!

  \end{itemize}

\<close>

subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<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/pstate.

    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>Questions to Isabelle experts\<close>

text \<open>

\begin{itemize}

\item how HANDLE these exceptions, e.g.:

    Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"

  GIVES

    "Inner syntax error

     Failed to parse term"

\item xxx

\item xxx

\item xxx

\item xxx

\end{itemize}

\<close>

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

text \<open>

\begin{itemize}

  \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