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 \ walther@59779: Legend: here + code since 200120 walther@59779: \(*DOC\ identifies stuff dedicated for isac/Doc/Lucas_Interpreter walther@59779: \(*?!?\ identifies a design question walther@59779: walther@59779: Distillation of "rounds of reforms": walther@59779: \TODOs from current changesets\ \ \Postponed from current changeset\ \ walther@59779: (*to be removed..*) \ \Separated tasks\ (*.. to be removed*) walther@59779: \ subsection of \Major reforms\ walther@59779: \ walther@59779: wneuper@59574: section \TODOs from current changesets\ wneuper@59568: text\ walther@59779: Shift more complicated issues from \Current changeset\ to \Postponed from current changeset\ wneuper@59568: \ wneuper@59574: subsection \Current changeset\ wneuper@59574: text \ 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@59998: \item Specify.find_next_step: References.select walther@59998: cpI = ["vonBelastungZu", "Biegelinien"]: References_Def.id walther@59998: ^^^^^ Problem.id walther@59998: \item xxx walther@59998: \item Calc.state_empty_post \ 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: \ walther@59846: subsection \Postponed from current changeset\ walther@59846: text \ 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 \ .. walther@59848: instead of Const (|???.Subproblem", "char list \ .. 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 \ walther@59814: \ ML \ 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: \ ML \ walther@59814: val t = @{term "aaa + bbb"} walther@59814: val t = @{term "Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation''])"}; walther@59814: \ ML \ walther@59814: val sss = Print_Mode.setmp [] (Syntax.string_of_term @{context}) t walther@59814: \ ML \ walther@59814: writeln sss (*.. here perfect: Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation'']) *) walther@59814: \ ML \ walther@59814: \ 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: \ walther@59851: subsection \Postponed --> Major reforms\ walther@59816: text \ 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 \
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: \ walther@59816: walther@59779: section \Major reforms\ walther@59779: text \ walther@59779: \ walther@59779: subsection \Exception Size raised\ walther@59779: text \ 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: \ walther@59779: subsection \Cleanup & review signatures wrt. implementation.pdf canonical argument order\ walther@59779: text \ 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: \ walther@59779: subsection \overall structure of code\ walther@59779: text \ 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: \ walther@59779: subsection \Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/\ walther@59779: text \ 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: \ wneuper@59574: subsection \Review modelling- + specification-phase\ wneuper@59574: text \ 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: \ wneuper@59574: subsection \taci list, type step\ wneuper@59574: text \ 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: \ wneuper@59574: subsection \Ctree\ wneuper@59574: text \ 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 \updatempty walther@59807: \item xxx wneuper@59568: \item xxx wneuper@59574: \item xxx walther@59807: \item xxx wneuper@59568: \end{itemize} wneuper@59574: \ wneuper@59574: subsection \replace theory/thy by context/ctxt\ wneuper@59574: text \ 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: \ wneuper@59583: subsection \Rfuns, Begin_/End_Detail', Rrls, Istate\ wneuper@59574: text \ 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: \ wneuper@59574: subsection \Inverse_Z_Transform.thy\ wneuper@59574: text \ 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: \ wneuper@59574: subsection \Adopt Isabelle's numerals for Isac\ wneuper@59574: text \ 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: \ walther@59816: subsection \Redesign equation solver\ wneuper@59591: text \ 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: \ walther@59816: subsection \Finetunig required for xmldata in kbase\ wneuper@59574: text \ 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: \ wneuper@59574: wneuper@59574: section \Hints for further development\ wneuper@59574: text \ wneuper@59574: \ wneuper@59591: subsection \Coding standards & some explanations for math-authors\ wneuper@59591: text \copy from doc/math-eng.tex WN.28.3.03 wneuper@59591: WN071228 extended\ wneuper@59591: wneuper@59591: subsubsection \Identifiers\ wneuper@59591: text \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\ wneuper@59591: wneuper@59591: subsubsection \Rule sets\ wneuper@59591: text \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: \ wneuper@59591: wneuper@59574: subsection \get proof-state\ wneuper@59574: text \ 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 \ 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: \ wneuper@59574: end wneuper@59574: end{verbatim} wneuper@59574: \ wneuper@59574: subsection \write Specification to jEdit\ wneuper@59574: text \ 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: \ wneuper@59574: subsection \follow Isabelle conventions (*Does not yet work in Isabelle2018\ wneuper@59574: text \ wneuper@59574: isabelle update -u path_cartouches wneuper@59574: isabelle update -u inner_syntax_cartouches wneuper@59574: \ wneuper@59582: section \Questions to Isabelle experts\ wneuper@59582: text \ 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", "\ ?b =!= 0 \ (?a = ?b) = (?a - ?b = 0)"))*) walther@59886: walther@59886: test/../mathengine-stateless.sml walther@59886: (*if ThmC.string_of_thm @ {thm rnorm_equation_add} = "\ ?b =!= 0 \ (?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 \ 'b \ 'b) \ 'a xlist \ 'b \ 'b" where walther@59886: xfoldr_Nil: "xfoldr f {|| ||} = id" | walther@59886: xfoldr_Cons: "xfoldr f (x @# xs) = f x \ 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: -> \further tests additional to src/.. files\ 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: \ wneuper@59582: wneuper@59574: section \For copy & paste\ wneuper@59574: text \ 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: \ wneuper@59574: subsection \xxx\ wneuper@59574: subsubsection \xxx\ neuper@52150: end