Wingman.Tactics

Documentation

data Saturation

Constructors

Unsaturated Int

Instances

Eq Saturation

Defined in Wingman.Tactics

Methods

(==) :: Saturation -> Saturation -> Bool

(/=) :: Saturation -> Saturation -> Bool

Ord Saturation

Defined in Wingman.Tactics

Methods

compare :: Saturation -> Saturation -> Ordering

(<) :: Saturation -> Saturation -> Bool

(<=) :: Saturation -> Saturation -> Bool

(>) :: Saturation -> Saturation -> Bool

(>=) :: Saturation -> Saturation -> Bool

max :: Saturation -> Saturation -> Saturation

min :: Saturation -> Saturation -> Saturation

Show Saturation

Defined in Wingman.Tactics

Methods

showsPrec :: Int -> Saturation -> ShowS

show :: Saturation -> String

showList :: [Saturation] -> ShowS

data IntroParams

Constructors

IntroduceAllUnnamed

IntroduceOnlyNamed [OccName]

IntroduceOnlyUnnamed Int

Instances

Eq IntroParams

Defined in Wingman.Tactics

Methods

(==) :: IntroParams -> IntroParams -> Bool

(/=) :: IntroParams -> IntroParams -> Bool

Ord IntroParams

Defined in Wingman.Tactics

Methods

compare :: IntroParams -> IntroParams -> Ordering

(<) :: IntroParams -> IntroParams -> Bool

(<=) :: IntroParams -> IntroParams -> Bool

(>) :: IntroParams -> IntroParams -> Bool

(>=) :: IntroParams -> IntroParams -> Bool

max :: IntroParams -> IntroParams -> IntroParams

min :: IntroParams -> IntroParams -> IntroParams

Show IntroParams

Defined in Wingman.Tactics

Methods

showsPrec :: Int -> IntroParams -> ShowS

show :: IntroParams -> String

showList :: [IntroParams] -> ShowS

pattern Saturated :: Saturation

assumption :: TacticsM ()

Use something in the hypothesis to fill the hole.

assume :: OccName -> TacticsM ()

Use something named in the hypothesis to fill the hole.

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

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

recursion :: TacticsM ()

restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()

intros :: TacticsM ()

Introduce a lambda binding every variable.

intros' :: IntroParams -> TacticsM ()

Introduce a lambda binding every variable.

introAndDestruct :: TacticsM ()

Introduce a single lambda argument, and immediately destruct it.

destructAuto :: HyInfo CType -> TacticsM ()

Case split, and leave holes in the matches.

destructOrHomoAuto :: HyInfo CType -> TacticsM ()

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 ()

Case split, and leave holes in the matches.

destructPun :: HyInfo CType -> TacticsM ()

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

homo :: HyInfo CType -> TacticsM ()

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

destructLambdaCase :: TacticsM ()

LambdaCase split, and leave holes in the matches.

homoLambdaCase :: TacticsM ()

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

apply :: Saturation -> HyInfo CType -> TacticsM ()

application :: TacticsM ()

split :: TacticsM ()

Choose between each of the goal's data constructors.

splitAuto :: TacticsM ()

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 ()

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

obvious :: TacticsM ()

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

sorry :: TacticsM ()

Sorry leaves a hole in its extract

metaprogram :: TacticsM ()

Sorry leaves a hole in its extract

requireNewHoles :: TacticsM () -> TacticsM ()

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

splitConLike :: ConLike -> TacticsM ()

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 ()

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 ()

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

userSplit :: OccName -> TacticsM ()

User-facing tactic to implement "Use constructor x"

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

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

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

localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a

refine :: TacticsM ()

auto' :: Int -> TacticsM ()

overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM ()

overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()

allNames :: Judgement -> Set OccName

applyMethod :: Class -> PredType -> OccName -> TacticsM ()

applyByName :: OccName -> TacticsM ()

applyByType :: Type -> TacticsM ()

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

nary :: Int -> TacticsM ()

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

self :: TacticsM ()

cata :: HyInfo CType -> TacticsM ()

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.

letBind :: [OccName] -> TacticsM ()

nested :: OccName -> TacticsM ()

Deeply nest an unsaturated function onto itself

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

Repeatedly bind a tactic on its first hole

deepening :: TacticsM () -> TacticsM ()

Try deep for arbitrary depths.

bindOne :: TacticsM a -> TacticsM a -> TacticsM a

collapse :: TacticsM ()

with_arg :: TacticsM ()

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

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

runTactic

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.