| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Test.Target.Monad
- whenVerbose :: Target () -> Target ()
- noteUsed :: (Symbol, Value) -> Target ()
- addDep :: Symbol -> Expr -> Target ()
- addConstraint :: Pred -> Target ()
- addConstructor :: Variable -> Target ()
- inModule :: Symbol -> Target a -> Target a
- making :: Sort -> Target a -> Target a
- lookupCtor :: Symbol -> Target SpecType
- guarded :: String -> Target Expr -> Target (Expr, Expr)
- fresh :: Sort -> Target Symbol
- freshChoice :: String -> Target Symbol
- freshInt :: Target Int
- getValue :: Symbol -> Target Value
- data Target a
- runTarget :: TargetOpts -> TargetState -> Target a -> IO a
- data TargetState = TargetState {
- variables :: ![Variable]
- choices :: ![Variable]
- constraints :: !Constraint
- deps :: !(HashMap Symbol [Symbol])
- realized :: ![(Symbol, Value)]
- dconEnv :: ![(Symbol, DataConP)]
- ctorEnv :: !DataConEnv
- measEnv :: !MeasureEnv
- embEnv :: !(TCEmb TyCon)
- tyconInfo :: !(HashMap TyCon RTyCon)
- freesyms :: ![(Symbol, Symbol)]
- constructors :: ![Variable]
- sigs :: ![(Symbol, SpecType)]
- chosen :: !(Maybe Symbol)
- sorts :: !(HashSet Sort)
- modName :: !Symbol
- filePath :: !FilePath
- makingTy :: !Sort
- smtContext :: !Context
- initState :: FilePath -> GhcSpec -> Context -> TargetState
- data TargetOpts = TargetOpts {}
- defaultOpts :: TargetOpts
Documentation
whenVerbose :: Target () -> Target () Source
addConstraint :: Pred -> Target () Source
addConstructor :: Variable -> Target () Source
lookupCtor :: Symbol -> Target SpecType Source
Find the refined type of a data constructor.
guarded :: String -> Target Expr -> Target (Expr, Expr) Source
Given a data constructor d and an action, create a new choice variable
c and execute the action while guarding any generated constraints with
c. Returns (action-result, c).
freshChoice :: String -> Target Symbol Source
Given a data constructor d, create a new choice variable corresponding to
d.
runTarget :: TargetOpts -> TargetState -> Target a -> IO a Source
data TargetState Source
Constructors
| TargetState | |
Fields
| |
Instances
data TargetOpts Source
Constructors
| TargetOpts | |
Fields
| |
Instances