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"
9 section \<open>TODOs from current changesets\<close>
11 Shift more complicated issues from the next subsection to the next but one!
13 subsection \<open>Current changeset\<close>
21 \item rm test/..--- check Scripts ---
23 \item reformat + rename "fun eval_leaf"+"fun get_stac"
25 ?consistency with subst term?
26 \item Tactic.Rewrite*': drop "bool"
28 \item exception PROG analogous to TERM
32 \item Prog_Tac: fun get_stac takes both Prog_Tac + Program --- wait for separate Taciical
33 then shift into common descendant
34 rename get_stac --> ?ptac?
38 \item separate code required in both, ProgLang & Interpret
40 \item /-------------------------------------------------------------------
41 \item check occurences of KEStore_Elems.add_rlss [("list_rls",
42 \item rename list_rls accordingly
43 \item ------------------------------------------------------------------/
45 \item lucas-interpreter.sml ----- vvvvvvvvv etc.
46 val (p'',_,_,pt'') = Generate.generate1 @ {theory} tac' (Istate.Pstate is, ctxt) (po', p_) pt
50 \item signature LIBRARY_C
51 \item Program.thy (*=========== record these ^^^ in 'tacs' in program.ML =========*)
52 \item sig/struc ..elems --> elem
58 \item distribute test/../scrtools.sml
61 \item simplify calls of scan_dn1, scan_dn2 etc
62 \item open Istate in LucinNEW
65 subsection \<open>Differences between code and paper\<close>
75 subsection \<open>Postponed from current changeset\<close>
79 \item re-organise code for Interpret
82 datatype step_result = Step of Ctree.state | Step_Failed of msg (*TODO: exn hierarchy*)
83 not other returns, because Step_Solve.add immediately after lucin, so all in Ctree.state.
85 \item Step_Specify in Specify/step-specify.sml in analogy to Interpret/... TODO
87 \item Step_Specify.check <-- Applicable.applicable_in
88 inserts all data into Tactic.T available -- not all are at time of call!
89 \item Step_Specify.add <-- Generate.generate1
90 \item Step_Specify.by_tactic : Tactic.input -> Ctree.state -> step_result
91 \item Step_Specify.by_formula: ?term? -> Ctree.state -> step_result
92 \item Step_Specify.find_next : Ctree.state -> step_result
94 \item Step_Solve in Interpret/step-solve.sml
96 \item Step_Solve.check <-- Applicable.applicable_in
97 inserts all data into Tactic.T available -- not all are at time of call!
98 \item Step_Solve.add <-- Generate.generate1
99 \item Step_Solve.by_tactic : Tactic.input -> Ctree.state -> step_result
100 ^^^^LucinNEW,begin_end_prog
101 \item Step_Solve.by_formula : term -> Ctree.state -> step_result
102 \item Step_Solve.find_next : Ctree.state -> step_result
103 ^^^^LucinNEW,do_solve_step; Apply_Method ever used???
105 \item Step in MathEngine/step.sml
107 \item Step.check : Step_Specify.check | Step_Solve.check depending on pos'
108 inserts all data into Tactic.T available -- not all are at time of call!
109 \item Step.add : Step_Specify.add | Step_Solve.add depending on pos'
110 \item Step.by_tactic : Step_Specify.by_tactic | Step_Solve.by_tactic depending on pos'
111 \item Step.by_formula: Step_Specify.by_formula | Step_Solve.by_formula depending on pos'
112 \item Step.find_next : Step_Specify.find_next | Step_Solve.find_next depending on pos'
116 \item MathEngBasic/calculation.sml
118 \item rename Calc --> Calc_
119 \item ? type Calc.T = CTree.state ?
120 \item Calc.add_step <-- Step_Specify.add + Step_Solve.add <-- Generate.generate*
127 \item decompose do_solve_step, begin_end_prog: mutual recursion only avoids multiple generate1
128 ! ^^^ in find_next_tactic --- ? ? ? in locate_input_tactic ?
130 \item Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
132 \item NEW structure Step.applicable Step.add
133 ^applicable_in ^generate1
135 \item revise Pstate {or, ...}; strange occurrence in program without Tactical.Or documented here
137 \item shift tests into NEW model.sml (upd, upds_envv, ..)
143 \item Applicable.applicable_in --> Step.applicable
144 \item Generate.generate1 --> Step.add ?-->? Calculation.add_step
147 \item Calculation ("Calc" is occupied ?!?) ?^^^? Calculation
149 \item Ctree.state ?-->? Calculation.T
150 \item Chead.calcstate --> Calculation.prestate
151 \item Chead.calcstate' --> Calculation.poststate
152 \item e_calcstate, e_calcstate' -"-
157 \item clarify handling of contexts
159 \item Check_Elementwise "Assumptions": prerequisite for ^^goal
160 rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
161 rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
163 \item cleanup fun me:
164 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
165 | me*) (_, tac) p _(*NEW remove*) pt =
166 + -------------------------^^^^^^
168 \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
169 \item rm ctxt from Subproblem' (is separated in associate!))
170 \item check Tactic.Subproblem': are 2 terms required?
172 \item Test_Some.--- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts --
173 --: wait for deleting Check_Elementwise Assumptions
175 \item lucas-intrpreter.scan_dn1: Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
178 \item reconsider "fun eval_leaf"
179 CAUTION: (1) currying with @@ requires 2 patterns for each tactic
180 (2) the non-curried version must return NONE for a
181 (3) non-matching patterns become an Program.Expr by fall-through.
182 (a, (*in these cases we hope, that a = SOME _*) --> exn ?PROGRAM?
183 rename ?ptac?, prog_tac
185 \item complete mstools.sml (* survey on handling contexts:
187 \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur.
188 \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper
190 \item check in states: length ?? > 1 with tracing these cases
193 \item Lucin.Ass_Weak etc \<longrightarrow> NEW structutre ? LItool ?
197 \item datatype L,R,D --> Istate
201 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
203 \item change Lucin.interpret_leaf "locate" "Isac_Knowledge" sr E a v t
204 to Lucin.interpret_leaf "locate" ctxt ( pstate ) !!srls in pstate!!^^
205 and redesign interpret_leaf .. eval_leaf .. associate
206 to Tactic.from_code :
207 + keep ! trace_script
208 + scrstate2str --> pstate2str
210 \item after review of Rrls, detail ?-->? istate
211 \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)
213 \item push srls into pstate
214 \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls)
226 \item trace_script: replace ' by " in writeln
228 \item librarys.ml --> libraryC.sml + text from termC.sml
235 \item pull update of Ctree.state out of 2 Lucin funs (locate_input_formula is different))
237 \item 1. check if Ctree.state can be updated OUTSIDE determine_next_step
238 \item 2. fun locate_input_tactic: pull generate1 out (because it stores ctxt also in cstate)
242 \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
243 DONE for find_next_tactic by Tactic.insert_assumptions m' ctxt
245 \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
246 \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
247 \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
250 \item DO DELETIONS AFTER analogous concentrations in find_next_tactic
253 \item ? what is the difference headline <--> cascmd in
254 Subproblem' (spec, oris, headline, fmz_, context, cascmd)
256 \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
257 \item extract common code from associate.. stac2tac_
261 section \<open>Separated tasks\<close>
264 subsection \<open>Simple\<close>
268 \item check location of files:
269 test/Tools/isac/Interpret/ptyps.thy
270 test/Tools/isac/Specify.ptyps.sml
272 \item check occurences of Atools in src/ test/
274 \item drop drop_questionmarks_
276 \item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _)
277 \item rename Base_Tool.thy <--- Base_Tool
279 \item test/.. tools.sml, atools.sml, scrtools.sml ...
281 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
282 \item Test.thy: met_test_sqrt2: deleted?!
284 \item Applicable.applicable_in --> Applicable.tactic_at
286 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
288 \item TermC.vars_of replace by vars (recognises numerals)
293 subsection \<open>Simple but laborous\<close>
298 \item rename field scr in meth
300 \item Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx, too*)
302 \item check match between args of partial_function and model-pattern of meth;
303 provide error message.
305 \item automatically extrac rls from program-code
306 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
312 \item drop "init_form" and use "Take" in programs (start with latter!)
314 \item deprive Check_elementwise, but keep it for Minisubpl
315 (which checks for Check_Postcond separated by another tactic)
316 This seems a prerequisite for appropriate handling of contexts at Check_Postcond.
320 subsection \<open>Questionable\<close>
323 \item finish output of trace_script with Check_Postcond (useful for SubProblem)
324 \item unify in signature LANGUAGE_TOOLS =\\
325 val pblterm: Rule.domID -> Celem.pblID -> term vvv vvv\\
326 val subpbl: string -> string list -> term unify with ^^^
328 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
329 Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
330 If Telem.safe is kept, consider merge with CTbasic.ostate
332 \item remove find_next_tactic from solve Apply_Method';
333 this enforces Pos.at_first_tactic, which should be dropped, too.
338 section \<open>Complex, related to --> other tasks\<close>
341 subsection \<open>Exception Size raised\<close>
343 During update Isabelle2018 --> Isabelle2019 we noticed, that
344 "isabelle build" uses resources more efficiently than "isabelle jedit".
345 The former works, but the latter causes
347 \item "Exception- Size raised"
349 \item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
350 in test/../biegelinie-*.xml.
352 This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
354 Find tools to investigate the Exception, and find ways around it eventually.
356 subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
359 \item there are comments in several signatures
360 \item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted
361 \item src/../Frontend/: signatures missing
365 subsection \<open>overall structure of code\<close>
368 \item try to separate Isac_Knowledge from MathEngine
369 common base: Knowledge_Author / ..??
371 \item ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)
377 subsection \<open>solve, loc_solve_, begin_end_prog, do_solve_step, ...\<close>
379 unify to calcstate, calcstate', ?Ctree.state?
381 \item begin_end_prog Check_Postcond' needs NO 2.find_next_tactic
382 solve Check_Postcond' needs, because NO prog_result in Tactic.input
383 and applicable_in cannot get it.
385 \item adopt the same for specification phase
389 subsection \<open>Review modelling- + specification-phase\<close>
392 \item "--- hack for funpack: generalise handling of meths which extend problem items ---"
394 \item see several locations of hack in code
395 \item these locations are NOT sufficient, see
396 test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
397 \item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,
398 this would be according to survey Notes (3) in src/../calchead.sml.
400 \item see "failed trial to generalise handling of meths"98298342fb6d
401 \item abstract specify + nxt_specif to common aux-funs;
402 see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
404 \item type model = itm list ?
405 \item review survey Notes in src/../calchead.sml: they are questionable
406 \item review copy-named, probably two issues commingled
408 \item special handling of "#Find#, because it is not a formal argument of partial_function
409 \item special naming for solutions of equation solving: x_1, x_2, ...
412 \item structure Tactic Specify -?-> Proglang (would require Model., Selem.)
414 \item this has been written in one go:
416 \item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
417 \item reconsider add_field': where is it used for what? Shift into mk_oris
418 \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
419 \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
420 \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
421 (relevant for pre-condition)
422 \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
427 subsection \<open>taci list, type step\<close>
430 \item states.sml: check, when "length tacis > 1"
431 \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
432 \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
436 subsection \<open>Ctree\<close>
439 \item review get_ctxt, update_ctxt, get_istate, upd_istate, upd_ctxt,
440 <---> update_loc', repl_loc (remove the latter)
441 \item delete field ctxt in PblObj in favour of loc
446 subsection \<open>replace theory/thy by context/ctxt\<close>
450 \item ??? can theory be retrieved from ctxt --- YES --- see Proof_Context.theory_of below
452 \item cleaup the many conversions string -- theory
453 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
454 \item 1. Rewrite.eval_true_, then
455 Lucin.interpret_leaf, Rewrite.eval_prog_expr, Generate.generate1, Lucin.stac2tac.
457 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
461 \item !!! Tactic.Refine_Problem uses Pattern.match, which takes a theory, NOT a ctxt
462 but there is Proof_Context.theory_of !!!
465 subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
468 \item removing from_pblobj_or_detail' causes many strange errors
469 \item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ...
471 \item probably only "normal_form" seems to be needed
472 \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
473 but that seems desirable
474 \item ?how is the relation to reverse-rewriting ???
475 \item "Rfuns" markers in test/../rational
477 \item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
478 rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
479 Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
480 Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
481 \item debug ^^^ related: is there an occurence of Steps with more than 1 element?
483 \item and do_solve_step (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
485 \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
488 subsection \<open>Inverse_Z_Transform.thy\<close>
491 \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
492 ? replace rewriting with substitution ?!?
493 The problem is related to the decision of typing for "d_d" and making bound variables free (while
494 shifting specific handling in equation solving etc. to the meta-logic).
495 \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
496 rewrite-rules; see \ref{new-var-rhs}.
497 \item Reconsider whole problem:
498 input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
501 subsection \<open>Adopt Isabelle's numerals for Isac\<close>
504 \item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
505 and have both representations in parallel for "nat".
510 subsection \<open>Auto_Prog\<close>
513 (1) fun prep_rls creates a Program with too general and wrong types.
514 (2) generated Programs (huge since strings are coded in ASCII) stored in rls drives
515 Build_Thydata towards limits of resources.
517 \item rename Auto_Prog.prep_rls --> Auto_Prog.generate
518 \item Auto_Prog.generate : term -> rls -> (*Program*)term
519 Ctree.current_formula---^^^^
522 \item generate Program on demand in from_pblobj_or_detail'
527 subsection \<open>Redesign specify-phase\<close>
531 \item Separate Specify/ Interpret/ MathEngine/
532 MathEngine.solve, ...,
533 ? or identify "layers" like in Isabelle?
538 subsection \<open>Redesign thms for equation solver\<close>
540 Existing solver is structured along the WRONG assumption,
541 that Poly.thy must be the LAST thy among all thys involved.
543 Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
545 subsection \<open>Finetunig required for xmldata\<close>
547 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
548 and in kbase html-representation generated from these xmldata.
549 Notes in ~~/xmldata/TODO.txt.
552 section \<open>Hints for further development\<close>
555 subsection \<open>Coding standards & some explanations for math-authors\<close>
556 text \<open>copy from doc/math-eng.tex WN.28.3.03
557 WN071228 extended\<close>
559 subsubsection \<open>Identifiers\<close>
560 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
561 not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
562 reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
563 problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
564 However, all the cases (1)..(4) require different typing for one and the same
565 identifier {\tt probe} which is impossible, and actually leads to strange errors
566 (for instance (1) is used as string, except in a script addressing a Subproblem).
568 These are the preliminary rules for naming identifiers>
570 \item [elements of a key] into the hierarchy of problems or methods must not contain
571 capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
572 \item [descriptions in problem-patterns] must contain at least 1 capital letter and
573 must not contain underscores, e.g. {\tt Probe, forPolynomials}.
574 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
575 beware of conflicts~!
576 \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
580 %WN071228 extended\<close>
582 subsubsection \<open>Rule sets\<close>
583 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
584 where it can be viewed using the knowledge browsers.
586 There are rulesets visible to the student, and there are rulesets visible (in general) only for
587 math authors. There are also rulesets which {\em must} exist for {\em each} theory;
588 these contain the identifier of the respective theory (including all capital letters)
589 as indicated by {\it Thy} below.
592 \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
593 normalform for all terms which can be expressed by the definitions of the respective theory
594 (and the respective parents).
595 \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
596 which can be expressed by the definitions of the respective theory (and the respective parents)
597 such, that the rewrites can be presented to the student.
598 \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
599 numerical constants only (i.e. all terms which can be expressed by the definitions of
600 the respective theory and the respective parent theories). In particular, this ruleset includes
601 evaluating in/equalities with numerical constants only.
602 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
603 are logically equivalent, where the latter often add to the assumptions
604 (e.g. in Check_elementwise).
607 The above rulesets are all visible to the user, and also may be input;
608 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
609 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
610 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
611 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
618 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
621 subsection \<open>get proof-state\<close>
623 Re: [isabelle] Programatically get "this"
624 ----------------------------------------------------
625 So here is my (Makarius') version of your initial example, following these principles:
631 val ctxt = @{context};
634 Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name
636 val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
641 subsection \<open>write Specification to jEdit\<close>
643 Re: [isabelle] Printing terms with type annotations
644 ----------------------------------------------------
645 On 06/02/2019 17:52, Moa Johansson wrote:
647 > I’m writing some code that should create a snippet of Isar script.
649 This is how Sledgehammer approximates this:
651 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
653 (The module name already shows that the proper terminology is "Isar
654 proof" (or "Isar proof text"). Proof scripts are a thing from the past,
655 before Isar. You can emulate old-style proof scripts via a sequence of
656 'apply' commands, but this is improper Isar.)
658 Note that there is no standard function in Isabelle/Pure, because the
659 problem to print just the right amount of type information is very
660 complex and not fully solved. One day, after 1 or 2 rounds of
661 refinements over the above approach, it might become generally available.
663 subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
665 isabelle update -u path_cartouches
666 isabelle update -u inner_syntax_cartouches
668 section \<open>Questions to Isabelle experts\<close>
671 \item what is the actual replacement of "hg log --follow" ?
673 \item how HANDLE these exceptions, e.g.:
674 Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
677 Failed to parse term"
679 \item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"
680 e.g. in test/Interpret/lucas-interpreter.sml
686 section \<open>For copy & paste\<close>
703 subsection \<open>xxx\<close>
704 subsubsection \<open>xxx\<close>