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

Wingman.CodeGen

Synopsis

Documentation

destructMatches Source #

Arguments

:: Bool 
-> (ConLike -> Judgement -> Rule)

How to construct each match

-> Maybe OccName

Scrutinee

-> CType

Type being destructed

-> Judgement 
-> RuleM (Synthesized [RawMatch]) 

destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)] Source #

Generate just the Matches for a case split on a specific type.

mkDestructPat :: Maybe (Set OccName) -> ConLike -> [OccName] -> ([OccName], Pat GhcPs) Source #

Produces a pattern for a data con and the names of its fields.

conLikeInstOrigArgTys' Source #

Arguments

:: ConLike

DataConstructor

-> [Type]

Universally quantified type arguments to a result type. It MUST NOT contain any dictionaries, coercion and existentials.

For example, for MkMyGADT :: b -> MyGADT a c, we must pass [a, c] as this argument but not b, as b is an existential.

-> [Type]

Types of arguments to the ConLike with returned type is instantiated with the second argument.

Essentially same as dataConInstOrigArgTys in GHC, but only accepts universally quantified types as the second arguments and automatically introduces existentials.

NOTE: The behaviour depends on GHC's dataConInstOrigArgTys. We need some tweaks if the compiler changes the implementation.

destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule Source #

Combinator for performing case splitting, and running sub-rules on the resulting matches.

destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule Source #

Combinator for performign case splitting, and running sub-rules on the resulting matches.

buildDataCon Source #

Arguments

:: Bool 
-> Judgement 
-> ConLike

The data con to build

-> [Type]

Type arguments for the data con

-> RuleM (Synthesized (LHsExpr GhcPs)) 

Construct a data con with subgoals for each field.

mkApply :: OccName -> [HsExpr GhcPs] -> LHsExpr GhcPs Source #

Make a function application, correctly handling the infix case.

letForEach Source #

Arguments

:: (OccName -> OccName)

How to name bound variables

-> (HyInfo CType -> TacticsM ())

The tactic to run

-> Hypothesis CType

Terms to generate bindings for

-> Judgement

The goal of original hole

-> RuleM (Synthesized (LHsExpr GhcPs)) 

Run a tactic over each term in the given Hypothesis, binding the results of each in a let expression.

nonrecLet :: [(OccName, Judgement)] -> Judgement -> RuleM (Synthesized (LHsExpr GhcPs)) Source #

Let-bind the given occname judgement pairs.

idiomize :: LHsExpr GhcPs -> LHsExpr GhcPs Source #

Converts a function application into applicative form