(*<*)

(*%: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

(*>*)