intensional-datatys-0.2.0.0: A GHC Core plugin for intensional datatype refinement checking

Safe Haskell	None
Language	Haskell2010

Intensional.InferM

Synopsis

type InferM = RWS InferEnv ConstraintSet InferState
type Context = Map Name Scheme
data InferEnv = InferEnv {
- modName :: Module
- varEnv :: Context
- inferLoc :: SrcSpan
}
data Stats = Stats {
- getK :: Int
- getD :: Int
- getV :: Int
- getI :: Int
- getN :: Int
}
runInferM :: InferM a -> Module -> Context -> (a, [Atomic], Stats)
saturate :: Refined a => InferM a -> InferM a
branchAny :: [DataCon] -> DataType TyCon -> InferM a -> InferM a
emitDD :: DataType TyCon -> DataType TyCon -> InferM ()
emitDK :: DataType TyCon -> [DataCon] -> SrcSpan -> InferM ()
emitKD :: DataCon -> SrcSpan -> DataType TyCon -> InferM ()
fresh :: InferM RVar
putVar :: Name -> Scheme -> InferM a -> InferM a
putVars :: Context -> InferM a -> InferM a
setLoc :: SrcSpan -> InferM a -> InferM a
getExternalName :: NamedThing a => a -> InferM Name
isTrivial :: TyCon -> Bool
isIneligible :: TyCon -> InferM Bool
noteD :: Int -> InferM ()
noteK :: Int -> InferM ()
incrN :: InferM ()
noteErrs :: ConstraintSet -> InferM ()
cexs :: ConstraintSet -> InferM ConstraintSet

Documentation

type InferM = RWS InferEnv ConstraintSet InferState Source #

type Context = Map Name Scheme Source #

data InferEnv Source #

Constructors

InferEnv
Fields modName :: Module varEnv :: Context inferLoc :: SrcSpan

data Stats Source #

Constructors

Stats
Fields getK :: Int getD :: Int getV :: Int getI :: Int getN :: Int

runInferM :: InferM a -> Module -> Context -> (a, [Atomic], Stats) Source #

saturate :: Refined a => InferM a -> InferM a Source #

branchAny :: [DataCon] -> DataType TyCon -> InferM a -> InferM a Source #

emitDD :: DataType TyCon -> DataType TyCon -> InferM () Source #

emitDK :: DataType TyCon -> [DataCon] -> SrcSpan -> InferM () Source #

emitKD :: DataCon -> SrcSpan -> DataType TyCon -> InferM () Source #

fresh :: InferM RVar Source #

putVar :: Name -> Scheme -> InferM a -> InferM a Source #

putVars :: Context -> InferM a -> InferM a Source #

setLoc :: SrcSpan -> InferM a -> InferM a Source #

getExternalName :: NamedThing a => a -> InferM Name Source #

isTrivial :: TyCon -> Bool Source #

isIneligible :: TyCon -> InferM Bool Source #

noteD :: Int -> InferM () Source #

noteK :: Int -> InferM () Source #

incrN :: InferM () Source #

noteErrs :: ConstraintSet -> InferM () Source #

Given a set of trivially unsatisfiable constraints es, noteErrs es is the action that records them in the accumulating set in the inference state.

cexs :: ConstraintSet -> InferM ConstraintSet Source #

Given a constraint set cs, cexs cs is the inference action that attempts to build a model of cs and returns the set of counterexamples.