neuper@42314
|
1 |
(* Title: todo's for isac core
|
neuper@42314
|
2 |
Author: Walther Neuper 111013
|
neuper@42314
|
3 |
(c) copyright due to lincense terms.
|
neuper@42314
|
4 |
*)
|
wneuper@59504
|
5 |
theory TODO
|
wneuper@59504
|
6 |
imports "~~/src/Doc/Prog_Prove/LaTeXsugar"
|
wneuper@59504
|
7 |
begin
|
neuper@42314
|
8 |
|
walther@59779
|
9 |
text \<open>
|
walther@59779
|
10 |
Legend: here + code since 200120
|
walther@59779
|
11 |
\<open>(*DOC\<close> identifies stuff dedicated for isac/Doc/Lucas_Interpreter
|
walther@59779
|
12 |
\<open>(*?!?\<close> identifies a design question
|
walther@59779
|
13 |
|
walther@59779
|
14 |
Distillation of "rounds of reforms":
|
walther@59779
|
15 |
\<open>TODOs from current changesets\<close> \<rightarrow> \<open>Postponed from current changeset\<close> \<rightarrow>
|
walther@59779
|
16 |
(*to be removed..*) \<rightarrow> \<open>Separated tasks\<close> (*.. to be removed*)
|
walther@59779
|
17 |
\<rightarrow> subsection of \<open>Major reforms\<close>
|
walther@59779
|
18 |
\<close>
|
walther@59779
|
19 |
|
wneuper@59574
|
20 |
section \<open>TODOs from current changesets\<close>
|
wneuper@59568
|
21 |
text\<open>
|
walther@59779
|
22 |
Shift more complicated issues from \<open>Current changeset\<close> to \<open>Postponed from current changeset\<close>
|
wneuper@59568
|
23 |
\<close>
|
wneuper@59574
|
24 |
subsection \<open>Current changeset\<close>
|
wneuper@59574
|
25 |
text \<open>
|
walther@59876
|
26 |
(*/------- to -------\*)
|
walther@59876
|
27 |
(*\------- to -------/*)
|
wneuper@59569
|
28 |
\begin{itemize}
|
walther@59887
|
29 |
\item ML_file "rule-set.sml" Know_Store -> MathEngBasic (=ThmC, Rewrite)
|
walther@59876
|
30 |
probably first review calcelems.sml
|
walther@59779
|
31 |
\item xxx
|
walther@59882
|
32 |
\item replace src/ Erls Rule_Set.Empty
|
walther@59842
|
33 |
\item xxx
|
walther@59882
|
34 |
\item xxx
|
walther@59882
|
35 |
\item xxx
|
walther@59882
|
36 |
\item rename ptyps.sml -> specify-etc.sml
|
walther@59882
|
37 |
rename Specify -> Specify_Etc
|
walther@59882
|
38 |
rename SpecifyNEW -> Specify
|
walther@59842
|
39 |
\item xxx
|
walther@59914
|
40 |
\item specific_from_prog in..end: replace o by |> (Test_Isac or Test_Some!)
|
walther@59914
|
41 |
\item xxx
|
walther@59914
|
42 |
\item cleanup ThmC in MathEngBasic
|
walther@59914
|
43 |
\item xxx
|
walther@59914
|
44 |
\item xxx
|
walther@59914
|
45 |
\item xxx
|
walther@59842
|
46 |
\item xxx
|
walther@59842
|
47 |
\item xxx
|
walther@59842
|
48 |
\item xxx
|
walther@59842
|
49 |
\item xxx
|
walther@59842
|
50 |
\item xxx
|
walther@59846
|
51 |
\end{itemize}
|
walther@59846
|
52 |
\<close>
|
walther@59846
|
53 |
subsection \<open>Postponed from current changeset\<close>
|
walther@59846
|
54 |
text \<open>
|
walther@59886
|
55 |
\begin{itemize}
|
walther@59886
|
56 |
\item xxx
|
walther@59886
|
57 |
\item xxx
|
walther@59851
|
58 |
\item xxx
|
walther@59919
|
59 |
\item use "Eval_Def" for renaming identifiers
|
walther@59851
|
60 |
\item xxx
|
walther@59886
|
61 |
\item why does Test_Build_Thydata.thy depend on ProgLang and not on CalcElements ?
|
walther@59851
|
62 |
\item xxx
|
walther@59851
|
63 |
\item xxx
|
walther@59846
|
64 |
\begin{itemize}
|
walther@59846
|
65 |
\item LI.do_next (*TODO RM..*) ???
|
walther@59846
|
66 |
\item generate.sml: RM datatype edit TOGETHER WITH datatype inout
|
walther@59846
|
67 |
\item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ
|
walther@59846
|
68 |
\item get_ctxt_LI should replace get_ctxt
|
walther@59846
|
69 |
\item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
|
walther@59846
|
70 |
\item rename Base_Tool.thy <--- Base_Tools
|
walther@59846
|
71 |
\item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
|
walther@59846
|
72 |
\item rename field scr in meth
|
walther@59820
|
73 |
\item DEL double code: nxt_specify_init_calc IN specify.sml + step-specify.sml
|
walther@59819
|
74 |
\item xxx
|
walther@59820
|
75 |
\item xxx
|
walther@59820
|
76 |
\item xxx
|
walther@59844
|
77 |
\item xxx
|
walther@59844
|
78 |
\item xxx
|
walther@59844
|
79 |
\item xxx
|
walther@59817
|
80 |
\item xxx
|
walther@59814
|
81 |
\item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}
|
walther@59848
|
82 |
there it is Free ("Subproblem", "char list \<times> ..
|
walther@59848
|
83 |
instead of Const (|???.Subproblem", "char list \<times> ..
|
walther@59848
|
84 |
AND THE STRING REPRESENTATION IS STRANGE:
|
walther@59848
|
85 |
Subproblem (''Test'',
|
walther@59848
|
86 |
??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation''
|
walther@59848
|
87 |
''test'')
|
walther@59814
|
88 |
ML \<open>
|
walther@59814
|
89 |
\<close> ML \<open>
|
walther@59814
|
90 |
term2str; (*defined by..*)
|
walther@59814
|
91 |
fun term_to_string''' thy t =
|
walther@59814
|
92 |
let
|
walther@59814
|
93 |
val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
|
walther@59814
|
94 |
in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
|
walther@59814
|
95 |
\<close> ML \<open>
|
walther@59814
|
96 |
val t = @{term "aaa + bbb"}
|
walther@59814
|
97 |
val t = @{term "Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation''])"};
|
walther@59814
|
98 |
\<close> ML \<open>
|
walther@59814
|
99 |
val sss = Print_Mode.setmp [] (Syntax.string_of_term @{context}) t
|
walther@59814
|
100 |
\<close> ML \<open>
|
walther@59814
|
101 |
writeln sss (*.. here perfect: Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation'']) *)
|
walther@59814
|
102 |
\<close> ML \<open>
|
walther@59814
|
103 |
\<close>
|
walther@59814
|
104 |
\item xxx
|
walther@59814
|
105 |
\item xxx
|
walther@59814
|
106 |
\item cleanup fun me:
|
walther@59814
|
107 |
fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
|
walther@59814
|
108 |
| me*) (_, tac) p _(*NEW remove*) pt =
|
walther@59814
|
109 |
+ -------------------------^^^^^^
|
walther@59814
|
110 |
# see test-code.sml fun me_trace
|
walther@59814
|
111 |
use this also for me, not only for me_ist_ctxt; del. me
|
walther@59814
|
112 |
this requires much updating in all test/*
|
walther@59802
|
113 |
\item xxx
|
walther@59802
|
114 |
\item xxx
|
walther@59779
|
115 |
\item generate, generate1: NO thy as arg.
|
walther@59803
|
116 |
Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
|
walther@59828
|
117 |
redesign return value (originally for output by fun me?)
|
walther@59779
|
118 |
\item xxx
|
walther@59779
|
119 |
\item shift tests into NEW model.sml (upd, upds_envv, ..)
|
walther@59779
|
120 |
\item xxx
|
walther@59779
|
121 |
\item xxx
|
walther@59814
|
122 |
\item clarify handling of contexts ctxt ContextC
|
walther@59779
|
123 |
\begin{itemize}
|
walther@59779
|
124 |
\item xxx
|
walther@59779
|
125 |
\item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
|
walther@59779
|
126 |
\item xxx
|
walther@59779
|
127 |
\item Check_Elementwise "Assumptions": prerequisite for ^^goal
|
walther@59779
|
128 |
rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
|
walther@59779
|
129 |
rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
|
walther@59779
|
130 |
\item xxx
|
walther@59779
|
131 |
\item xxx
|
walther@59779
|
132 |
\end{itemize}
|
walther@59779
|
133 |
\item xxx
|
walther@59779
|
134 |
\item xxx
|
walther@59779
|
135 |
\item complete mstools.sml (* survey on handling contexts:
|
walther@59779
|
136 |
\item xxx
|
walther@59779
|
137 |
\item xxx
|
walther@59779
|
138 |
\item xxx
|
walther@59779
|
139 |
\item xxx
|
walther@59779
|
140 |
\item librarys.ml --> libraryC.sml + text from termC.sml
|
walther@59779
|
141 |
\item xxx
|
walther@59779
|
142 |
\item xxx
|
walther@59779
|
143 |
\item xxx
|
walther@59779
|
144 |
\item xxx
|
walther@59779
|
145 |
\item xxx
|
walther@59779
|
146 |
\item xxx
|
walther@59779
|
147 |
\item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
|
walther@59779
|
148 |
DONE for find_next_step by Tactic.insert_assumptions m' ctxt
|
walther@59779
|
149 |
\begin{itemize}
|
walther@59779
|
150 |
\item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
|
walther@59779
|
151 |
\item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
|
walther@59779
|
152 |
\item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
|
walther@59779
|
153 |
\item xxx
|
walther@59779
|
154 |
\item xxx
|
walther@59779
|
155 |
\item DO DELETIONS AFTER analogous concentrations in find_next_step
|
walther@59779
|
156 |
\end{itemize}
|
walther@59779
|
157 |
\item xxx
|
walther@59779
|
158 |
\item ? what is the difference headline <--> cascmd in
|
walther@59779
|
159 |
Subproblem' (spec, oris, headline, fmz_, context, cascmd)
|
walther@59779
|
160 |
\item xxx
|
walther@59881
|
161 |
\item inform: TermC.parse (ThyC.get_theory "Isac_Knowledge") istr --> parseNEW context istr
|
walther@59799
|
162 |
\item xxx
|
walther@59816
|
163 |
\item unify/clarify stac2tac_ |
|
walther@59779
|
164 |
\begin{itemize}
|
walther@59779
|
165 |
\item xxx
|
walther@59816
|
166 |
\item extract common code from associate.. stac2tac_xxx
|
walther@59823
|
167 |
\item rename LItool.tac_from_prog -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,
|
walther@59779
|
168 |
\item xxx
|
walther@59779
|
169 |
\item xxx
|
walther@59779
|
170 |
\end{itemize}
|
walther@59779
|
171 |
\item xxx
|
walther@59779
|
172 |
\item unify in signature LANGUAGE_TOOLS =\\
|
walther@59903
|
173 |
val pblterm: ThyC.id -> Problem.id -> term vvv vvv\\
|
walther@59779
|
174 |
val subpbl: string -> string list -> term unify with ^^^
|
walther@59779
|
175 |
\item xxx
|
walther@59779
|
176 |
\item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
|
walther@59779
|
177 |
Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
|
walther@59779
|
178 |
If Telem.safe is kept, consider merge with CTbasic.ostate
|
walther@59779
|
179 |
\item xxx
|
walther@59779
|
180 |
\item remove find_next_step from solve Apply_Method';
|
walther@59779
|
181 |
this enforces Pos.at_first_tactic, which should be dropped, too.
|
walther@59779
|
182 |
\item xxx
|
walther@59779
|
183 |
\item xxx
|
walther@59816
|
184 |
\item xxx
|
walther@59779
|
185 |
\end{itemize}
|
walther@59779
|
186 |
\<close>
|
walther@59851
|
187 |
subsection \<open>Postponed --> Major reforms\<close>
|
walther@59816
|
188 |
text \<open>
|
walther@59816
|
189 |
\begin{itemize}
|
walther@59816
|
190 |
\item xxx
|
walther@59846
|
191 |
\item revisit bootstrap Calcelements. rule->calcelems->termC
|
walther@59868
|
192 |
would be nice, but is hard: UnparseC.terms -> TermC.s_to_string
|
walther@59820
|
193 |
\item xxx
|
walther@59820
|
194 |
\item replace all Ctree.update_* with Ctree.cupdate_problem
|
walther@59820
|
195 |
\item xxx
|
walther@59816
|
196 |
\item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
|
walther@59816
|
197 |
\item xxx
|
walther@59816
|
198 |
\item exception PROG analogous to TERM
|
walther@59816
|
199 |
\item xxx
|
walther@59816
|
200 |
\item sig/struc ..elems --> ..elem
|
walther@59816
|
201 |
\item xxx
|
walther@59816
|
202 |
\item distille CAS-command, CAScmd, etc into a struct
|
walther@59816
|
203 |
\item xxx
|
walther@59816
|
204 |
\item check location of files:
|
walther@59816
|
205 |
test/Tools/isac/Interpret/ptyps.thy
|
walther@59816
|
206 |
test/Tools/isac/Specify.ptyps.sml
|
walther@59816
|
207 |
\item xxx
|
walther@59816
|
208 |
\item check occurences of Atools in src/ test/
|
walther@59816
|
209 |
\item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _)
|
walther@59816
|
210 |
\item xxx
|
walther@59816
|
211 |
\item rm Float
|
walther@59816
|
212 |
\item xxx
|
walther@59816
|
213 |
\item Diff.thy: differentiateX --> differentiate after removal of script-constant
|
walther@59816
|
214 |
\item Test.thy: met_test_sqrt2: deleted?!
|
walther@59816
|
215 |
\item xxx
|
walther@59887
|
216 |
\item Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx, too*)
|
walther@59816
|
217 |
\item xxx
|
walther@59816
|
218 |
\item automatically extrac rls from program-code
|
walther@59816
|
219 |
? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
|
walther@59816
|
220 |
\item xxx
|
walther@59901
|
221 |
\item finish output of LItool.trace with Check_Postcond (useful for SubProblem)
|
walther@59816
|
222 |
\item xxx
|
walther@59851
|
223 |
\item replace Rule_Set.empty by Rule_Set.Empty
|
walther@59851
|
224 |
latter is more clear, but replacing ***breaks rewriting over all examples***,
|
walther@59851
|
225 |
e.g. see ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x'
|
walther@59851
|
226 |
in Minisubplb/200-start-method-NEXT_STEP.sml:
|
walther@59851
|
227 |
(*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
|
walther@59851
|
228 |
(*+*) prls =
|
walther@59852
|
229 |
(*+*) Rls {calc = [], erls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =
|
walther@59878
|
230 |
(*+*) ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Erls}:
|
walther@59851
|
231 |
(*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !
|
walther@59851
|
232 |
(*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had
|
walther@59851
|
233 |
(*+*)val Empty = prls (* <---ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x' *)
|
walther@59851
|
234 |
( *+*)val ["sqroot-test", "univariate", "equation", "test"] = cpI
|
walther@59851
|
235 |
THAT INDICATES, that much rewriting/evaluating JUST WORKED BY CHANCE?!?
|
walther@59816
|
236 |
\item xxx
|
walther@59816
|
237 |
\item xxx
|
walther@59816
|
238 |
\item xxx
|
walther@59816
|
239 |
\item xxx
|
walther@59816
|
240 |
\item xxx
|
walther@59816
|
241 |
\item xxx
|
walther@59816
|
242 |
\item xxx
|
walther@59816
|
243 |
\end{itemize}
|
walther@59816
|
244 |
\<close>
|
walther@59816
|
245 |
|
walther@59779
|
246 |
section \<open>Major reforms\<close>
|
walther@59779
|
247 |
text \<open>
|
walther@59779
|
248 |
\<close>
|
walther@59779
|
249 |
subsection \<open>Exception Size raised\<close>
|
walther@59779
|
250 |
text \<open>
|
walther@59779
|
251 |
During update Isabelle2018 --> Isabelle2019 we noticed, that
|
walther@59779
|
252 |
"isabelle build" uses resources more efficiently than "isabelle jedit".
|
walther@59779
|
253 |
The former works, but the latter causes
|
walther@59779
|
254 |
\begin{itemize}
|
walther@59779
|
255 |
\item "Exception- Size raised"
|
walther@59779
|
256 |
in Build_Thydata.thy
|
walther@59779
|
257 |
\item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
|
walther@59779
|
258 |
in test/../biegelinie-*.xml.
|
walther@59779
|
259 |
\end{itemize}
|
walther@59779
|
260 |
This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
|
walther@59779
|
261 |
|
walther@59779
|
262 |
Find tools to investigate the Exception, and find ways around it eventually.
|
walther@59779
|
263 |
\<close>
|
walther@59779
|
264 |
subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
|
walther@59779
|
265 |
text \<open>
|
walther@59779
|
266 |
\begin{itemize}
|
walther@59779
|
267 |
\item there are comments in several signatures
|
walther@59779
|
268 |
\item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted
|
walther@59779
|
269 |
\item src/../Frontend/: signatures missing
|
walther@59779
|
270 |
\item xxx
|
walther@59779
|
271 |
\end{itemize}
|
walther@59779
|
272 |
\<close>
|
walther@59779
|
273 |
subsection \<open>overall structure of code\<close>
|
walther@59779
|
274 |
text \<open>
|
walther@59779
|
275 |
\begin{itemize}
|
walther@59779
|
276 |
\item try to separate Isac_Knowledge from MathEngine
|
walther@59779
|
277 |
common base: Knowledge_Author / ..??
|
walther@59779
|
278 |
\item xxx
|
walther@59779
|
279 |
\item ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)
|
walther@59779
|
280 |
\item xxx
|
walther@59779
|
281 |
\item xxx
|
walther@59779
|
282 |
\item xxx
|
walther@59779
|
283 |
\end{itemize}
|
walther@59779
|
284 |
\<close>
|
walther@59779
|
285 |
subsection \<open>Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/\<close>
|
walther@59779
|
286 |
text \<open>
|
walther@59779
|
287 |
\begin{itemize}
|
walther@59779
|
288 |
\item xxx
|
walther@59800
|
289 |
\item xxx
|
walther@59734
|
290 |
\item re-organise code for Interpret
|
walther@59734
|
291 |
\begin{itemize}
|
walther@59816
|
292 |
\item Step*: Step_Specify | Step_Solve | Step
|
walther@59734
|
293 |
\begin{itemize}
|
walther@59816
|
294 |
\item *.check | *.add ARE TOO LATE IN BUILD with Step_Specify | Step_Solve
|
walther@59816
|
295 |
Specify_Step.check | Specify_Step.add <-- Applicable.applicable_in
|
walther@59816
|
296 |
Solve_Step.check | Solve_Step.add <-- Generate.generate1
|
walther@59816
|
297 |
\item xxx
|
walther@59743
|
298 |
\end{itemize}
|
walther@59734
|
299 |
\item xxx
|
walther@59848
|
300 |
\item Prog_Tac: fun get_first_argument takes both Prog_Tac + Program --- wait for separate Tactical
|
walther@59800
|
301 |
then shift into common descendant
|
walther@59734
|
302 |
\item xxx
|
walther@59734
|
303 |
\end{itemize}
|
walther@59734
|
304 |
\item xxx
|
walther@59778
|
305 |
\item xxx
|
walther@59791
|
306 |
\item ??????????? WHY CAN LI.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
|
walther@59778
|
307 |
\item xxx
|
walther@59778
|
308 |
\item xxx
|
walther@59778
|
309 |
\end{itemize}
|
walther@59778
|
310 |
\<close>
|
wneuper@59574
|
311 |
subsection \<open>Review modelling- + specification-phase\<close>
|
wneuper@59574
|
312 |
text \<open>
|
wneuper@59574
|
313 |
\begin{itemize}
|
walther@59816
|
314 |
\item xxx
|
walther@59820
|
315 |
\item xxx
|
walther@59820
|
316 |
\item xxx
|
walther@59816
|
317 |
\item check match between args of partial_function and model-pattern of meth;
|
walther@59816
|
318 |
provide error message.
|
walther@59778
|
319 |
\item xxx
|
wneuper@59574
|
320 |
\item "--- hack for funpack: generalise handling of meths which extend problem items ---"
|
wneuper@59569
|
321 |
\begin{itemize}
|
wneuper@59574
|
322 |
\item see several locations of hack in code
|
wneuper@59574
|
323 |
\item these locations are NOT sufficient, see
|
wneuper@59574
|
324 |
test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
|
wneuper@59574
|
325 |
\item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,
|
wneuper@59574
|
326 |
this would be according to survey Notes (3) in src/../calchead.sml.
|
wneuper@59574
|
327 |
\end{itemize}
|
wneuper@59574
|
328 |
\item see "failed trial to generalise handling of meths"98298342fb6d
|
wneuper@59574
|
329 |
\item abstract specify + nxt_specif to common aux-funs;
|
wneuper@59574
|
330 |
see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
|
wneuper@59574
|
331 |
\item xxx
|
wneuper@59574
|
332 |
\item type model = itm list ?
|
wneuper@59574
|
333 |
\item review survey Notes in src/../calchead.sml: they are questionable
|
wneuper@59574
|
334 |
\item review copy-named, probably two issues commingled
|
wneuper@59574
|
335 |
\begin{itemize}
|
wneuper@59574
|
336 |
\item special handling of "#Find#, because it is not a formal argument of partial_function
|
wneuper@59574
|
337 |
\item special naming for solutions of equation solving: x_1, x_2, ...
|
wneuper@59569
|
338 |
\end{itemize}
|
wneuper@59569
|
339 |
\item xxx
|
walther@59634
|
340 |
\item structure Tactic Specify -?-> Proglang (would require Model., Selem.)
|
walther@59634
|
341 |
\item xxx
|
wneuper@59574
|
342 |
\item this has been written in one go:
|
wneuper@59574
|
343 |
\begin{itemize}
|
wneuper@59574
|
344 |
\item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
|
wneuper@59574
|
345 |
\item reconsider add_field': where is it used for what? Shift into mk_oris
|
wneuper@59574
|
346 |
\item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
|
wneuper@59574
|
347 |
\item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
|
wneuper@59574
|
348 |
\item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
|
wneuper@59574
|
349 |
(relevant for pre-condition)
|
wneuper@59574
|
350 |
\item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
|
wneuper@59574
|
351 |
\item
|
wneuper@59574
|
352 |
\end{itemize}
|
wneuper@59574
|
353 |
\end{itemize}
|
wneuper@59574
|
354 |
\<close>
|
wneuper@59574
|
355 |
subsection \<open>taci list, type step\<close>
|
wneuper@59574
|
356 |
text \<open>
|
walther@59762
|
357 |
taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
|
walther@59762
|
358 |
and probably, because the Kernel interface separated setNextTactic and applyTactic.
|
walther@59816
|
359 |
Both are no good reasons to make code more complicated.
|
walther@59814
|
360 |
|
walther@59816
|
361 |
!!! taci list is used in do_next !!!
|
walther@59814
|
362 |
|
wneuper@59574
|
363 |
\begin{itemize}
|
walther@59762
|
364 |
\item xxx
|
walther@59820
|
365 |
\item can lev_on_total replace lev_on ? ..Test_Isac_Short + rename lev_on_total -> lev_on
|
walther@59820
|
366 |
\item xxx
|
walther@59775
|
367 |
\item Step* functions should return Calc.T instead of Chead.calcstate'
|
walther@59762
|
368 |
\item xxx
|
wneuper@59574
|
369 |
\item states.sml: check, when "length tacis > 1"
|
wneuper@59574
|
370 |
\item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
|
wneuper@59574
|
371 |
\item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
|
wneuper@59569
|
372 |
\item xxx
|
walther@59816
|
373 |
\item brute force setting all empty ([], [], ptp) works!?! but ptp causes errors -- investigate!
|
walther@59762
|
374 |
\item xxx
|
wneuper@59573
|
375 |
\end{itemize}
|
wneuper@59574
|
376 |
\<close>
|
wneuper@59574
|
377 |
subsection \<open>Ctree\<close>
|
wneuper@59574
|
378 |
text \<open>
|
walther@59815
|
379 |
analysis
|
walther@59815
|
380 |
# mixture pos' .. pos in cappend_*, append_* is confusing
|
walther@59844
|
381 |
# existpt p pt andalso Tactic.is_empty DIFFERENT IN append_*, cappend_* is confusing
|
walther@59815
|
382 |
"exception PTREE "get_obj: pos =" ^^^^^: ^^^^ due to cut !!!
|
walther@59815
|
383 |
NOTE: exn IN if..andalso.. IS NOT!!! DETECTED, THIS is confusing
|
walther@59815
|
384 |
see test/../--- Minisubpbl/800-append-on-Frm.sml ---
|
walther@59815
|
385 |
# ?!? "cut branches below cannot be decided here" in append_atomic
|
walther@59815
|
386 |
# sign. of functions too different ?!?canonical arg.order ?!?
|
wneuper@59568
|
387 |
\begin{itemize}
|
walther@59807
|
388 |
\item xxx
|
walther@59815
|
389 |
\item remove update_branch, update_*? -- make branch, etc args of append_*
|
walther@59815
|
390 |
\item xxx
|
walther@59816
|
391 |
\item close sig Ctree, contains cappend_* ?only? --- ?make parallel to ?Pide_Store?
|
walther@59813
|
392 |
\item xxx
|
walther@59807
|
393 |
\item unify args to Ctree.state (pt, p)
|
walther@59846
|
394 |
\item fun update_env .. repl_env \<rightarrow>updatempty
|
walther@59807
|
395 |
\item xxx
|
wneuper@59568
|
396 |
\item xxx
|
wneuper@59574
|
397 |
\item xxx
|
walther@59807
|
398 |
\item xxx
|
wneuper@59568
|
399 |
\end{itemize}
|
wneuper@59574
|
400 |
\<close>
|
wneuper@59574
|
401 |
subsection \<open>replace theory/thy by context/ctxt\<close>
|
wneuper@59574
|
402 |
text \<open>
|
wneuper@59574
|
403 |
\begin{itemize}
|
walther@59660
|
404 |
\item xxx
|
walther@59748
|
405 |
\item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
|
walther@59748
|
406 |
special case: Tactic.Refine_Problem
|
walther@59748
|
407 |
\item xxx
|
walther@59748
|
408 |
\item theory can be retrieved from ctxt by Proof_Context.theory_of
|
walther@59660
|
409 |
\item xxx
|
wneuper@59577
|
410 |
\item cleaup the many conversions string -- theory
|
wneuper@59577
|
411 |
\item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
|
wneuper@59574
|
412 |
\item 1. Rewrite.eval_true_, then
|
walther@59823
|
413 |
LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.tac_from_prog.
|
wneuper@59577
|
414 |
\item fun associate
|
walther@59881
|
415 |
let val thy = ThyC.get_theory "Isac_Knowledge";(*TODO*)
|
wneuper@59574
|
416 |
\item xxx
|
wneuper@59574
|
417 |
\item xxx
|
walther@59802
|
418 |
\item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
|
walther@59802
|
419 |
\item push srls into pstate
|
walther@59851
|
420 |
\item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule_Set.Empty)
|
walther@59851
|
421 |
^^^^^^^^^^^^^^^
|
wneuper@59577
|
422 |
\item xxx
|
wneuper@59574
|
423 |
\end{itemize}
|
wneuper@59574
|
424 |
\<close>
|
wneuper@59583
|
425 |
subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
|
wneuper@59574
|
426 |
text \<open>
|
walther@59878
|
427 |
remove refactor Rfuns, Rule.Prog, Rule.Empty_Prog, RrlsState: this is a concept never brought to work.
|
walther@59850
|
428 |
Clarify relation to reverse rewriting!
|
wneuper@59562
|
429 |
\begin{itemize}
|
walther@59850
|
430 |
\item separate mut.recursion program with rule and rls by deleting fild scr in rls
|
walther@59850
|
431 |
(possible since CS 43160c1e775a
|
walther@59850
|
432 |
` "replace Prog. in prep_rls by Auto_Prog.gen, which generates Prog. on the fly" )
|
wneuper@59573
|
433 |
\item xxx
|
wneuper@59569
|
434 |
\item probably only "normal_form" seems to be needed
|
wneuper@59569
|
435 |
\item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
|
wneuper@59569
|
436 |
but that seems desirable
|
wneuper@59569
|
437 |
\item ?how is the relation to reverse-rewriting ???
|
wneuper@59569
|
438 |
\item "Rfuns" markers in test/../rational
|
wneuper@59562
|
439 |
\item xxx
|
walther@59667
|
440 |
\item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
|
wneuper@59573
|
441 |
rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
|
wneuper@59583
|
442 |
Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
|
wneuper@59573
|
443 |
Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
|
wneuper@59573
|
444 |
\item debug ^^^ related: is there an occurence of Steps with more than 1 element?
|
wneuper@59569
|
445 |
\item xxx
|
walther@59760
|
446 |
\item and do_next (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
|
wneuper@59573
|
447 |
\item xxx
|
wneuper@59573
|
448 |
\item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
|
walther@59850
|
449 |
\item xxx
|
walther@59850
|
450 |
\item ?finally Prog could go from Calcelems to ProgLang?
|
wneuper@59562
|
451 |
\end{itemize}
|
wneuper@59574
|
452 |
\<close>
|
wneuper@59574
|
453 |
subsection \<open>Inverse_Z_Transform.thy\<close>
|
wneuper@59574
|
454 |
text \<open>
|
wneuper@59538
|
455 |
\begin{itemize}
|
wneuper@59550
|
456 |
\item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
|
wneuper@59550
|
457 |
? replace rewriting with substitution ?!?
|
wneuper@59537
|
458 |
The problem is related to the decision of typing for "d_d" and making bound variables free (while
|
wneuper@59550
|
459 |
shifting specific handling in equation solving etc. to the meta-logic).
|
wneuper@59550
|
460 |
\item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
|
wneuper@59550
|
461 |
rewrite-rules; see \ref{new-var-rhs}.
|
wneuper@59538
|
462 |
\item Reconsider whole problem:
|
wneuper@59538
|
463 |
input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
|
wneuper@59538
|
464 |
\end{itemize}
|
wneuper@59574
|
465 |
\<close>
|
wneuper@59574
|
466 |
subsection \<open>Adopt Isabelle's numerals for Isac\<close>
|
wneuper@59574
|
467 |
text \<open>
|
wneuper@59540
|
468 |
\begin{itemize}
|
wneuper@59574
|
469 |
\item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
|
wneuper@59574
|
470 |
and have both representations in parallel for "nat".
|
wneuper@59574
|
471 |
\item xxx
|
wneuper@59574
|
472 |
\item xxx
|
wneuper@59540
|
473 |
\end{itemize}
|
wneuper@59574
|
474 |
\<close>
|
walther@59816
|
475 |
subsection \<open>Redesign equation solver\<close>
|
wneuper@59591
|
476 |
text \<open>
|
wneuper@59591
|
477 |
Existing solver is structured along the WRONG assumption,
|
walther@59816
|
478 |
that Poly.thy must be the LAST thy among all thys involved -- while the opposite is the case.
|
wneuper@59591
|
479 |
|
wneuper@59591
|
480 |
Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
|
wneuper@59591
|
481 |
\<close>
|
walther@59816
|
482 |
subsection \<open>Finetunig required for xmldata in kbase\<close>
|
wneuper@59574
|
483 |
text \<open>
|
wneuper@59574
|
484 |
See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
|
wneuper@59574
|
485 |
and in kbase html-representation generated from these xmldata.
|
wneuper@59574
|
486 |
Notes in ~~/xmldata/TODO.txt.
|
wneuper@59574
|
487 |
\<close>
|
wneuper@59574
|
488 |
|
wneuper@59574
|
489 |
section \<open>Hints for further development\<close>
|
wneuper@59574
|
490 |
text \<open>
|
wneuper@59574
|
491 |
\<close>
|
wneuper@59591
|
492 |
subsection \<open>Coding standards & some explanations for math-authors\<close>
|
wneuper@59591
|
493 |
text \<open>copy from doc/math-eng.tex WN.28.3.03
|
wneuper@59591
|
494 |
WN071228 extended\<close>
|
wneuper@59591
|
495 |
|
wneuper@59591
|
496 |
subsubsection \<open>Identifiers\<close>
|
wneuper@59591
|
497 |
text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
|
wneuper@59591
|
498 |
not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
|
wneuper@59591
|
499 |
reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
|
wneuper@59591
|
500 |
problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
|
wneuper@59591
|
501 |
However, all the cases (1)..(4) require different typing for one and the same
|
wneuper@59591
|
502 |
identifier {\tt probe} which is impossible, and actually leads to strange errors
|
wneuper@59591
|
503 |
(for instance (1) is used as string, except in a script addressing a Subproblem).
|
wneuper@59591
|
504 |
|
wneuper@59591
|
505 |
These are the preliminary rules for naming identifiers>
|
wneuper@59591
|
506 |
\begin{description}
|
wneuper@59591
|
507 |
\item [elements of a key] into the hierarchy of problems or methods must not contain
|
wneuper@59591
|
508 |
capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
|
wneuper@59591
|
509 |
\item [descriptions in problem-patterns] must contain at least 1 capital letter and
|
wneuper@59591
|
510 |
must not contain underscores, e.g. {\tt Probe, forPolynomials}.
|
wneuper@59591
|
511 |
\item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
|
wneuper@59591
|
512 |
beware of conflicts~!
|
wneuper@59591
|
513 |
\item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
|
wneuper@59591
|
514 |
\item [???] ???
|
wneuper@59591
|
515 |
\item [???] ???
|
wneuper@59591
|
516 |
\end{description}
|
wneuper@59591
|
517 |
%WN071228 extended\<close>
|
wneuper@59591
|
518 |
|
wneuper@59591
|
519 |
subsubsection \<open>Rule sets\<close>
|
wneuper@59591
|
520 |
text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
|
wneuper@59591
|
521 |
where it can be viewed using the knowledge browsers.
|
wneuper@59591
|
522 |
|
wneuper@59591
|
523 |
There are rulesets visible to the student, and there are rulesets visible (in general) only for
|
wneuper@59591
|
524 |
math authors. There are also rulesets which {\em must} exist for {\em each} theory;
|
wneuper@59591
|
525 |
these contain the identifier of the respective theory (including all capital letters)
|
wneuper@59591
|
526 |
as indicated by {\it Thy} below.
|
wneuper@59591
|
527 |
|
wneuper@59591
|
528 |
\begin{description}
|
wneuper@59591
|
529 |
\item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
|
wneuper@59591
|
530 |
normalform for all terms which can be expressed by the definitions of the respective theory
|
wneuper@59591
|
531 |
(and the respective parents).
|
wneuper@59591
|
532 |
\item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
|
wneuper@59591
|
533 |
which can be expressed by the definitions of the respective theory (and the respective parents)
|
wneuper@59591
|
534 |
such, that the rewrites can be presented to the student.
|
wneuper@59591
|
535 |
\item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
|
wneuper@59591
|
536 |
numerical constants only (i.e. all terms which can be expressed by the definitions of
|
wneuper@59591
|
537 |
the respective theory and the respective parent theories). In particular, this ruleset includes
|
wneuper@59591
|
538 |
evaluating in/equalities with numerical constants only.
|
wneuper@59591
|
539 |
WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
|
wneuper@59591
|
540 |
are logically equivalent, where the latter often add to the assumptions
|
wneuper@59591
|
541 |
(e.g. in Check_elementwise).
|
wneuper@59591
|
542 |
\end{description}
|
wneuper@59591
|
543 |
|
wneuper@59591
|
544 |
The above rulesets are all visible to the user, and also may be input;
|
wneuper@59591
|
545 |
thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
|
wneuper@59591
|
546 |
KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
|
wneuper@59591
|
547 |
using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
|
wneuper@59591
|
548 |
The following rulesets are used for internal purposes and usually invisible to the (naive) user:
|
wneuper@59591
|
549 |
|
wneuper@59591
|
550 |
\begin{description}
|
wneuper@59591
|
551 |
\item [*\_erls] TODO
|
wneuper@59591
|
552 |
\item [*\_prls]
|
wneuper@59591
|
553 |
\item [*\_srls]
|
wneuper@59591
|
554 |
\end{description}
|
walther@59852
|
555 |
{\tt Rule_Set.append_rules, Rule_Set.merge, remove_rls} TODO
|
wneuper@59591
|
556 |
\<close>
|
wneuper@59591
|
557 |
|
wneuper@59574
|
558 |
subsection \<open>get proof-state\<close>
|
wneuper@59574
|
559 |
text \<open>
|
wneuper@59574
|
560 |
Re: [isabelle] Programatically get "this"
|
wneuper@59574
|
561 |
----------------------------------------------------
|
wneuper@59574
|
562 |
So here is my (Makarius') version of your initial example, following these principles:
|
wneuper@59574
|
563 |
begin{verbatim}
|
wneuper@59574
|
564 |
notepad
|
wneuper@59574
|
565 |
begin
|
wneuper@59574
|
566 |
assume a: A
|
wneuper@59574
|
567 |
ML_val \<open>
|
wneuper@59574
|
568 |
val ctxt = @{context};
|
wneuper@59558
|
569 |
|
wneuper@59574
|
570 |
val this_name =
|
walther@59748
|
571 |
Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN);
|
wneuper@59574
|
572 |
val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
|
wneuper@59574
|
573 |
\<close>
|
wneuper@59574
|
574 |
end
|
wneuper@59574
|
575 |
end{verbatim}
|
wneuper@59574
|
576 |
\<close>
|
wneuper@59574
|
577 |
subsection \<open>write Specification to jEdit\<close>
|
wneuper@59574
|
578 |
text \<open>
|
wneuper@59574
|
579 |
Re: [isabelle] Printing terms with type annotations
|
wneuper@59574
|
580 |
----------------------------------------------------
|
wneuper@59574
|
581 |
On 06/02/2019 17:52, Moa Johansson wrote:
|
wneuper@59574
|
582 |
>
|
wneuper@59574
|
583 |
> I’m writing some code that should create a snippet of Isar script.
|
wneuper@59574
|
584 |
|
wneuper@59574
|
585 |
This is how Sledgehammer approximates this:
|
wneuper@59574
|
586 |
|
wneuper@59574
|
587 |
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
|
wneuper@59574
|
588 |
|
wneuper@59574
|
589 |
(The module name already shows that the proper terminology is "Isar
|
wneuper@59574
|
590 |
proof" (or "Isar proof text"). Proof scripts are a thing from the past,
|
wneuper@59574
|
591 |
before Isar. You can emulate old-style proof scripts via a sequence of
|
wneuper@59574
|
592 |
'apply' commands, but this is improper Isar.)
|
wneuper@59574
|
593 |
|
wneuper@59574
|
594 |
Note that there is no standard function in Isabelle/Pure, because the
|
wneuper@59574
|
595 |
problem to print just the right amount of type information is very
|
wneuper@59574
|
596 |
complex and not fully solved. One day, after 1 or 2 rounds of
|
wneuper@59574
|
597 |
refinements over the above approach, it might become generally available.
|
wneuper@59574
|
598 |
\<close>
|
wneuper@59574
|
599 |
subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
|
wneuper@59574
|
600 |
text \<open>
|
wneuper@59574
|
601 |
isabelle update -u path_cartouches
|
wneuper@59574
|
602 |
isabelle update -u inner_syntax_cartouches
|
wneuper@59574
|
603 |
\<close>
|
wneuper@59582
|
604 |
section \<open>Questions to Isabelle experts\<close>
|
wneuper@59582
|
605 |
text \<open>
|
wneuper@59582
|
606 |
\begin{itemize}
|
walther@59848
|
607 |
\item ad ERROR Undefined fact "all_left" in Test_Isac: error-pattern.sml
|
walther@59848
|
608 |
Undefined fact: "xfoldr_Nil" inssort.sml
|
walther@59886
|
609 |
(* probably two different reasons:
|
walther@59886
|
610 |
src/../LinEq.thy
|
walther@59886
|
611 |
(*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
|
walther@59886
|
612 |
all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
|
walther@59886
|
613 |
|
walther@59886
|
614 |
src/../PolyEq.thy
|
walther@59886
|
615 |
(*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
|
walther@59886
|
616 |
all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
|
walther@59886
|
617 |
|
walther@59886
|
618 |
test/../partial_fractions.sml
|
walther@59886
|
619 |
(*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
|
walther@59886
|
620 |
(*[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)"))*)
|
walther@59886
|
621 |
|
walther@59886
|
622 |
test/../mathengine-stateless.sml
|
walther@59886
|
623 |
(*if ThmC.string_of_thm @ {thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
|
walther@59886
|
624 |
then () else error "string_of_thm changed";*)
|
walther@59886
|
625 |
|
walther@59886
|
626 |
(*---------------------------------------------------------------------------------------------*)
|
walther@59886
|
627 |
src/../LinEq.thy
|
walther@59886
|
628 |
primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
|
walther@59886
|
629 |
xfoldr_Nil: "xfoldr f {|| ||} = id" |
|
walther@59886
|
630 |
xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
|
walther@59886
|
631 |
|
walther@59886
|
632 |
src/../InsSort.thy
|
walther@59886
|
633 |
srls = Rule_Set.empty, calc = [], rules = [
|
walther@59886
|
634 |
Rule.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
|
walther@59886
|
635 |
*)
|
walther@59841
|
636 |
\item xxx
|
walther@59841
|
637 |
\item xxx
|
walther@59842
|
638 |
\item ?OK Test_Isac_Short with
|
walther@59842
|
639 |
LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
|
walther@59842
|
640 |
instead
|
walther@59846
|
641 |
LI.by_tactic tac (Istate.empty, ContextC.empty) ptp
|
walther@59842
|
642 |
in step-solve ?
|
walther@59842
|
643 |
\item xxx
|
walther@59842
|
644 |
\item test from last CS with outcommented re-def of code ->
|
walther@59842
|
645 |
-> \<open>further tests additional to src/.. files\<close>
|
walther@59842
|
646 |
ADDTESTS/redefined-code.sml
|
walther@59841
|
647 |
\item xxx
|
walther@59841
|
648 |
\item efb749b79361 Test_Some_Short.thy has 2 errors, which disappear in thy ?!?:
|
walther@59841
|
649 |
ML_file "Interpret/error-pattern.sml" Undefined fact: "all_left"
|
walther@59841
|
650 |
ML_file "Knowledge/inssort.sml" Undefined fact: "xfoldr_Nil"
|
walther@59841
|
651 |
\item xxx
|
wneuper@59591
|
652 |
\item what is the actual replacement of "hg log --follow" ?
|
wneuper@59591
|
653 |
\item xxx
|
wneuper@59582
|
654 |
\item how HANDLE these exceptions, e.g.:
|
wneuper@59582
|
655 |
Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
|
wneuper@59582
|
656 |
GIVES
|
wneuper@59582
|
657 |
"Inner syntax error
|
wneuper@59582
|
658 |
Failed to parse term"
|
wneuper@59582
|
659 |
\item xxx
|
walther@59734
|
660 |
\item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"
|
walther@59734
|
661 |
e.g. in test/Interpret/lucas-interpreter.sml
|
wneuper@59582
|
662 |
\item xxx
|
wneuper@59582
|
663 |
\item xxx
|
wneuper@59582
|
664 |
\end{itemize}
|
wneuper@59582
|
665 |
\<close>
|
wneuper@59582
|
666 |
|
wneuper@59574
|
667 |
section \<open>For copy & paste\<close>
|
wneuper@59574
|
668 |
text \<open>
|
wneuper@59582
|
669 |
\begin{itemize}
|
walther@59778
|
670 |
\item xxx
|
wneuper@59558
|
671 |
\begin{itemize}
|
wneuper@59558
|
672 |
\item xxx
|
wneuper@59540
|
673 |
\begin{itemize}
|
wneuper@59558
|
674 |
\item xxx
|
wneuper@59540
|
675 |
\begin{itemize}
|
wneuper@59558
|
676 |
\item xxx
|
wneuper@59574
|
677 |
\begin{itemize}
|
wneuper@59574
|
678 |
\item xxx
|
wneuper@59574
|
679 |
\end{itemize}
|
wneuper@59540
|
680 |
\end{itemize}
|
wneuper@59540
|
681 |
\end{itemize}
|
wneuper@59504
|
682 |
\end{itemize}
|
wneuper@59504
|
683 |
\end{itemize}
|
wneuper@59504
|
684 |
\<close>
|
wneuper@59574
|
685 |
subsection \<open>xxx\<close>
|
wneuper@59574
|
686 |
subsubsection \<open>xxx\<close>
|
neuper@52150
|
687 |
end
|