Ide.Plugin.Tactic.CodeGen

Documentation

useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()

countRecursiveCall :: TacticState -> TacticState

Doing recursion incurs a small penalty in the score.

addUnusedTopVals :: MonadState TacticState m => Set OccName -> m ()

Insert some values into the unused top values field. These are subsequently removed via useOccName.

destructMatches

Arguments

:: (DataCon -> Judgement -> Rule)

How to construct each match

-> Maybe OccName

Scrutinee

-> CType

Type being destructed

-> Judgement

-> RuleM (Trace, [RawMatch])

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

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

infixifyPatIfNecessary :: DataCon -> Pat GhcPs -> Pat GhcPs

unzipTrace :: [(Trace, a)] -> (Trace, [a])

dataConInstOrigArgTys'

Arguments

:: DataCon

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 DataCon 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' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule

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

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

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

buildDataCon

Arguments

:: Judgement

-> DataCon

The data con to build

-> [Type]

Type arguments for the data con

-> RuleM (Trace, LHsExpr GhcPs)

Construct a data con with subgoals for each field.

module Ide.Plugin.Tactic.CodeGen.Utils