More on the tactics

darcs-hash:20060729164028-974a0-b7707c6e5023da7be82d8ff62a775777a3af2105.gz

papers/bib/literature.bib

@@ -1,5 +1,10 @@
 % Autogenerated by db2bib.pl on Wed Dec 10 17:59:27 2003
 
+@misc{haddock,
+  title = {Haddock: A {Haskell} Documentation Tool},
+  howpublished = {\url{http://www.haskell.org/haddock/}}
+}
+
 @inproceedings{offshoring,
   title = {Implicitly Heterogeneous Multi-Stage Programming},
   author = {Jason Eckhardt and Roumen Kaibachev and Emir Pa\v{s}al\'{i}c and Kedar Swadi and Walid Taha},

papers/ivor/ivor.tex

@@ -21,6 +21,8 @@
 \newcommand{\Ivor}{\textsc{Ivor}}
 \newcommand{\Funl}{\textsc{Funl}}
 
+\newcommand{\hdecl}[1]{\texttt{#1}}
+
 \begin{document}
 
 \title{\Ivor{} the Proof Engine}

papers/ivor/tactics.tex

@@ -3,7 +3,10 @@ \section{The \Ivor{} Library}
 Given the basic operations defined in section \ref{holeops}, we can
 create a library of tactics. In this section, I will introduce the
 basic tactics available to the library user, along with the Haskell
-interface for constructing and manipulating $\source$ terms.
+interface for constructing and manipulating $\source$ terms. This
+section includes only the most basic operations; the API is however
+fully documented with the Haddock tool~\cite{haddock}, with
+documentation available on the web\footnote{\url{http://www.dcs.st-and.ac.uk/~eb/Ivor/doc/}}.
 
 \subsection{Definitions and Context}
 
@@ -12,8 +15,132 @@ \subsection{Definitions and Context}
 
 \subsection{Theorems}
 
+\hdecl{
+theorem :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context
+}
+
 \subsection{Basic Tactics}
 
+A tactic is an operation on a goal in the current system state; we
+define a type synonym \hdecl{Tactic} for functions which operate as
+tactics. Tactics modify system state and may fail, hence a tactic
+function returns a monad:
+
+\hdecl{type Tactic = forall m . Monad m => Goal -> Context -> m Context}
+
+The proof state can be thought of as a $\source$ term, containing a
+number of hole bindings. A tactic operates on one of these hole
+bindings, specified by the \texttt{Goal} argument. This can be a named
+binding, \texttt{goal :: Name -> Goal}, or the default goal
+\texttt{defaultGoal::Name}. The default goal is the first goal
+generated by the most recent tactic application.
+
+\subsubsection{Hole Manipluations}
+
+The four basic operations on holes, \demph{claim}, \demph{fill},
+\demph{abandon} and \demph{solve} are given the following types:
+\begin{verbatim}
+claim :: IsTerm a => Name -> a -> Tactic
+fill :: IsTerm a => a -> Tactic
+abandon :: Tactic
+solve :: Tactic
+\end{verbatim}
+
+The \texttt{claim} function takes a name and a type for the new hole,
+and the \texttt{fill} function takes the guess to attach to the
+specified hole. In addition, \texttt{fill} attempts to solve other
+goals by unification.
+
+It can be inconvenient to have to \texttt{solve} every goal after a
+\texttt{fill} (although sometimes this level of control is
+useful). For this reason, a tactic \texttt{keepSolving} is provided
+which solves all goals with a hole-free guess attached,
+
+\subsubsection{Introductions}
+
+A basic operation on terms is to introduce $\lambda$ bindings into the
+context. The \texttt{intro} and \texttt{introName} tactics operate on
+a goal of the form $\fbind{\vx}{\vS}\to\vT$, introducing
+$\lam{\vx}{\vS}$ into the context and updating the goal to
+$\vT$. \texttt{introName} allows a user specified name choice,
+otherwise \Ivor{} chooses the name.
+
+\begin{verbatim}
+intro :: Tactic
+introName :: Name -> Tactic
+\end{verbatim}
+
+\subsubsection{Refinement}
+
+The \texttt{refine} tactic solves a goal by an application of a
+function to arguments. Refining attempts to solve a goal of type
+$\vT$, when given a term $\vt\Hab\all{\tx}{\tS}\SC\vT$. The tactic
+creates a subgoal for each argument $\vx_i$, attempting to solve it by
+unfication.
+
+\begin{verbatim}
+refine :: IsTerm a => a -> Tactic
+\end{verbatim}
+
+For example, given a goal
+\DM{
+\hole{\vv}{\Vect\:\Nat\:(\suc\:\vn)}
+}
+
+Refining by $\Vcons$ creates subgoals for all four arguments, and
+attaches a guess to $\vv$:
+\DM{
+\AR{
+\hole{\vA}{\Type}\\
+\hole{\vk}{\Nat}\\
+\hole{\vx}{\vA}\\
+\hole{\vxs}{\Vect\:\vA\:\vk}\\
+\guess{\vv}{\Vect\:\Nat\:(\suc\:\vn)}{\Vcons\:\vA\:\vk\:\vx\:\vxs}
+}
+}
+
+However, for $\Vcons\:\vA\:\vk\:\vx\:\vxs$ to have type
+$\Vect\:\Nat\:(\suc\:\vn)$ requires that $\vA=\Nat$ and $\vk=\vn$.
+Refinement therefore completes by unifying these, leaving the
+following goals:
+\DM{
+\AR{
+\hole{\vx}{\Nat}\\
+\hole{\vxs}{\Vect\:\Nat\:\vn}\\
+\guess{\vv}{\Vect\:\Nat\:(\suc\:\vn)}{\Vcons\:\Nat\:\vn\:\vx\:\vxs}
+}
+}
+
+\subsubsection{Elimination}
+
+\begin{verbatim}
+induction :: IsTerm a => a -> Tactic
+cases :: IsTerm a => a -> Tactic
+by :: IsTerm a => a -> Tactic
+\end{verbatim}
+
+\subsubsection{Rewriting}
+
+\begin{verbatim}
+replace :: (IsTerm a, IsTerm b, IsTerm c, IsTerm d) =>
+    a -> b -> c -> d -> Bool -> Tactic
+\end{verbatim}
+
 \subsection{Tactic Combinators}
 
+\subsubsection{Sequencing Tactics}
+
+\hdecl{(>->) :: Tactic -> Tactic -> Tactic}
+
+\hdecl{(>=>) :: Tactic -> Tactic -> Tactic}
+
+\hdecl{(>+>) :: Tactic -> Tactic -> Tactic}
+
+\subsubsection{Handling Failure}
+
+\hdecl{try :: Tactic -> Tactic -> Tactic -> Tactic}
+
+
+\subsection{The Shell}
+
 \subsection{Extending and Embedding}