refinery-0.4.0.0: ChangeLog.md
# Changelog for refinery
* 0.4.0.0
- How failure is handled has been refined somewhat. Previously, if a
tactic failed, then the extraction process was terminated, and
`proofs` would return a `Left` describing the error. This design
worked, but led to some suboptimal error reporting. To fix this,
the `Failure` constructor from `ProofStateT` has been changed from
```
| Failure err
```
to
```
| Failure err (ext' -> ProofStateT ext' ext err s m goal)
```
This allows us the option to continue the extraction process even
in the face of failure. This option is exercised in `partialProofs`
and `runPartialTacticT`.
- A bunch of helpful combinators have been added for extract
manipulation inside of tactics.
- `proofs` no longer returns a tuple, but rather a record type
```
data Proof s meta goal ext = Proof { pf_extract :: ext, pf_state :: s, pf_unsolvedGoals :: [(meta, goal)] }
```
- Added `handler`, and removed the `MonadError` instance for `TacticT`.
Now, instead of recovering from errors (which was fraught with subtle issues),
we allow the user to annotate errors instead.
- Added some useful tactic combinators:
- tweak
- peek
- poke
- inspect
- some_
- Swapped the order of arguments to `mapExtract` to line up with `Profunctor`
- Reworked `MonadExtract` to support named holes.
- Added `reify` and `resume` combinators, which are used for inspecting the current proof state during tactic execution.
* 0.3.0.0
- Reworked the core types of the library, which fixed a lot of the weird behavior
that users were experiencing.
* 0.2.0.0
- Added Alternative/MonadPlus instances to ProofStateT, TacticT, RuleT
* 0.1.0.0
- Initial Release of the library