Wingman.CodeGen

Documentation

destructMatches

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

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

mkDestructPat :: Maybe (Set OccName) -> ConLike -> [OccName] -> ([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' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule

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

destructLambdaCase' :: Bool -> (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.

letForEach

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

Let-bind the given occname judgement pairs.

module Wingman.CodeGen.Utils