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 from -------\*)
27 (*\------- to from -------/*)
29 \item resume step 6.10: unsuccessful trials with combination of types on Outer_Syntax
30 note: test in Calculation.thy is outcommented
32 \item re-arrange Isac's bootstrap: look for "after devel.of BridgeJEdit"
35 \item Input_Descript.descriptor -> Input_Descript.T
38 \item relate Prog_Epxr.lhs to Thm.lhs_of
40 \item as soon as src/../parseC.sml is stable,
41 remove defs from Test_Parse_Isac.thy
42 + and shift tests from Test_Parse_Isac -> test/../parseC.sml
44 \item Specify.find_next_step: References.select_input
45 cpI = ["vonBelastungZu", "Biegelinien"]: References_Def.id
48 \item Calc.state_empty_post \<rightarrow> Calc.state_post_empty
50 \item distribute code from test/../calchead.sml
52 \item rename Tactic.Calculate -> Tactic.Evaluate
54 \item replace src/ Erls by Rule_Set.Empty
56 \item rename ptyps.sml -> specify-etc.sml
57 rename Specify -> Specify_Etc
58 rename Specify -> Specify
60 \item specific_from_prog in..end: replace o by |> (Test_Isac or Test_Some!)
62 \item cleanup ThmC in MathEngBasic
73 subsection \<open>Postponed from current changeset\<close>
77 \item make steps around SubProblem more consistent:
78 SubProblem (thy, [pbl]) is bypassed by Model_Problem, if it is 1st Tactic in a Program.
80 * the Tactic SubProblem (thy, [pbl]) creates the formula SubProblem (thy, [pbl])
82 * the Tactic Model_Problem starts Specification
84 see test/../sub-problem.sml
86 \item Specify_Step.add has dummy argument Istate_Def.Uistate -- remove down to Ctree
88 \item Step_Specify.by_tactic (Tactic.Model_Problem' (id, _, met))
89 by_tactic (Tactic.Specify_Theory' domID)
90 had very old, strange code at 11b5b8b81876
91 ?redes Model_Problem', Specify_Theory' <--> Specify_Method: Step_Specify.complet_for ?
92 INTERMED. NO REPAIR: NOT PROMPTED IN TESTS
94 \item unify code Specify.find_next_step <--> Step_Specify.by_tactic (Tactic.Specify_Method'
96 \item Isa20.implementation: 0.2.4 Printing ML values ?INSTEAD? *.TO_STRING ???
97 ??? writeln ( make_string {x = x, y = y}); ???
99 \item revise O_Model and I_Model with an example with more than 1 variant.
101 \item ctxt is superfluous in specify-phase due to type constraints from Input_Descript.thy
103 \item Derive.do_one: TODO find code in common with complete_solve
104 Derive.embed: TODO rewrite according to CAO (+ no intermediate access to Ctree)
106 \item Solve_Check: postponed parsing input to _ option
108 \item ? "fetch-tactics.sml" from Mathengine -> BridgeLibisabelle ?
110 \item ? unify struct.Step and struct.Solve in MathEngine ?
112 \item use "Eval_Def" for renaming identifiers
114 \item why does Test_Build_Thydata.thy depend on ProgLang and not on CalcElements ?
118 \item LI.do_next (*TODO RM..*) ???
119 \item generate.sml: RM datatype edit TOGETHER WITH datatype inout
120 \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ
121 \item get_ctxt_LI should replace get_ctxt
122 \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
123 \item rename Base_Tool.thy <--- Base_Tools
124 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
125 \item rename field program in meth
133 \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}
134 there it is Free ("Subproblem", "char list \<times> ..
135 instead of Const (|???.Subproblem", "char list \<times> ..
136 AND THE STRING REPRESENTATION IS STRANGE:
137 Subproblem (''Test'',
138 ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation''
142 term2str; (*defined by..*)
143 fun term_to_string''' thy t =
145 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
146 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
148 val t = @{term "aaa + bbb"}
149 val t = @{term "Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation''])"};
151 val sss = Print_Mode.setmp [] (Syntax.string_of_term @{context}) t
153 writeln sss (*.. here perfect: Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation'']) *)
158 \item cleanup fun me:
159 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
160 | me*) (_, tac) p _(*NEW remove*) pt =
161 + -------------------------^^^^^^
162 # see test-code.sml fun me_trace
163 use this also for me, not only for me_ist_ctxt; del. me
164 this requires much updating in all test/*
166 \item shift tests into NEW model.sml (upd, upds_envv, ..)
168 \item clarify handling of contexts ctxt ContextC
171 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
173 \item Check_Elementwise "Assumptions": prerequisite for ^^goal
174 rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
175 rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
181 \item complete mstools.sml (* survey on handling contexts:
186 \item librarys.ml --> libraryC.sml + text from termC.sml
193 \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
194 DONE for find_next_step by Tactic.insert_assumptions m' ctxt
196 \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
197 \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
200 \item DO DELETIONS AFTER analogous concentrations in find_next_step
203 \item ? what is the difference headline <--> cascmd in
204 Subproblem' (spec, oris, headline, fmz_, context, cascmd)
205 \item Substitute' what does "re-calculation mean in the datatype comment?
207 \item inform: TermC.parse (ThyC.get_theory "Isac_Knowledge") istr --> parseNEW context istr
209 \item unify/clarify stac2tac_ |
212 \item extract common code from associate.. stac2tac_xxx
213 \item rename LItool.tac_from_prog -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,
218 \item unify in signature LANGUAGE_TOOLS =\\
219 val pblterm: ThyC.id -> Problem.id -> term vvv vvv\\
220 val subpbl: string -> string list -> term unify with ^^^
222 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
223 Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
224 If Telem.safe is kept, consider merge with CTbasic.ostate
226 \item remove find_next_step from solve Apply_Method';
227 this enforces Pos.at_first_tactic, which should be dropped, too.
233 subsection \<open>Postponed --> Major reforms\<close>
238 \item make parser mutually recursive for Problem .. Solution
239 preps. in Test_Parse_Isac:
241 subsubsection "problem_mini" shows a principal issue with recursive parsing
242 probably due to !2! arguments of parser (as shown in Cookbook)
243 Test_Parsers_Cookbook:
244 (* recursive parser p.140 \<section>6.1 adapted to tokens: *) shows differences,
245 which might help understanding the principal issue
246 see also Test_Parsers subsection "recursive parsing"
250 \item revisit bootstrap Calcelements. rule->calcelems->termC
251 would be nice, but is hard: UnparseC.terms -> TermC.s_to_string
253 \item replace all Ctree.update_* with Ctree.cupdate_problem
255 \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
257 \item exception PROG analogous to TERM
259 \item sig/struc ..elems --> ..elem
261 \item distille CAS-command, CAScmd, etc into a struct
263 \item check location of files:
264 test/Tools/isac/Interpret/ptyps.thy
265 test/Tools/isac/Specify.ptyps.sml
267 \item check occurences of Atools in src/ test/
268 \item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _)
272 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
273 \item Test.thy: met_test_sqrt2: deleted?!
275 \item Rewrite_Ord.id := overwritel (! Rewrite_Ord.id, (*<<<---- use Know_Store.xxx, too*)
277 \item automatically extrac rls from program-code
278 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
280 \item finish output of LItool.trace with Check_Postcond (useful for SubProblem)
282 \item replace Rule_Set.empty by Rule_Set.Empty
283 latter is more clear, but replacing ***breaks rewriting over all examples***,
284 e.g. see ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x'
285 in Minisubplb/200-start-method-NEXT_STEP.sml:
286 (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
288 (*+*) Rls {calc = [], asm_rls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =
289 (*+*) ("dummy_ord", fn), rules = [], program = Empty_Prog, prog_rls = Erls}:
290 (*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !
291 (*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had
292 (*+*)val Empty = where_rls (* <---ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x' *)
293 ( *+*)val ["sqroot-test", "univariate", "equation", "test"] = cpI
294 THAT INDICATES, that much rewriting/evaluating JUST WORKED BY CHANCE?!?
305 section \<open>Major reforms\<close>
308 subsection \<open>Exception Size raised\<close>
310 During update Isabelle2018 --> Isabelle2019 we noticed, that
311 "isabelle build" uses resources more efficiently than "isabelle jedit".
312 The former works, but the latter causes
314 \item "Exception- Size raised"
316 \item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
317 in test/../biegelinie-*.xml.
319 This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
321 Find tools to investigate the Exception, and find ways around it eventually.
323 subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
326 \item there are comments in several signatures
327 \item ML_file "$ISABELLE_ISAC/Interpret/specification-elems.sml" can be (almost) deleted
328 \item src/../Frontend/: signatures missing
332 subsection \<open>overall structure of code\<close>
335 \item try to separate Isac_Knowledge from MathEngine
336 common base: Knowledge_Author / ..??
338 \item ML_file "$ISABELLE_ISAC/Interpret/ctree.sml" (*shift to base in common with Interpret*)
344 subsection \<open>Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/\<close>
349 \item re-organise code for Interpret
351 \item Step*: Step_Specify | Step_Solve | Step DONE
353 \item Prog_Tac: fun get_first_argument takes both Prog_Tac + Program --- wait for separate Tactical
354 then shift into common descendant
359 \item ??????????? WHY CAN LI.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
364 subsection \<open>Review modelling- + specification-phase\<close>
370 \item check match between args of partial_function and model-pattern of meth;
371 provide error message.
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, ...
394 \item this has been written in one go:
396 \item reconsidering Pre_Conds.max_variant, use problem with meth ["Diff_App", "max_by_calculus"]
397 \item reconsider add_field': where is it used for what? Shift into mk_oris
398 \item reconsider by_i_models: where is it used for what? max_variant ONLY???
399 \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
400 \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
401 (relevant for where_-condition)
402 \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
407 subsection \<open>taci list, type step\<close>
409 taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
410 and probably, because the Kernel interface separated setNextTactic and applyTactic.
411 Both are no good reasons to make code more complicated.
413 !!! taci list is used in do_next !!!
417 \item can lev_on_total replace lev_on ? ..Test_Isac_Short + rename lev_on_total -> lev_on
419 \item Step* functions should return Calc.T instead of Calc.state_post
421 \item states.sml: check, when "length tacis > 1"
422 \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
423 \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
425 \item brute force setting all empty ([], [], ptp) works!?! but ptp causes errors -- investigate!
429 subsection \<open>Ctree\<close>
432 # mixture pos' .. pos in cappend_*, append_* is confusing
433 # existpt p pt andalso Tactic.is_empty DIFFERENT IN append_*, cappend_* is confusing
434 "exception PTREE "get_obj: pos =" ^^^^^: ^^^^ due to cut !!!
435 NOTE: exn IN if..andalso.. IS NOT!!! DETECTED, THIS is confusing
436 see test/../--- Minisubpbl/800-append-on-Frm.sml ---
437 # ?!? "cut branches below cannot be decided here" in append_atomic
438 # sign. of functions too different ?!?canonical arg.order ?!?
441 \item remove update_branch, update_*? -- make branch, etc args of append_*
443 \item close sig Ctree, contains cappend_* ?only? --- ?make parallel to ?Pide_Store?
445 \item unify args to Ctree.state (pt, p)
446 \item fun update_env .. repl_env \<rightarrow>updatempty
453 subsection \<open>replace theory/thy by context/ctxt\<close>
457 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
458 special case: Tactic.Refine_Problem
460 \item theory can be retrieved from ctxt by Proof_Context.theory_of
462 \item cleaup the many conversions string -- theory
463 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
464 \item 1. Rewrite.eval_true_, then
465 LItool.check_leaf, Rewrite.eval_prog_expr, Step.add, LItool.tac_from_prog.
467 let val thy = ThyC.get_theory "Isac_Knowledge";(*TODO*)
470 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
471 \item push prog_rls into pstate
472 \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 prog_rls tac cstate (progr, Rule_Set.Empty)
477 subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
479 remove refactor Rfuns, Rule.Prog, Rule.Empty_Prog, RrlsState: this is a concept never brought to work.
480 Clarify relation to reverse rewriting!
482 \item separate mut.recursion program with rule and rls by deleting fild program in rls
483 (possible since CS 43160c1e775a
484 ` "replace Prog. in prep_rls by Auto_Prog.gen, which generates Prog. on the fly" )
486 \item probably only "normal_form" seems to be needed
487 \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
488 but that seems desirable
489 \item ?how is the relation to reverse-rewriting ???
490 \item "Rfuns" markers in test/../rational
492 \item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
493 rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
494 Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
495 Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
496 \item debug ^^^ related: is there an occurence of Steps with more than 1 element?
498 \item and do_next (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
500 \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
502 \item ?finally Prog could go from Calcelems to ProgLang?
505 subsection \<open>Inverse_Z_Transform.thy\<close>
508 \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
509 ? replace rewriting with substitution ?!?
510 The problem is related to the decision of typing for "d_d" and making bound variables free (while
511 shifting specific handling in equation solving etc. to the meta-logic).
512 \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
513 rewrite-rules; see \ref{new-var-rhs}.
514 \item Reconsider whole problem:
515 input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
518 subsection \<open>Adopt Isabelle's numerals for Isac\<close>
521 \item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
522 and have both representations in parallel for "nat".
527 subsection \<open>Redesign equation solver\<close>
529 Existing solver is structured along the WRONG assumption,
530 that Poly.thy must be the LAST thy among all thys involved -- while the opposite is the case.
532 Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
534 subsection \<open>Finetunig required for xmldata in kbase\<close>
536 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
537 and in kbase html-representation generated from these xmldata.
538 Notes in ~~/xmldata/TODO.txt.
541 section \<open>Hints for further development\<close>
544 subsection \<open>Coding standards & some explanations for math-authors\<close>
545 text \<open>copy from doc/math-eng.tex WN.28.3.03
546 WN071228 extended\<close>
548 subsubsection \<open>Identifiers\<close>
549 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
550 not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
551 reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
552 problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
553 However, all the cases (1)..(4) require different typing for one and the same
554 identifier {\tt probe} which is impossible, and actually leads to strange errors
555 (for instance (1) is used as string, except in a script addressing a Subproblem).
557 These are the preliminary rules for naming identifiers>
559 \item [elements of a key] into the hierarchy of problems or methods must not contain
560 capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
561 \item [descriptions in problem-patterns] must contain at least 1 capital letter and
562 must not contain underscores, e.g. {\tt Probe, forPolynomials}.
563 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
564 beware of conflicts~!
565 \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
569 %WN071228 extended\<close>
571 subsubsection \<open>Rule sets\<close>
572 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
573 where it can be viewed using the knowledge browsers.
575 There are rulesets visible to the student, and there are rulesets visible (in general) only for
576 math authors. There are also rulesets which {\em must} exist for {\em each} theory;
577 these contain the identifier of the respective theory (including all capital letters)
578 as indicated by {\it Thy} below.
581 \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
582 normalform for all terms which can be expressed by the definitions of the respective theory
583 (and the respective parents).
584 \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
585 which can be expressed by the definitions of the respective theory (and the respective parents)
586 such, that the rewrites can be presented to the student.
587 \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
588 numerical constants only (i.e. all terms which can be expressed by the definitions of
589 the respective theory and the respective parent theories). In particular, this ruleset includes
590 evaluating in/equalities with numerical constants only.
591 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
592 are logically equivalent, where the latter often add to the assumptions
593 (e.g. in Check_elementwise).
596 The above rulesets are all visible to the user, and also may be input;
597 thus they must be contained in {\tt Theory_Data} (Know_Store.add_rlss,
598 Know_Store.get_rlss). All these rulesets must undergo a preparation
599 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
600 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
607 {\tt Rule_Set.append_rules, Rule_Set.merge, remove_rls} TODO
610 subsection \<open>get proof-state\<close>
612 Re: [isabelle] Programatically get "this"
613 ----------------------------------------------------
614 So here is my (Makarius') version of your initial example, following these principles:
620 val ctxt = @{context};
623 Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN);
624 val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
629 subsection \<open>write Specification to jEdit\<close>
631 Re: [isabelle] Printing terms with type annotations
632 ----------------------------------------------------
633 On 06/02/2019 17:52, Moa Johansson wrote:
635 > I’m writing some code that should create a snippet of Isar script.
637 This is how Sledgehammer approximates this:
639 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
641 (The module name already shows that the proper terminology is "Isar
642 proof" (or "Isar proof text"). Proof scripts are a thing from the past,
643 before Isar. You can emulate old-style proof scripts via a sequence of
644 'apply' commands, but this is improper Isar.)
646 Note that there is no standard function in Isabelle/Pure, because the
647 problem to print just the right amount of type information is very
648 complex and not fully solved. One day, after 1 or 2 rounds of
649 refinements over the above approach, it might become generally available.
651 subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
653 isabelle update -u path_cartouches
654 isabelle update -u inner_syntax_cartouches
656 section \<open>Questions to Isabelle experts\<close>
659 \item ad ERROR Undefined fact "all_left" in Test_Isac: error-pattern.sml
660 Undefined fact: "xfoldr_Nil" inssort.sml
661 (* probably two different reasons:
663 (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
664 all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
667 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
668 all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
670 test/../partial_fractions.sml
671 (*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
672 (*[7, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"))*)
674 test/../mathengine-stateless.sml
675 (*if ThmC.string_of_thm @ {thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
676 then () else error "string_of_thm changed";*)
678 (*---------------------------------------------------------------------------------------------*)
680 primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
681 xfoldr_Nil: "xfoldr f {|| ||} = id" |
682 xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
685 prog_rls = Rule_Set.empty, calc = [], rules = [
686 Rule.Thm ("xfoldr_Nil",(*num_str*) @ {thm xfoldr_Nil} (* foldr ?f [] = id *)),
690 \item ?OK Test_Isac_Short with
691 LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
693 LI.by_tactic tac (Istate.empty, ContextC.empty) ptp
696 \item test from last CS with outcommented re-def of code ->
697 -> \<open>further tests additional to src/.. files\<close>
698 ADDTESTS/redefined-code.sml
700 \item efb749b79361 Test_Some_Short.thy has 2 errors, which disappear in thy ?!?:
701 ML_file "Interpret/error-pattern.sml" Undefined fact: "all_left"
702 ML_file "Knowledge/inssort.sml" Undefined fact: "xfoldr_Nil"
704 \item what is the actual replacement of "hg log --follow" ?
706 \item how HANDLE these exceptions, e.g.:
707 Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
710 Failed to parse term"
712 \item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"
713 e.g. in test/Interpret/lucas-interpreter.sml
719 section \<open>For copy & paste\<close>
737 subsection \<open>xxx\<close>
738 subsubsection \<open>xxx\<close>