Safe Haskell	None
Language	Haskell2010

Wingman.CodeGen

Synopsis

destructMatches :: Bool -> (ConLike -> Judgement -> Rule) -> Maybe OccName -> CType -> Judgement -> RuleM (Synthesized [RawMatch])
destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
mkDestructPat :: Maybe (Set OccName) -> ConLike -> [OccName] -> ([OccName], Pat GhcPs)
infixifyPatIfNecessary :: ConLike -> Pat GhcPs -> Pat GhcPs
unzipTrace :: [Synthesized a] -> Synthesized [a]
conLikeInstOrigArgTys' :: ConLike -> [Type] -> [Type]
conLikeExTys :: ConLike -> [TyCoVar]
patSynExTys :: PatSyn -> [TyCoVar]
destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule
buildDataCon :: Bool -> Judgement -> ConLike -> [Type] -> RuleM (Synthesized (LHsExpr GhcPs))
mkApply :: OccName -> [HsExpr GhcPs] -> LHsExpr GhcPs
letForEach :: (OccName -> OccName) -> (HyInfo CType -> TacticsM ()) -> Hypothesis CType -> Judgement -> RuleM (Synthesized (LHsExpr GhcPs))
module Wingman.CodeGen.Utils

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.

infixifyPatIfNecessary :: ConLike -> Pat GhcPs -> Pat GhcPs Source #

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

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.

conLikeExTys :: ConLike -> [TyCoVar] Source #

patSynExTys :: PatSyn -> [TyCoVar] Source #

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.

module Wingman.CodeGen.Utils