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