h$75D      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopq Safe-Inferredrstuvwxy Safe-Inferred&589<>refinery; captures the notion of substituting metavariables of type meta into judgements of type jdg. This really only matters when you are dealing with dependent types, specifically existentials. For instance, consider the goal  (x : A) (B x) The type of the second goal we would produce here _depends_ on the solution to the first goal, so we need to know how to substitute holes in judgements in order to properly implement .refinerydependentSubst meta e j# will substitute all occurances of meta in j with e. This method only really makes sense if you have goals that depend on earlier extracts. If this isn't the case, don't implement this.refinery; captures the notion of substituting metavariables of type meta into an extract of type ext. Note that these substitutions should most likely _not_ be capture avoiding.refinerysubstMeta meta e1 e2# will substitute all occurances of meta in e2 with e1.refineryThe result of executing .refineryA so called "partial proof". These are proofs that encountered errors during execution.refinery;Represents a single result of the execution of some tactic.refineryThe extract of the tactic. refinery)The state at the end of tactic execution. refineryAll the goals that were still unsolved by the end of tactic execution. refinery > describes the effects required to generate named holes. The meta type parameter here is a so called "metavariable", which can be thought of as a name for a hole. refinery!Generates a named "hole" of type ext0, which should represent an incomplete extract. refinery'Generates an "unsolvable hole" of type err, which should represent an incomplete extract that we have no hope of solving.These will get generated when you generate partial extracts via .refineryThe core data type of the library. This represents a reified, in-progress proof strategy for a particular goal.0NOTE: We need to split up the extract type into ext' and ext0, as we want to be functorial (and monadic) in ext, but it shows up in both co and contravariant positions. Splitting the type variable up into two solves this problem, at the cost of looking ugly.refineryRepresents a subgoal, and a continuation that tells us what to do with the resulting extract.refineryRun an effect.refinery1Run a stateful computation. We don't want to use z2 here, as it doesn't play nice with backtracking.refinery$Combine together the results of two  ProofState6s, preserving the order that they were synthesized in.refinery Similar to , but will interleave the results, rather than just appending them. This is useful if the first argument produces potentially infinite results.refinery runs the first proofstate, and only runs the second if the first does not produce any successful results.refinery2Silent failure. Always causes a backtrack, unlike .refineryThis does double duty, depending on whether or not the user calls  or . In the first case, we ignore the continutation, backtrack, and return an error in the result of . In the second, we treat this as a sort of "unsolvable subgoal", and call the continuation with a hole.refineryAn installed error handler. These allow us to add annotations to errors, or run effects.refineryRepresents a simple extract.refinery Interpret a  into a list of (possibly incomplete) extracts. This function will cause a proof to terminate when it encounters a , and will return a {. If you want to still recieve an extract even when you encounter a failure, you should use .refinery Interpret a  into a list of (possibly incomplete) extracts. This function will continue producing an extract when it encounters a , leaving a hole in the extract in it's place. If you want the extraction to terminate when you encounter an error, you should use .refinery subgoals fs p0 will apply a list of functions producing a new  to each of the subgoals of p in order. If the list of functions is longer than the number of subgoals, then the extra functions are ignored. If the list of functions is shorter, then we simply apply pure" to all of the remaining subgoals.refinerymapExtract f g p allows yout to modify the extract type of a ProofState. This witness the  Profunctor instance of , which we can't write without a newtype due to the position of the type variablesrefinery speculate s p will record the current state of the proof as part of the extraction process. In doing so, this will also remove any subgoal constructors by filling them with holes.   (c) Reed Mullanix 2019 BSD-stylereedmullanix@gmail.comNone89<>?c5refineryA 55 is a monad transformer for creating inference rules.8refineryA 8 is a monad transformer that performs proof refinement. The type variables signifiy:jdg - The goal type. This is the thing we are trying to construct a proof of.ext - The extract type. This is what we will recieve after running the tactic.err - The error type. We can use |/ to abort the computation with a provided errors - The state type.m - The base monad.a$ - The return value. This to make 8 a monad, and will always be  'Prelude.()'9One of the most important things about this type is it's } instance. t1 >> t2 Will execute t1, against the current goal, and then execute t2( on _all_ of the subgoals generated by t2.This Monad instance is lawful, and has been tested thouroughly, and a version of it has been formally verified in Agda. _However_, just because it is correct doesn't mean that it lines up with your intuitions of how Monads behave! In practice, it feels like a combination of the Non-Determinisitic Monads and some of the Time Travelling ones. That doesn't mean that it's impossible to understand, just that it may push the boundaries of you intuitions.;refinery'Helper function for producing a tactic.<refineryproofState t j will deconstruct a tactic t into a  by running it at j.=refineryLike <%, but we discard the return value of t.>refinery6Map the unwrapped computation using the given function?refinery3Create a subgoal, and return the resulting extract.@refineryCreate an "unsolvable" hole. These holes are ignored by subsequent tactics, but do not cause a backtracking failure. 56789:;<=>?@ 89:;<=>567?@None9>?4WrefineryCreate a tactic that applies each of the tactics in the list to one subgoal.When the number of subgoals is greater than the number of provided tactics, the identity tactic is applied to the remainder. When the number of subgoals is less than the number of provided tactics, the remaining tactics are ignored.Xrefineryt1  % t2" will interleave the execution of t1 and t2. This is useful if t1 will produce an infinite number of extracts, as we will still run t2. This is contrasted with t1  | t2, which will not ever consider t2 if t1) produces an infinite number of extracts.Yrefinery.Tries to run a tactic, backtracking on failureZrefinery commit t1 t2 will run t1, and then run t2 only if t1> (and all subsequent tactics) failed to produce any successes.NOTE: commit does have some sneaky semantics that you have to be aware of. Specifically, it interacts a bit surprisingly with ~-. Namely, the following algebraic law holds 9 commit t1 t2 >>= f = commit (t1 >>= f) (t2 >>= f) + For instance, if you have something like %commit t1 t2 >>= somethingThatMayFail2, then this law implies that this is the same as commit (t1 >>= somethingThatMayFail) (t2 >>= somethingThatMayFail)%, which means that we might execute t2 _even if_ t1 seemingly succeeds.[refinery9Runs a tactic 0 or more times until it fails. Note that [( is almost always the right choice over . Due to the semantics of ,  will create a bunch of partially solved goals along the way, one for each iteration.\refinery9Runs a tactic 1 or more times until it fails. Note that \( is almost always the right choice over . Due to the semantics of ,  will create a bunch of partially solved goals along the way, one for each iteration.]refineryGet the current goal^refineryInspect the current goal._refinery choice ts will run all of the tactics in the list against the current subgoals, and interleave their extracts in a manner similar to X.`refinery failure err will create an unsolvable hole that will be ignored by subsequent tactics.arefinery handler f will install an "error handler". These let you add more context to errors, and potentially run effects. For instance, you may want to take note that a particular situation is unsolvable, and that we shouldn't attempt to run this series of tactics against a given goal again.Note that handlers further down the stack get run before those higher up the stack. For instance, consider the following example: - handler f >> handler g >> failure err  Here, g will get run before f.brefinery A variant of a that doesn't modify the error at all, and solely exists to run effects.crefineryprogress eq err t applies the tactic t, and checks to see if the resulting subgoals are all equal to the initial goal by using eq. If they are, it throws err.drefinery ensure p f t runs the tactic t>, and applies a predicate to the state after the execution of t$. We also run a "cleanup" function f. Note that the predicate is applied to the state _before_ the cleanup function is run.erefineryApply the first tactic, and then apply the second tactic focused on the n th subgoal.frefinery tweak f t3 lets us modify the extract produced by the tactic t.grefineryRuns a tactic, producing a list of possible extracts, along with a list of unsolved subgoals. Note that this function will backtrack on errors. If you want a version that provides partial proofs, use ihrefineryRun a tactic, and get just the list of extracts, ignoring any other information.irefineryRuns a tactic, producing a list of possible extracts, along with a list of unsolved subgoals. Note that this function will produce a so called "Partial Proof". This means that we no longer backtrack on errors, but rather leave an unsolved hole, and continue synthesizing a extract. If you want a version that backgracks on errors, see g.1Note that this version is inherently slower than g-, as it needs to continue producing extracts.jrefineryTurn an inference rule that examines the current goal into a tactic.krefinery%Turn an inference rule into a tactic.lrefinery reify t f will execute the tactic t, and resolve all of it's subgoals by filling them with holes. The resulting subgoals and partial extract are then passed to f.mrefineryresume goals partial4 allows for resumption of execution after a call to l. If your language doesn't support dependent subgoals, consider using resume' instead.nrefinery A version of resume that doesn't perform substitution into the goal types. This only makes sense if your language doesn't support dependent subgoals. If it does, use resume instead, as this will leave the dependent subgoals with holes in them.orefinery pruning t p will execute t, and then apply p to any subgoals it generates. If this predicate returns an error, we terminate the execution. Otherwise, we resume execution via n.prefinerypeek t p will execute t, and then apply p to the extract it produces. If this predicate returns an error, we terminate the execution. Otherwise, we resume execution via n.Note that the extract produced may contain holes, as it is the extract produced by running _just_ t against the current goal.qrefinery attempt t1 t2 will partially execute t1$, inspect it's result, and only run t2 if it fails. If t1 succeeded, we will n execution of it.- 58?@WXYZ[\]^_`abcdefghijklmnopq-8gih WXYZ[\_cd`abf]^e 5jk?@lmnopqX3        !"#$%&'()*+,-./0123456789::;<<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~~~~~~'refinery-0.4.0.0-E4mMDIorSqGEmfwVST0gYbRefinery.ProofStateRefinery.Tactic.InternalRefinery.TacticPaths_refineryresumerunPartialTacticTDependentMetaSubstdependentSubst MetaSubst substMeta PartialProofProof pf_extractpf_statepf_unsolvedGoals MonadExtractholeunsolvableHole ProofStateTSubgoalEffectStatefulAlt InterleaveCommitEmptyFailureHandleAxiomproofs partialProofssubgoals mapExtract speculate$fMonadStatesProofStateT$fMonadThrowProofStateT$fMonadIOProofStateT$fMonadPlusProofStateT$fAlternativeProofStateT$fMonadTransProofStateT$fMonadProofStateT$fMFunctorTYPEProofStateT$fApplicativeProofStateT$fShowProofStateT $fMonadExtractmetaexterrsExceptT $fMonadExtractmetaexterrsWriterT!$fMonadExtractmetaexterrsWriterT0$fMonadExtractmetaexterrsStateT $fMonadExtractmetaexterrsReaderT$fEqPartialProof$fShowPartialProof$fGenericPartialProof $fEqProof $fShowProof$fGenericProof$fGenericProofStateT$fFunctorProofStateTRuleTunRuleTTacticT unTacticTtactic proofState proofState_ mapTacticTsubgoal unsolvable$fMonadStatesTacticT$fMonadTransTacticT$fMFunctorTYPETacticT $fShowTacticT$fMonadIORuleT$fMFunctorTYPERuleT$fMonadTransRuleT$fMonadStatesRuleT $fMonadRuleT$fAlternativeRuleT$fApplicativeRuleT$fFunctorRuleT $fShowRuleT$fGenericRuleT$fFunctorTacticT$fApplicativeTacticT$fAlternativeTacticT$fMonadTacticT$fMonadPlusTacticT$fMonadIOTacticT$fMonadThrowTacticT$fGenericTacticT<@><%>trycommitmany_some_goalinspectchoicefailurehandlerhandler_progressensurefocustweak runTacticT evalTacticTrulerule_reifyresume'pruningpeekattemptversion getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileNametransformers-0.5.6.2Control.Monad.Trans.State.LazyStateTbase Data.EitherLeft mtl-2.2.2Control.Monad.Error.Class throwErrorGHC.BaseMonad>>=many Alternativesome