Removing the need to 'solve' or 'keepSolving' everywhere

darcs-hash:20060729234531-974a0-9578f70ef19fc14496d9db8ab4372f3de284bdb1.gz

Ivor/TT.lhs

@@ -884,7 +884,7 @@ Convert an internal tactic into a publicly available tactic.
 > -- by unification and solves them (with 'solve').
 > -- See 'refineWith' and 'basicRefine' for slight variations.
 > refine :: IsTerm a => a -> Tactic
-> refine tm = basicRefine tm >=> trySolve
+> refine tm = basicRefine tm >-> keepSolving
 
 > -- | Solve a goal by applying a function.
 > -- If the term given has arguments, this will create a subgoal for each.
@@ -941,8 +941,10 @@ Convert an internal tactic into a publicly available tactic.
 
 > -- | Attach a solution to a goal.
 > fill :: IsTerm a => a -> Tactic
-> fill guess = do rawguess <- raw guess
->                 runTac (Tactics.fill rawguess)
+> fill guess = fill' guess >-> keepSolving
+
+> fill' guess = do rawguess <- raw guess
+>                  runTac (Tactics.fill rawguess)
 
 > -- | Remove a solution from a goal.
 > abandon :: Tactic
@@ -1099,15 +1101,15 @@ FIXME: Choose a sensible name here
 > -- | Apply an eliminator. 
 > by :: IsTerm a => a -- ^ An elimination rule applied to a target.
 >        -> Tactic
-> by rule = by' rule >=> attack
+> by rule = (by' rule >=> attack) >=> keepSolving
 
 > by' rule = do rawrule <- raw rule
 >               runTac (Tactics.by rawrule)
 
 > -- | Apply the appropriate induction rule to the term.
 > induction :: IsTerm a => a -- ^ target of the elimination
 >                -> Tactic
-> induction tm = induction' tm >=> attack
+> induction tm = (induction' tm >=> attack) >=> keepSolving
 
 > induction' tm = do rawtm <- raw tm
 >                    runTac (Tactics.casetac True rawtm)
@@ -1116,7 +1118,7 @@ FIXME: Choose a sensible name here
 > -- Like 'induction', but no induction hypotheses generated.
 > cases :: IsTerm a => a -- ^ target of the case analysis
 >                -> Tactic
-> cases tm = cases' tm >=> attack
+> cases tm = (cases' tm >=> attack) >=> keepSolving
 > cases' tm = do rawtm <- raw tm
 >                runTac (Tactics.casetac False rawtm)
 

TODO

@@ -2,10 +2,8 @@ Short term things to do:
 
 * Current naive proof state representation is far too slow. Come up
   with something better.
-* API shouldn't really need to require use of attack/solve except in
-  specialised cases (e.g. fine control over refinement). Change it so
-  that shell and api are more or less consistent.
 * Keep track of level in proof state.
+* Keep track of binding level in context, and check at point of use.
 * Allow dump of global context to disk, for fast reloading.
 * Syntax for equality.
 * Elimination with a motive.

papers/ivor/corett.tex

@@ -8,7 +8,8 @@ \subsection{The Core Calculus}
 The core type theory of \Ivor{} is a strongly normalising dependent
 type theory with inductive families~\cite{dybjer94}, similar to Luo's
 UTT~\cite{luo94} or the Calculus of Inductive Constructions in
-\Coq{}~\cite{coq-manual}. This language, which I call $\source$, is an
+\Coq{}~\cite{coq-manual}. 
+This language, which I call $\source$, is an
 enriched lambda calculus, with the usual properties of subject
 reduction, Church Rosser, and uniqueness of types up to
 conversion. The strong normalisation property (i.e. that evaluation
@@ -295,3 +296,4 @@ \subsection{Hole Manipulation}
 \end{array}
 }
 
+

papers/ivor/examples.tex

@@ -1,4 +1,5 @@
-\section{First Order Logic Theorem Prover}
+\section{A First Order Logic Theorem Prover}
 
 \section{\Funl{}, a Functional Language with a Built-in Theorem Prover}
 
+

papers/ivor/tactics.tex

@@ -130,17 +130,18 @@ \subsection{Tactic Combinators}
 
 \subsubsection{Sequencing Tactics}
 
-\hdecl{(>->) :: Tactic -> Tactic -> Tactic}
-
-\hdecl{(>=>) :: Tactic -> Tactic -> Tactic}
-
-\hdecl{(>+>) :: Tactic -> Tactic -> Tactic}
+\begin{verbatim}
+(>->) :: Tactic -> Tactic -> Tactic
+(>=>) :: Tactic -> Tactic -> Tactic
+(>+>) :: Tactic -> Tactic -> Tactic
+\end{verbatim}
 
 \subsubsection{Handling Failure}
 
-\hdecl{try :: Tactic -> Tactic -> Tactic -> Tactic}
-
+\begin{verbatim}
+try :: Tactic -> Tactic -> Tactic -> Tactic
+\end{verbatim}
 
 \subsection{The Shell}
 
-\subsection{Extending and Embedding}
+\subsection{Extending and Embedding}