
neuper@42314: (* Title:  todo's for isac core
neuper@42314:    Author: Walther Neuper 111013
neuper@42314:    (c) copyright due to lincense terms.
neuper@42314: *)
wneuper@59504: theory TODO
wneuper@59504: imports "~~/src/Doc/Prog_Prove/LaTeXsugar"
wneuper@59504: begin
neuper@42314: 
walther@59779: text \<open>
walther@59779: Legend: here + code since 200120
walther@59779:   \<open>(*DOC\<close> identifies stuff dedicated for isac/Doc/Lucas_Interpreter
walther@59779:   \<open>(*?!?\<close> identifies a design question
walther@59779: 
walther@59779: Distillation of "rounds of reforms":
walther@59779:   \<open>TODOs from current changesets\<close> \<rightarrow> \<open>Postponed from current changeset\<close> \<rightarrow>
walther@59779:   (*to be removed..*) \<rightarrow> \<open>Separated tasks\<close> (*.. to be removed*)
walther@59779:   \<rightarrow> subsection of \<open>Major reforms\<close>
walther@59779: \<close>
walther@59779: 
wneuper@59574: section \<open>TODOs from current changesets\<close>
wneuper@59568: text\<open>
walther@59779:   Shift more complicated issues from  \<open>Current changeset\<close> to \<open>Postponed from current changeset\<close>
wneuper@59568: \<close>
wneuper@59574: subsection \<open>Current changeset\<close>
wneuper@59574: text \<open>
walther@59938: (*/------- to  from -------\*)
walther@59938: (*\------- to  from -------/*)
wneuper@59569:   \begin{itemize}
walther@60176:   \item resume step 6.10: unsuccessful trials with combination of types on Outer_Syntax
walther@60176:     note: test in Calculation.thy is outcommented
walther@60175:   \item xxx
walther@60164:   \item re-arrange Isac's bootstrap: look for  "after devel.of BridgeJEdit"
walther@59927:   \item xxx
walther@60011:   \item xxx
walther@60125:   \item Input_Descript.descriptor -> Input_Descript.T
walther@60125:   \item xxx
walther@60125:   \item Step_Specify.initialisePIDE: remove hdl in return-value
walther@60125:         rename Step_Specify.nxt_specify_init_calc
walther@60125:   \item xxx
walther@60089:   \item relate Prog_Epxr.lhs to Thm.lhs_of
walther@60089:   \item xxx
walther@60045:   \item as soon as src/../parseC.sml is stable,
walther@60045:     remove defs from Test_Parse_Isac.thy
walther@60045:     + and shift tests from Test_Parse_Isac -> test/../parseC.sml
walther@59998:   \item xxx
Walther@60494:   \item Specify.find_next_step: References.select_input
walther@59998:     cpI = ["vonBelastungZu", "Biegelinien"]: References_Def.id
walther@59998:                                       ^^^^^  Problem.id
walther@59998:   \item xxx
walther@59998:   \item Calc.state_empty_post \<rightarrow> Calc.state_post_empty
walther@59998:   \item xxx
walther@59986:   \item distribute code from test/../calchead.sml
walther@59986:   \item xxx
walther@59935:   \item rename Tactic.Calculate -> Tactic.Evaluate
walther@59779:   \item xxx
walther@59923:   \item replace src/ Erls by Rule_Set.Empty
walther@59882:   \item xxx
walther@59882:   \item rename ptyps.sml -> specify-etc.sml
walther@59882:         rename Specify -> Specify_Etc
walther@59976:         rename Specify -> Specify
walther@59842:   \item xxx
walther@59914:   \item specific_from_prog in..end: replace o by |> (Test_Isac or Test_Some!)
walther@59914:   \item xxx
walther@59914:   \item cleanup ThmC in MathEngBasic
walther@59914:   \item xxx
walther@59914:   \item xxx
walther@59914:   \item xxx
walther@59842:   \item xxx
walther@59842:   \item xxx
walther@59842:   \item xxx
walther@59842:   \item xxx
walther@59842:   \item xxx
walther@59846:   \end{itemize}
walther@59846: \<close>
walther@59846: subsection \<open>Postponed from current changeset\<close>
walther@59846: text \<open>
walther@59886:   \begin{itemize}
walther@59886:   \item xxx
walther@60026:   \item make steps around SubProblem more consistent:
walther@60026:     SubProblem (thy, [pbl]) is bypassed by Model_Problem, if it is 1st Tactic in a Program.
walther@60026:     Design:
walther@60026:     * the Tactic SubProblem (thy, [pbl]) creates the formula SubProblem (thy, [pbl])
walther@60026:       (only the headline !)
walther@60026:     * the Tactic Model_Problem starts Specification
walther@60026:       (with an empty Model)
walther@60026:     see test/../sub-problem.sml
walther@60026:   \item xxx
walther@60016:   \item Specify_Step.add has dummy argument Istate_Def.Uistate -- remove down to Ctree
walther@60016:   \item xxx
walther@60015:   \item Step_Specify.by_tactic (Tactic.Model_Problem' (id, _, met))
walther@60015:                      by_tactic (Tactic.Specify_Theory' domID)
walther@60015:     had very old, strange code at 11b5b8b81876
walther@60015:     ?redes Model_Problem', Specify_Theory' <--> Specify_Method: Step_Specify.complet_for ?
walther@60015:     INTERMED. NO REPAIR: NOT PROMPTED IN TESTS
walther@60015:   \item xxx
walther@60002:   \item unify code Specify.find_next_step <--> Step_Specify.by_tactic (Tactic.Specify_Method'
walther@60002:   \item xxx
walther@59998:   \item Isa20.implementation: 0.2.4 Printing ML values ?INSTEAD? *.TO_STRING ???
walther@59998:     ??? writeln ( make_string {x = x, y = y}); ???
walther@59998:   \item xxx
walther@59953:   \item revise O_Model and I_Model with an example with more than 1 variant.
walther@59953:   \item xxx
walther@60125:   \item ctxt is superfluous in specify-phase due to type constraints from Input_Descript.thy
walther@59944:   \item xxx
walther@59934:   \item Derive.do_one: TODO find code in common with complete_solve
walther@59934:         Derive.embed: TODO rewrite according to CAO (+ no intermediate access to Ctree)
walther@59934:   \item xxx
walther@59930:   \item Solve_Check: postponed parsing input to _ option
walther@59930:   \item xxx
walther@59921:   \item ? "fetch-tactics.sml" from Mathengine -> BridgeLibisabelle ?
walther@59886:   \item xxx
walther@59921:   \item ? unify struct.Step and struct.Solve in MathEngine ?
walther@59851:   \item xxx
walther@59919:   \item use "Eval_Def" for renaming identifiers
walther@59851:   \item xxx
walther@59886:   \item why does Test_Build_Thydata.thy depend on ProgLang and not on CalcElements ?
walther@59851:   \item xxx
walther@59851:   \item xxx
walther@59846:   \begin{itemize}
walther@59846:   \item LI.do_next (*TODO RM..*) ???
walther@59846:   \item generate.sml: RM datatype edit TOGETHER WITH datatype inout
walther@59846:   \item TermC.list2isalist: typ -> term list -> term  .. should NOT requires typ
walther@59846:   \item get_ctxt_LI should replace get_ctxt
walther@59846:   \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
walther@59846:   \item rename   Base_Tool.thy  <---         Base_Tools
walther@59846:   \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
walther@59846:   \item rename field scr in meth
walther@59819:   \item xxx
walther@59820:   \item xxx
walther@59820:   \item xxx
walther@59844:   \item xxx
walther@59844:   \item xxx
walther@59844:   \item xxx
walther@59817:   \item xxx
walther@59814:   \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}
walther@59848:      there it is Free ("Subproblem", "char list \<times> ..
walther@59848:      instead of  Const (|???.Subproblem", "char list \<times> ..
walther@59848:      AND THE STRING REPRESENTATION IS STRANGE: 
walther@59848:        Subproblem (''Test'',
walther@59848:         ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation''
walther@59848:          ''test'')
walther@59814:      ML \<open>
walther@59814:      \<close> ML \<open>
walther@59814:      term2str; (*defined by..*)
walther@59814:      fun term_to_string''' thy t =
walther@59814:        let
walther@59814:          val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
walther@59814:        in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
walther@59814:      \<close> ML \<open>
walther@59814:      val t = @{term "aaa + bbb"}
walther@59814:      val t = @{term "Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation''])"};
walther@59814:      \<close> ML \<open>
walther@59814:      val sss = Print_Mode.setmp [] (Syntax.string_of_term @{context}) t
walther@59814:      \<close> ML \<open>
walther@59814:      writeln sss (*.. here perfect: Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation'']) *)
walther@59814:      \<close> ML \<open>
walther@59814:      \<close>
walther@59814:   \item xxx
walther@59814:   \item xxx
walther@59814:   \item cleanup fun me:
walther@59814:     fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me:  Empty_Tac at " ^ pos'2str p)
walther@59814:       | me*) (_, tac) p _(*NEW remove*) pt =
walther@59814:     + -------------------------^^^^^^
walther@59814:     # see test-code.sml fun me_trace
walther@59814:       use this also for me, not only for me_ist_ctxt; del. me
walther@59814:       this requires much updating in all test/*
walther@59802:   \item xxx
walther@59779:   \item shift tests into NEW model.sml (upd, upds_envv, ..)
walther@59779:   \item xxx
walther@59814:   \item clarify handling of contexts ctxt ContextC
walther@59779:     \begin{itemize}
walther@59779:     \item xxx
walther@59779:     \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
walther@59779:     \item xxx
walther@59779:     \item Check_Elementwise "Assumptions": prerequisite for ^^goal
walther@59779:       rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
walther@59779:       rm Assumptions  :: bool  (* TODO: remove with making ^^^ idle *)
walther@59779:     \item xxx
walther@59779:     \item xxx
walther@59779:     \end{itemize}
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item complete mstools.sml (* survey on handling contexts:
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item librarys.ml --> libraryC.sml + text from termC.sml
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
walther@59779:                                    DONE  for find_next_step by Tactic.insert_assumptions m' ctxt 
walther@59779:     \begin{itemize}
walther@59779:     \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
walther@59779:     \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
walther@59779:     \item xxx
walther@59779:     \item xxx
walther@59779:     \item DO DELETIONS AFTER analogous concentrations in find_next_step
walther@59779:     \end{itemize}
walther@59779:   \item xxx
walther@59779:   \item ? what is the difference headline <--> cascmd in
walther@59779:     Subproblem' (spec, oris, headline, fmz_, context, cascmd)
walther@59924:   \item Substitute' what does "re-calculation mean in the datatype comment?
walther@59779:   \item xxx
walther@59881:   \item inform: TermC.parse (ThyC.get_theory "Isac_Knowledge") istr --> parseNEW context istr
walther@59799:   \item xxx
walther@59816:   \item unify/clarify stac2tac_ | 
walther@59779:     \begin{itemize}
walther@59779:     \item xxx
walther@59816:     \item extract common code from associate.. stac2tac_xxx
walther@59823:     \item rename LItool.tac_from_prog -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,
walther@59779:     \item xxx
walther@59779:     \item xxx
walther@59779:     \end{itemize}
walther@59779:   \item xxx
walther@59779:   \item unify in signature LANGUAGE_TOOLS =\\
walther@59903:     val pblterm: ThyC.id -> Problem.id -> term     vvv        vvv\\
walther@59779:     val subpbl: string -> string list -> term          unify with ^^^
walther@59779:   \item xxx
walther@59779:   \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
walther@59779:     Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
walther@59779:     If Telem.safe is kept, consider merge with CTbasic.ostate
walther@59779:   \item xxx
walther@59779:   \item remove find_next_step from solve Apply_Method';
walther@59779:     this enforces Pos.at_first_tactic, which should be dropped, too.
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59816:   \item xxx
walther@59779:   \end{itemize}
walther@59779: \<close>
walther@59851: subsection \<open>Postponed --> Major reforms\<close>
walther@59816: text \<open>
walther@59816:   \begin{itemize}
walther@59816:   \item xxx          
walther@60040:   \item xxx
walther@60040:   \item make parser mutually recursive for Problem .. Solution
walther@60040:     preps. in Test_Parse_Isac:
walther@60040:       Test_Parse_Isac:
walther@60040:         subsubsection "problem_mini" shows a principal issue with recursive parsing
walther@60040:         probably due to !2! arguments of parser (as shown in Cookbook)
walther@60040:       Test_Parsers_Cookbook:
walther@60040:         (* recursive parser p.140 \<section>6.1 adapted to tokens: *) shows differences,
walther@60040:         which might help understanding the principal issue
walther@60040:     see also Test_Parsers  subsection "recursive parsing"
walther@60040:   \item xxx
walther@60040:   \item xxx          
walther@60040:   \item xxx          
walther@59846:   \item revisit bootstrap Calcelements. rule->calcelems->termC
walther@59868:     would be nice, but is hard: UnparseC.terms -> TermC.s_to_string
walther@59820:   \item xxx
walther@59820:   \item replace all Ctree.update_* with Ctree.cupdate_problem
walther@59820:   \item xxx
walther@59816:   \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
walther@59816:   \item xxx
walther@59816:   \item exception PROG analogous to TERM
walther@59816:   \item xxx
walther@59816:   \item sig/struc ..elems --> ..elem
walther@59816:   \item xxx          
walther@59816:   \item distille CAS-command, CAScmd, etc into a struct
walther@59816:   \item xxx          
walther@59816:   \item check location of files:
walther@59816:         test/Tools/isac/Interpret/ptyps.thy
walther@59816:         test/Tools/isac/Specify.ptyps.sml
walther@59816:   \item xxx
walther@59816:   \item check occurences of Atools in src/ test/
walther@59816:   \item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _) 
walther@59816:   \item xxx          
walther@59816:   \item rm Float
walther@59816:   \item xxx
walther@59816:   \item Diff.thy: differentiateX --> differentiate after removal of script-constant
walther@59816:   \item Test.thy: met_test_sqrt2: deleted?!
walther@59816:   \item xxx          
walther@59887:   \item Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx, too*)
walther@59816:   \item xxx
walther@59816:     \item automatically extrac rls from program-code 
walther@59816:       ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
walther@59816:   \item xxx          
walther@59901:   \item finish output of LItool.trace with Check_Postcond (useful for SubProblem)
walther@59816:   \item xxx
walther@59851:   \item replace Rule_Set.empty by Rule_Set.Empty
walther@59851:     latter is more clear, but replacing ***breaks rewriting over all examples***,
walther@59851:     e.g. see ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x'
walther@59851:     in Minisubplb/200-start-method-NEXT_STEP.sml:
walther@59851:      (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
walther@59851:      (*+*)  prls =
walther@59852:      (*+*)    Rls {calc = [], erls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =
walther@59878:      (*+*)      ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Erls}:
walther@59851:      (*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !
walther@59851:      (*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had
walther@59851:      (*+*)val Empty = prls (* <---ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x' *)
walther@59851:      ( *+*)val ["sqroot-test", "univariate", "equation", "test"] = cpI
walther@59851:     THAT INDICATES, that much rewriting/evaluating JUST WORKED BY CHANCE?!?
walther@59816:   \item xxx          
walther@59816:   \item xxx
walther@59816:   \item xxx          
walther@59816:   \item xxx
walther@59816:   \item xxx          
walther@59816:   \item xxx
walther@59816:   \item xxx          
walther@59816:   \end{itemize}
walther@59816: \<close>
walther@59816: 
walther@59779: section \<open>Major reforms\<close>
walther@59779: text \<open>
walther@59779: \<close>
walther@59779: subsection \<open>Exception Size raised\<close>
walther@59779: text \<open>
walther@59779:   During update Isabelle2018 --> Isabelle2019 we noticed, that
walther@59779:   "isabelle build" uses resources more efficiently than "isabelle jedit".
walther@59779:   The former works, but the latter causes 
walther@59779:   \begin{itemize}
walther@59779:   \item "Exception- Size raised"
walther@59779:     in Build_Thydata.thy
walther@59779:   \item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
walther@59779:     in test/../biegelinie-*.xml.
walther@59779:   \end{itemize}
walther@59779:   This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
walther@59779: 
walther@59779:   Find tools to investigate the Exception, and find ways around it eventually.
walther@59779: \<close>
walther@59779: subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
walther@59779: text \<open>
walther@59779:   \begin{itemize}
walther@59779:   \item there are comments in several signatures
wenzelm@60192:   \item ML_file "$ISABELLE_ISAC/Interpret/specification-elems.sml" can be (almost) deleted
walther@59779:   \item src/../Frontend/: signatures missing
walther@59779:   \item xxx
walther@59779:   \end{itemize}
walther@59779: \<close>
walther@59779: subsection \<open>overall structure of code\<close>
walther@59779: text \<open>
walther@59779:   \begin{itemize}
walther@59779:   \item try to separate Isac_Knowledge from MathEngine
walther@59779:     common base: Knowledge_Author / ..??
walther@59779:   \item xxx
wenzelm@60192:   \item  ML_file "$ISABELLE_ISAC/Interpret/ctree.sml" (*shift to base in common with Interpret*)
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \item xxx
walther@59779:   \end{itemize}
walther@59779: \<close>
walther@59779: subsection \<open>Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/\<close>
walther@59779: text \<open>
walther@59779:   \begin{itemize}
walther@59779:   \item xxx
walther@59800:   \item xxx
walther@59734:   \item re-organise code for Interpret
walther@59734:     \begin{itemize}
walther@59933:     \item Step*: Step_Specify | Step_Solve | Step DONE
walther@59734:     \item xxx
walther@59848:     \item Prog_Tac: fun get_first_argument takes both Prog_Tac + Program --- wait for separate Tactical
walther@59800:       then shift into common descendant
walther@59734:     \item xxx
walther@59734:     \end{itemize}
walther@59734:   \item xxx
walther@59778:   \item xxx
walther@59791:   \item ??????????? WHY CAN LI.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
walther@59778:   \item xxx
walther@59778:   \item xxx
walther@59778:   \end{itemize}
walther@59778: \<close>
wneuper@59574: subsection \<open>Review modelling- + specification-phase\<close>
wneuper@59574: text \<open>
wneuper@59574:   \begin{itemize}
walther@59816:   \item xxx
walther@59820:   \item xxx
walther@59820:   \item xxx
walther@59816:   \item check match between args of partial_function and model-pattern of meth;
walther@59816:      provide error message.
walther@59778:   \item xxx
wneuper@59574:   \item "--- hack for funpack: generalise handling of meths which extend problem items ---"
wneuper@59569:     \begin{itemize}
wneuper@59574:     \item see several locations of hack in code
wneuper@59574:     \item these locations are NOT sufficient, see
wneuper@59574:       test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
wneuper@59574:     \item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,
wneuper@59574:       this would be according to survey Notes (3) in src/../calchead.sml.
wneuper@59574:     \end{itemize}
wneuper@59574:   \item see "failed trial to generalise handling of meths"98298342fb6d
wneuper@59574:   \item abstract specify + nxt_specif to common aux-funs;
wneuper@59574:     see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
wneuper@59574:   \item xxx
wneuper@59574:   \item type model = itm list ?
wneuper@59574:   \item review survey Notes in src/../calchead.sml: they are questionable
wneuper@59574:   \item review copy-named, probably two issues commingled 
wneuper@59574:     \begin{itemize}
wneuper@59574:     \item special handling of "#Find#, because it is not a formal argument of partial_function
wneuper@59574:     \item special naming for solutions of equation solving: x_1, x_2, ...
wneuper@59569:     \end{itemize}
wneuper@59569:   \item xxx
walther@59634:   \item xxx
wneuper@59574:   \item this has been written in one go:
wneuper@59574:     \begin{itemize}
Walther@60477:     \item reconsidering I_Model.max_variant, use problem with meth ["Diff_App", "max_by_calculus"]
wneuper@59574:     \item reconsider add_field': where is it used for what? Shift into mk_oris
Walther@60477:     \item reconsider match_itms_oris: where is it used for what? max_variant ONLY???
wneuper@59574:     \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
wneuper@59574:     \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
wneuper@59574:       (relevant for pre-condition)
wneuper@59574:     \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
wneuper@59574:     \item 
wneuper@59574:     \end{itemize}
wneuper@59574:   \end{itemize}
wneuper@59574: \<close>
wneuper@59574: subsection \<open>taci list, type step\<close>
wneuper@59574: text \<open>
walther@59762: taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
walther@59762: and probably, because the Kernel interface separated setNextTactic and applyTactic.
walther@59816: Both are no good reasons to make code more complicated.
walther@59814: 
walther@59816: !!! taci list is used in do_next !!!
walther@59814: 
wneuper@59574:   \begin{itemize}
walther@59762:   \item xxx
walther@59820:   \item can lev_on_total replace lev_on ? ..Test_Isac_Short + rename lev_on_total -> lev_on
walther@59820:   \item xxx
walther@59981:   \item Step* functions should return Calc.T instead of Calc.state_post
walther@59762:   \item xxx
wneuper@59574:   \item states.sml: check, when "length tacis > 1"
wneuper@59574:   \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
wneuper@59574:   \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
wneuper@59569:   \item xxx
walther@59816:   \item brute force setting all empty ([], [], ptp) works!?! but ptp causes errors -- investigate!
walther@59762:   \item xxx
wneuper@59573:   \end{itemize}
wneuper@59574: \<close>
wneuper@59574: subsection \<open>Ctree\<close>
wneuper@59574: text \<open>
walther@59815: analysis
walther@59815: # mixture pos' .. pos in cappend_*, append_* is confusing
walther@59844: # existpt p pt andalso Tactic.is_empty DIFFERENT IN append_*, cappend_* is confusing
walther@59815:   "exception PTREE "get_obj: pos =" ^^^^^: ^^^^ due to cut !!!
walther@59815:   NOTE: exn IN if..andalso.. IS NOT!!! DETECTED, THIS                       is confusing
walther@59815:   see test/../--- Minisubpbl/800-append-on-Frm.sml ---
walther@59815: # ?!? "cut branches below cannot be decided here" in append_atomic
walther@59815: # sign. of functions too different ?!?canonical arg.order ?!?
wneuper@59568:   \begin{itemize}
walther@59807:   \item xxx
walther@59815:   \item remove update_branch, update_*? -- make branch, etc args of append_*
walther@59815:   \item xxx
walther@59816:   \item close sig Ctree, contains cappend_* ?only? --- ?make parallel to ?Pide_Store?
walther@59813:   \item xxx
walther@59807:   \item unify args to Ctree.state (pt, p)
walther@59846:   \item  fun update_env       .. repl_env                   \<rightarrow>updatempty
walther@59807:   \item xxx
wneuper@59568:   \item xxx
wneuper@59574:   \item xxx
walther@59807:   \item xxx
wneuper@59568:   \end{itemize}
wneuper@59574: \<close>
wneuper@59574: subsection \<open>replace theory/thy by context/ctxt\<close>
wneuper@59574: text \<open>
wneuper@59574:   \begin{itemize}
walther@59660:   \item xxx
walther@59748:   \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
walther@59748:     special case: Tactic.Refine_Problem
walther@59748:   \item xxx
walther@59748:   \item theory can be retrieved from ctxt by Proof_Context.theory_of
walther@59660:   \item xxx
wneuper@59577:   \item cleaup the many conversions string -- theory
wneuper@59577:   \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
wneuper@59574:   \item 1. Rewrite.eval_true_, then
walther@59933:     LItool.check_leaf, Rewrite.eval_prog_expr, Step.add, LItool.tac_from_prog.
wneuper@59577:   \item fun associate
walther@59881:     let val thy = ThyC.get_theory "Isac_Knowledge";(*TODO*)
wneuper@59574:   \item xxx
wneuper@59574:   \item xxx
walther@59802:   \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr   .use  Term.exists_Const
walther@59802:   \item push srls into pstate
walther@59851:   \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule_Set.Empty)
walther@59851:                                                                                       ^^^^^^^^^^^^^^^
wneuper@59577:   \item xxx
wneuper@59574:   \end{itemize}
wneuper@59574: \<close>
wneuper@59583: subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
wneuper@59574: text \<open>
walther@59878: remove refactor Rfuns, Rule.Prog, Rule.Empty_Prog, RrlsState: this is a concept never brought to work.
walther@59850:   Clarify relation to reverse rewriting!
wneuper@59562:   \begin{itemize}
walther@59850:   \item separate mut.recursion program with rule and rls by deleting fild scr in rls
walther@59850:     (possible since CS 43160c1e775a
walther@59850:   ` "replace Prog. in prep_rls by Auto_Prog.gen, which generates Prog. on the fly" )
wneuper@59573:   \item xxx
wneuper@59569:   \item probably only "normal_form" seems to be needed
wneuper@59569:   \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
wneuper@59569:     but that seems desirable
wneuper@59569:   \item ?how is the relation to reverse-rewriting ???
wneuper@59569:   \item "Rfuns" markers in test/../rational
wneuper@59562:   \item xxx
walther@59667:   \item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
wneuper@59573:     rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
wneuper@59583:     Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
wneuper@59573:     Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
wneuper@59573:   \item debug ^^^ related: is there an occurence of Steps with more than 1 element?
wneuper@59569:   \item xxx
walther@59760:   \item and do_next (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
wneuper@59573:   \item xxx
wneuper@59573:   \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
walther@59850:   \item xxx
walther@59850:   \item ?finally Prog could go from Calcelems to ProgLang?
wneuper@59562:   \end{itemize}
wneuper@59574: \<close>
wneuper@59574: subsection \<open>Inverse_Z_Transform.thy\<close>
wneuper@59574: text \<open>
wneuper@59538:   \begin{itemize}
wneuper@59550:   \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
wneuper@59550:   ? replace rewriting with substitution ?!?
wneuper@59537:   The problem is related to the decision of typing for "d_d" and making bound variables free (while
wneuper@59550:   shifting specific handling in equation solving etc. to the meta-logic). 
wneuper@59550:   \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
wneuper@59550:     rewrite-rules; see \ref{new-var-rhs}.
wneuper@59538:   \item Reconsider whole problem:
wneuper@59538:     input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
wneuper@59538:   \end{itemize}
wneuper@59574: \<close>
wneuper@59574: subsection \<open>Adopt Isabelle's numerals for Isac\<close>
wneuper@59574: text \<open>
wneuper@59540:   \begin{itemize}
wneuper@59574:   \item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
wneuper@59574:     and have both representations in parallel for "nat".
wneuper@59574:   \item xxx
wneuper@59574:   \item xxx
wneuper@59540:   \end{itemize}
wneuper@59574: \<close>
walther@59816: subsection \<open>Redesign equation solver\<close>
wneuper@59591: text \<open>
wneuper@59591:   Existing solver is structured along the WRONG assumption,
walther@59816:   that Poly.thy must be the LAST thy among all thys involved -- while the opposite is the case.
wneuper@59591: 
wneuper@59591:   Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
wneuper@59591: \<close>
walther@59816: subsection \<open>Finetunig required for xmldata in kbase\<close>
wneuper@59574: text \<open>
wneuper@59574:   See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
wneuper@59574:   and in kbase html-representation generated from these xmldata.
wneuper@59574:   Notes in ~~/xmldata/TODO.txt.
wneuper@59574: \<close>
wneuper@59574: 
wneuper@59574: section \<open>Hints for further development\<close>
wneuper@59574: text \<open>
wneuper@59574: \<close>
wneuper@59591: subsection \<open>Coding standards & some explanations for math-authors\<close>
wneuper@59591: text \<open>copy from doc/math-eng.tex WN.28.3.03
wneuper@59591: WN071228 extended\<close>
wneuper@59591: 
wneuper@59591: subsubsection \<open>Identifiers\<close>
wneuper@59591: text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
wneuper@59591:   not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
wneuper@59591:   reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
wneuper@59591:   problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
wneuper@59591:   However, all the cases (1)..(4) require different typing for one and the same
wneuper@59591:   identifier {\tt probe} which is impossible, and actually leads to strange errors
wneuper@59591:   (for instance (1) is used as string, except in a script addressing a Subproblem).
wneuper@59591: 
wneuper@59591:   These are the preliminary rules for naming identifiers>
wneuper@59591:   \begin{description}
wneuper@59591:   \item [elements of a key] into the hierarchy of problems or methods must not contain
wneuper@59591:     capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
wneuper@59591:   \item [descriptions in problem-patterns] must contain at least 1 capital letter and
wneuper@59591:     must not contain underscores, e.g. {\tt Probe, forPolynomials}.
wneuper@59591:   \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
wneuper@59591:     beware of conflicts~!
wneuper@59591:   \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
wneuper@59591:   \item [???] ???
wneuper@59591:   \item [???] ???
wneuper@59591:   \end{description}
wneuper@59591: %WN071228 extended\<close>
wneuper@59591: 
wneuper@59591: subsubsection \<open>Rule sets\<close>
wneuper@59591: text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
wneuper@59591:   where it can be viewed using the knowledge browsers.
wneuper@59591: 
wneuper@59591:   There are rulesets visible to the student, and there are rulesets visible (in general) only for
wneuper@59591:   math authors. There are also rulesets which {\em must} exist for {\em each} theory;
wneuper@59591:   these contain the identifier of the respective theory (including all capital letters) 
wneuper@59591:   as indicated by {\it Thy} below.
wneuper@59591: 
wneuper@59591:   \begin{description}
wneuper@59591:   \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
wneuper@59591:     normalform for all terms which can be expressed by the definitions of the respective theory
wneuper@59591:     (and the respective parents).
wneuper@59591:   \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
wneuper@59591:     which can be expressed by the definitions of the respective theory (and the respective parents)
wneuper@59591:     such, that the rewrites can be presented to the student.
wneuper@59591:   \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with 
wneuper@59591:     numerical constants only (i.e. all terms which can be expressed by the definitions of
wneuper@59591:     the respective theory and the respective parent theories). In particular, this ruleset includes
wneuper@59591:     evaluating in/equalities with numerical constants only.
wneuper@59591:     WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
wneuper@59591:     are logically equivalent, where the latter often add to the assumptions
wneuper@59591:     (e.g. in Check_elementwise).
wneuper@59591:   \end{description}
wneuper@59591: 
wneuper@59591:   The above rulesets are all visible to the user, and also may be input; 
wneuper@59591:   thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
wneuper@59591:   KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
wneuper@59591:   using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
wneuper@59591:   The following rulesets are used for internal purposes and usually invisible to the (naive) user:
wneuper@59591: 
wneuper@59591:   \begin{description}
wneuper@59591:   \item [*\_erls] TODO
wneuper@59591:   \item [*\_prls] 
wneuper@59591:   \item [*\_srls] 
wneuper@59591:   \end{description}
walther@59852: {\tt Rule_Set.append_rules, Rule_Set.merge, remove_rls} TODO
wneuper@59591: \<close>
wneuper@59591: 
wneuper@59574: subsection \<open>get proof-state\<close>
wneuper@59574: text \<open>
wneuper@59574:   Re: [isabelle] Programatically get "this"
wneuper@59574:   ----------------------------------------------------
wneuper@59574:   So here is my (Makarius') version of your initial example, following these principles:
wneuper@59574:   begin{verbatim}
wneuper@59574:     notepad
wneuper@59574:     begin
wneuper@59574:       assume a: A
wneuper@59574:       ML_val \<open>
wneuper@59574:         val ctxt = @{context};
wneuper@59558:     
wneuper@59574:         val this_name =
walther@59748:           Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN);
wneuper@59574:         val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
wneuper@59574:       \<close>
wneuper@59574:     end
wneuper@59574:   end{verbatim}
wneuper@59574: \<close>
wneuper@59574: subsection \<open>write Specification to jEdit\<close>
wneuper@59574: text \<open>
wneuper@59574:   Re: [isabelle] Printing terms with type annotations
wneuper@59574:   ----------------------------------------------------
wneuper@59574:   On 06/02/2019 17:52, Moa Johansson wrote:
wneuper@59574:   >
wneuper@59574:   > I’m writing some code that should create a snippet of Isar script.
wneuper@59574:   
wneuper@59574:   This is how Sledgehammer approximates this:
wneuper@59574:   
wneuper@59574:   http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
wneuper@59574:   
wneuper@59574:   (The module name already shows that the proper terminology is "Isar
wneuper@59574:   proof" (or "Isar proof text").  Proof scripts are a thing from the past,
wneuper@59574:   before Isar. You can emulate old-style proof scripts via a sequence of
wneuper@59574:   'apply' commands, but this is improper Isar.)
wneuper@59574:   
wneuper@59574:   Note that there is no standard function in Isabelle/Pure, because the
wneuper@59574:   problem to print just the right amount of type information is very
wneuper@59574:   complex and not fully solved. One day, after 1 or 2 rounds of
wneuper@59574:   refinements over the above approach, it might become generally available.
wneuper@59574: \<close>
wneuper@59574: subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
wneuper@59574: text \<open>
wneuper@59574:   isabelle update -u path_cartouches
wneuper@59574:   isabelle update -u inner_syntax_cartouches
wneuper@59574: \<close>
wneuper@59582: section \<open>Questions to Isabelle experts\<close>
wneuper@59582: text \<open>
wneuper@59582: \begin{itemize}
walther@59848: \item ad ERROR Undefined fact "all_left"        in Test_Isac: error-pattern.sml
walther@59848:                Undefined fact: "xfoldr_Nil"                   inssort.sml
walther@59886:     (* probably two different reasons:
walther@59886:     src/../LinEq.thy
walther@59886:       (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
walther@59886:       all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
walther@59886:     
walther@59886:     src/../PolyEq.thy
walther@59886:       (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
walther@59886:       all_left:              "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
walther@59886:     
walther@59886:     test/../partial_fractions.sml
walther@59886:     (*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
walther@59886:     (*[7, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"))*)
walther@59886:     
walther@59886:     test/../mathengine-stateless.sml
walther@59886:     (*if ThmC.string_of_thm @ {thm rnorm_equation_add} =  "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
walther@59886:     then () else error "string_of_thm changed";*)
walther@59886:     
walther@59886:     (*---------------------------------------------------------------------------------------------*)
walther@59886:     src/../LinEq.thy
walther@59886:     primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
walther@59886:     xfoldr_Nil:  "xfoldr f {|| ||} = id" |
walther@59886:     xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
walther@59886:     
walther@59886:     src/../InsSort.thy
walther@59886:         srls = Rule_Set.empty, calc = [], rules = [
walther@59886:           Rule.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
walther@59886:     *)
walther@59841: \item xxx
walther@59841: \item xxx
walther@59842: \item ?OK Test_Isac_Short with
walther@59842:     LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
walther@59842:   instead
walther@59846:     LI.by_tactic tac (Istate.empty, ContextC.empty) ptp
walther@59842:   in step-solve ?
walther@59842: \item xxx
walther@59842: \item test from last CS with outcommented re-def of code -> 
walther@59842:   -> \<open>further tests additional to src/.. files\<close>
walther@59842:       ADDTESTS/redefined-code.sml
walther@59841: \item xxx
walther@59841: \item efb749b79361 Test_Some_Short.thy has 2 errors, which disappear in thy ?!?:
walther@59841:   ML_file "Interpret/error-pattern.sml" Undefined fact: "all_left"
walther@59841:   ML_file "Knowledge/inssort.sml" Undefined fact: "xfoldr_Nil"
walther@59841: \item xxx
wneuper@59591: \item what is the actual replacement of "hg log --follow" ?
wneuper@59591: \item xxx
wneuper@59582: \item how HANDLE these exceptions, e.g.:
wneuper@59582:     Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
wneuper@59582:   GIVES
wneuper@59582:     "Inner syntax error
wneuper@59582:      Failed to parse term"
wneuper@59582: \item xxx
walther@59734: \item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"
walther@59734:   e.g. in test/Interpret/lucas-interpreter.sml
wneuper@59582: \item xxx
wneuper@59582: \item xxx
wneuper@59582: \end{itemize}
wneuper@59582: \<close>
wneuper@59582: 
wneuper@59574: section \<open>For copy & paste\<close>
wneuper@59574: text \<open>
wneuper@59582: \begin{itemize}
walther@59778: \item xxx
wneuper@59558:   \begin{itemize}
wneuper@59558:   \item xxx
wneuper@59540:     \begin{itemize}
wneuper@59558:     \item xxx
wneuper@59540:       \begin{itemize}
wneuper@59558:       \item xxx
wneuper@59574:         \begin{itemize}
wneuper@59574:         \item xxx
wneuper@59574:         \end{itemize}
wneuper@59540:       \end{itemize}
wneuper@59540:     \end{itemize}
wneuper@59504:   \end{itemize}
wneuper@59504: \end{itemize}
wneuper@59504: \<close>
wneuper@59574: subsection \<open>xxx\<close>
wneuper@59574: subsubsection \<open>xxx\<close>
neuper@52150: end




