LI: prep. test to re-build locate_input_term
1 (* Title: todo's for isac core
2 Author: Walther Neuper 111013
3 (c) copyright due to lincense terms.
6 imports "~~/src/Doc/Prog_Prove/LaTeXsugar"
10 Legend: here + code since 200120
11 \<open>(*DOC\<close> identifies stuff dedicated for isac/Doc/Lucas_Interpreter
12 \<open>(*?!?\<close> identifies a design question
14 Distillation of "rounds of reforms":
15 \<open>TODOs from current changesets\<close> \<rightarrow> \<open>Postponed from current changeset\<close> \<rightarrow>
16 (*to be removed..*) \<rightarrow> \<open>Separated tasks\<close> (*.. to be removed*)
17 \<rightarrow> subsection of \<open>Major reforms\<close>
20 section \<open>TODOs from current changesets\<close>
22 Shift more complicated issues from \<open>Current changeset\<close> to \<open>Postponed from current changeset\<close>
24 subsection \<open>Current changeset\<close>
34 \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
37 check_tac cc ist (form_arg, prog_tac) to
38 check_tac cc ist (prog_tac, form_arg)
41 \item rm test/..--- check Scripts ---
43 \item reformat + rename "fun eval_leaf"+"fun get_stac"
45 ?consistency with subst term?
46 \item Tactic.Rewrite*': drop "bool"
48 \item exception PROG analogous to TERM
50 \item Prog_Tac: fun get_stac takes both Prog_Tac + Program --- wait for separate Tactical
51 then shift into common descendant
52 rename get_stac --> ?ptac?
54 \item separate code required in both, ProgLang & Interpret (e.g?)
56 \item /-------------------------------------------------------------------
57 \item check occurences of KEStore_Elems.add_rlss [("list_rls",
58 \item rename list_rls accordingly
59 \item ------------------------------------------------------------------/
62 \item signature LIBRARY_C
63 \item Program.thy (*=========== record these ^^^ in 'tacs' in program.ML =========*)
64 \item sig/struc ..elems --> elem
70 \item distribute test/../scrtools.sml
73 \item simplify calls of scan_dn1, scan_dn etc
74 \item open Istate in LI
77 subsection \<open>Postponed from current changeset\<close>
81 \item generate, generate1: NO thy as arg.
83 \item decompose do_next, by_tactic: mutual recursion only avoids multiple generate1
84 ! ^^^ in find_next_step --- ? ? ? in locate_input_tactic ?
86 \item Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
88 \item NEW structure Step.applicable Step.add
89 ^applicable_in ^generate1
91 \item revise Pstate {or, ...}; strange occurrence in program without Tactical.Or documented here
93 \item shift tests into NEW model.sml (upd, upds_envv, ..)
96 \item clarify handling of contexts
99 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
101 \item Check_Elementwise "Assumptions": prerequisite for ^^goal
102 rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
103 rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
105 \item cleanup fun me:
106 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
107 | me*) (_, tac) p _(*NEW remove*) pt =
108 + -------------------------^^^^^^
110 \item remove ctxt from Tactic.T; this makes use of ctxt more explicit (e.g. in LI)
112 \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
113 \item rm ctxt from Subproblem' (is separated in associate!))
115 \item check Tactic.Subproblem': are 2 terms required?
117 \item Test_Some.--- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts --
118 --: wait for deleting Check_Elementwise Assumptions
120 \item lucas-intrpreter.scan_dn1: Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
124 \item complete mstools.sml (* survey on handling contexts:
129 \item datatype L,R,D --> Istate
133 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
135 \item pstate2str --> pstate2str
137 \item after review of Rrls, detail ?-->? istate
138 \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)
140 \item push srls into pstate
141 \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls)
147 \item trace_script: replace ' by " in writeln
149 \item librarys.ml --> libraryC.sml + text from termC.sml
156 \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
157 DONE for find_next_step by Tactic.insert_assumptions m' ctxt
159 \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
160 \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
161 \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
164 \item DO DELETIONS AFTER analogous concentrations in find_next_step
167 \item ? what is the difference headline <--> cascmd in
168 Subproblem' (spec, oris, headline, fmz_, context, cascmd)
170 \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
171 \item extract common code from associate.. stac2tac_
172 rename LItool.stac2tac -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,
173 .. see \<open>Separate ..\<close>
177 section \<open>Separated tasks\<close>
179 This section shall be removed, because
180 the distinction \<open>Simple\<close> | \<open>Simple but laborous\<close> | \<open>Questionable\<close>
181 is too distracting when working \<open>TODOs from current changesets\<close>.
183 subsection \<open>Simple\<close>
188 \item check location of files:
189 test/Tools/isac/Interpret/ptyps.thy
190 test/Tools/isac/Specify.ptyps.sml
192 \item check occurences of Atools in src/ test/
194 \item drop drop_questionmarks_
196 \item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _)
197 \item rename Base_Tool.thy <--- Base_Tool
199 \item test/.. tools.sml, atools.sml, scrtools.sml ...
201 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
202 \item Test.thy: met_test_sqrt2: deleted?!
204 \item Applicable.applicable_in --> Applicable.tactic_at
206 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
208 \item TermC.vars_of replace by vars (recognises numerals)
213 subsection \<open>Simple but laborous\<close>
218 \item rename field scr in meth
220 \item Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx, too*)
222 \item check match between args of partial_function and model-pattern of meth;
223 provide error message.
225 \item automatically extrac rls from program-code
226 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
232 \item drop "init_form" and use "Take" in programs (start with latter!)
234 \item deprive Check_elementwise, but keep it for Minisubpl
235 (which checks for Check_Postcond separated by another tactic)
236 This seems a prerequisite for appropriate handling of contexts at Check_Postcond.
240 subsection \<open>Questionable\<close>
243 \item finish output of trace_script with Check_Postcond (useful for SubProblem)
244 \item unify in signature LANGUAGE_TOOLS =\\
245 val pblterm: Rule.domID -> Celem.pblID -> term vvv vvv\\
246 val subpbl: string -> string list -> term unify with ^^^
248 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
249 Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
250 If Telem.safe is kept, consider merge with CTbasic.ostate
252 \item remove find_next_step from solve Apply_Method';
253 this enforces Pos.at_first_tactic, which should be dropped, too.
258 section \<open>Major reforms\<close>
261 subsection \<open>Exception Size raised\<close>
263 During update Isabelle2018 --> Isabelle2019 we noticed, that
264 "isabelle build" uses resources more efficiently than "isabelle jedit".
265 The former works, but the latter causes
267 \item "Exception- Size raised"
269 \item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
270 in test/../biegelinie-*.xml.
272 This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
274 Find tools to investigate the Exception, and find ways around it eventually.
276 subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
279 \item there are comments in several signatures
280 \item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted
281 \item src/../Frontend/: signatures missing
285 subsection \<open>overall structure of code\<close>
288 \item try to separate Isac_Knowledge from MathEngine
289 common base: Knowledge_Author / ..??
291 \item ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)
297 subsection \<open>solve, loc_solve_, by_tactic, do_next, ...\<close>
299 unify to calcstate, calcstate', ?Calc.T?
301 \item by_tactic Check_Postcond' needs NO 2.find_next_step
302 solve Check_Postcond' needs, because NO prog_result in Tactic.input
303 and applicable_in cannot get it.
305 \item adopt the same for specification phase
309 subsection \<open>Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/\<close>
313 \item re-organise code for Interpret
317 \item Step_Specify in Specify/step-specify.sml in analogy to Interpret/... TODO
319 \item Step_Specify.check <-- Applicable.applicable_in
320 \item Step_Specify.add <-- Generate.generate1
321 \item Step_Specify.do_next :
322 \item Step_Specify.by_tactic : ? depending on PIDE
323 \item Step_Specify.by_/// = Step_Specify.by_tactic ? depending on PIDE
325 \item Step_Solve in Interpret/step-solve.sml
327 \item Step_Solve.check <-- Applicable.applicable_in
328 inserts all data into Tactic.T available -- not all are available at time of call!
329 \item Step_Solve.add <-- Generate.generate1
330 \item Step_Solve.do_next :
331 \item Step_Solve.by_tactic :
332 \item Step_Solve.by_term : term -> Calc.T -> ...stay as is
334 \item Step in MathEngine/step.sml
336 \item Step.check : Step_Specify.check | Step_Solve.check depending on pos'
337 inserts all data into Tactic.T available -- not all are at time of call!
338 \item Step.add : Step_Specify.add | Step_Solve.add depending on pos'
339 \item Step.do_next : Step_Specify.find_next | Step_Solve.find_next depending on pos'
340 \item Step.by_tactic : Step_Specify.by_tactic | Step_Solve.by_tactic depending on pos'
341 \item : Step_Specify.^^^^^^^^^ | Step_Solve.by_term
343 \item NOTE on mut.rec: Step.do_next calls Step_Solve.do_next + Step_Specify.do_next
344 ^ Math_Engine.nxt_specify_
345 so some restructuring is required.
346 INTERMEDIATE STEP: Step.do_next is still Math_Engine.do_next
352 \item plan separate handling of tactics for Specify/ Interpret/
354 \item already prep. MathEngineBasic/tactic-def.sml + tactic.sml
355 \item new: Specify/spec-tac.sml .. Interpret/solve-tac.sml: generate --> insert, etc
356 \item reduce occurrences of "tactic" in TODO.thy
360 \item ??????????? WHY CAN LI.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
363 MathEngine.solve, ...,
364 ? or identify "layers" like in Isabelle?
368 subsection \<open>Review modelling- + specification-phase\<close>
371 \item first do above "Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/"
373 \item "--- hack for funpack: generalise handling of meths which extend problem items ---"
375 \item see several locations of hack in code
376 \item these locations are NOT sufficient, see
377 test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
378 \item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,
379 this would be according to survey Notes (3) in src/../calchead.sml.
381 \item see "failed trial to generalise handling of meths"98298342fb6d
382 \item abstract specify + nxt_specif to common aux-funs;
383 see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
385 \item type model = itm list ?
386 \item review survey Notes in src/../calchead.sml: they are questionable
387 \item review copy-named, probably two issues commingled
389 \item special handling of "#Find#, because it is not a formal argument of partial_function
390 \item special naming for solutions of equation solving: x_1, x_2, ...
393 \item structure Tactic Specify -?-> Proglang (would require Model., Selem.)
395 \item this has been written in one go:
397 \item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
398 \item reconsider add_field': where is it used for what? Shift into mk_oris
399 \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
400 \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
401 \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
402 (relevant for pre-condition)
403 \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
408 subsection \<open>taci list, type step\<close>
410 taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
411 and probably, because the Kernel interface separated setNextTactic and applyTactic.
412 Both are no good reasons to make code more complicated. For instance Math_Engine.do_next
413 could drop half of the code. So try to use Calc.T only.
416 \item Step* functions should return Calc.T instead of Chead.calcstate'
418 \item states.sml: check, when "length tacis > 1"
419 \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
420 \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
422 \item brute force setting all empty ([], [], ptp) but ptp causes errors -- investigate!
426 subsection \<open>Ctree\<close>
429 \item review get_ctxt, update_ctxt, get_istate, upd_istate, upd_ctxt,
430 <---> update_loc', repl_loc (remove the latter)
431 \item delete field ctxt in PblObj in favour of loc
436 subsection \<open>replace theory/thy by context/ctxt\<close>
440 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
441 special case: Tactic.Refine_Problem
443 \item theory can be retrieved from ctxt by Proof_Context.theory_of
445 \item cleaup the many conversions string -- theory
446 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
447 \item 1. Rewrite.eval_true_, then
448 LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.stac2tac.
450 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
456 subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
459 \item removing from_pblobj_or_detail' causes many strange errors
460 \item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ...
462 \item probably only "normal_form" seems to be needed
463 \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
464 but that seems desirable
465 \item ?how is the relation to reverse-rewriting ???
466 \item "Rfuns" markers in test/../rational
468 \item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
469 rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
470 Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
471 Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
472 \item debug ^^^ related: is there an occurence of Steps with more than 1 element?
474 \item and do_next (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
476 \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
479 subsection \<open>Inverse_Z_Transform.thy\<close>
482 \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
483 ? replace rewriting with substitution ?!?
484 The problem is related to the decision of typing for "d_d" and making bound variables free (while
485 shifting specific handling in equation solving etc. to the meta-logic).
486 \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
487 rewrite-rules; see \ref{new-var-rhs}.
488 \item Reconsider whole problem:
489 input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
492 subsection \<open>Adopt Isabelle's numerals for Isac\<close>
495 \item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
496 and have both representations in parallel for "nat".
501 subsection \<open>Auto_Prog\<close>
504 (1) fun prep_rls creates a Program with too general and wrong types.
505 (2) generated Programs (huge since strings are coded in ASCII) stored in rls drives
506 Build_Thydata towards limits of resources.
508 \item rename Auto_Prog.prep_rls --> Auto_Prog.generate
509 \item Auto_Prog.generate : term -> rls -> (*Program*)term
510 Ctree.current_formula---^^^^
513 \item generate Program on demand in from_pblobj_or_detail'
518 subsection \<open>Redesign thms for equation solver\<close>
520 Existing solver is structured along the WRONG assumption,
521 that Poly.thy must be the LAST thy among all thys involved.
523 Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
525 subsection \<open>Finetunig required for xmldata\<close>
527 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
528 and in kbase html-representation generated from these xmldata.
529 Notes in ~~/xmldata/TODO.txt.
532 section \<open>Hints for further development\<close>
535 subsection \<open>Coding standards & some explanations for math-authors\<close>
536 text \<open>copy from doc/math-eng.tex WN.28.3.03
537 WN071228 extended\<close>
539 subsubsection \<open>Identifiers\<close>
540 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
541 not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
542 reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
543 problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
544 However, all the cases (1)..(4) require different typing for one and the same
545 identifier {\tt probe} which is impossible, and actually leads to strange errors
546 (for instance (1) is used as string, except in a script addressing a Subproblem).
548 These are the preliminary rules for naming identifiers>
550 \item [elements of a key] into the hierarchy of problems or methods must not contain
551 capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
552 \item [descriptions in problem-patterns] must contain at least 1 capital letter and
553 must not contain underscores, e.g. {\tt Probe, forPolynomials}.
554 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
555 beware of conflicts~!
556 \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
560 %WN071228 extended\<close>
562 subsubsection \<open>Rule sets\<close>
563 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
564 where it can be viewed using the knowledge browsers.
566 There are rulesets visible to the student, and there are rulesets visible (in general) only for
567 math authors. There are also rulesets which {\em must} exist for {\em each} theory;
568 these contain the identifier of the respective theory (including all capital letters)
569 as indicated by {\it Thy} below.
572 \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
573 normalform for all terms which can be expressed by the definitions of the respective theory
574 (and the respective parents).
575 \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
576 which can be expressed by the definitions of the respective theory (and the respective parents)
577 such, that the rewrites can be presented to the student.
578 \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
579 numerical constants only (i.e. all terms which can be expressed by the definitions of
580 the respective theory and the respective parent theories). In particular, this ruleset includes
581 evaluating in/equalities with numerical constants only.
582 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
583 are logically equivalent, where the latter often add to the assumptions
584 (e.g. in Check_elementwise).
587 The above rulesets are all visible to the user, and also may be input;
588 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
589 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
590 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
591 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
598 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
601 subsection \<open>get proof-state\<close>
603 Re: [isabelle] Programatically get "this"
604 ----------------------------------------------------
605 So here is my (Makarius') version of your initial example, following these principles:
611 val ctxt = @{context};
614 Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN);
615 val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
620 subsection \<open>write Specification to jEdit\<close>
622 Re: [isabelle] Printing terms with type annotations
623 ----------------------------------------------------
624 On 06/02/2019 17:52, Moa Johansson wrote:
626 > I’m writing some code that should create a snippet of Isar script.
628 This is how Sledgehammer approximates this:
630 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
632 (The module name already shows that the proper terminology is "Isar
633 proof" (or "Isar proof text"). Proof scripts are a thing from the past,
634 before Isar. You can emulate old-style proof scripts via a sequence of
635 'apply' commands, but this is improper Isar.)
637 Note that there is no standard function in Isabelle/Pure, because the
638 problem to print just the right amount of type information is very
639 complex and not fully solved. One day, after 1 or 2 rounds of
640 refinements over the above approach, it might become generally available.
642 subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
644 isabelle update -u path_cartouches
645 isabelle update -u inner_syntax_cartouches
647 section \<open>Questions to Isabelle experts\<close>
650 \item what is the actual replacement of "hg log --follow" ?
652 \item how HANDLE these exceptions, e.g.:
653 Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
656 Failed to parse term"
658 \item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"
659 e.g. in test/Interpret/lucas-interpreter.sml
665 section \<open>For copy & paste\<close>
683 subsection \<open>xxx\<close>
684 subsubsection \<open>xxx\<close>