hls-tactics-plugin-1.6.2.0: Wingman plugin for Haskell Language Server
Safe HaskellNone
LanguageHaskell2010

Wingman.Tactics

Synopsis

Documentation

newtype Saturation Source #

Constructors

Unsaturated Int 

assumption :: TacticsM () Source #

Use something in the hypothesis to fill the hole.

assume :: OccName -> TacticsM () Source #

Use something named in the hypothesis to fill the hole.

use :: Saturation -> OccName -> TacticsM () Source #

Like apply, but uses an OccName available in the context or the module

intros :: TacticsM () Source #

Introduce a lambda binding every variable.

intros' :: IntroParams -> TacticsM () Source #

Introduce a lambda binding every variable.

introAndDestruct :: TacticsM () Source #

Introduce a single lambda argument, and immediately destruct it.

destructAuto :: HyInfo CType -> TacticsM () Source #

Case split, and leave holes in the matches.

destructOrHomoAuto :: HyInfo CType -> TacticsM () Source #

When running auto, in order to prune the auto search tree, we try a homomorphic destruct whenever possible. If that produces any results, we can probably just prune the other side.

destruct :: HyInfo CType -> TacticsM () Source #

Case split, and leave holes in the matches.

destructPun :: HyInfo CType -> TacticsM () Source #

Case split, and leave holes in the matches. Performs record punning.

homo :: HyInfo CType -> TacticsM () Source #

Case split, using the same data constructor in the matches.

destructLambdaCase :: TacticsM () Source #

LambdaCase split, and leave holes in the matches.

homoLambdaCase :: TacticsM () Source #

LambdaCase split, using the same data constructor in the matches.

split :: TacticsM () Source #

Choose between each of the goal's data constructors.

splitAuto :: TacticsM () Source #

Choose between each of the goal's data constructors. Different than split because it won't split a data con if it doesn't result in any new goals.

splitSingle :: TacticsM () Source #

Like split, but only works if there is a single matching data constructor for the goal.

obvious :: TacticsM () Source #

Like split, but prunes any data constructors which have holes.

sorry :: TacticsM () Source #

Sorry leaves a hole in its extract

metaprogram :: TacticsM () Source #

Sorry leaves a hole in its extract

requireNewHoles :: TacticsM () -> TacticsM () Source #

Allow the given tactic to proceed if and only if it introduces holes that have a different goal than current goal.

splitConLike :: ConLike -> TacticsM () Source #

Attempt to instantiate the given ConLike to solve the goal.

INVARIANT: Assumes the given ConLike is appropriate to construct the type with.

splitDataCon :: DataCon -> TacticsM () Source #

Attempt to instantiate the given data constructor to solve the goal.

INVARIANT: Assumes the given datacon is appropriate to construct the type with.

destructAll :: TacticsM () Source #

Perform a case split on each top-level argument. Used to implement the "Destruct all function arguments" action.

userSplit :: OccName -> TacticsM () Source #

User-facing tactic to implement "Use constructor x"

matching :: (Judgement -> TacticsM ()) -> TacticsM () Source #

matching f takes a function from a judgement to a Tactic, and then applies the resulting Tactic.

attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM () Source #

applyByType :: Type -> TacticsM () Source #

Make a function application where the function being applied itself is a hole.

nary :: Int -> TacticsM () Source #

Make an n-ary function call of the form (_ :: forall a b. a -> a -> b) _ _.

cata :: HyInfo CType -> TacticsM () Source #

Perform a catamorphism when destructing the given HyInfo. This will result in let binding, making values that call the defining function on each destructed value.

nested :: OccName -> TacticsM () Source #

Deeply nest an unsaturated function onto itself

deep :: Int -> TacticsM () -> TacticsM () Source #

Repeatedly bind a tactic on its first hole

deepening :: TacticsM () -> TacticsM () Source #

Try deep for arbitrary depths.

hyDiff :: TacticsM () -> TacticsM (Hypothesis CType) Source #

Determine the difference in hypothesis due to running a tactic. Also, it runs the tactic.

idiom :: TacticsM () -> TacticsM () Source #

Attempt to run the given tactic in "idiom bracket" mode. For example, if the current goal is

(_ :: [r])

then idiom apply will remove the applicative context, resulting in a hole:

(_ :: r)

and then use apply to solve it. Let's say this results in:

(f (_ :: a) (_ :: b))

Finally, idiom lifts this back into the original applicative:

(f $ (_ :: [a]) * (_ :: [b]))

Idiom will fail fast if the current goal doesn't have an applicative instance.

runTactic Source #

Arguments

:: Int

Timeout

-> Context 
-> Judgement 
-> TacticsM ()

Tactic to use

-> IO (Either [TacticError] RunTacticResults) 

Attempt to generate a term of the right type using in-scope bindings, and a given tactic.