| Copyright | (c) 2013-2015 Galois, Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell98 |
Cryptol.Symbolic
Description
- proverConfigs :: [(String, SMTConfig)]
- proverNames :: [String]
- lookupProver :: String -> SMTConfig
- type SatResult = [(Type, Expr, Value)]
- data ProverResult
- allSatSMTResults :: AllSatResult -> [SMTResult]
- thmSMTResults :: ThmResult -> [SMTResult]
- satProve :: Bool -> Maybe Int -> (String, Bool, Bool) -> [DeclGroup] -> Maybe FilePath -> (Expr, Schema) -> ModuleCmd ProverResult
- satProveOffline :: Bool -> Bool -> Bool -> [DeclGroup] -> Maybe FilePath -> (Expr, Schema) -> ModuleCmd ProverResult
- protectStack :: Bool -> ModuleCmd ProverResult -> ModuleCmd ProverResult
- parseValues :: [FinType] -> [CW] -> ([Value], [CW])
- parseValue :: FinType -> [CW] -> (Value, [CW])
- allDeclGroups :: ModuleEnv -> [DeclGroup]
- data FinType
- numType :: Type -> Maybe Int
- finType :: Type -> Maybe FinType
- unFinType :: FinType -> Type
- predArgTypes :: Schema -> Either String [FinType]
- forallFinType :: FinType -> Symbolic Value
- existsFinType :: FinType -> Symbolic Value
- data Env = Env {}
- emptyEnv :: Bool -> Env
- bindVar :: (QName, Value) -> Env -> Env
- lookupVar :: QName -> Env -> Maybe Value
- bindType :: TVar -> TValue -> Env -> Env
- lookupType :: TVar -> Env -> Maybe TValue
- evalExpr :: Env -> Expr -> Value
- evalType :: Env -> Type -> TValue
- evalSel :: Selector -> Value -> Value
- evalDecls :: Env -> [DeclGroup] -> Env
- evalDeclGroup :: Env -> DeclGroup -> Env
- evalDecl :: Env -> Decl -> (QName, Value)
- copyBySchema :: Env -> Schema -> Value -> Value
- copyByType :: Env -> TValue -> Value -> Value
- evalComp :: Env -> TValue -> Expr -> [[Match]] -> Value
- branchEnvs :: Env -> [Match] -> [Env]
- evalMatch :: Env -> Match -> [Env]
Documentation
proverConfigs :: [(String, SMTConfig)] Source
proverNames :: [String] Source
lookupProver :: String -> SMTConfig Source
data ProverResult Source
A prover result is either an error message, an empty result (eg for the offline prover), a counterexample or a lazy list of satisfying assignments.
Constructors
| AllSatResult [SatResult] | |
| ThmResult [Type] | |
| EmptyResult | |
| ProverError String |
allSatSMTResults :: AllSatResult -> [SMTResult] Source
thmSMTResults :: ThmResult -> [SMTResult] Source
satProveOffline :: Bool -> Bool -> Bool -> [DeclGroup] -> Maybe FilePath -> (Expr, Schema) -> ModuleCmd ProverResult Source
allDeclGroups :: ModuleEnv -> [DeclGroup] Source
forallFinType :: FinType -> Symbolic Value Source
existsFinType :: FinType -> Symbolic Value Source
evalDeclGroup :: Env -> DeclGroup -> Env Source
copyBySchema :: Env -> Schema -> Value -> Value Source
Make a copy of the given value, building the spine based only on the type without forcing the value argument. This lets us avoid strictness problems when evaluating recursive definitions.
branchEnvs :: Env -> [Match] -> [Env] Source
Turn a list of matches into the final environments for each iteration of the branch.