Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
- countRecursiveCall :: TacticState -> TacticState
- addUnusedTopVals :: MonadState TacticState m => Set OccName -> m ()
- destructMatches :: (DataCon -> Judgement -> Rule) -> Maybe OccName -> CType -> Judgement -> RuleM (Trace, [RawMatch])
- mkDestructPat :: DataCon -> [OccName] -> Pat GhcPs
- infixifyPatIfNecessary :: DataCon -> Pat GhcPs -> Pat GhcPs
- unzipTrace :: [(Trace, a)] -> (Trace, [a])
- dataConInstOrigArgTys' :: DataCon -> [Type] -> [Type]
- destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
- destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
- buildDataCon :: Judgement -> DataCon -> [Type] -> RuleM (Trace, LHsExpr GhcPs)
- mkCon :: DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs
- coerceName :: HasOccName a => a -> RdrNameStr
- var' :: Var a => OccName -> a
- bvar' :: BVar a => OccName -> a
- mkFunc :: String -> HsExpr GhcPs
- mkVal :: String -> HsExpr GhcPs
- infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
- appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
Documentation
useOccName :: MonadState TacticState m => Judgement -> OccName -> m () Source #
countRecursiveCall :: TacticState -> TacticState Source #
Doing recursion incurs a small penalty in the score.
addUnusedTopVals :: MonadState TacticState m => Set OccName -> m () Source #
Insert some values into the unused top values field. These are
subsequently removed via useOccName
.
mkDestructPat :: DataCon -> [OccName] -> Pat GhcPs Source #
Produces a pattern for a data con and the names of its fields.
unzipTrace :: [(Trace, a)] -> (Trace, [a]) Source #
dataConInstOrigArgTys' Source #
:: DataCon |
|
-> [Type] | Universally quantified type arguments to a result type. It MUST NOT contain any dictionaries, coercion and existentials. For example, for |
-> [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) -> OccName -> Judgement -> Rule Source #
Combinator for performing case splitting, and running sub-rules on the resulting matches.
destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule Source #
Combinator for performign case splitting, and running sub-rules on the resulting matches.
:: 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.
coerceName :: HasOccName a => a -> RdrNameStr Source #