Wingman.CodeGen

Documentation

destructMatches

Arguments

:: (ConLike -> Judgement -> Rule)

How to construct each match

-> Maybe OccName

Scrutinee

-> CType

Type being destructed

-> Judgement

-> RuleM (Synthesized [RawMatch])

mkDestructPat :: ConLike -> [OccName] -> Pat GhcPs

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

infixifyPatIfNecessary :: ConLike -> Pat GhcPs -> Pat GhcPs

unzipTrace :: [Synthesized a] -> Synthesized [a]

conLikeInstOrigArgTys'

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.

conLikeExTys :: ConLike -> [TyCoVar]

patSynExTys :: PatSyn -> [TyCoVar]

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

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

destructLambdaCase' :: (ConLike -> Judgement -> Rule) -> Judgement -> Rule

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

buildDataCon

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

Make a function application, correctly handling the infix case.

module Wingman.CodeGen.Utils