| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Constraint.Monad
Description
This module contains various functions that add/update in the CG monad.
Synopsis
- addC :: SubC -> String -> CG ()
- addPost :: CGEnv -> SpecType -> CG SpecType
- addW :: WfC -> CG ()
- addWarning :: Error -> CG ()
- addIdA :: Var -> Annot SpecType -> CG ()
- boundRecVar :: SrcSpan -> AnnInfo (Annot a) -> Bool
- addLocA :: Maybe Var -> SrcSpan -> Annot SpecType -> CG ()
- updateLocA :: Maybe SrcSpan -> SpecType -> CG ()
- addA :: Outputable a => SrcSpan -> Maybe a -> b -> AnnInfo b -> AnnInfo b
- addHole :: SrcSpan -> Var -> SpecType -> CGEnv -> CG ()
- addHoleANF :: (Var, SrcSpan) -> Var -> CoreExpr -> SpecType -> CG ()
- linkANFToHole :: Var -> (Var, SrcSpan) -> CG ()
- isANFInHole :: Var -> CG (Maybe (Var, SrcSpan))
- lookupNewType :: TyCon -> CG (Maybe SpecType)
- envToSub :: [(a, b)] -> ([(a, b)], b, b)
Documentation
addWarning :: Error -> CG () Source #
Add a warning
addIdA :: Var -> Annot SpecType -> CG () Source #
Add Identifier Annotations, used for annotation binders (i.e. at binder sites)
addLocA :: Maybe Var -> SrcSpan -> Annot SpecType -> CG () Source #
Used for annotating reads (i.e. at Var x sites)
updateLocA :: Maybe SrcSpan -> SpecType -> CG () Source #
Update annotations for a location, due to (ghost) predicate applications
addHole :: SrcSpan -> Var -> SpecType -> CGEnv -> CG () Source #
Record a term hole together with the type we assigned to it and the local environment needed to render a useful warning later.
addHoleANF :: (Var, SrcSpan) -> Var -> CoreExpr -> SpecType -> CG () Source #
Remember an ANF expression that mentions a hole-linked binder so the final warning can report the surrounding expressions that constrain the hole.
linkANFToHole :: Var -> (Var, SrcSpan) -> CG () Source #
Associate an ANF binder with the concrete hole occurrence it was created from so later traversals can recover the original hole.
isANFInHole :: Var -> CG (Maybe (Var, SrcSpan)) Source #
Resolve an ANF binder back to the hole occurrence that introduced it, if
the binder was previously linked by linkANFToHole.