pcQueryType :: QueryType: The type of query to run
pcProverName :: String: Which prover to use (one of the strings in proverConfigs)
pcVerbose :: Bool: Verbosity flag passed to SBV
pcExtraDecls :: [DeclGroup]: Extra declarations to bring into scope for symbolic simulation
pcSmtFile :: Maybe FilePath: Optionally output the SMTLIB query to a file
pcExpr :: Expr: The typechecked expression to evaluate
pcSchema :: Schema: The Schema of pcExpr

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

satSMTResults :: SatResult -> [SMTResult] Source

allSatSMTResults :: AllSatResult -> [SMTResult] Source

thmSMTResults :: ThmResult -> [SMTResult] Source

proverError :: String -> ModuleCmd ProverResult Source

satProve :: ProverCommand -> ModuleCmd ProverResult Source

satProveOffline :: ProverCommand -> ModuleCmd (Either String String) Source

protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a Source

parseValues :: [FinType] -> [CW] -> ([Value], [CW]) Source

parseValue :: FinType -> [CW] -> (Value, [CW]) Source

allDeclGroups :: ModuleEnv -> [DeclGroup] Source

data FinType Source

Constructors

FTBit
FTSeq Int FinType
FTTuple [FinType]
FTRecord [(Name, FinType)]

numType :: Type -> Maybe Int Source

finType :: Type -> Maybe FinType Source

unFinType :: FinType -> Type Source

predArgTypes :: Schema -> Either String [FinType] Source

forallFinType :: FinType -> Symbolic Value Source

existsFinType :: FinType -> Symbolic Value Source

data Env Source

Constructors

Env
Fields envVars :: Map QName Value envTypes :: Map TVar TValue

Instances

Monoid Env Source

emptyEnv :: Env Source

bindVar :: (QName, Value) -> Env -> Env Source

Bind a variable in the evaluation environment.

lookupVar :: QName -> Env -> Maybe Value Source

Lookup a variable in the environment.

bindType :: TVar -> TValue -> Env -> Env Source

Bind a type variable of kind *.

lookupType :: TVar -> Env -> Maybe TValue Source

Lookup a type variable.

evalExpr :: Env -> Expr -> Value Source

evalType :: Env -> Type -> TValue Source

evalSel :: Selector -> Value -> Value Source

evalDecls :: Env -> [DeclGroup] -> Env Source

evalDeclGroup :: Env -> DeclGroup -> Env Source

evalDecl :: Env -> Decl -> (QName, Value) 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.

copyByType :: Env -> TValue -> Value -> Value Source

evalComp :: Env -> TValue -> Expr -> [[Match]] -> Value Source

Evaluate a comprehension.

branchEnvs :: Env -> [Match] -> [Env] Source

Turn a list of matches into the final environments for each iteration of the branch.

evalMatch :: Env -> Match -> [Env] Source

Turn a match into the list of environments it represents.