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>
18 rename Env.upd_env -> Env.update & Co.
20 \item finalise changes in istate, scan_dn2, scan_dn1 & Co
22 \item remove remaining src/ which opens structure "(E," "(_,"
24 \item cleanup arguments of scan_dn2, scan_dn1 & Co
25 + Test_Isac/../lucas-interpreter.sml, Minisubpbl/
26 \item draw changes into remaining tests
31 \item fun handle_leaf: trace_prog .. separate message
33 \item rm test/..--- check Scripts ---
35 \item reformat + rename "fun subst_stacexpr"+"fun get_stac"
37 ?consistency with subst term?
38 \item Tactic.Rewrite*: drop "bool"
40 \item Prog_Tac.contain + Tactical.contain using contains_Const
41 \item exception PROG analogous to TERM
45 \item Prog_Tac: fun get_stac takes both Prog_Tac + Program --- wait for separate Taciical
46 then shift into common descendant
47 rename get_stac --> ?ptac?
51 \item separate code required in both, ProgLang & Interpret
53 \item /-------------------------------------------------------------------
54 \item check occurences of KEStore_Elems.add_rlss [("list_rls",
55 \item rename list_rls accordingly
56 \item ------------------------------------------------------------------/
58 \item lucas-interpreter.sml ----- vvvvvvvvv etc.
59 val (p'',_,_,pt'') = Generate.generate1 @ {theory} tac' (Istate.Pstate is, ctxt) (po', p_) pt
63 \item signature LIBRARY_C
64 \item Program.thy (*=========== record these ^^^ in 'tacs' in program.ML =========*)
65 \item sig/struc ..elems --> elem
71 \item distribute test/../scrtools.sml
74 \item simplify calls of scan_dn1, scan_dn2 etc
75 \item open Istate in LucinNEW
78 subsection \<open>Differences between code and paper\<close>
81 Rewrite'_Inst:: "[(char list * real) list, char list, bool, 'a] => 'a"
82 ->Rewrite'_Inst:: "[(char list * 'a) list, char list, 'a] => 'a"
84 Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10)
85 ->Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10)
86 + If :: "[bool, 'a => 'a, 'a => 'a, 'a] => 'a"
88 subsection \<open>Postponed from current changeset\<close>
93 \item shift tests into NEW model.sml (upd, upds_envv, ..)
97 \item clarify handling of contexts
99 \item Check_Elementwise "Assumptions": prerequisite for ^^goal
100 rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
101 rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
103 \item cleanup fun me:
104 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
105 | me*) (_, tac) p _(*NEW remove*) pt =
106 + -------------------------^^^^^^
108 \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
109 \item rm ctxt from Subproblem' (is separated in associate!))
110 \item check Tactic.Subproblem': are 2 terms required?
112 \item Test_Some.--- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts --
113 --: wait for deleting Check_Elementwise Assumptions
115 \item lucas-intrpreter.scan_dn1: Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
118 \item reconsider "fun subst_stacexpr"
119 CAUTION: (1) currying with @@ requires 2 patterns for each tactic
120 (2) the non-curried version must return NONE for a
121 (3) non-matching patterns become an Celem.Expr by fall-through.
122 (a, (*in these cases we hope, that a = SOME _*) --> exn ?PROGRAM?
123 rename ?ptac?, prog_tac
125 \item complete mstools.sml (* survey on handling contexts:
127 \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur.
128 \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper
130 \item check in states: length ?? > 1 with tracing these cases
133 \item Lucin.Ass_Weak etc \<longrightarrow> NEW structutre ? LItool ?
137 \item datatype L,R,D --> Istate
141 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
143 \item change Lucin.handle_leaf "locate" "Isac_Knowledge" sr E a v t
144 to Lucin.handle_leaf "locate" ctxt ( pstate ) !!srls in pstate!!^^
145 and redesign handle_leaf .. subst_stacexpr .. associate
146 to Tactic.from_code :
147 + keep ! trace_script
148 + scrstate2str --> pstate2str
150 \item after review of Rrls, detail ?-->? istate
151 \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)
153 \item push srls into pstate
154 \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls)
166 \item trace_script: replace ' by " in writeln
168 \item librarys.ml --> libraryC.sml + text from termC.sml
175 \item pull update of Ctree.state out of 2 Lucin funs (locate_input_formula is different))
177 \item 1. check if Ctree.state can be updated OUTSIDE determine_next_step
178 \item 2. fun locate_input_tactic: pull generate1 out (because it stores ctxt also in cstate)
182 \item concentrate "insert_assumptions" in "associate" ?for determine_next_tactic ?where?
184 \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
185 \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
186 \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
189 \item DO DELETIONS AFTER analogous concentrations in determine_next_tactic
192 \item ? what is the difference headline <--> cascmd in
193 Subproblem' (spec, oris, headline, fmz_, context, cascmd)
195 \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
196 \item extract common code from associate.. stac2tac_
200 section \<open>Separated tasks\<close>
203 subsection \<open>Simple\<close>
207 \item check location of files:
208 test/Tools/isac/Interpret/ptyps.thy
209 test/Tools/isac/Specify.ptyps.sml
211 \item check occurences of Atools in src/ test/
213 \item drop drop_questionmarks_
215 \item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _)
216 \item rename Base_Tool.thy <--- Base_Tool
218 \item test/.. tools.sml, atools.sml, scrtools.sml ...
220 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
221 \item Test.thy: met_test_sqrt2: deleted?!
223 \item Applicable.applicable_in --> Applicable.tactic_at
225 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
227 \item TermC.vars_of replace by vars (recognises numerals)
232 subsection \<open>Simple but laborous\<close>
237 \item rename field scr in meth
239 \item Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx, too*)
241 \item check match between args of partial_function and model-pattern of meth;
242 provide error message.
244 \item automatically extrac rls from program-code
245 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
251 \item drop "init_form" and use "Take" in programs (start with latter!)
253 \item deprive Check_elementwise, but keep it for Minisubpl
254 (which checks for Check_Postcond separated by another tactic)
255 This seems a prerequisite for appropriate handling of contexts at Check_Postcond.
259 subsection \<open>Questionable\<close>
262 \item finish output of trace_script with Check_Postcond (useful for SubProblem)
263 \item unify in signature LANGUAGE_TOOLS =\\
264 val pblterm: Rule.domID -> Celem.pblID -> term vvv vvv\\
265 val subpbl: string -> string list -> term unify with ^^^
267 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
268 Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
269 If Telem.safe is kept, consider merge with CTbasic.ostate
274 section \<open>Complex, related to --> other tasks\<close>
277 subsection \<open>Exception Size raised\<close>
279 During update Isabelle2018 --> Isabelle2019 we noticed, that
280 "isabelle build" uses resources more efficiently than "isabelle jedit".
281 The former works, but the latter causes
283 \item "Exception- Size raised"
285 \item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
286 in test/../biegelinie-*.xml.
288 This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
290 Find tools to investigate the Exception, and find ways around it eventually.
292 subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
295 \item there are comments in several signatures
296 \item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted
297 \item src/../Frontend/: signatures missing
301 subsection \<open>overall structure of code\<close>
304 \item try to separate Isac_Knowledge from MathEngine
305 common base: Knowledge_Author / ..??
307 \item ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)
313 subsection \<open>solve, loc_solve_, ...\<close>
315 unify to calcstate, calcstate'
317 \item ?delete Check_Postcond' in begin_end_prog (already done in solve?)
318 in case both are needed, unify !
320 \item ? rename begin_end_prog -> check_switch_prog
321 \item adopt the same for specification phase
325 subsection \<open>Review modelling- + specification-phase\<close>
328 \item "--- hack for funpack: generalise handling of meths which extend problem items ---"
330 \item see several locations of hack in code
331 \item these locations are NOT sufficient, see
332 test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
333 \item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,
334 this would be according to survey Notes (3) in src/../calchead.sml.
336 \item see "failed trial to generalise handling of meths"98298342fb6d
337 \item abstract specify + nxt_specif to common aux-funs;
338 see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
340 \item type model = itm list ?
341 \item review survey Notes in src/../calchead.sml: they are questionable
342 \item review copy-named, probably two issues commingled
344 \item special handling of "#Find#, because it is not a formal argument of partial_function
345 \item special naming for solutions of equation solving: x_1, x_2, ...
348 \item structure Tactic Specify -?-> Proglang (would require Model., Selem.)
350 \item this has been written in one go:
352 \item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
353 \item reconsider add_field': where is it used for what? Shift into mk_oris
354 \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
355 \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
356 \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
357 (relevant for pre-condition)
358 \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
363 subsection \<open>taci list, type step\<close>
366 \item states.sml: check, when "length tacis > 1"
367 \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
368 \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
372 subsection \<open>Ctree\<close>
375 \item review get_ctxt, update_ctxt, get_istate, upd_istate, upd_ctxt,
376 <---> update_loc', repl_loc (remove the latter)
377 \item delete field ctxt in PblObj in favour of loc
382 subsection \<open>replace theory/thy by context/ctxt\<close>
386 \item ??? can theory be retrieved from ctxt --- YES --- see Proof_Context.theory_of below
388 \item cleaup the many conversions string -- theory
389 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
390 \item 1. Rewrite.eval_true_, then
391 Lucin.handle_leaf, Rewrite.eval_listexpr_, Generate.generate1, Lucin.stac2tac.
393 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
397 \item !!! Tactic.Refine_Problem uses Pattern.match, which takes a theory, NOT a ctxt
398 but there is Proof_Context.theory_of !!!
401 subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
404 \item removing from_pblobj_or_detail' causes many strange errors
405 \item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ...
407 \item probably only "normal_form" seems to be needed
408 \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
409 but that seems desirable
410 \item ?how is the relation to reverse-rewriting ???
411 \item "Rfuns" markers in test/../rational
413 \item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
414 rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
415 Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
416 Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
417 \item debug ^^^ related: is there an occurence of Steps with more than 1 element?
419 \item and do_solve_step (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
421 \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
424 subsection \<open>Inverse_Z_Transform.thy\<close>
427 \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
428 ? replace rewriting with substitution ?!?
429 The problem is related to the decision of typing for "d_d" and making bound variables free (while
430 shifting specific handling in equation solving etc. to the meta-logic).
431 \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
432 rewrite-rules; see \ref{new-var-rhs}.
433 \item Reconsider whole problem:
434 input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
437 subsection \<open>Adopt Isabelle's numerals for Isac\<close>
440 \item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
441 and have both representations in parallel for "nat".
446 subsection \<open>Auto_Prog\<close>
449 (1) fun prep_rls creates a Program with too general and wrong types.
450 (2) generated Programs (huge since strings are coded in ASCII) stored in rls drives
451 Build_Thydata towards limits of resources.
453 \item rename Auto_Prog.prep_rls --> Auto_Prog.generate
454 \item Auto_Prog.generate : term -> rls -> (*Program*)term
455 Ctree.current_formula---^^^^
458 \item generate Program on demand in from_pblobj_or_detail'
463 subsection \<open>Redesign specify-phase\<close>
467 \item Separate Specify/ Interpret/ MathEngine/
468 MathEngine.solve, ...,
469 ? or identify "layers" like in Isabelle?
474 subsection \<open>Redesign thms for equation solver\<close>
476 Existing solver is structured along the WRONG assumption,
477 that Poly.thy must be the LAST thy among all thys involved.
479 Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
481 subsection \<open>Finetunig required for xmldata\<close>
483 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
484 and in kbase html-representation generated from these xmldata.
485 Notes in ~~/xmldata/TODO.txt.
488 section \<open>Hints for further development\<close>
491 subsection \<open>Coding standards & some explanations for math-authors\<close>
492 text \<open>copy from doc/math-eng.tex WN.28.3.03
493 WN071228 extended\<close>
495 subsubsection \<open>Identifiers\<close>
496 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
497 not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
498 reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
499 problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
500 However, all the cases (1)..(4) require different typing for one and the same
501 identifier {\tt probe} which is impossible, and actually leads to strange errors
502 (for instance (1) is used as string, except in a script addressing a Subproblem).
504 These are the preliminary rules for naming identifiers>
506 \item [elements of a key] into the hierarchy of problems or methods must not contain
507 capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
508 \item [descriptions in problem-patterns] must contain at least 1 capital letter and
509 must not contain underscores, e.g. {\tt Probe, forPolynomials}.
510 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
511 beware of conflicts~!
512 \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
516 %WN071228 extended\<close>
518 subsubsection \<open>Rule sets\<close>
519 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
520 where it can be viewed using the knowledge browsers.
522 There are rulesets visible to the student, and there are rulesets visible (in general) only for
523 math authors. There are also rulesets which {\em must} exist for {\em each} theory;
524 these contain the identifier of the respective theory (including all capital letters)
525 as indicated by {\it Thy} below.
528 \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
529 normalform for all terms which can be expressed by the definitions of the respective theory
530 (and the respective parents).
531 \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
532 which can be expressed by the definitions of the respective theory (and the respective parents)
533 such, that the rewrites can be presented to the student.
534 \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
535 numerical constants only (i.e. all terms which can be expressed by the definitions of
536 the respective theory and the respective parent theories). In particular, this ruleset includes
537 evaluating in/equalities with numerical constants only.
538 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
539 are logically equivalent, where the latter often add to the assumptions
540 (e.g. in Check_elementwise).
543 The above rulesets are all visible to the user, and also may be input;
544 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
545 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
546 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
547 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
554 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
557 subsection \<open>get proof-state\<close>
559 Re: [isabelle] Programatically get "this"
560 ----------------------------------------------------
561 So here is my (Makarius') version of your initial example, following these principles:
567 val ctxt = @{context};
570 Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name
572 val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
577 subsection \<open>write Specification to jEdit\<close>
579 Re: [isabelle] Printing terms with type annotations
580 ----------------------------------------------------
581 On 06/02/2019 17:52, Moa Johansson wrote:
583 > I’m writing some code that should create a snippet of Isar script.
585 This is how Sledgehammer approximates this:
587 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
589 (The module name already shows that the proper terminology is "Isar
590 proof" (or "Isar proof text"). Proof scripts are a thing from the past,
591 before Isar. You can emulate old-style proof scripts via a sequence of
592 'apply' commands, but this is improper Isar.)
594 Note that there is no standard function in Isabelle/Pure, because the
595 problem to print just the right amount of type information is very
596 complex and not fully solved. One day, after 1 or 2 rounds of
597 refinements over the above approach, it might become generally available.
599 subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
601 isabelle update -u path_cartouches
602 isabelle update -u inner_syntax_cartouches
604 section \<open>Questions to Isabelle experts\<close>
607 \item what is the actual replacement of "hg log --follow" ?
609 \item how HANDLE these exceptions, e.g.:
610 Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
613 Failed to parse term"
621 section \<open>For copy & paste\<close>
638 subsection \<open>xxx\<close>
639 subsubsection \<open>xxx\<close>