(*<*)

 (*%:wrap=soft:maxLineLen=78:*)

 (*partially copied from

   ~/material/texts/emat/lucin-isa/paper-isabisac/Lucin_Isa_IJCAR.thy *)

 theory Lucas_Interpreter

   imports "~~/src/Tools/isac/Interpret/Interpret"

 begin

 ML \<open>

   open LI

   open Istate

   open TermC

 \<close>

 (*>*)

 text \<open>

 \section{Lucas--Interpretation (\LI)}\label{lucin}

 %=============================================================================

 The interpreter is named after the inventor of top-down-parsing in the ALGOL 

 project~\cite{pl:formal-lang-hist}, Peter Lucas. As a dedicated expert in 

 programming languages he initially objected ``yet another programming 

 language'' (in analogy to ``Yacc'' \cite{Yacc-1975}), but then he helped to 

 clarify the unusual requirements for a novel programming language in the 

 \sisac-project, which later led to the notion of \LI. 

 \LI{} is the most prominent component in a prototype developed in the 

 \sisac-project, there embedded in a mathematics-engine, which interacts with a 

 dialogue-module in a Java-based front-end managing interaction with students 

 (out of scope of this paper).

 \subsection{The Concept of \LI}\label{concept-LI}

 %-----------------------------------------------------------------------------

 The concept of \LI{} is simple: \LI{} \emph{acts as a debugger on functional 

 programs with hard-coded breakpoints, where control is handed over to a 

 student; a student, however, does \emph{not} interact with the software 

 presenting the program, but with the software presenting steps of forward 

 reasoning, where the steps are rigorously constructed by tactics acting as the 

 break-points mentioned}. Following the \LI{} terminology, we will call 

 ``programs'' the functions defined with the function package and refer to 

 their evaluation as ``execution''.

 \paragraph{Types occurring in the signatures} of \LI{} are as follows. Besides 

 the program of type @{ML_type Program.T} there is an interpreter state 

 @{ML_type Istate.T}, a record type passing data from one step of execution to 

 the next step, in particular a location in the program, where the next step 

 will be read off, and an environment for evaluating the step.

 As invisible in the program language as the interpreter state is @{ML_type 

 Calc.T}, a ``calculation'' as a sequence of steps in forward reasoning, a 

 variant of ``structured derivations'' \cite{back-SD-2010}. Visible in the 

 language and in the signature, however, are the tactics @{ML_type Tactic.T}, 

 which create steps in a calculation.

 Novel in connection with calculations is the idea to maintain a logical 

 context in order to provide automated provers with data required for checking 

 input by the student. Isabelle's @{ML_type Proof.context}, as is, turned out 

 perfect for this task~\cite{mlehnf:bakk-11}.

 \paragraph{The signatures of the main functions,} the functions @{term 

 find_next_step}, \\@{term locate_input_tactic} and @{term locate_input_term}, 

 are as follows:\label{sig-lucin}

 \<close>

 (*<*)ML(*>*) \<open>

 signature LUCAS_INTERPRETER =

 sig

   datatype next_step_result =

       Next_Step of Istate.T * Proof.context * Tactic.T

     | Helpless | End_Program of Istate.T * Tactic.T

   val find_next_step: Program.T -> Calc.T -> Istate.T -> Proof.context

     -> next_step_result

   datatype input_tactic_result =

       Safe_Step of Istate.T * Proof.context * Tactic.T

     | Unsafe_Step of Istate.T * Proof.context * Tactic.T

     | Not_Locatable of message

   val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context

       -> Tactic.T -> input_tactic_result

   datatype input_term_result =

     Found_Step of Calc.T | Not_Derivable

   val locate_input_term: Calc.T -> term -> input_term_result

 end

 \<close>

 text \<open>

 \begin{description}

 \item[@{term find_next_step}] accomplishes what usually is expected from a 

 @{ML_type Program.T}: find a @{term Next_Step} to be executed, in the case of 

 \LI{} to be inserted into a \texttt{\small Calc.T} under construction. This 

 step can be a @{ML_type Tactic.T}, directly found in @{term next_step_result}, 

 or a @{ML_type term} produced by applying the tactic. If such a step cannot be 

 found (due to previous student interaction), \LI{} is @{term Helpless}.

 \item[@{term locate_input_tactic}] gets a  @{ML_type Tactic.T} as argument 

 (which has been input and checked applicable in  @{ML_type  Calc.T}) and tries 

 to locate it in the \texttt{Prog.T} such that a @{term Next_Step} can be 

 generated from the subsequent location in the @{ML_type Program.T}. A step can 

 be an @{term Unsafe_Step}, if the input @{ML_type Tactic.T} cannot safely be 

 associated with any tactic in the @{ML_type Program.T}. This function has a 

 signature similar to @{term find_next_step} (here the respective input 

 @{ML_type Tactic.T} and the one in the result are the same) in order to unify 

 internal technicalities of \LI{}.

 \item[@{term locate_input_term}] tries to find a derivation from the current 

 @{ML_type Proof.context} for the term input to @{ML_type Calc.T} and to locate 

 a \texttt{Tactic.T} in the @{ML_type Program.T}, which as @{term Found_Step} 

 allows to find a next step later. Such a @{term Found_Step} can be located in 

 another program (a sub-program or a calling program); thus @{ML_type 

 Program.T}, @{ML_type Istate.T} and @{ML_type Proof.context} are packed into 

 @{ML_type Calc.T} at appropriate positions and do not show up in the 

 signature.

 \end{description}

 Automated reasoning is concern of the third function @{term 

 locate_input_term}, actually a typical application case for Isabelle's 

 Sledgehammer~\cite{sledgehammer-tutorial}, but not yet realised and 

 preliminarily substituted by \sisac's simplifier. @{term locate_input_term} is 

 the function used predominantly in interaction with students: these input term 

 by term into the calculation under construction (as familiar from 

 paper\&pencil work) and \LI{} checks for correctness automatically.

 \<close>

 text \<open>

 \subsection{Examples for \LI}\label{expl-lucin}

 %-----------------------------------------------------------------------------

 \LI's novel concept relating program execution with construction of 

 calculations is best demonstrated by examples. The first one is from 

 structural engineering given by the following problem statement:\\

 \medskip

 % first column

 \begin{minipage}{0.55\textwidth}

 \textit{Determine the bending line of a beam of length $L$,

 which consists of homogeneous material, which is clamped on one side

 and which is under constant line load $q_0$; see the Figure right.}\\

 \end{minipage}

 \hfill

 %second column

 \begin{minipage}{0.42\textwidth}

   \includegraphics[width=0.6\textwidth]{bend-7-70-en.png}\\

 \end{minipage}

 \medskip

 This problem is solved by the following program, which is shown by a 

 screen-shot\footnote{The corresponding code is at 

 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/Knowledge/Biegelinie.thy\#l174}.

 %When inner syntax double-quotes are discontinued eventually, the inner syntax 

 of the HOL library may use double quotes for char/string literals, instead of 

 slightly odd double single-quotes.

 }

 in order to demonstrate the colouring helpful for programmers (compare the old 

 bare string version in \cite[p.~92]{wn:proto-sys}).

 \begin{figure} [htb]

   \centering

   \includegraphics[width=\textwidth]{fun-pack-biegelinie-2.png}

   \caption{The program implemented by the function package}

   \label{fig:fun-pack-biegelinie}

 \end{figure}

 The program is implemented as a @{theory_text partial_function}: it calculates 

 results for a whole class of problems and termination cannot be proven in such 

 generality, although preconditions guard execution.

 %

 The program reflects a ``divide \& conquer'' strategy by calling three @{term 

 SubProblem}s. It was implemented for field-tests in German-speaking countries, 

 so arguments of the @{term SubProblem}s are in German, because they appear in 

 the calculation as well. The third @{term SubProblem} adopts the format from 

 Computer Algebra. The calculation, if finished successfully, looks as follows 

 (a screen-shot of intermediate steps on the prototype's front-end is shown in 

 \cite[p.~97]{wn:proto-sys}):\label{biegel_calc}

 {\footnotesize\begin{tabbing}

 123\=12\=12\=12\=12\=12\=12\=123\=123\=123\=123\=\kill

 01\> Problem (Biegelinie, [Biegelinien]) \\

 02\>\> Specification: \\

 03\>\> Solution: \\

 04\>\>\> Problem (Biegelinie, [vonBelastungZu, Biegelinien]) \\

 05\>\>\> $[$\>$V\,x = c + -1\cdot q_0\cdot x, $\\

 06\>\>\>    \>$M_b\,x = c_2 + c\cdot x + \frac{-1\cdot q_0}{2\cdot x ^ 2}, $\\

 07\>\>\>    \>$\frac{d}{dx}y\,x =  c_3 + \frac{-1}{EI} \cdot (c_2\cdot x + 

 \frac{c}{2\cdot x ^ 2} + \frac{-1\cdot q_0}{6\cdot x ^ 3}, $\\

 08\>\>\>    \>$y\,x =  c_4 + c_3\cdot x +  \frac{-1}{EI} \cdot  

 (\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot 

 q_0}{24}\cdot x ^ 4)\;\;]$ \\

 09\>\>\> Problem (Biegelinie, [setzeRandbedingungen, Biegelinien])\\

 10\>\>\> $[$\>$L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L \cdot c + 

 -1 \dot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;]$\\

 11\>\>\> solveSystem $(L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L 

 \cdot c + -1 \cdot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;],\; [c, c_2, 

 c_3, c_4])$\\

 12\>\>\> $[$\>$c = L \cdot q_0 ,\; c_2 = \frac{-1 \cdot L ^ 2 \cdot q_0}{2},\; 

 c_3 = 0,\; c_4 = 0]$\\

 13  \` Take $y\,x =  c_4 + c_3\cdot x +  \frac{-1}{EI} \cdot  

 (\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot 

 q_0}{24}\cdot x ^ 4)$ \\

 14\>\>\> $y\,x = c_4 + c_3 \cdot x + \frac{-1}{EI} \cdot (\frac{c_2}{2} \cdot 

 x ^ 2 + \frac{c}{6} \cdot x ^ 3 + \frac{-1 \cdot q_0}{24} \cdot x ^ 4)$\\

 15  \` Substitute $[c,c_2,c_3,c_4]$ \\

 16\>\>\> $y\,x = 0 + 0 \cdot x + \frac{-1}{EI} \cdot (\frac{\frac{-1 \cdot L ^ 

 2 \cdot q_0}{2}}{2} \cdot x ^ 2 + \frac{L \cdot q_0}{6} \cdot x ^ 3 + \frac{-1 

 \cdot q_0}{24} \cdot x ^ 4)$\label{exp-biegel-Substitute}\\

 17  \` Rewrite\_Set\_Inst $([({\it bdv},x)], {\it make\_ratpoly\_in})$ \\

 18\>\>\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L 

 \cdot q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$\\

 19\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L \cdot 

 q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$

 \end{tabbing}}

 The calculation is what a student interacts with. Above the \texttt{\small 

 Specification} is folded in, the specification phase and respective user 

 interaction is skipped here. The \texttt{\small Solution} must be constructed 

 step-wise line by line (while the line numbers do not belong to the 

 calculation) in forward reasoning. 

 \label{1-2-3}A student inputs either (1) a term (displayed on the left above 

 with indentations) or (2) a tactic (shifted to the right margin). If the 

 student gets stuck (3) a next step (as a term or a tactic) is suggested by 

 \LI{}, which works behind the scenes; the corresponding functions have been 

 introduced in \S\ref{concept-LI} (for (1) @{term locate_input_term}, (2) 

 @{term locate_input_tactic} and for (3) @{term find_next_step}).

 \medskip

 This example hopefully clarifies the relation between program and calculation 

 in \LI{}: execution of the program stops at tactics (above called  

 break-points), displays the tactic or the result produced by the tactic (as 

 decided by the dialogue-module) in the calculation under construction, hands 

 over control to the student working on the calculation and resumes checking 

 user input.

 \paragraph{A typical example from Computer Algebra}\label{expl-rewrite} shall 

 shed light on a notions introduced later, on tacticals. The program in 

 Fig.\ref{fig:fun-pack-diff} %on p.\pageref{fig:fun-pack-diff}

 simplifies rational terms (typed as ``real'' due to limited development 

 resources):

 \begin{figure} [htb]

   \centering

   \includegraphics[width=0.95\textwidth]{fun-pack-simplify.png}

  %\includegraphics[width=0.85\textwidth]{fig/scrshot/fun-pack/fun-pack-diff.png}

   \caption{Simplification implemented by the function package}

   \label{fig:fun-pack-diff}

 \end{figure}

 The program executes the tactic @{const Rewrite'_Set}\footnote{Isabelle's 

 document preparation system preserves the apostroph from the definition, while 

 Isabelle's pretty printer drops it in the presentation of the program as 

 above.}

 with different canonical term rewriting systems (called ``rule sets'' in 

 \sisac) guided by tacticals. The output (disregarding user interaction) is a 

 calculation with steps of simplification, where the steps are created by  

 @{const Rewrite'_Set}.

 Chained functions (by \texttt{\small \#>}) %TODO which antiquot?

 are applied curried to @{ML_type term}. The initial part of the chain, from 

 \texttt{\small ''discard\_minus''} to \texttt{\small ''cancel''} does 

 preprocessing, for instance replaces $\;a - b\;$ by $\;a + (-b)\;$ in 

 \texttt{\small ''discard\_minus''} for reducing 

 the number of theorems to be used in simplification.

 %

 The second chain of @{const Rewrite'_Set} is @{const Repeat}ed until no 

 further rewrites are possible; this is necessary in case of nested fractions.

 In cases like the one above, a confluent and terminating term rewrite system, 

 not only \emph{all} correct input terms are accepted, but also \emph{all} 

 incorrect input is rejected as @{term Not_Derivable} by the function  @{term 

 locate_input_term}.

 \section{Adaptation of Isabelle's Functions}\label{lucin-funpack}

 %=============================================================================

 Isabelle's function package presents functions in ``inner syntax'' to users, 

 i.e. as terms in Isabelle/HOL. The \LI{} design recognised these terms 

 suitable for parse trees of programs, Isabelle realised the same idea in a 

 more general way with the function package a few years later --- so migration 

 from \sisac's programs to Isabelle's functions was surprisingly easy. The main 

 features required were tactics, tacticals and program expressions as described 

 below.

 \subsection{Tactics Creating Steps in Calculations}\label{tactics}

 %-----------------------------------------------------------------------------

 The examples in the previous section showed how tactics in programs create 

 steps in calculations. Tactics in programs are defined as follows\footnote{

 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/Prog_Tac.thy\#l36}}

 :

 \<close>

 consts

   Calculate          :: "[char list, 'a] => 'a"

   Rewrite            :: "[char list, 'a] => 'a"

   Rewrite'_Inst      :: "[(char list * 'a) list, char list, 'a] => 'a"   

   Rewrite'_Set       :: "[char list, 'a] => 'a"

   Rewrite'_Set'_Inst :: "[((char list) * 'a) list, char list, 'a] => 'a"

   Or'_to'_List       :: "bool => 'a list"

   SubProblem         ::

     "[char list * char list list * char list list, arg list] => 'a"

   Substitute         :: "[bool list, 'a] => 'a"

   Take               :: "'a => 'a"

 text \<open>

 These tactics transform a term of some type @{typ "'a"} to a resulting term of 

 the same type.  @{const[names_short] Calculate} applies operators like $+,-,*$ 

 as @{typ "char list"} (i.e. a string in inner syntax) to numerals of type  

 @{typ "'a"}. The tactics beginning with @{const[names_short] Rewrite} do 

 exactly what they indicate by applying a theorem (in the program given by type 

 @{typ "char list"}) or a list of theorems, called  ``rule-set''. The 

 corresponding \texttt{\small \_Inst} variants instantiate bound variables with 

 respective constants before rewriting (this is due to the user requirement, 

 that terms in calculations are close to traditional notation, which excludes 

 $\lambda$-terms), for instance modelling bound variables in equation solving. 

 @{const[names_short] Or'_to'_List} is due to a similar requirement: logically 

 appropriate for describing solution sets in equation solving are equalities 

 connected by $\land,\lor$, but traditional notation uses sets (and these are 

 still lists for convenience). @{const[names_short] SubProblem}s not only take 

 arguments (@{typ "arg list"} like any (sub-)program, but also three references 

 into \sisac's knowledge base  (theory, formal specification, method) for 

 guided interaction in the specification phase.

 Tactics appear simple: they operate on terms adhering to one type --- 

 different types are handled by different tactics and (sub-) programs; and they 

 cover only basic functionality --- but they operate on terms, which are well 

 tooled by Isabelle and which can contain functions evaluated as program 

 expressions introduced in the next but one subsection.

 Section \S\ref{expl-lucin} showed how tactics can be input by students. So 

 tactics in programs have analogies for user input with type @{ML_type 

 Tactic.input} defined at\footnote{

 \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 

 paper). And there is another @{ML_type Tactic.T} defined at\footnote{

 \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 

 signature of Lucas-Interpretation on p.\pageref{sig-lucin}.

 \subsection{Tacticals Guiding Flow of Execution}\label{tacticals}

 %-----------------------------------------------------------------------------

 The example on p.\pageref{expl-rewrite} for canonical rewriting showed, how 

 tacticals guide the flow of execution. The complete list of tacticals is as 

 follows.

 \<close>

 consts

   Chain    :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10)

   If       :: "[bool, 'a => 'a, 'a => 'a, 'a] => 'a"

   Or       :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)

   Repeat   :: "['a => 'a, 'a] => 'a" 

   Try      :: "['a => 'a, 'a] => 'a"

   While    :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)

 text \<open>

 \texttt{\small Chain}  is forward application of functions and made an infix 

 operator @{const[names_short] Chain}; @{const[names_short] If} decides by 

 @{typ bool}en expression for execution of one of two arguments of type @{typ 

 "'a => 'a"} (which can be combinations of tacticals or tactics); 

 @{const[names_short] Or} decides on execution of one of the arguments 

 depending of applicability of tactics; @{const[names_short] Repeat} is a one 

 way loop which terminates, if the argument is not applicable (e.g. 

 applicability of a theorem for rewriting on a term) any more; 

 @{const[names_short] Try} skips the argument if not applicable and 

 @{const[names_short] While} is a zero way loop as usual.

 \subsection{Program Expressions to be Evaluated}\label{prog-expr}

 %-----------------------------------------------------------------------------

 Some tacticals, \texttt{If} and \texttt{While}, involve boolean expressions, 

 which need to be evaluated: such expressions denote another element of 

 programs. This kind of element has been shown in the example on 

 p.\pageref{fig:fun-pack-biegelinie} as argument of  @{const[names_short] 

 Take}: sometimes it is necessary to pick parts of elements of a calculation, 

 for instance the last element from a list. So Isabelle's @{theory_text List} 

 is adapted for \sisac's purposes in @{theory_text ListC}\footnote{

 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/ListC.thy}}.

 %

 Such expressions are substituted from the environment in @{ML_type Istate.T}, 

 evaluated to terms by rewriting (and for that purpose using the same rewrite 

 engine as for the tactics @{const[names_short] Rewrite}*) and marked by the 

 constructor @{term Term_Val} which is introduced below.

 \section{Implementation of \LI}\label{LI-impl}

 %=============================================================================

 The implementation of the interpreter is as experimental as is the respective 

 programming language introduced in the previous section. So below there will 

 be particularly such implementation details, which are required for discussing 

 open design \& implementation issues.

 All of the function package's syntactic part plus semantic markup is perfect 

 for \LI. The evaluation part of the function package, however, implements 

 automated evaluation in one go and automated 

 code-generation~\cite{code-gen-tutorial} --- both goals are not compatible 

 with \sisac's goal to feature step-wise construction of calculations, so this 

 part had to be done from scratch.

 \subsection{Scanning the Parse Tree}\label{scanning}

 %-----------------------------------------------------------------------------

 Isabelle's function package parses the program body from function definitions 

 to terms, the data structure of simply typed $\lambda$ terms, which also 

 encode the objects of proofs. Thus there is a remarkable collection of tools, 

 readily available in Isabelle; but this collection does not accommodate the 

 requirement of scanning a term to a certain location, remembering the location 

 and returning there later, as required by \LI. So this has been introduced

 \<close> 

 (*<*)ML(*>*) \<open>

 datatype lrd = L | R | D

 type path = lrd list

 \<close> 

 (*<*)ML \<open>

 open TermC (*avoids type clashes below from the new typ above*)

 \<close> 

     ML(*>*) \<open>

 fun at_location [] t = t

   | at_location (D :: p) (Abs(_, _, body)) = at_location p body

   | at_location (L :: p) (t1 $ _) = at_location p t1

   | at_location (R :: p) (_ $ t2) = at_location p t2

   | at_location l t =

     raise TERM ("at_location: no " ^ string_of_path l ^ " for ", [t]);

 \<close>

 text \<open>

 with a @{term path} to a location according to the term constructors 

 \texttt{\small \$} and @{term Abs}. This is an implementation detail; an 

 abstract, denotational view starts with this datatype

 \<close> 

 (*<*)ML(*>*) \<open>

 datatype expr_val =

     Term_Val of term  | Reject_Tac

   | Accept_Tac of Istate.pstate * Proof.context * Tactic.T

 \<close>

 text \<open>

 which models the meaning of an expression in the parse-tree: this is either a  

 @{term Term_Val}ue  (introduced in \S\ref{prog-expr}) or a tactic (introduced 

 in \S\ref{tactics}); the latter is either accepted by  @{term Accept_Tac} or 

 rejected by  @{term Reject_Tac}; an error value is still missing.

 %

 The arguments of the above constant @{term Accept_Tac} are the same as 

 introduced for \LI{} in \S\ref{concept-LI}. Thus @{ML_type expr_val} is the 

 return value for functions scanning the parse-tree for an acceptable tactic:

 \<close> 

 (*<*)ML \<open>

 open LI (*avoids type clashes below from the new typ above*)

 \<close> 

     ML(*>*) \<open>

 scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val;

 scan_dn: Calc.T * Proof.context -> Istate.pstate -> term -> expr_val;

 go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val;

 scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val;

 check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> 

 expr_val;

 \<close>

 text \<open>

 The first argument of each function above, if of type  @{ML_type term}, is the 

 whole program. It is not required by @{term scan_dn}, simple top-down 

 scanning, and by @{term check_tac}, if a tactic has been reached. The 

 rightmost argument, if of type  @{ML_type term}, serves matching as shown 

 later. @{term scan_to_tactic} recognises, whether interpretation is just 

 starting a new program (@{term "path = []"}) or interpretation resumes at a 

 certain location:

 \<close> 

 (*<*)ML \<open>

 open Celem

 open LI

 \<close> 

     ML(*>*) \<open>

 fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) =

     if path = []

     then scan_dn cc (ist |> set_path [R]) (Program.body_of prog)

     else go_scan_up (prog, cc) ist

   | scan_to_tactic _ _ =

     raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"

 \<close>

     text \<open>

 @{term scan_dn} sets the path in the interpreter state @{term ist} to @{term 

 R}, the program body, while @{term go_scan_up} goes one level up the path in 

 order to call @{term go_scan_up}. Both functions, scanning down and up, are 

 shown below\footnote{

 Referring to the example in Fig.\ref{fig:fun-pack-diff} on 

 p.\pageref{fig:fun-pack-diff} we show the interpreter code only for tacticals 

 @{const[names_short] Try}, @{const[names_short] Repeat} and chaining 

 \texttt{\small \#>} (which is \texttt{\small "Tactical.Chain"} in the code). 

 We also omit the cases for uncurried application, which only occurs once (in 

 the first, i.e. the out-most @{const[names_short] Try}) in the example.

 }:

 \<close> 

 (*<*)ML(*>*) \<open>

 fun scan_dn cc (ist as {act_arg, ...}) (Const ("Tactical.Try", _) $ e) =

     (case scan_dn cc (ist |> path_down [R]) e of

       Reject_Tac => Term_Val act_arg

     | goback => goback)

   | scan_dn cc ist (Const ("Tactical.Repeat", _) $ e) =

     scan_dn cc (ist |> path_down [R]) e

   | scan_dn cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =

     (case scan_dn cc (ist |> path_down [L, R]) e1 of

 	    Term_Val v => scan_dn cc (ist |> path_down [R] |> set_act v) e2

     | goback => goback)

 (*|*)

   | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t =

     if Tactical.contained_in t

     then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])

     else

       case LItool.check_leaf "next  " ctxt eval (get_subst ist) t of

   	    (Program.Expr s, _) => Term_Val s

       | (Program.Tac prog_tac, form_arg) =>

           check_tac cc ist (prog_tac, form_arg)

 \<close>

     text \<open>

 The last case of @{term scan_dn} must have reached a leaf. @{term check_leaf} 

 distinguishes between @{term Expr} and @{term Tac}; the former returns a 

 @{term Term_Val}, the latter returns the result of @{term check_tac} called by 

 @{term scan_dn}, where the result is either @{term Accept_Tac} or @{term 

 Reject_Tac}. In case of  @{term Accept_Tac} scanning is stalled (in 

 \S\ref{expl-lucin} such a tactic has been called a beak-point), the respective 

 tactic is returned (together with corresponding @{ML_type Istate.T} and 

 @{ML_type Proof.context}) to the mathematics-engine. 

 In case of @{term Reject_Tac} an explicit back tracking by @{term scan_up} 

 tries other branches with @{term scan_dn}.

 \medskip

 @{term scan_up} is as simple as @{term scan_dn}; an essential difference is, 

 that the former requires the whole program for @{term go_scan_up} as follows:

 \<close> 

 (*<*)ML(*>*) \<open>

 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept,...})=

     if path = [R]

     then

       if found_accept then Term_Val act_arg else Reject_Tac

     else 

       scan_up pcc (ist |> path_up) (go_up path sc)

 and scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up pcc ist

   | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =

     (case scan_dn cc (ist |> path_down [R]) e of

       Accept_Tac ict => Accept_Tac ict

     | Reject_Tac => go_scan_up pcc ist

     | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))

   | scan_up pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) =

     go_scan_up pcc ist

   | scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) =

       let 

         val e2 = check_Seq_up ist sc

       in

         case scan_dn cc (ist |> path_up_down [R]) e2 of

           Accept_Tac ict => Accept_Tac ict

         | Reject_Tac => go_scan_up pcc (ist |> path_up)

         | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> 

 set_found)

       end

 (*|*)

 \<close>

 text \<open>

 \subsection{Use of Isabelle's Contexts}\label{ctxt}

 %-----------------------------------------------------------------------------

 Isabelle's \textit{``logical context represents the background that is 

 required for formulating statements and composing proofs. It acts as a medium 

 to produce formal content, depending on earlier material (declarations, 

 results etc.).''} \cite{implem-tutorial}. The \sisac-prototype introduced 

 Isabelle's @{ML_structure Context} in collaboration with a 

 student~\cite{mlehnf:bakk-11}, now uses them throughout construction of 

 problem solutions and implements a specific structure @{ML_structure 

 ContextC}\footnote{A closing ``C'' indicates an \sisac{} extension, see 

 {\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/00612574cbfd/src/Tools/isac/CalcElements/contextC.sml}}}.

 At the beginning of the specification phase (briefly touched by tactic 

 @{term[names_short] SubProblem} in \S\ref{expl-lucin} and explained in little 

 more detail in the subsequent section) an Isabelle theory must be specified, 

 this is followed by \texttt{\small Proof\_Context.init\_global} in the 

 specification module. Then \texttt{\small Proof\_Context.initialise'} takes a 

 formalisation of the problem as strings, which are parsed by \texttt{\small  

 Syntax.read\_term} using the context, and finally the resulting term's types 

 are recorded in the context by \texttt{\small Variable.declare\_constraints}. 

 The latter relieves students from type constraints for input terms. Finally, 

 as soon as a problem type is specified, the respective preconditions are 

 stored by \texttt{\small ContextC.insert\_assumptions}.

 \medskip

 During \LI{} the context is updated with assumptions generated by conditional 

 rewriting and by switching to and from sub-programs. An example for the former 

 is tactic  @{term[names_short] SubProblem} applied with theorem $x \ne 0 

 \Rightarrow (\frac{a}{x} = b) = (a = b\cdot x)$ during equation solving.

 A still not completely solved issue is switching to and from 

 @{term[names_short] SubProblem}s; the scope of an interpreter's environment is 

 different from a logical context's scope. When calling a sub-program, \sisac{} 

 uses \texttt{\small Proof\_Context.initialise}, but returning execution from a 

 @{term[names_short] SubProblem} is not so clear. For instance, if such a 

 sub-program determined the solutions $[x=0,\;x=\sqrt{2}]$, while the calling 

 program maintains the assumption $x\not=0$ from above, then the solution $x=0$ 

 must be dropped, this is clear. But how determine in full generality, which 

 context data to consider when returning execution to a calling program? 

 Presently the decision in \texttt{\small 

 ContextC.subpbl\_to\_caller}\footnote{

 \url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/ce071aa3eae4/src/Tools/isac/CalcElements/contextC.sml\#l73}} 

 is, to transfer all content data which contain at least one variable of the 

 calling program and drop them on contradiction.

 \subsection{Guarding and Embedding Execution}\label{embedding}

 %-----------------------------------------------------------------------------

 Guardin

 @{theory_text partial_function}s as used by \LI{} are alien to HOL for 

 fundamental reasons. And when the \sisac-project started with the aim to 

 support learning mathematics as taught at engineering faculties, it was clear, 

 that formal specifications should guard execution of programs under \LI{} 

 (i.e. execution only starts, when the specification's preconditions evaluate 

 to true).

 So formal specification is required for technical reasons \emph{and} for 

 educational reasons in engineering education. The \sisac-project designed a 

 separate specification phase, where input to a problem and corresponding 

 output as well as preconditions and post-condition are handled explicitly by 

 students; example in  Fig.\ref{fig:fun-pack-biegelinie} shows several 

 @{term[names_short] SubProblem}s, which lead to mutual recursion between 

 specification phase and phases creating a solution (supported by \LI).

 \paragraph{Embedding} \LI{} into a dialogue-module is required in order to 

 meet user requirements in educational settings. Looking at the calculation 

 shown on p.\pageref{biegel_calc} and considering the power of the three 

 mainfunction (1)\dots(3) mentioned in the respective comment on 

 p.\pageref{1-2-3}, it is clear, that in particular @{term[names_short] 

 find_next_step} needs control: The dialogue-module hands over control to a 

 student at each step of \LI, but students should also be warned against using 

 a button creating the next step too frequently. A careful reduction of help 

 from \LI{} might make the learning system also usable for written exams.

 \<close>

 (*<*)

 end

 (*>*)