Cryptol.Symbolic

Description

Synopsis

• proverConfigs :: [(String, SMTConfig)]
• proverNames :: [String]
• lookupProver :: String -> SMTConfig
• type SatResult = [(Type, Expr, Value)]
• data SatNum
  • = AllSat
  • | SomeSat Int
• data QueryType
  • = SatQuery SatNum
  • | ProveQuery
• data ProverCommand = ProverCommand {
  • pcQueryType :: QueryType
  • pcProverName :: String
  • pcVerbose :: Bool
  • pcExtraDecls :: [DeclGroup]
  • pcSmtFile :: Maybe FilePath
  • pcExpr :: Expr
  • pcSchema :: Schema
  }
• data ProverResult
  • = AllSatResult [SatResult]
  • | ThmResult [Type]
  • | EmptyResult
  • | ProverError String
• satSMTResults :: SatResult -> [SMTResult]
• allSatSMTResults :: AllSatResult -> [SMTResult]
• thmSMTResults :: ThmResult -> [SMTResult]
• proverError :: String -> ModuleCmd ProverResult
• satProve :: ProverCommand -> ModuleCmd ProverResult
• satProveOffline :: ProverCommand -> ModuleCmd (Either String String)
• protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
• parseValues :: [FinType] -> [CW] -> ([Value], [CW])
• parseValue :: FinType -> [CW] -> (Value, [CW])
• allDeclGroups :: ModuleEnv -> [DeclGroup]
• data FinType
  • = FTBit
  • | FTSeq Int FinType
  • | FTTuple [FinType]
  • | FTRecord [(Ident, FinType)]
• numType :: Integer -> Maybe Int
• finType :: TValue -> Maybe FinType
• unFinType :: FinType -> Type
• predArgTypes :: Schema -> Either String [FinType]
• forallFinType :: FinType -> Symbolic Value
• existsFinType :: FinType -> Symbolic Value
• data Env = Env {
  • envVars :: Map Name Value
  • envTypes :: Map TVar (Either Nat' TValue)
  }
• bindVar :: (Name, Value) -> Env -> Env
• lookupVar :: Name -> Env -> Maybe Value
• bindType :: TVar -> Either Nat' TValue -> Env -> Env
• lookupType :: TVar -> Env -> Maybe (Either Nat' TValue)
• evalExpr :: Env -> Expr -> Value
• evalValType :: Env -> Type -> TValue
• evalNumType :: Env -> Type -> Nat'
• evalSel :: Selector -> Value -> Value
• evalDecls :: Env -> [DeclGroup] -> Env
• evalDeclGroup :: Env -> DeclGroup -> Env
• evalDecl :: Env -> Decl -> (Name, 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