1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy Wed Mar 11 15:25:52 2020 +0100
1.3 @@ -0,0 +1,615 @@
1.4 +(*<*)
1.5 +(*%:wrap=soft:maxLineLen=78:*)
1.6 +(*partially copied from
1.7 + ~/material/texts/emat/lucin-isa/paper-isabisac/Lucin_Isa_IJCAR.thy *)
1.8 +theory Lucas_Interpreter
1.9 + imports "~~/src/Tools/isac/Interpret/Interpret"
1.10 +begin
1.11 +ML \<open>
1.12 + open LI
1.13 + open Istate
1.14 + open TermC
1.15 +\<close>
1.16 +(*>*)
1.17 +
1.18 +text \<open>
1.19 +\section{Lucas--Interpretation (\LI)}\label{lucin}
1.20 +%=============================================================================
1.21 +The interpreter is named after the inventor of top-down-parsing in the ALGOL
1.22 +project~\cite{pl:formal-lang-hist}, Peter Lucas. As a dedicated expert in
1.23 +programming languages he initially objected ``yet another programming
1.24 +language'' (in analogy to ``Yacc'' \cite{Yacc-1975}), but then he helped to
1.25 +clarify the unusual requirements for a novel programming language in the
1.26 +\sisac-project, which later led to the notion of \LI.
1.27 +
1.28 +\LI{} is the most prominent component in a prototype developed in the
1.29 +\sisac-project, there embedded in a mathematics-engine, which interacts with a
1.30 +dialogue-module in a Java-based front-end managing interaction with students
1.31 +(out of scope of this paper).
1.32 +
1.33 +\subsection{The Concept of \LI}\label{concept-LI}
1.34 +%-----------------------------------------------------------------------------
1.35 +The concept of \LI{} is simple: \LI{} \emph{acts as a debugger on functional
1.36 +programs with hard-coded breakpoints, where control is handed over to a
1.37 +student; a student, however, does \emph{not} interact with the software
1.38 +presenting the program, but with the software presenting steps of forward
1.39 +reasoning, where the steps are rigorously constructed by tactics acting as the
1.40 +break-points mentioned}. Following the \LI{} terminology, we will call
1.41 +``programs'' the functions defined with the function package and refer to
1.42 +their evaluation as ``execution''.
1.43 +
1.44 +\paragraph{Types occurring in the signatures} of \LI{} are as follows. Besides
1.45 +the program of type @{ML_type Program.T} there is an interpreter state
1.46 +@{ML_type Istate.T}, a record type passing data from one step of execution to
1.47 +the next step, in particular a location in the program, where the next step
1.48 +will be read off, and an environment for evaluating the step.
1.49 +As invisible in the program language as the interpreter state is @{ML_type
1.50 +Calc.T}, a ``calculation'' as a sequence of steps in forward reasoning, a
1.51 +variant of ``structured derivations'' \cite{back-SD-2010}. Visible in the
1.52 +language and in the signature, however, are the tactics @{ML_type Tactic.T},
1.53 +which create steps in a calculation.
1.54 +
1.55 +Novel in connection with calculations is the idea to maintain a logical
1.56 +context in order to provide automated provers with data required for checking
1.57 +input by the student. Isabelle's @{ML_type Proof.context}, as is, turned out
1.58 +perfect for this task~\cite{mlehnf:bakk-11}.
1.59 +
1.60 +\paragraph{The signatures of the main functions,} the functions @{term
1.61 +find_next_step}, \\@{term locate_input_tactic} and @{term locate_input_term},
1.62 +are as follows:\label{sig-lucin}
1.63 +\<close>
1.64 +(*<*)ML(*>*) \<open>
1.65 +signature LUCAS_INTERPRETER =
1.66 +sig
1.67 + datatype next_step_result =
1.68 + Next_Step of Istate.T * Proof.context * Tactic.T
1.69 + | Helpless | End_Program of Istate.T * Tactic.T
1.70 + val find_next_step: Program.T -> Calc.T -> Istate.T -> Proof.context
1.71 + -> next_step_result
1.72 +
1.73 + datatype input_tactic_result =
1.74 + Safe_Step of Istate.T * Proof.context * Tactic.T
1.75 + | Unsafe_Step of Istate.T * Proof.context * Tactic.T
1.76 + | Not_Locatable of message
1.77 + val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context
1.78 + -> Tactic.T -> input_tactic_result
1.79 +
1.80 + datatype input_term_result =
1.81 + Found_Step of Calc.T | Not_Derivable
1.82 + val locate_input_term: Calc.T -> term -> input_term_result
1.83 +end
1.84 +\<close>
1.85 +text \<open>
1.86 +\begin{description}
1.87 +\item[@{term find_next_step}] accomplishes what usually is expected from a
1.88 +@{ML_type Program.T}: find a @{term Next_Step} to be executed, in the case of
1.89 +\LI{} to be inserted into a \texttt{\small Calc.T} under construction. This
1.90 +step can be a @{ML_type Tactic.T}, directly found in @{term next_step_result},
1.91 +or a @{ML_type term} produced by applying the tactic. If such a step cannot be
1.92 +found (due to previous student interaction), \LI{} is @{term Helpless}.
1.93 +
1.94 +\item[@{term locate_input_tactic}] gets a @{ML_type Tactic.T} as argument
1.95 +(which has been input and checked applicable in @{ML_type Calc.T}) and tries
1.96 +to locate it in the \texttt{Prog.T} such that a @{term Next_Step} can be
1.97 +generated from the subsequent location in the @{ML_type Program.T}. A step can
1.98 +be an @{term Unsafe_Step}, if the input @{ML_type Tactic.T} cannot safely be
1.99 +associated with any tactic in the @{ML_type Program.T}. This function has a
1.100 +signature similar to @{term find_next_step} (here the respective input
1.101 +@{ML_type Tactic.T} and the one in the result are the same) in order to unify
1.102 +internal technicalities of \LI{}.
1.103 +
1.104 +\item[@{term locate_input_term}] tries to find a derivation from the current
1.105 +@{ML_type Proof.context} for the term input to @{ML_type Calc.T} and to locate
1.106 +a \texttt{Tactic.T} in the @{ML_type Program.T}, which as @{term Found_Step}
1.107 +allows to find a next step later. Such a @{term Found_Step} can be located in
1.108 +another program (a sub-program or a calling program); thus @{ML_type
1.109 +Program.T}, @{ML_type Istate.T} and @{ML_type Proof.context} are packed into
1.110 +@{ML_type Calc.T} at appropriate positions and do not show up in the
1.111 +signature.
1.112 +\end{description}
1.113 +
1.114 +Automated reasoning is concern of the third function @{term
1.115 +locate_input_term}, actually a typical application case for Isabelle's
1.116 +Sledgehammer~\cite{sledgehammer-tutorial}, but not yet realised and
1.117 +preliminarily substituted by \sisac's simplifier. @{term locate_input_term} is
1.118 +the function used predominantly in interaction with students: these input term
1.119 +by term into the calculation under construction (as familiar from
1.120 +paper\&pencil work) and \LI{} checks for correctness automatically.
1.121 +\<close>
1.122 +text \<open>
1.123 +\subsection{Examples for \LI}\label{expl-lucin}
1.124 +%-----------------------------------------------------------------------------
1.125 +\LI's novel concept relating program execution with construction of
1.126 +calculations is best demonstrated by examples. The first one is from
1.127 +structural engineering given by the following problem statement:\\
1.128 +\medskip
1.129 +
1.130 +% first column
1.131 +\begin{minipage}{0.55\textwidth}
1.132 +\textit{Determine the bending line of a beam of length $L$,
1.133 +which consists of homogeneous material, which is clamped on one side
1.134 +and which is under constant line load $q_0$; see the Figure right.}\\
1.135 +\end{minipage}
1.136 +\hfill
1.137 +%second column
1.138 +\begin{minipage}{0.42\textwidth}
1.139 + \includegraphics[width=0.6\textwidth]{bend-7-70-en.png}\\
1.140 +\end{minipage}
1.141 +
1.142 +\medskip
1.143 +This problem is solved by the following program, which is shown by a
1.144 +screen-shot\footnote{The corresponding code is at
1.145 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/Knowledge/Biegelinie.thy\#l174}.
1.146 +%When inner syntax double-quotes are discontinued eventually, the inner syntax
1.147 +of the HOL library may use double quotes for char/string literals, instead of
1.148 +slightly odd double single-quotes.
1.149 +}
1.150 +in order to demonstrate the colouring helpful for programmers (compare the old
1.151 +bare string version in \cite[p.~92]{wn:proto-sys}).
1.152 +\begin{figure} [htb]
1.153 + \centering
1.154 + \includegraphics[width=\textwidth]{fun-pack-biegelinie-2.png}
1.155 + \caption{The program implemented by the function package}
1.156 + \label{fig:fun-pack-biegelinie}
1.157 +\end{figure}
1.158 +The program is implemented as a @{theory_text partial_function}: it calculates
1.159 +results for a whole class of problems and termination cannot be proven in such
1.160 +generality, although preconditions guard execution.
1.161 +%
1.162 +The program reflects a ``divide \& conquer'' strategy by calling three @{term
1.163 +SubProblem}s. It was implemented for field-tests in German-speaking countries,
1.164 +so arguments of the @{term SubProblem}s are in German, because they appear in
1.165 +the calculation as well. The third @{term SubProblem} adopts the format from
1.166 +Computer Algebra. The calculation, if finished successfully, looks as follows
1.167 +(a screen-shot of intermediate steps on the prototype's front-end is shown in
1.168 +\cite[p.~97]{wn:proto-sys}):\label{biegel_calc}
1.169 +{\footnotesize\begin{tabbing}
1.170 +123\=12\=12\=12\=12\=12\=12\=123\=123\=123\=123\=\kill
1.171 +01\> Problem (Biegelinie, [Biegelinien]) \\
1.172 +02\>\> Specification: \\
1.173 +03\>\> Solution: \\
1.174 +04\>\>\> Problem (Biegelinie, [vonBelastungZu, Biegelinien]) \\
1.175 +05\>\>\> $[$\>$V\,x = c + -1\cdot q_0\cdot x, $\\
1.176 +06\>\>\> \>$M_b\,x = c_2 + c\cdot x + \frac{-1\cdot q_0}{2\cdot x ^ 2}, $\\
1.177 +07\>\>\> \>$\frac{d}{dx}y\,x = c_3 + \frac{-1}{EI} \cdot (c_2\cdot x +
1.178 +\frac{c}{2\cdot x ^ 2} + \frac{-1\cdot q_0}{6\cdot x ^ 3}, $\\
1.179 +08\>\>\> \>$y\,x = c_4 + c_3\cdot x + \frac{-1}{EI} \cdot
1.180 +(\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot
1.181 +q_0}{24}\cdot x ^ 4)\;\;]$ \\
1.182 +09\>\>\> Problem (Biegelinie, [setzeRandbedingungen, Biegelinien])\\
1.183 +10\>\>\> $[$\>$L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L \cdot c +
1.184 +-1 \dot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;]$\\
1.185 +11\>\>\> solveSystem $(L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L
1.186 +\cdot c + -1 \cdot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;],\; [c, c_2,
1.187 +c_3, c_4])$\\
1.188 +12\>\>\> $[$\>$c = L \cdot q_0 ,\; c_2 = \frac{-1 \cdot L ^ 2 \cdot q_0}{2},\;
1.189 +c_3 = 0,\; c_4 = 0]$\\
1.190 +13 \` Take $y\,x = c_4 + c_3\cdot x + \frac{-1}{EI} \cdot
1.191 +(\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot
1.192 +q_0}{24}\cdot x ^ 4)$ \\
1.193 +
1.194 +14\>\>\> $y\,x = c_4 + c_3 \cdot x + \frac{-1}{EI} \cdot (\frac{c_2}{2} \cdot
1.195 +x ^ 2 + \frac{c}{6} \cdot x ^ 3 + \frac{-1 \cdot q_0}{24} \cdot x ^ 4)$\\
1.196 +15 \` Substitute $[c,c_2,c_3,c_4]$ \\
1.197 +
1.198 +16\>\>\> $y\,x = 0 + 0 \cdot x + \frac{-1}{EI} \cdot (\frac{\frac{-1 \cdot L ^
1.199 +2 \cdot q_0}{2}}{2} \cdot x ^ 2 + \frac{L \cdot q_0}{6} \cdot x ^ 3 + \frac{-1
1.200 +\cdot q_0}{24} \cdot x ^ 4)$\label{exp-biegel-Substitute}\\
1.201 +17 \` Rewrite\_Set\_Inst $([({\it bdv},x)], {\it make\_ratpoly\_in})$ \\
1.202 +
1.203 +18\>\>\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L
1.204 +\cdot q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$\\
1.205 +19\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L \cdot
1.206 +q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$
1.207 +\end{tabbing}}
1.208 +The calculation is what a student interacts with. Above the \texttt{\small
1.209 +Specification} is folded in, the specification phase and respective user
1.210 +interaction is skipped here. The \texttt{\small Solution} must be constructed
1.211 +step-wise line by line (while the line numbers do not belong to the
1.212 +calculation) in forward reasoning.
1.213 +\label{1-2-3}A student inputs either (1) a term (displayed on the left above
1.214 +with indentations) or (2) a tactic (shifted to the right margin). If the
1.215 +student gets stuck (3) a next step (as a term or a tactic) is suggested by
1.216 +\LI{}, which works behind the scenes; the corresponding functions have been
1.217 +introduced in \S\ref{concept-LI} (for (1) @{term locate_input_term}, (2)
1.218 +@{term locate_input_tactic} and for (3) @{term find_next_step}).
1.219 +
1.220 +\medskip
1.221 +This example hopefully clarifies the relation between program and calculation
1.222 +in \LI{}: execution of the program stops at tactics (above called
1.223 +break-points), displays the tactic or the result produced by the tactic (as
1.224 +decided by the dialogue-module) in the calculation under construction, hands
1.225 +over control to the student working on the calculation and resumes checking
1.226 +user input.
1.227 +
1.228 +\paragraph{A typical example from Computer Algebra}\label{expl-rewrite} shall
1.229 +shed light on a notions introduced later, on tacticals. The program in
1.230 +Fig.\ref{fig:fun-pack-diff} %on p.\pageref{fig:fun-pack-diff}
1.231 +simplifies rational terms (typed as ``real'' due to limited development
1.232 +resources):
1.233 +\begin{figure} [htb]
1.234 + \centering
1.235 + \includegraphics[width=0.95\textwidth]{fun-pack-simplify.png}
1.236 + %\includegraphics[width=0.85\textwidth]{fig/scrshot/fun-pack/fun-pack-diff.png}
1.237 + \caption{Simplification implemented by the function package}
1.238 + \label{fig:fun-pack-diff}
1.239 +\end{figure}
1.240 +
1.241 +The program executes the tactic @{const Rewrite'_Set}\footnote{Isabelle's
1.242 +document preparation system preserves the apostroph from the definition, while
1.243 +Isabelle's pretty printer drops it in the presentation of the program as
1.244 +above.}
1.245 +with different canonical term rewriting systems (called ``rule sets'' in
1.246 +\sisac) guided by tacticals. The output (disregarding user interaction) is a
1.247 +calculation with steps of simplification, where the steps are created by
1.248 +@{const Rewrite'_Set}.
1.249 +
1.250 +Chained functions (by \texttt{\small \#>}) %TODO which antiquot?
1.251 +are applied curried to @{ML_type term}. The initial part of the chain, from
1.252 +\texttt{\small ''discard\_minus''} to \texttt{\small ''cancel''} does
1.253 +preprocessing, for instance replaces $\;a - b\;$ by $\;a + (-b)\;$ in
1.254 +\texttt{\small ''discard\_minus''} for reducing
1.255 +the number of theorems to be used in simplification.
1.256 +%
1.257 +The second chain of @{const Rewrite'_Set} is @{const Repeat}ed until no
1.258 +further rewrites are possible; this is necessary in case of nested fractions.
1.259 +
1.260 +In cases like the one above, a confluent and terminating term rewrite system,
1.261 +not only \emph{all} correct input terms are accepted, but also \emph{all}
1.262 +incorrect input is rejected as @{term Not_Derivable} by the function @{term
1.263 +locate_input_term}.
1.264 +
1.265 +
1.266 +\section{Adaptation of Isabelle's Functions}\label{lucin-funpack}
1.267 +%=============================================================================
1.268 +Isabelle's function package presents functions in ``inner syntax'' to users,
1.269 +i.e. as terms in Isabelle/HOL. The \LI{} design recognised these terms
1.270 +suitable for parse trees of programs, Isabelle realised the same idea in a
1.271 +more general way with the function package a few years later --- so migration
1.272 +from \sisac's programs to Isabelle's functions was surprisingly easy. The main
1.273 +features required were tactics, tacticals and program expressions as described
1.274 +below.
1.275 +
1.276 +\subsection{Tactics Creating Steps in Calculations}\label{tactics}
1.277 +%-----------------------------------------------------------------------------
1.278 +The examples in the previous section showed how tactics in programs create
1.279 +steps in calculations. Tactics in programs are defined as follows\footnote{
1.280 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/Prog_Tac.thy\#l36}}
1.281 +:
1.282 +\<close>
1.283 +consts
1.284 + Calculate :: "[char list, 'a] => 'a"
1.285 + Rewrite :: "[char list, 'a] => 'a"
1.286 + Rewrite'_Inst :: "[(char list * 'a) list, char list, 'a] => 'a"
1.287 + Rewrite'_Set :: "[char list, 'a] => 'a"
1.288 + Rewrite'_Set'_Inst :: "[((char list) * 'a) list, char list, 'a] => 'a"
1.289 + Or'_to'_List :: "bool => 'a list"
1.290 + SubProblem ::
1.291 + "[char list * char list list * char list list, arg list] => 'a"
1.292 + Substitute :: "[bool list, 'a] => 'a"
1.293 + Take :: "'a => 'a"
1.294 +
1.295 +text \<open>
1.296 +These tactics transform a term of some type @{typ "'a"} to a resulting term of
1.297 +the same type. @{const[names_short] Calculate} applies operators like $+,-,*$
1.298 +as @{typ "char list"} (i.e. a string in inner syntax) to numerals of type
1.299 +@{typ "'a"}. The tactics beginning with @{const[names_short] Rewrite} do
1.300 +exactly what they indicate by applying a theorem (in the program given by type
1.301 +@{typ "char list"}) or a list of theorems, called ``rule-set''. The
1.302 +corresponding \texttt{\small \_Inst} variants instantiate bound variables with
1.303 +respective constants before rewriting (this is due to the user requirement,
1.304 +that terms in calculations are close to traditional notation, which excludes
1.305 +$\lambda$-terms), for instance modelling bound variables in equation solving.
1.306 +@{const[names_short] Or'_to'_List} is due to a similar requirement: logically
1.307 +appropriate for describing solution sets in equation solving are equalities
1.308 +connected by $\land,\lor$, but traditional notation uses sets (and these are
1.309 +still lists for convenience). @{const[names_short] SubProblem}s not only take
1.310 +arguments (@{typ "arg list"} like any (sub-)program, but also three references
1.311 +into \sisac's knowledge base (theory, formal specification, method) for
1.312 +guided interaction in the specification phase.
1.313 +
1.314 +Tactics appear simple: they operate on terms adhering to one type ---
1.315 +different types are handled by different tactics and (sub-) programs; and they
1.316 +cover only basic functionality --- but they operate on terms, which are well
1.317 +tooled by Isabelle and which can contain functions evaluated as program
1.318 +expressions introduced in the next but one subsection.
1.319 +
1.320 +Section \S\ref{expl-lucin} showed how tactics can be input by students. So
1.321 +tactics in programs have analogies for user input with type @{ML_type
1.322 +Tactic.input} defined at\footnote{
1.323 +\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
1.324 +paper). And there is another @{ML_type Tactic.T} defined at\footnote{
1.325 +\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
1.326 +signature of Lucas-Interpretation on p.\pageref{sig-lucin}.
1.327 +
1.328 +\subsection{Tacticals Guiding Flow of Execution}\label{tacticals}
1.329 +%-----------------------------------------------------------------------------
1.330 +The example on p.\pageref{expl-rewrite} for canonical rewriting showed, how
1.331 +tacticals guide the flow of execution. The complete list of tacticals is as
1.332 +follows.
1.333 +\<close>
1.334 +consts
1.335 + Chain :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10)
1.336 + If :: "[bool, 'a => 'a, 'a => 'a, 'a] => 'a"
1.337 + Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
1.338 + Repeat :: "['a => 'a, 'a] => 'a"
1.339 + Try :: "['a => 'a, 'a] => 'a"
1.340 + While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
1.341 +
1.342 +text \<open>
1.343 +\texttt{\small Chain} is forward application of functions and made an infix
1.344 +operator @{const[names_short] Chain}; @{const[names_short] If} decides by
1.345 +@{typ bool}en expression for execution of one of two arguments of type @{typ
1.346 +"'a => 'a"} (which can be combinations of tacticals or tactics);
1.347 +@{const[names_short] Or} decides on execution of one of the arguments
1.348 +depending of applicability of tactics; @{const[names_short] Repeat} is a one
1.349 +way loop which terminates, if the argument is not applicable (e.g.
1.350 +applicability of a theorem for rewriting on a term) any more;
1.351 +@{const[names_short] Try} skips the argument if not applicable and
1.352 +@{const[names_short] While} is a zero way loop as usual.
1.353 +
1.354 +\subsection{Program Expressions to be Evaluated}\label{prog-expr}
1.355 +%-----------------------------------------------------------------------------
1.356 +Some tacticals, \texttt{If} and \texttt{While}, involve boolean expressions,
1.357 +which need to be evaluated: such expressions denote another element of
1.358 +programs. This kind of element has been shown in the example on
1.359 +p.\pageref{fig:fun-pack-biegelinie} as argument of @{const[names_short]
1.360 +Take}: sometimes it is necessary to pick parts of elements of a calculation,
1.361 +for instance the last element from a list. So Isabelle's @{theory_text List}
1.362 +is adapted for \sisac's purposes in @{theory_text ListC}\footnote{
1.363 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/ListC.thy}}.
1.364 +%
1.365 +Such expressions are substituted from the environment in @{ML_type Istate.T},
1.366 +evaluated to terms by rewriting (and for that purpose using the same rewrite
1.367 +engine as for the tactics @{const[names_short] Rewrite}*) and marked by the
1.368 +constructor @{term Term_Val} which is introduced below.
1.369 +
1.370 +
1.371 +\section{Implementation of \LI}\label{LI-impl}
1.372 +%=============================================================================
1.373 +The implementation of the interpreter is as experimental as is the respective
1.374 +programming language introduced in the previous section. So below there will
1.375 +be particularly such implementation details, which are required for discussing
1.376 +open design \& implementation issues.
1.377 +
1.378 +All of the function package's syntactic part plus semantic markup is perfect
1.379 +for \LI. The evaluation part of the function package, however, implements
1.380 +automated evaluation in one go and automated
1.381 +code-generation~\cite{code-gen-tutorial} --- both goals are not compatible
1.382 +with \sisac's goal to feature step-wise construction of calculations, so this
1.383 +part had to be done from scratch.
1.384 +
1.385 +
1.386 +\subsection{Scanning the Parse Tree}\label{scanning}
1.387 +%-----------------------------------------------------------------------------
1.388 +Isabelle's function package parses the program body from function definitions
1.389 +to terms, the data structure of simply typed $\lambda$ terms, which also
1.390 +encode the objects of proofs. Thus there is a remarkable collection of tools,
1.391 +readily available in Isabelle; but this collection does not accommodate the
1.392 +requirement of scanning a term to a certain location, remembering the location
1.393 +and returning there later, as required by \LI. So this has been introduced
1.394 +\<close>
1.395 +(*<*)ML(*>*) \<open>
1.396 +datatype lrd = L | R | D
1.397 +type path = lrd list
1.398 +\<close>
1.399 +(*<*)ML \<open>
1.400 +open TermC (*avoids type clashes below from the new typ above*)
1.401 +\<close>
1.402 + ML(*>*) \<open>
1.403 +fun at_location [] t = t
1.404 + | at_location (D :: p) (Abs(_, _, body)) = at_location p body
1.405 + | at_location (L :: p) (t1 $ _) = at_location p t1
1.406 + | at_location (R :: p) (_ $ t2) = at_location p t2
1.407 + | at_location l t =
1.408 + raise TERM ("at_location: no " ^ string_of_path l ^ " for ", [t]);
1.409 +\<close>
1.410 +text \<open>
1.411 +with a @{term path} to a location according to the term constructors
1.412 +\texttt{\small \$} and @{term Abs}. This is an implementation detail; an
1.413 +abstract, denotational view starts with this datatype
1.414 +\<close>
1.415 +(*<*)ML(*>*) \<open>
1.416 +datatype expr_val =
1.417 + Term_Val of term | Reject_Tac
1.418 + | Accept_Tac of Istate.pstate * Proof.context * Tactic.T
1.419 +\<close>
1.420 +text \<open>
1.421 +which models the meaning of an expression in the parse-tree: this is either a
1.422 +@{term Term_Val}ue (introduced in \S\ref{prog-expr}) or a tactic (introduced
1.423 +in \S\ref{tactics}); the latter is either accepted by @{term Accept_Tac} or
1.424 +rejected by @{term Reject_Tac}; an error value is still missing.
1.425 +%
1.426 +The arguments of the above constant @{term Accept_Tac} are the same as
1.427 +introduced for \LI{} in \S\ref{concept-LI}. Thus @{ML_type expr_val} is the
1.428 +return value for functions scanning the parse-tree for an acceptable tactic:
1.429 +\<close>
1.430 +(*<*)ML \<open>
1.431 +open LI (*avoids type clashes below from the new typ above*)
1.432 +\<close>
1.433 + ML(*>*) \<open>
1.434 +scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val;
1.435 +scan_dn: Calc.T * Proof.context -> Istate.pstate -> term -> expr_val;
1.436 +go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val;
1.437 +scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val;
1.438 +check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option ->
1.439 +expr_val;
1.440 +\<close>
1.441 +text \<open>
1.442 +The first argument of each function above, if of type @{ML_type term}, is the
1.443 +whole program. It is not required by @{term scan_dn}, simple top-down
1.444 +scanning, and by @{term check_tac}, if a tactic has been reached. The
1.445 +rightmost argument, if of type @{ML_type term}, serves matching as shown
1.446 +later. @{term scan_to_tactic} recognises, whether interpretation is just
1.447 +starting a new program (@{term "path = []"}) or interpretation resumes at a
1.448 +certain location:
1.449 +\<close>
1.450 +(*<*)ML \<open>
1.451 +open Celem
1.452 +open LI
1.453 +\<close>
1.454 + ML(*>*) \<open>
1.455 +fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) =
1.456 + if path = []
1.457 + then scan_dn cc (ist |> set_path [R]) (Program.body_of prog)
1.458 + else go_scan_up (prog, cc) ist
1.459 + | scan_to_tactic _ _ =
1.460 + raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"
1.461 +\<close>
1.462 + text \<open>
1.463 +@{term scan_dn} sets the path in the interpreter state @{term ist} to @{term
1.464 +R}, the program body, while @{term go_scan_up} goes one level up the path in
1.465 +order to call @{term go_scan_up}. Both functions, scanning down and up, are
1.466 +shown below\footnote{
1.467 +Referring to the example in Fig.\ref{fig:fun-pack-diff} on
1.468 +p.\pageref{fig:fun-pack-diff} we show the interpreter code only for tacticals
1.469 +@{const[names_short] Try}, @{const[names_short] Repeat} and chaining
1.470 +\texttt{\small \#>} (which is \texttt{\small "Tactical.Chain"} in the code).
1.471 +We also omit the cases for uncurried application, which only occurs once (in
1.472 +the first, i.e. the out-most @{const[names_short] Try}) in the example.
1.473 +}:
1.474 +\<close>
1.475 +(*<*)ML(*>*) \<open>
1.476 +fun scan_dn cc (ist as {act_arg, ...}) (Const ("Tactical.Try", _) $ e) =
1.477 + (case scan_dn cc (ist |> path_down [R]) e of
1.478 + Reject_Tac => Term_Val act_arg
1.479 + | goback => goback)
1.480 + | scan_dn cc ist (Const ("Tactical.Repeat", _) $ e) =
1.481 + scan_dn cc (ist |> path_down [R]) e
1.482 + | scan_dn cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
1.483 + (case scan_dn cc (ist |> path_down [L, R]) e1 of
1.484 + Term_Val v => scan_dn cc (ist |> path_down [R] |> set_act v) e2
1.485 + | goback => goback)
1.486 +(*|*)
1.487 + | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t =
1.488 + if Tactical.contained_in t
1.489 + then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])
1.490 + else
1.491 + case LItool.check_leaf "next " ctxt eval (get_subst ist) t of
1.492 + (Program.Expr s, _) => Term_Val s
1.493 + | (Program.Tac prog_tac, form_arg) =>
1.494 + check_tac cc ist (prog_tac, form_arg)
1.495 +\<close>
1.496 + text \<open>
1.497 +The last case of @{term scan_dn} must have reached a leaf. @{term check_leaf}
1.498 +distinguishes between @{term Expr} and @{term Tac}; the former returns a
1.499 +@{term Term_Val}, the latter returns the result of @{term check_tac} called by
1.500 +@{term scan_dn}, where the result is either @{term Accept_Tac} or @{term
1.501 +Reject_Tac}. In case of @{term Accept_Tac} scanning is stalled (in
1.502 +\S\ref{expl-lucin} such a tactic has been called a beak-point), the respective
1.503 +tactic is returned (together with corresponding @{ML_type Istate.T} and
1.504 +@{ML_type Proof.context}) to the mathematics-engine.
1.505 +In case of @{term Reject_Tac} an explicit back tracking by @{term scan_up}
1.506 +tries other branches with @{term scan_dn}.
1.507 +
1.508 +\medskip
1.509 +@{term scan_up} is as simple as @{term scan_dn}; an essential difference is,
1.510 +that the former requires the whole program for @{term go_scan_up} as follows:
1.511 +\<close>
1.512 +(*<*)ML(*>*) \<open>
1.513 +fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept,...})=
1.514 + if path = [R]
1.515 + then
1.516 + if found_accept then Term_Val act_arg else Reject_Tac
1.517 + else
1.518 + scan_up pcc (ist |> path_up) (go_up path sc)
1.519 +and scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up pcc ist
1.520 + | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
1.521 + (case scan_dn cc (ist |> path_down [R]) e of
1.522 + Accept_Tac ict => Accept_Tac ict
1.523 + | Reject_Tac => go_scan_up pcc ist
1.524 + | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
1.525 + | scan_up pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) =
1.526 + go_scan_up pcc ist
1.527 + | scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) =
1.528 + let
1.529 + val e2 = check_Seq_up ist sc
1.530 + in
1.531 + case scan_dn cc (ist |> path_up_down [R]) e2 of
1.532 + Accept_Tac ict => Accept_Tac ict
1.533 + | Reject_Tac => go_scan_up pcc (ist |> path_up)
1.534 + | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |>
1.535 +set_found)
1.536 + end
1.537 +(*|*)
1.538 +\<close>
1.539 +text \<open>
1.540 +\subsection{Use of Isabelle's Contexts}\label{ctxt}
1.541 +%-----------------------------------------------------------------------------
1.542 +Isabelle's \textit{``logical context represents the background that is
1.543 +required for formulating statements and composing proofs. It acts as a medium
1.544 +to produce formal content, depending on earlier material (declarations,
1.545 +results etc.).''} \cite{implem-tutorial}. The \sisac-prototype introduced
1.546 +Isabelle's @{ML_structure Context} in collaboration with a
1.547 +student~\cite{mlehnf:bakk-11}, now uses them throughout construction of
1.548 +problem solutions and implements a specific structure @{ML_structure
1.549 +ContextC}\footnote{A closing ``C'' indicates an \sisac{} extension, see
1.550 +{\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/00612574cbfd/src/Tools/isac/CalcElements/contextC.sml}}}.
1.551 +
1.552 +At the beginning of the specification phase (briefly touched by tactic
1.553 +@{term[names_short] SubProblem} in \S\ref{expl-lucin} and explained in little
1.554 +more detail in the subsequent section) an Isabelle theory must be specified,
1.555 +this is followed by \texttt{\small Proof\_Context.init\_global} in the
1.556 +specification module. Then \texttt{\small Proof\_Context.initialise'} takes a
1.557 +formalisation of the problem as strings, which are parsed by \texttt{\small
1.558 +Syntax.read\_term} using the context, and finally the resulting term's types
1.559 +are recorded in the context by \texttt{\small Variable.declare\_constraints}.
1.560 +The latter relieves students from type constraints for input terms. Finally,
1.561 +as soon as a problem type is specified, the respective preconditions are
1.562 +stored by \texttt{\small ContextC.insert\_assumptions}.
1.563 +
1.564 +\medskip
1.565 +During \LI{} the context is updated with assumptions generated by conditional
1.566 +rewriting and by switching to and from sub-programs. An example for the former
1.567 +is tactic @{term[names_short] SubProblem} applied with theorem $x \ne 0
1.568 +\Rightarrow (\frac{a}{x} = b) = (a = b\cdot x)$ during equation solving.
1.569 +
1.570 +A still not completely solved issue is switching to and from
1.571 +@{term[names_short] SubProblem}s; the scope of an interpreter's environment is
1.572 +different from a logical context's scope. When calling a sub-program, \sisac{}
1.573 +uses \texttt{\small Proof\_Context.initialise}, but returning execution from a
1.574 +@{term[names_short] SubProblem} is not so clear. For instance, if such a
1.575 +sub-program determined the solutions $[x=0,\;x=\sqrt{2}]$, while the calling
1.576 +program maintains the assumption $x\not=0$ from above, then the solution $x=0$
1.577 +must be dropped, this is clear. But how determine in full generality, which
1.578 +context data to consider when returning execution to a calling program?
1.579 +Presently the decision in \texttt{\small
1.580 +ContextC.subpbl\_to\_caller}\footnote{
1.581 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/ce071aa3eae4/src/Tools/isac/CalcElements/contextC.sml\#l73}}
1.582 +is, to transfer all content data which contain at least one variable of the
1.583 +calling program and drop them on contradiction.
1.584 +
1.585 +\subsection{Guarding and Embedding Execution}\label{embedding}
1.586 +%-----------------------------------------------------------------------------
1.587 +Guardin
1.588 +
1.589 +@{theory_text partial_function}s as used by \LI{} are alien to HOL for
1.590 +fundamental reasons. And when the \sisac-project started with the aim to
1.591 +support learning mathematics as taught at engineering faculties, it was clear,
1.592 +that formal specifications should guard execution of programs under \LI{}
1.593 +(i.e. execution only starts, when the specification's preconditions evaluate
1.594 +to true).
1.595 +
1.596 +So formal specification is required for technical reasons \emph{and} for
1.597 +educational reasons in engineering education. The \sisac-project designed a
1.598 +separate specification phase, where input to a problem and corresponding
1.599 +output as well as preconditions and post-condition are handled explicitly by
1.600 +students; example in Fig.\ref{fig:fun-pack-biegelinie} shows several
1.601 +@{term[names_short] SubProblem}s, which lead to mutual recursion between
1.602 +specification phase and phases creating a solution (supported by \LI).
1.603 +
1.604 +\paragraph{Embedding} \LI{} into a dialogue-module is required in order to
1.605 +meet user requirements in educational settings. Looking at the calculation
1.606 +shown on p.\pageref{biegel_calc} and considering the power of the three
1.607 +mainfunction (1)\dots(3) mentioned in the respective comment on
1.608 +p.\pageref{1-2-3}, it is clear, that in particular @{term[names_short]
1.609 +find_next_step} needs control: The dialogue-module hands over control to a
1.610 +student at each step of \LI, but students should also be warned against using
1.611 +a button creating the next step too frequently. A careful reduction of help
1.612 +from \LI{} might make the learning system also usable for written exams.
1.613 +
1.614 +\<close>
1.615 +
1.616 +(*<*)
1.617 +end
1.618 +(*>*)