| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Solver.Monad
Description
This is a wrapper around IO that permits SMT queries
Synopsis
- type SolveM ann = StateT (SolverState ann) IO
- liftSMT :: SmtM a -> SolveM ann a
- runSolverM :: Config -> SolverInfo ann -> ElabParam -> SolveM ann a -> IO a
- getContext :: SolveM ann Context
- filterRequired :: Cand a -> Expr -> SolveM ann [a]
- filterValid :: SrcSpan -> Expr -> Cand a -> SolveM ann [a]
- smtEnablembqi :: SolveM ann ()
- sendConcreteBindingsToSMT :: IBindEnv -> BindEnv ann -> (IBindEnv -> SolveM ann a) -> SolveM ann a
- data Stats
- tickIter :: Bool -> SolveM ann Int
- stats :: SolveM ann Stats
- numIter :: Stats -> Int
- data SolverState ann = SS {}
- modifyContext :: (Context -> Context) -> SolveM ann ()
Type
type SolveM ann = StateT (SolverState ann) IO Source #
Solver Monadic API --------------------------------------------------------
Execution
runSolverM :: Config -> SolverInfo ann -> ElabParam -> SolveM ann a -> IO a Source #
getContext :: SolveM ann Context Source #
SMT Query
filterRequired :: Cand a -> Expr -> SolveM ann [a] Source #
`filterRequired [(x1, p1),...,(xn, pn)] q` returns a minimal list [xi] s.t. / [pi] => q
filterValid :: SrcSpan -> Expr -> Cand a -> SolveM ann [a] Source #
`filterValid p [(q1, x1),...,(qn, xn)]` returns the list `[ xi | p => qi]`
smtEnablembqi :: SolveM ann () Source #
sendConcreteBindingsToSMT :: IBindEnv -> BindEnv ann -> (IBindEnv -> SolveM ann a) -> SolveM ann a Source #
SMT Interface -------------------------------------------------------------
Takes the environment of bindings already known to the SMT, and the environment of all bindings that need to be known.
Yields the ids of bindings known to the SMT
Debug
Instances
data SolverState ann Source #