| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Wingman.Tactics
Synopsis
- newtype Saturation = Unsaturated Int
- data IntroParams
- pattern Saturated :: Saturation
- assumption :: TacticsM ()
- assume :: OccName -> TacticsM ()
- use :: Saturation -> OccName -> TacticsM ()
- recursion :: TacticsM ()
- restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()
- intros :: TacticsM ()
- intros' :: IntroParams -> TacticsM ()
- introAndDestruct :: TacticsM ()
- destructAuto :: HyInfo CType -> TacticsM ()
- destructOrHomoAuto :: HyInfo CType -> TacticsM ()
- destruct :: HyInfo CType -> TacticsM ()
- destructPun :: HyInfo CType -> TacticsM ()
- homo :: HyInfo CType -> TacticsM ()
- destructLambdaCase :: TacticsM ()
- homoLambdaCase :: TacticsM ()
- apply :: Saturation -> HyInfo CType -> TacticsM ()
- application :: TacticsM ()
- split :: TacticsM ()
- splitAuto :: TacticsM ()
- splitSingle :: TacticsM ()
- obvious :: TacticsM ()
- sorry :: TacticsM ()
- metaprogram :: TacticsM ()
- requireNewHoles :: TacticsM () -> TacticsM ()
- splitConLike :: ConLike -> TacticsM ()
- splitDataCon :: DataCon -> TacticsM ()
- destructAll :: TacticsM ()
- userSplit :: OccName -> TacticsM ()
- matching :: (Judgement -> TacticsM ()) -> TacticsM ()
- 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 ()
- nary :: Int -> TacticsM ()
- self :: TacticsM ()
- cata :: HyInfo CType -> TacticsM ()
- letBind :: [OccName] -> TacticsM ()
- nested :: OccName -> TacticsM ()
- deep :: Int -> TacticsM () -> TacticsM ()
- deepening :: TacticsM () -> TacticsM ()
- bindOne :: TacticsM a -> TacticsM a -> TacticsM a
- collapse :: TacticsM ()
- with_arg :: TacticsM ()
- hyDiff :: TacticsM () -> TacticsM (Hypothesis CType)
- idiom :: TacticsM () -> TacticsM ()
- subgoalWith :: Judgement -> TacticsM () -> RuleM (Synthesized (LHsExpr GhcPs))
- runTactic :: Int -> Context -> Judgement -> TacticsM () -> IO (Either [TacticError] RunTacticResults)
Documentation
newtype Saturation Source #
Constructors
| Unsaturated Int |
Instances
| Eq Saturation Source # | |
Defined in Wingman.Tactics | |
| Ord Saturation Source # | |
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 Source # | |
Defined in Wingman.Tactics Methods showsPrec :: Int -> Saturation -> ShowS # show :: Saturation -> String # showList :: [Saturation] -> ShowS # | |
data IntroParams Source #
Constructors
| IntroduceAllUnnamed | |
| IntroduceOnlyNamed [OccName] | |
| IntroduceOnlyUnnamed Int |
Instances
| Eq IntroParams Source # | |
Defined in Wingman.Tactics | |
| Ord IntroParams Source # | |
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 Source # | |
Defined in Wingman.Tactics Methods showsPrec :: Int -> IntroParams -> ShowS # show :: IntroParams -> String # showList :: [IntroParams] -> ShowS # | |
pattern Saturated :: Saturation Source #
assumption :: TacticsM () Source #
Use something in the hypothesis to fill the hole.
intros' :: IntroParams -> TacticsM () Source #
Introduce a lambda binding every variable.
introAndDestruct :: TacticsM () Source #
Introduce a single lambda argument, and immediately destruct it.
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.
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.
application :: TacticsM () Source #
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.
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.
matching :: (Judgement -> TacticsM ()) -> TacticsM () Source #
matching f takes a function from a judgement to a Tactic, and
then applies the resulting Tactic.
applyByName :: OccName -> 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.
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:
Idiom will fail fast if the current goal doesn't have an applicative instance.
subgoalWith :: Judgement -> TacticsM () -> RuleM (Synthesized (LHsExpr GhcPs)) Source #