Test.Target.Monad

Synopsis

• whenVerbose :: Target () -> Target ()
• noteUsed :: (Symbol, Value) -> Target ()
• addDep :: Symbol -> Expr -> Target ()
• addConstraint :: Expr -> Target ()
• addConstructor :: Variable -> Target ()
• addSort :: Sort -> Target ()
• addVariable :: Variable -> Target ()
• inModule :: Symbol -> Target a -> Target a
• making :: Sort -> Target a -> Target a
• lookupCtor :: Symbol -> SpecType -> 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)]
  • 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 {
  • depth :: !Int
  • solver :: !SMTSolver
  • verbose :: !Bool
  • logging :: !Bool
  • keepGoing :: !Bool
  • maxSuccess :: !(Maybe Int)
  • scDepth :: !Bool
  • ghcOpts :: ![String]
  }
• defaultOpts :: TargetOpts

Documentation