|
1 (*<*) |
|
2 (*%:wrap=soft:maxLineLen=78:*) |
|
3 (*partially copied from |
|
4 ~/material/texts/emat/lucin-isa/paper-isabisac/Lucin_Isa_IJCAR.thy *) |
|
5 theory Lucas_Interpreter |
|
6 imports "~~/src/Tools/isac/Interpret/Interpret" |
|
7 begin |
|
8 ML \<open> |
|
9 open LI |
|
10 open Istate |
|
11 open TermC |
|
12 \<close> |
|
13 (*>*) |
|
14 |
|
15 text \<open> |
|
16 \section{Lucas--Interpretation (\LI)}\label{lucin} |
|
17 %============================================================================= |
|
18 The interpreter is named after the inventor of top-down-parsing in the ALGOL |
|
19 project~\cite{pl:formal-lang-hist}, Peter Lucas. As a dedicated expert in |
|
20 programming languages he initially objected ``yet another programming |
|
21 language'' (in analogy to ``Yacc'' \cite{Yacc-1975}), but then he helped to |
|
22 clarify the unusual requirements for a novel programming language in the |
|
23 \sisac-project, which later led to the notion of \LI. |
|
24 |
|
25 \LI{} is the most prominent component in a prototype developed in the |
|
26 \sisac-project, there embedded in a mathematics-engine, which interacts with a |
|
27 dialogue-module in a Java-based front-end managing interaction with students |
|
28 (out of scope of this paper). |
|
29 |
|
30 \subsection{The Concept of \LI}\label{concept-LI} |
|
31 %----------------------------------------------------------------------------- |
|
32 The concept of \LI{} is simple: \LI{} \emph{acts as a debugger on functional |
|
33 programs with hard-coded breakpoints, where control is handed over to a |
|
34 student; a student, however, does \emph{not} interact with the software |
|
35 presenting the program, but with the software presenting steps of forward |
|
36 reasoning, where the steps are rigorously constructed by tactics acting as the |
|
37 break-points mentioned}. Following the \LI{} terminology, we will call |
|
38 ``programs'' the functions defined with the function package and refer to |
|
39 their evaluation as ``execution''. |
|
40 |
|
41 \paragraph{Types occurring in the signatures} of \LI{} are as follows. Besides |
|
42 the program of type @{ML_type Program.T} there is an interpreter state |
|
43 @{ML_type Istate.T}, a record type passing data from one step of execution to |
|
44 the next step, in particular a location in the program, where the next step |
|
45 will be read off, and an environment for evaluating the step. |
|
46 As invisible in the program language as the interpreter state is @{ML_type |
|
47 Calc.T}, a ``calculation'' as a sequence of steps in forward reasoning, a |
|
48 variant of ``structured derivations'' \cite{back-SD-2010}. Visible in the |
|
49 language and in the signature, however, are the tactics @{ML_type Tactic.T}, |
|
50 which create steps in a calculation. |
|
51 |
|
52 Novel in connection with calculations is the idea to maintain a logical |
|
53 context in order to provide automated provers with data required for checking |
|
54 input by the student. Isabelle's @{ML_type Proof.context}, as is, turned out |
|
55 perfect for this task~\cite{mlehnf:bakk-11}. |
|
56 |
|
57 \paragraph{The signatures of the main functions,} the functions @{term |
|
58 find_next_step}, \\@{term locate_input_tactic} and @{term locate_input_term}, |
|
59 are as follows:\label{sig-lucin} |
|
60 \<close> |
|
61 (*<*)ML(*>*) \<open> |
|
62 signature LUCAS_INTERPRETER = |
|
63 sig |
|
64 datatype next_step_result = |
|
65 Next_Step of Istate.T * Proof.context * Tactic.T |
|
66 | Helpless | End_Program of Istate.T * Tactic.T |
|
67 val find_next_step: Program.T -> Calc.T -> Istate.T -> Proof.context |
|
68 -> next_step_result |
|
69 |
|
70 datatype input_tactic_result = |
|
71 Safe_Step of Istate.T * Proof.context * Tactic.T |
|
72 | Unsafe_Step of Istate.T * Proof.context * Tactic.T |
|
73 | Not_Locatable of message |
|
74 val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context |
|
75 -> Tactic.T -> input_tactic_result |
|
76 |
|
77 datatype input_term_result = |
|
78 Found_Step of Calc.T | Not_Derivable |
|
79 val locate_input_term: Calc.T -> term -> input_term_result |
|
80 end |
|
81 \<close> |
|
82 text \<open> |
|
83 \begin{description} |
|
84 \item[@{term find_next_step}] accomplishes what usually is expected from a |
|
85 @{ML_type Program.T}: find a @{term Next_Step} to be executed, in the case of |
|
86 \LI{} to be inserted into a \texttt{\small Calc.T} under construction. This |
|
87 step can be a @{ML_type Tactic.T}, directly found in @{term next_step_result}, |
|
88 or a @{ML_type term} produced by applying the tactic. If such a step cannot be |
|
89 found (due to previous student interaction), \LI{} is @{term Helpless}. |
|
90 |
|
91 \item[@{term locate_input_tactic}] gets a @{ML_type Tactic.T} as argument |
|
92 (which has been input and checked applicable in @{ML_type Calc.T}) and tries |
|
93 to locate it in the \texttt{Prog.T} such that a @{term Next_Step} can be |
|
94 generated from the subsequent location in the @{ML_type Program.T}. A step can |
|
95 be an @{term Unsafe_Step}, if the input @{ML_type Tactic.T} cannot safely be |
|
96 associated with any tactic in the @{ML_type Program.T}. This function has a |
|
97 signature similar to @{term find_next_step} (here the respective input |
|
98 @{ML_type Tactic.T} and the one in the result are the same) in order to unify |
|
99 internal technicalities of \LI{}. |
|
100 |
|
101 \item[@{term locate_input_term}] tries to find a derivation from the current |
|
102 @{ML_type Proof.context} for the term input to @{ML_type Calc.T} and to locate |
|
103 a \texttt{Tactic.T} in the @{ML_type Program.T}, which as @{term Found_Step} |
|
104 allows to find a next step later. Such a @{term Found_Step} can be located in |
|
105 another program (a sub-program or a calling program); thus @{ML_type |
|
106 Program.T}, @{ML_type Istate.T} and @{ML_type Proof.context} are packed into |
|
107 @{ML_type Calc.T} at appropriate positions and do not show up in the |
|
108 signature. |
|
109 \end{description} |
|
110 |
|
111 Automated reasoning is concern of the third function @{term |
|
112 locate_input_term}, actually a typical application case for Isabelle's |
|
113 Sledgehammer~\cite{sledgehammer-tutorial}, but not yet realised and |
|
114 preliminarily substituted by \sisac's simplifier. @{term locate_input_term} is |
|
115 the function used predominantly in interaction with students: these input term |
|
116 by term into the calculation under construction (as familiar from |
|
117 paper\&pencil work) and \LI{} checks for correctness automatically. |
|
118 \<close> |
|
119 text \<open> |
|
120 \subsection{Examples for \LI}\label{expl-lucin} |
|
121 %----------------------------------------------------------------------------- |
|
122 \LI's novel concept relating program execution with construction of |
|
123 calculations is best demonstrated by examples. The first one is from |
|
124 structural engineering given by the following problem statement:\\ |
|
125 \medskip |
|
126 |
|
127 % first column |
|
128 \begin{minipage}{0.55\textwidth} |
|
129 \textit{Determine the bending line of a beam of length $L$, |
|
130 which consists of homogeneous material, which is clamped on one side |
|
131 and which is under constant line load $q_0$; see the Figure right.}\\ |
|
132 \end{minipage} |
|
133 \hfill |
|
134 %second column |
|
135 \begin{minipage}{0.42\textwidth} |
|
136 \includegraphics[width=0.6\textwidth]{bend-7-70-en.png}\\ |
|
137 \end{minipage} |
|
138 |
|
139 \medskip |
|
140 This problem is solved by the following program, which is shown by a |
|
141 screen-shot\footnote{The corresponding code is at |
|
142 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/Knowledge/Biegelinie.thy\#l174}. |
|
143 %When inner syntax double-quotes are discontinued eventually, the inner syntax |
|
144 of the HOL library may use double quotes for char/string literals, instead of |
|
145 slightly odd double single-quotes. |
|
146 } |
|
147 in order to demonstrate the colouring helpful for programmers (compare the old |
|
148 bare string version in \cite[p.~92]{wn:proto-sys}). |
|
149 \begin{figure} [htb] |
|
150 \centering |
|
151 \includegraphics[width=\textwidth]{fun-pack-biegelinie-2.png} |
|
152 \caption{The program implemented by the function package} |
|
153 \label{fig:fun-pack-biegelinie} |
|
154 \end{figure} |
|
155 The program is implemented as a @{theory_text partial_function}: it calculates |
|
156 results for a whole class of problems and termination cannot be proven in such |
|
157 generality, although preconditions guard execution. |
|
158 % |
|
159 The program reflects a ``divide \& conquer'' strategy by calling three @{term |
|
160 SubProblem}s. It was implemented for field-tests in German-speaking countries, |
|
161 so arguments of the @{term SubProblem}s are in German, because they appear in |
|
162 the calculation as well. The third @{term SubProblem} adopts the format from |
|
163 Computer Algebra. The calculation, if finished successfully, looks as follows |
|
164 (a screen-shot of intermediate steps on the prototype's front-end is shown in |
|
165 \cite[p.~97]{wn:proto-sys}):\label{biegel_calc} |
|
166 {\footnotesize\begin{tabbing} |
|
167 123\=12\=12\=12\=12\=12\=12\=123\=123\=123\=123\=\kill |
|
168 01\> Problem (Biegelinie, [Biegelinien]) \\ |
|
169 02\>\> Specification: \\ |
|
170 03\>\> Solution: \\ |
|
171 04\>\>\> Problem (Biegelinie, [vonBelastungZu, Biegelinien]) \\ |
|
172 05\>\>\> $[$\>$V\,x = c + -1\cdot q_0\cdot x, $\\ |
|
173 06\>\>\> \>$M_b\,x = c_2 + c\cdot x + \frac{-1\cdot q_0}{2\cdot x ^ 2}, $\\ |
|
174 07\>\>\> \>$\frac{d}{dx}y\,x = c_3 + \frac{-1}{EI} \cdot (c_2\cdot x + |
|
175 \frac{c}{2\cdot x ^ 2} + \frac{-1\cdot q_0}{6\cdot x ^ 3}, $\\ |
|
176 08\>\>\> \>$y\,x = c_4 + c_3\cdot x + \frac{-1}{EI} \cdot |
|
177 (\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot |
|
178 q_0}{24}\cdot x ^ 4)\;\;]$ \\ |
|
179 09\>\>\> Problem (Biegelinie, [setzeRandbedingungen, Biegelinien])\\ |
|
180 10\>\>\> $[$\>$L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L \cdot c + |
|
181 -1 \dot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;]$\\ |
|
182 11\>\>\> solveSystem $(L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L |
|
183 \cdot c + -1 \cdot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;],\; [c, c_2, |
|
184 c_3, c_4])$\\ |
|
185 12\>\>\> $[$\>$c = L \cdot q_0 ,\; c_2 = \frac{-1 \cdot L ^ 2 \cdot q_0}{2},\; |
|
186 c_3 = 0,\; c_4 = 0]$\\ |
|
187 13 \` Take $y\,x = c_4 + c_3\cdot x + \frac{-1}{EI} \cdot |
|
188 (\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot |
|
189 q_0}{24}\cdot x ^ 4)$ \\ |
|
190 |
|
191 14\>\>\> $y\,x = c_4 + c_3 \cdot x + \frac{-1}{EI} \cdot (\frac{c_2}{2} \cdot |
|
192 x ^ 2 + \frac{c}{6} \cdot x ^ 3 + \frac{-1 \cdot q_0}{24} \cdot x ^ 4)$\\ |
|
193 15 \` Substitute $[c,c_2,c_3,c_4]$ \\ |
|
194 |
|
195 16\>\>\> $y\,x = 0 + 0 \cdot x + \frac{-1}{EI} \cdot (\frac{\frac{-1 \cdot L ^ |
|
196 2 \cdot q_0}{2}}{2} \cdot x ^ 2 + \frac{L \cdot q_0}{6} \cdot x ^ 3 + \frac{-1 |
|
197 \cdot q_0}{24} \cdot x ^ 4)$\label{exp-biegel-Substitute}\\ |
|
198 17 \` Rewrite\_Set\_Inst $([({\it bdv},x)], {\it make\_ratpoly\_in})$ \\ |
|
199 |
|
200 18\>\>\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L |
|
201 \cdot q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$\\ |
|
202 19\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L \cdot |
|
203 q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$ |
|
204 \end{tabbing}} |
|
205 The calculation is what a student interacts with. Above the \texttt{\small |
|
206 Specification} is folded in, the specification phase and respective user |
|
207 interaction is skipped here. The \texttt{\small Solution} must be constructed |
|
208 step-wise line by line (while the line numbers do not belong to the |
|
209 calculation) in forward reasoning. |
|
210 \label{1-2-3}A student inputs either (1) a term (displayed on the left above |
|
211 with indentations) or (2) a tactic (shifted to the right margin). If the |
|
212 student gets stuck (3) a next step (as a term or a tactic) is suggested by |
|
213 \LI{}, which works behind the scenes; the corresponding functions have been |
|
214 introduced in \S\ref{concept-LI} (for (1) @{term locate_input_term}, (2) |
|
215 @{term locate_input_tactic} and for (3) @{term find_next_step}). |
|
216 |
|
217 \medskip |
|
218 This example hopefully clarifies the relation between program and calculation |
|
219 in \LI{}: execution of the program stops at tactics (above called |
|
220 break-points), displays the tactic or the result produced by the tactic (as |
|
221 decided by the dialogue-module) in the calculation under construction, hands |
|
222 over control to the student working on the calculation and resumes checking |
|
223 user input. |
|
224 |
|
225 \paragraph{A typical example from Computer Algebra}\label{expl-rewrite} shall |
|
226 shed light on a notions introduced later, on tacticals. The program in |
|
227 Fig.\ref{fig:fun-pack-diff} %on p.\pageref{fig:fun-pack-diff} |
|
228 simplifies rational terms (typed as ``real'' due to limited development |
|
229 resources): |
|
230 \begin{figure} [htb] |
|
231 \centering |
|
232 \includegraphics[width=0.95\textwidth]{fun-pack-simplify.png} |
|
233 %\includegraphics[width=0.85\textwidth]{fig/scrshot/fun-pack/fun-pack-diff.png} |
|
234 \caption{Simplification implemented by the function package} |
|
235 \label{fig:fun-pack-diff} |
|
236 \end{figure} |
|
237 |
|
238 The program executes the tactic @{const Rewrite'_Set}\footnote{Isabelle's |
|
239 document preparation system preserves the apostroph from the definition, while |
|
240 Isabelle's pretty printer drops it in the presentation of the program as |
|
241 above.} |
|
242 with different canonical term rewriting systems (called ``rule sets'' in |
|
243 \sisac) guided by tacticals. The output (disregarding user interaction) is a |
|
244 calculation with steps of simplification, where the steps are created by |
|
245 @{const Rewrite'_Set}. |
|
246 |
|
247 Chained functions (by \texttt{\small \#>}) %TODO which antiquot? |
|
248 are applied curried to @{ML_type term}. The initial part of the chain, from |
|
249 \texttt{\small ''discard\_minus''} to \texttt{\small ''cancel''} does |
|
250 preprocessing, for instance replaces $\;a - b\;$ by $\;a + (-b)\;$ in |
|
251 \texttt{\small ''discard\_minus''} for reducing |
|
252 the number of theorems to be used in simplification. |
|
253 % |
|
254 The second chain of @{const Rewrite'_Set} is @{const Repeat}ed until no |
|
255 further rewrites are possible; this is necessary in case of nested fractions. |
|
256 |
|
257 In cases like the one above, a confluent and terminating term rewrite system, |
|
258 not only \emph{all} correct input terms are accepted, but also \emph{all} |
|
259 incorrect input is rejected as @{term Not_Derivable} by the function @{term |
|
260 locate_input_term}. |
|
261 |
|
262 |
|
263 \section{Adaptation of Isabelle's Functions}\label{lucin-funpack} |
|
264 %============================================================================= |
|
265 Isabelle's function package presents functions in ``inner syntax'' to users, |
|
266 i.e. as terms in Isabelle/HOL. The \LI{} design recognised these terms |
|
267 suitable for parse trees of programs, Isabelle realised the same idea in a |
|
268 more general way with the function package a few years later --- so migration |
|
269 from \sisac's programs to Isabelle's functions was surprisingly easy. The main |
|
270 features required were tactics, tacticals and program expressions as described |
|
271 below. |
|
272 |
|
273 \subsection{Tactics Creating Steps in Calculations}\label{tactics} |
|
274 %----------------------------------------------------------------------------- |
|
275 The examples in the previous section showed how tactics in programs create |
|
276 steps in calculations. Tactics in programs are defined as follows\footnote{ |
|
277 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/Prog_Tac.thy\#l36}} |
|
278 : |
|
279 \<close> |
|
280 consts |
|
281 Calculate :: "[char list, 'a] => 'a" |
|
282 Rewrite :: "[char list, 'a] => 'a" |
|
283 Rewrite'_Inst :: "[(char list * 'a) list, char list, 'a] => 'a" |
|
284 Rewrite'_Set :: "[char list, 'a] => 'a" |
|
285 Rewrite'_Set'_Inst :: "[((char list) * 'a) list, char list, 'a] => 'a" |
|
286 Or'_to'_List :: "bool => 'a list" |
|
287 SubProblem :: |
|
288 "[char list * char list list * char list list, arg list] => 'a" |
|
289 Substitute :: "[bool list, 'a] => 'a" |
|
290 Take :: "'a => 'a" |
|
291 |
|
292 text \<open> |
|
293 These tactics transform a term of some type @{typ "'a"} to a resulting term of |
|
294 the same type. @{const[names_short] Calculate} applies operators like $+,-,*$ |
|
295 as @{typ "char list"} (i.e. a string in inner syntax) to numerals of type |
|
296 @{typ "'a"}. The tactics beginning with @{const[names_short] Rewrite} do |
|
297 exactly what they indicate by applying a theorem (in the program given by type |
|
298 @{typ "char list"}) or a list of theorems, called ``rule-set''. The |
|
299 corresponding \texttt{\small \_Inst} variants instantiate bound variables with |
|
300 respective constants before rewriting (this is due to the user requirement, |
|
301 that terms in calculations are close to traditional notation, which excludes |
|
302 $\lambda$-terms), for instance modelling bound variables in equation solving. |
|
303 @{const[names_short] Or'_to'_List} is due to a similar requirement: logically |
|
304 appropriate for describing solution sets in equation solving are equalities |
|
305 connected by $\land,\lor$, but traditional notation uses sets (and these are |
|
306 still lists for convenience). @{const[names_short] SubProblem}s not only take |
|
307 arguments (@{typ "arg list"} like any (sub-)program, but also three references |
|
308 into \sisac's knowledge base (theory, formal specification, method) for |
|
309 guided interaction in the specification phase. |
|
310 |
|
311 Tactics appear simple: they operate on terms adhering to one type --- |
|
312 different types are handled by different tactics and (sub-) programs; and they |
|
313 cover only basic functionality --- but they operate on terms, which are well |
|
314 tooled by Isabelle and which can contain functions evaluated as program |
|
315 expressions introduced in the next but one subsection. |
|
316 |
|
317 Section \S\ref{expl-lucin} showed how tactics can be input by students. So |
|
318 tactics in programs have analogies for user input with type @{ML_type |
|
319 Tactic.input} defined at\footnote{ |
|
320 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/MathEngBasic/tactic-def.sml\#l122}}. These tactics also cover the specification phase (wich is out of scope of the |
|
321 paper). And there is another @{ML_type Tactic.T} defined at\footnote{ |
|
322 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/MathEngBasic/tactic-def.sml\#l241}} for internal use by the mathematics-engine, which already appeared in the |
|
323 signature of Lucas-Interpretation on p.\pageref{sig-lucin}. |
|
324 |
|
325 \subsection{Tacticals Guiding Flow of Execution}\label{tacticals} |
|
326 %----------------------------------------------------------------------------- |
|
327 The example on p.\pageref{expl-rewrite} for canonical rewriting showed, how |
|
328 tacticals guide the flow of execution. The complete list of tacticals is as |
|
329 follows. |
|
330 \<close> |
|
331 consts |
|
332 Chain :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10) |
|
333 If :: "[bool, 'a => 'a, 'a => 'a, 'a] => 'a" |
|
334 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10) |
|
335 Repeat :: "['a => 'a, 'a] => 'a" |
|
336 Try :: "['a => 'a, 'a] => 'a" |
|
337 While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9) |
|
338 |
|
339 text \<open> |
|
340 \texttt{\small Chain} is forward application of functions and made an infix |
|
341 operator @{const[names_short] Chain}; @{const[names_short] If} decides by |
|
342 @{typ bool}en expression for execution of one of two arguments of type @{typ |
|
343 "'a => 'a"} (which can be combinations of tacticals or tactics); |
|
344 @{const[names_short] Or} decides on execution of one of the arguments |
|
345 depending of applicability of tactics; @{const[names_short] Repeat} is a one |
|
346 way loop which terminates, if the argument is not applicable (e.g. |
|
347 applicability of a theorem for rewriting on a term) any more; |
|
348 @{const[names_short] Try} skips the argument if not applicable and |
|
349 @{const[names_short] While} is a zero way loop as usual. |
|
350 |
|
351 \subsection{Program Expressions to be Evaluated}\label{prog-expr} |
|
352 %----------------------------------------------------------------------------- |
|
353 Some tacticals, \texttt{If} and \texttt{While}, involve boolean expressions, |
|
354 which need to be evaluated: such expressions denote another element of |
|
355 programs. This kind of element has been shown in the example on |
|
356 p.\pageref{fig:fun-pack-biegelinie} as argument of @{const[names_short] |
|
357 Take}: sometimes it is necessary to pick parts of elements of a calculation, |
|
358 for instance the last element from a list. So Isabelle's @{theory_text List} |
|
359 is adapted for \sisac's purposes in @{theory_text ListC}\footnote{ |
|
360 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/ListC.thy}}. |
|
361 % |
|
362 Such expressions are substituted from the environment in @{ML_type Istate.T}, |
|
363 evaluated to terms by rewriting (and for that purpose using the same rewrite |
|
364 engine as for the tactics @{const[names_short] Rewrite}*) and marked by the |
|
365 constructor @{term Term_Val} which is introduced below. |
|
366 |
|
367 |
|
368 \section{Implementation of \LI}\label{LI-impl} |
|
369 %============================================================================= |
|
370 The implementation of the interpreter is as experimental as is the respective |
|
371 programming language introduced in the previous section. So below there will |
|
372 be particularly such implementation details, which are required for discussing |
|
373 open design \& implementation issues. |
|
374 |
|
375 All of the function package's syntactic part plus semantic markup is perfect |
|
376 for \LI. The evaluation part of the function package, however, implements |
|
377 automated evaluation in one go and automated |
|
378 code-generation~\cite{code-gen-tutorial} --- both goals are not compatible |
|
379 with \sisac's goal to feature step-wise construction of calculations, so this |
|
380 part had to be done from scratch. |
|
381 |
|
382 |
|
383 \subsection{Scanning the Parse Tree}\label{scanning} |
|
384 %----------------------------------------------------------------------------- |
|
385 Isabelle's function package parses the program body from function definitions |
|
386 to terms, the data structure of simply typed $\lambda$ terms, which also |
|
387 encode the objects of proofs. Thus there is a remarkable collection of tools, |
|
388 readily available in Isabelle; but this collection does not accommodate the |
|
389 requirement of scanning a term to a certain location, remembering the location |
|
390 and returning there later, as required by \LI. So this has been introduced |
|
391 \<close> |
|
392 (*<*)ML(*>*) \<open> |
|
393 datatype lrd = L | R | D |
|
394 type path = lrd list |
|
395 \<close> |
|
396 (*<*)ML \<open> |
|
397 open TermC (*avoids type clashes below from the new typ above*) |
|
398 \<close> |
|
399 ML(*>*) \<open> |
|
400 fun at_location [] t = t |
|
401 | at_location (D :: p) (Abs(_, _, body)) = at_location p body |
|
402 | at_location (L :: p) (t1 $ _) = at_location p t1 |
|
403 | at_location (R :: p) (_ $ t2) = at_location p t2 |
|
404 | at_location l t = |
|
405 raise TERM ("at_location: no " ^ string_of_path l ^ " for ", [t]); |
|
406 \<close> |
|
407 text \<open> |
|
408 with a @{term path} to a location according to the term constructors |
|
409 \texttt{\small \$} and @{term Abs}. This is an implementation detail; an |
|
410 abstract, denotational view starts with this datatype |
|
411 \<close> |
|
412 (*<*)ML(*>*) \<open> |
|
413 datatype expr_val = |
|
414 Term_Val of term | Reject_Tac |
|
415 | Accept_Tac of Istate.pstate * Proof.context * Tactic.T |
|
416 \<close> |
|
417 text \<open> |
|
418 which models the meaning of an expression in the parse-tree: this is either a |
|
419 @{term Term_Val}ue (introduced in \S\ref{prog-expr}) or a tactic (introduced |
|
420 in \S\ref{tactics}); the latter is either accepted by @{term Accept_Tac} or |
|
421 rejected by @{term Reject_Tac}; an error value is still missing. |
|
422 % |
|
423 The arguments of the above constant @{term Accept_Tac} are the same as |
|
424 introduced for \LI{} in \S\ref{concept-LI}. Thus @{ML_type expr_val} is the |
|
425 return value for functions scanning the parse-tree for an acceptable tactic: |
|
426 \<close> |
|
427 (*<*)ML \<open> |
|
428 open LI (*avoids type clashes below from the new typ above*) |
|
429 \<close> |
|
430 ML(*>*) \<open> |
|
431 scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val; |
|
432 scan_dn: Calc.T * Proof.context -> Istate.pstate -> term -> expr_val; |
|
433 go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val; |
|
434 scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val; |
|
435 check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> |
|
436 expr_val; |
|
437 \<close> |
|
438 text \<open> |
|
439 The first argument of each function above, if of type @{ML_type term}, is the |
|
440 whole program. It is not required by @{term scan_dn}, simple top-down |
|
441 scanning, and by @{term check_tac}, if a tactic has been reached. The |
|
442 rightmost argument, if of type @{ML_type term}, serves matching as shown |
|
443 later. @{term scan_to_tactic} recognises, whether interpretation is just |
|
444 starting a new program (@{term "path = []"}) or interpretation resumes at a |
|
445 certain location: |
|
446 \<close> |
|
447 (*<*)ML \<open> |
|
448 open Celem |
|
449 open LI |
|
450 \<close> |
|
451 ML(*>*) \<open> |
|
452 fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) = |
|
453 if path = [] |
|
454 then scan_dn cc (ist |> set_path [R]) (Program.body_of prog) |
|
455 else go_scan_up (prog, cc) ist |
|
456 | scan_to_tactic _ _ = |
|
457 raise ERROR "scan_to_tactic1: uncovered pattern in fun.def" |
|
458 \<close> |
|
459 text \<open> |
|
460 @{term scan_dn} sets the path in the interpreter state @{term ist} to @{term |
|
461 R}, the program body, while @{term go_scan_up} goes one level up the path in |
|
462 order to call @{term go_scan_up}. Both functions, scanning down and up, are |
|
463 shown below\footnote{ |
|
464 Referring to the example in Fig.\ref{fig:fun-pack-diff} on |
|
465 p.\pageref{fig:fun-pack-diff} we show the interpreter code only for tacticals |
|
466 @{const[names_short] Try}, @{const[names_short] Repeat} and chaining |
|
467 \texttt{\small \#>} (which is \texttt{\small "Tactical.Chain"} in the code). |
|
468 We also omit the cases for uncurried application, which only occurs once (in |
|
469 the first, i.e. the out-most @{const[names_short] Try}) in the example. |
|
470 }: |
|
471 \<close> |
|
472 (*<*)ML(*>*) \<open> |
|
473 fun scan_dn cc (ist as {act_arg, ...}) (Const ("Tactical.Try", _) $ e) = |
|
474 (case scan_dn cc (ist |> path_down [R]) e of |
|
475 Reject_Tac => Term_Val act_arg |
|
476 | goback => goback) |
|
477 | scan_dn cc ist (Const ("Tactical.Repeat", _) $ e) = |
|
478 scan_dn cc (ist |> path_down [R]) e |
|
479 | scan_dn cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) = |
|
480 (case scan_dn cc (ist |> path_down [L, R]) e1 of |
|
481 Term_Val v => scan_dn cc (ist |> path_down [R] |> set_act v) e2 |
|
482 | goback => goback) |
|
483 (*|*) |
|
484 | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t = |
|
485 if Tactical.contained_in t |
|
486 then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t]) |
|
487 else |
|
488 case LItool.check_leaf "next " ctxt eval (get_subst ist) t of |
|
489 (Program.Expr s, _) => Term_Val s |
|
490 | (Program.Tac prog_tac, form_arg) => |
|
491 check_tac cc ist (prog_tac, form_arg) |
|
492 \<close> |
|
493 text \<open> |
|
494 The last case of @{term scan_dn} must have reached a leaf. @{term check_leaf} |
|
495 distinguishes between @{term Expr} and @{term Tac}; the former returns a |
|
496 @{term Term_Val}, the latter returns the result of @{term check_tac} called by |
|
497 @{term scan_dn}, where the result is either @{term Accept_Tac} or @{term |
|
498 Reject_Tac}. In case of @{term Accept_Tac} scanning is stalled (in |
|
499 \S\ref{expl-lucin} such a tactic has been called a beak-point), the respective |
|
500 tactic is returned (together with corresponding @{ML_type Istate.T} and |
|
501 @{ML_type Proof.context}) to the mathematics-engine. |
|
502 In case of @{term Reject_Tac} an explicit back tracking by @{term scan_up} |
|
503 tries other branches with @{term scan_dn}. |
|
504 |
|
505 \medskip |
|
506 @{term scan_up} is as simple as @{term scan_dn}; an essential difference is, |
|
507 that the former requires the whole program for @{term go_scan_up} as follows: |
|
508 \<close> |
|
509 (*<*)ML(*>*) \<open> |
|
510 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept,...})= |
|
511 if path = [R] |
|
512 then |
|
513 if found_accept then Term_Val act_arg else Reject_Tac |
|
514 else |
|
515 scan_up pcc (ist |> path_up) (go_up path sc) |
|
516 and scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up pcc ist |
|
517 | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) = |
|
518 (case scan_dn cc (ist |> path_down [R]) e of |
|
519 Accept_Tac ict => Accept_Tac ict |
|
520 | Reject_Tac => go_scan_up pcc ist |
|
521 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found)) |
|
522 | scan_up pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = |
|
523 go_scan_up pcc ist |
|
524 | scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) = |
|
525 let |
|
526 val e2 = check_Seq_up ist sc |
|
527 in |
|
528 case scan_dn cc (ist |> path_up_down [R]) e2 of |
|
529 Accept_Tac ict => Accept_Tac ict |
|
530 | Reject_Tac => go_scan_up pcc (ist |> path_up) |
|
531 | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> |
|
532 set_found) |
|
533 end |
|
534 (*|*) |
|
535 \<close> |
|
536 text \<open> |
|
537 \subsection{Use of Isabelle's Contexts}\label{ctxt} |
|
538 %----------------------------------------------------------------------------- |
|
539 Isabelle's \textit{``logical context represents the background that is |
|
540 required for formulating statements and composing proofs. It acts as a medium |
|
541 to produce formal content, depending on earlier material (declarations, |
|
542 results etc.).''} \cite{implem-tutorial}. The \sisac-prototype introduced |
|
543 Isabelle's @{ML_structure Context} in collaboration with a |
|
544 student~\cite{mlehnf:bakk-11}, now uses them throughout construction of |
|
545 problem solutions and implements a specific structure @{ML_structure |
|
546 ContextC}\footnote{A closing ``C'' indicates an \sisac{} extension, see |
|
547 {\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/00612574cbfd/src/Tools/isac/CalcElements/contextC.sml}}}. |
|
548 |
|
549 At the beginning of the specification phase (briefly touched by tactic |
|
550 @{term[names_short] SubProblem} in \S\ref{expl-lucin} and explained in little |
|
551 more detail in the subsequent section) an Isabelle theory must be specified, |
|
552 this is followed by \texttt{\small Proof\_Context.init\_global} in the |
|
553 specification module. Then \texttt{\small Proof\_Context.initialise'} takes a |
|
554 formalisation of the problem as strings, which are parsed by \texttt{\small |
|
555 Syntax.read\_term} using the context, and finally the resulting term's types |
|
556 are recorded in the context by \texttt{\small Variable.declare\_constraints}. |
|
557 The latter relieves students from type constraints for input terms. Finally, |
|
558 as soon as a problem type is specified, the respective preconditions are |
|
559 stored by \texttt{\small ContextC.insert\_assumptions}. |
|
560 |
|
561 \medskip |
|
562 During \LI{} the context is updated with assumptions generated by conditional |
|
563 rewriting and by switching to and from sub-programs. An example for the former |
|
564 is tactic @{term[names_short] SubProblem} applied with theorem $x \ne 0 |
|
565 \Rightarrow (\frac{a}{x} = b) = (a = b\cdot x)$ during equation solving. |
|
566 |
|
567 A still not completely solved issue is switching to and from |
|
568 @{term[names_short] SubProblem}s; the scope of an interpreter's environment is |
|
569 different from a logical context's scope. When calling a sub-program, \sisac{} |
|
570 uses \texttt{\small Proof\_Context.initialise}, but returning execution from a |
|
571 @{term[names_short] SubProblem} is not so clear. For instance, if such a |
|
572 sub-program determined the solutions $[x=0,\;x=\sqrt{2}]$, while the calling |
|
573 program maintains the assumption $x\not=0$ from above, then the solution $x=0$ |
|
574 must be dropped, this is clear. But how determine in full generality, which |
|
575 context data to consider when returning execution to a calling program? |
|
576 Presently the decision in \texttt{\small |
|
577 ContextC.subpbl\_to\_caller}\footnote{ |
|
578 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/ce071aa3eae4/src/Tools/isac/CalcElements/contextC.sml\#l73}} |
|
579 is, to transfer all content data which contain at least one variable of the |
|
580 calling program and drop them on contradiction. |
|
581 |
|
582 \subsection{Guarding and Embedding Execution}\label{embedding} |
|
583 %----------------------------------------------------------------------------- |
|
584 Guardin |
|
585 |
|
586 @{theory_text partial_function}s as used by \LI{} are alien to HOL for |
|
587 fundamental reasons. And when the \sisac-project started with the aim to |
|
588 support learning mathematics as taught at engineering faculties, it was clear, |
|
589 that formal specifications should guard execution of programs under \LI{} |
|
590 (i.e. execution only starts, when the specification's preconditions evaluate |
|
591 to true). |
|
592 |
|
593 So formal specification is required for technical reasons \emph{and} for |
|
594 educational reasons in engineering education. The \sisac-project designed a |
|
595 separate specification phase, where input to a problem and corresponding |
|
596 output as well as preconditions and post-condition are handled explicitly by |
|
597 students; example in Fig.\ref{fig:fun-pack-biegelinie} shows several |
|
598 @{term[names_short] SubProblem}s, which lead to mutual recursion between |
|
599 specification phase and phases creating a solution (supported by \LI). |
|
600 |
|
601 \paragraph{Embedding} \LI{} into a dialogue-module is required in order to |
|
602 meet user requirements in educational settings. Looking at the calculation |
|
603 shown on p.\pageref{biegel_calc} and considering the power of the three |
|
604 mainfunction (1)\dots(3) mentioned in the respective comment on |
|
605 p.\pageref{1-2-3}, it is clear, that in particular @{term[names_short] |
|
606 find_next_step} needs control: The dialogue-module hands over control to a |
|
607 student at each step of \LI, but students should also be warned against using |
|
608 a button creating the next step too frequently. A careful reduction of help |
|
609 from \LI{} might make the learning system also usable for written exams. |
|
610 |
|
611 \<close> |
|
612 |
|
613 (*<*) |
|
614 end |
|
615 (*>*) |