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>
26 (*/------- to -------\*)
27 (*\------- to -------/*)
29 \item ML_file "rule-set.sml" KEStore -> MathEngBasic (=ThmC, Rewrite)
30 probably first review calcelems.sml
41 subsection \<open>Postponed from current changeset\<close>
43 \item "TODO CLEANUP Thm"
45 Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
46 thmID : type for data from user input + program
47 thmDeriv : type for thy_hierarchy ONLY
48 obsolete types : thm' (SEE "ad thm'"), thm''.
49 revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
50 activate : ThmC.cut_id'
53 \item use "Exec_Def" for renaming identifiers
59 \item LI.do_next (*TODO RM..*) ???
60 \item generate.sml: RM datatype edit TOGETHER WITH datatype inout
61 \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ
62 \item get_ctxt_LI should replace get_ctxt
63 \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
64 \item rename Base_Tool.thy <--- Base_Tools
65 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
66 \item rename field scr in meth
67 \item DEL double code: nxt_specify_init_calc IN specify.sml + step-specify.sml
75 \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}
76 there it is Free ("Subproblem", "char list \<times> ..
77 instead of Const (|???.Subproblem", "char list \<times> ..
78 AND THE STRING REPRESENTATION IS STRANGE:
80 ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation''
84 term2str; (*defined by..*)
85 fun term_to_string''' thy t =
87 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
88 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
90 val t = @{term "aaa + bbb"}
91 val t = @{term "Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation''])"};
93 val sss = Print_Mode.setmp [] (Syntax.string_of_term @{context}) t
95 writeln sss (*.. here perfect: Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation'']) *)
100 \item cleanup fun me:
101 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
102 | me*) (_, tac) p _(*NEW remove*) pt =
103 + -------------------------^^^^^^
104 # see test-code.sml fun me_trace
105 use this also for me, not only for me_ist_ctxt; del. me
106 this requires much updating in all test/*
109 \item generate, generate1: NO thy as arg.
110 Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
111 redesign return value (originally for output by fun me?)
113 \item shift tests into NEW model.sml (upd, upds_envv, ..)
116 \item clarify handling of contexts ctxt ContextC
119 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
121 \item Check_Elementwise "Assumptions": prerequisite for ^^goal
122 rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
123 rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
129 \item complete mstools.sml (* survey on handling contexts:
134 \item librarys.ml --> libraryC.sml + text from termC.sml
141 \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
142 DONE for find_next_step by Tactic.insert_assumptions m' ctxt
144 \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
145 \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
146 \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
149 \item DO DELETIONS AFTER analogous concentrations in find_next_step
152 \item ? what is the difference headline <--> cascmd in
153 Subproblem' (spec, oris, headline, fmz_, context, cascmd)
155 \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
157 \item unify/clarify stac2tac_ |
160 \item extract common code from associate.. stac2tac_xxx
161 \item rename LItool.tac_from_prog -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,
166 \item unify in signature LANGUAGE_TOOLS =\\
167 val pblterm: ThyC.id -> Celem.pblID -> term vvv vvv\\
168 val subpbl: string -> string list -> term unify with ^^^
170 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
171 Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
172 If Telem.safe is kept, consider merge with CTbasic.ostate
174 \item remove find_next_step from solve Apply_Method';
175 this enforces Pos.at_first_tactic, which should be dropped, too.
181 subsection \<open>Postponed --> Major reforms\<close>
185 \item revisit bootstrap Calcelements. rule->calcelems->termC
186 would be nice, but is hard: UnparseC.terms -> TermC.s_to_string
188 \item replace all Ctree.update_* with Ctree.cupdate_problem
190 \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
192 \item exception PROG analogous to TERM
194 \item sig/struc ..elems --> ..elem
196 \item distille CAS-command, CAScmd, etc into a struct
198 \item check location of files:
199 test/Tools/isac/Interpret/ptyps.thy
200 test/Tools/isac/Specify.ptyps.sml
202 \item check occurences of Atools in src/ test/
203 \item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _)
207 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
208 \item Test.thy: met_test_sqrt2: deleted?!
210 \item Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use KEStore.xxx, too*)
212 \item automatically extrac rls from program-code
213 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
215 \item finish output of trace_LI with Check_Postcond (useful for SubProblem)
217 \item replace Rule_Set.empty by Rule_Set.Empty
218 latter is more clear, but replacing ***breaks rewriting over all examples***,
219 e.g. see ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x'
220 in Minisubplb/200-start-method-NEXT_STEP.sml:
221 (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
223 (*+*) Rls {calc = [], erls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =
224 (*+*) ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Erls}:
225 (*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !
226 (*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had
227 (*+*)val Empty = prls (* <---ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x' *)
228 ( *+*)val ["sqroot-test", "univariate", "equation", "test"] = cpI
229 THAT INDICATES, that much rewriting/evaluating JUST WORKED BY CHANCE?!?
240 section \<open>Major reforms\<close>
243 subsection \<open>Exception Size raised\<close>
245 During update Isabelle2018 --> Isabelle2019 we noticed, that
246 "isabelle build" uses resources more efficiently than "isabelle jedit".
247 The former works, but the latter causes
249 \item "Exception- Size raised"
251 \item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
252 in test/../biegelinie-*.xml.
254 This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
256 Find tools to investigate the Exception, and find ways around it eventually.
258 subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
261 \item there are comments in several signatures
262 \item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted
263 \item src/../Frontend/: signatures missing
267 subsection \<open>overall structure of code\<close>
270 \item try to separate Isac_Knowledge from MathEngine
271 common base: Knowledge_Author / ..??
273 \item ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)
279 subsection \<open>Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/\<close>
284 \item re-organise code for Interpret
286 \item Step*: Step_Specify | Step_Solve | Step
288 \item *.check | *.add ARE TOO LATE IN BUILD with Step_Specify | Step_Solve
289 Specify_Step.check | Specify_Step.add <-- Applicable.applicable_in
290 Solve_Step.check | Solve_Step.add <-- Generate.generate1
294 \item Prog_Tac: fun get_first_argument takes both Prog_Tac + Program --- wait for separate Tactical
295 then shift into common descendant
300 \item ??????????? WHY CAN LI.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
305 subsection \<open>Review modelling- + specification-phase\<close>
311 \item check match between args of partial_function and model-pattern of meth;
312 provide error message.
314 \item "--- hack for funpack: generalise handling of meths which extend problem items ---"
316 \item see several locations of hack in code
317 \item these locations are NOT sufficient, see
318 test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
319 \item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,
320 this would be according to survey Notes (3) in src/../calchead.sml.
322 \item see "failed trial to generalise handling of meths"98298342fb6d
323 \item abstract specify + nxt_specif to common aux-funs;
324 see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
326 \item type model = itm list ?
327 \item review survey Notes in src/../calchead.sml: they are questionable
328 \item review copy-named, probably two issues commingled
330 \item special handling of "#Find#, because it is not a formal argument of partial_function
331 \item special naming for solutions of equation solving: x_1, x_2, ...
334 \item structure Tactic Specify -?-> Proglang (would require Model., Selem.)
336 \item this has been written in one go:
338 \item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
339 \item reconsider add_field': where is it used for what? Shift into mk_oris
340 \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
341 \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
342 \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
343 (relevant for pre-condition)
344 \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
349 subsection \<open>taci list, type step\<close>
351 taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
352 and probably, because the Kernel interface separated setNextTactic and applyTactic.
353 Both are no good reasons to make code more complicated.
355 !!! taci list is used in do_next !!!
359 \item can lev_on_total replace lev_on ? ..Test_Isac_Short + rename lev_on_total -> lev_on
361 \item Step* functions should return Calc.T instead of Chead.calcstate'
363 \item states.sml: check, when "length tacis > 1"
364 \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
365 \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
367 \item brute force setting all empty ([], [], ptp) works!?! but ptp causes errors -- investigate!
371 subsection \<open>Ctree\<close>
374 # mixture pos' .. pos in cappend_*, append_* is confusing
375 # existpt p pt andalso Tactic.is_empty DIFFERENT IN append_*, cappend_* is confusing
376 "exception PTREE "get_obj: pos =" ^^^^^: ^^^^ due to cut !!!
377 NOTE: exn IN if..andalso.. IS NOT!!! DETECTED, THIS is confusing
378 see test/../--- Minisubpbl/800-append-on-Frm.sml ---
379 # ?!? "cut branches below cannot be decided here" in append_atomic
380 # sign. of functions too different ?!?canonical arg.order ?!?
383 \item remove update_branch, update_*? -- make branch, etc args of append_*
385 \item close sig Ctree, contains cappend_* ?only? --- ?make parallel to ?Pide_Store?
387 \item unify args to Ctree.state (pt, p)
388 \item fun update_env .. repl_env \<rightarrow>updatempty
395 subsection \<open>replace theory/thy by context/ctxt\<close>
399 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
400 special case: Tactic.Refine_Problem
402 \item theory can be retrieved from ctxt by Proof_Context.theory_of
404 \item cleaup the many conversions string -- theory
405 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
406 \item 1. Rewrite.eval_true_, then
407 LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.tac_from_prog.
409 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
412 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
413 \item push srls into pstate
414 \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule_Set.Empty)
419 subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
421 remove refactor Rfuns, Rule.Prog, Rule.Empty_Prog, RrlsState: this is a concept never brought to work.
422 Clarify relation to reverse rewriting!
424 \item separate mut.recursion program with rule and rls by deleting fild scr in rls
425 (possible since CS 43160c1e775a
426 ` "replace Prog. in prep_rls by Auto_Prog.gen, which generates Prog. on the fly" )
428 \item probably only "normal_form" seems to be needed
429 \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
430 but that seems desirable
431 \item ?how is the relation to reverse-rewriting ???
432 \item "Rfuns" markers in test/../rational
434 \item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
435 rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
436 Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
437 Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
438 \item debug ^^^ related: is there an occurence of Steps with more than 1 element?
440 \item and do_next (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
442 \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
444 \item ?finally Prog could go from Calcelems to ProgLang?
447 subsection \<open>Inverse_Z_Transform.thy\<close>
450 \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
451 ? replace rewriting with substitution ?!?
452 The problem is related to the decision of typing for "d_d" and making bound variables free (while
453 shifting specific handling in equation solving etc. to the meta-logic).
454 \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
455 rewrite-rules; see \ref{new-var-rhs}.
456 \item Reconsider whole problem:
457 input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
460 subsection \<open>Adopt Isabelle's numerals for Isac\<close>
463 \item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
464 and have both representations in parallel for "nat".
469 subsection \<open>Redesign equation solver\<close>
471 Existing solver is structured along the WRONG assumption,
472 that Poly.thy must be the LAST thy among all thys involved -- while the opposite is the case.
474 Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
476 subsection \<open>Finetunig required for xmldata in kbase\<close>
478 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
479 and in kbase html-representation generated from these xmldata.
480 Notes in ~~/xmldata/TODO.txt.
483 section \<open>Hints for further development\<close>
486 subsection \<open>Coding standards & some explanations for math-authors\<close>
487 text \<open>copy from doc/math-eng.tex WN.28.3.03
488 WN071228 extended\<close>
490 subsubsection \<open>Identifiers\<close>
491 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
492 not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
493 reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
494 problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
495 However, all the cases (1)..(4) require different typing for one and the same
496 identifier {\tt probe} which is impossible, and actually leads to strange errors
497 (for instance (1) is used as string, except in a script addressing a Subproblem).
499 These are the preliminary rules for naming identifiers>
501 \item [elements of a key] into the hierarchy of problems or methods must not contain
502 capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
503 \item [descriptions in problem-patterns] must contain at least 1 capital letter and
504 must not contain underscores, e.g. {\tt Probe, forPolynomials}.
505 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
506 beware of conflicts~!
507 \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
511 %WN071228 extended\<close>
513 subsubsection \<open>Rule sets\<close>
514 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
515 where it can be viewed using the knowledge browsers.
517 There are rulesets visible to the student, and there are rulesets visible (in general) only for
518 math authors. There are also rulesets which {\em must} exist for {\em each} theory;
519 these contain the identifier of the respective theory (including all capital letters)
520 as indicated by {\it Thy} below.
523 \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
524 normalform for all terms which can be expressed by the definitions of the respective theory
525 (and the respective parents).
526 \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
527 which can be expressed by the definitions of the respective theory (and the respective parents)
528 such, that the rewrites can be presented to the student.
529 \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
530 numerical constants only (i.e. all terms which can be expressed by the definitions of
531 the respective theory and the respective parent theories). In particular, this ruleset includes
532 evaluating in/equalities with numerical constants only.
533 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
534 are logically equivalent, where the latter often add to the assumptions
535 (e.g. in Check_elementwise).
538 The above rulesets are all visible to the user, and also may be input;
539 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
540 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
541 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
542 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
549 {\tt Rule_Set.append_rules, Rule_Set.merge, remove_rls} TODO
552 subsection \<open>get proof-state\<close>
554 Re: [isabelle] Programatically get "this"
555 ----------------------------------------------------
556 So here is my (Makarius') version of your initial example, following these principles:
562 val ctxt = @{context};
565 Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN);
566 val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
571 subsection \<open>write Specification to jEdit\<close>
573 Re: [isabelle] Printing terms with type annotations
574 ----------------------------------------------------
575 On 06/02/2019 17:52, Moa Johansson wrote:
577 > I’m writing some code that should create a snippet of Isar script.
579 This is how Sledgehammer approximates this:
581 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
583 (The module name already shows that the proper terminology is "Isar
584 proof" (or "Isar proof text"). Proof scripts are a thing from the past,
585 before Isar. You can emulate old-style proof scripts via a sequence of
586 'apply' commands, but this is improper Isar.)
588 Note that there is no standard function in Isabelle/Pure, because the
589 problem to print just the right amount of type information is very
590 complex and not fully solved. One day, after 1 or 2 rounds of
591 refinements over the above approach, it might become generally available.
593 subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
595 isabelle update -u path_cartouches
596 isabelle update -u inner_syntax_cartouches
598 section \<open>Questions to Isabelle experts\<close>
601 \item ad ERROR Undefined fact "all_left" in Test_Isac: error-pattern.sml
602 Undefined fact: "xfoldr_Nil" inssort.sml
605 \item ?OK Test_Isac_Short with
606 LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
608 LI.by_tactic tac (Istate.empty, ContextC.empty) ptp
611 \item test from last CS with outcommented re-def of code ->
612 -> \<open>further tests additional to src/.. files\<close>
613 ADDTESTS/redefined-code.sml
615 \item efb749b79361 Test_Some_Short.thy has 2 errors, which disappear in thy ?!?:
616 ML_file "Interpret/error-pattern.sml" Undefined fact: "all_left"
617 ML_file "Knowledge/inssort.sml" Undefined fact: "xfoldr_Nil"
619 \item what is the actual replacement of "hg log --follow" ?
621 \item how HANDLE these exceptions, e.g.:
622 Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
625 Failed to parse term"
627 \item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"
628 e.g. in test/Interpret/lucas-interpreter.sml
634 section \<open>For copy & paste\<close>
652 subsection \<open>xxx\<close>
653 subsubsection \<open>xxx\<close>