Module Main

test :: Int -> String -> IO ()   

testv :: String -> IO ()   

testcv :: String -> IO ()   

banner :: String   

main :: IO ()   

verifyNonFailingModules :: Options -> [String] -> [String] -> IO ()   

verifyNonFailingMod :: Options -> String -> IO ()   

loadAnalysisWithImports :: (Read a, Show a) => Analysis a -> AProg TypeExpr -> IO (ProgInfo a)   

makeTransState :: Int -> [(Int,TypeExpr)] -> TransState   

Further infos:

• solution complete, i.e., able to compute all solutions

emptyTransState :: TransState   

getFreshVarIndex :: StateT TransState IO Int   

setFreshVarIndex :: Int -> StateT TransState IO ()   

getFreshVar :: StateT TransState IO Int   

incFreshVarIndex :: TransState -> TransState   

getVarTypes :: StateT TransState IO [(Int,TypeExpr)]   

addVarTypes :: [(Int,TypeExpr)] -> StateT TransState IO ()   

getAssertion :: StateT TransState IO Term   

setAssertion :: Term -> StateT TransState IO ()   

addToAssertion :: Term -> StateT TransState IO ()   

proveNonFailingFuncs :: Options -> ProgInfo [((String,String),Int)] -> IORef VState -> [AFuncDecl TypeExpr] -> IO ()   

proveNonFailingFunc :: Options -> ProgInfo [((String,String),Int)] -> IORef VState -> AFuncDecl TypeExpr -> IO ()   

proveNonFailingRule :: Options -> ProgInfo [((String,String),Int)] -> IORef VState -> (String,String) -> TypeExpr -> ARule TypeExpr -> IO ()   

missingConsInBranch :: ProgInfo [((String,String),Int)] -> [ABranchExpr TypeExpr] -> [((String,String),Int)]   

simpExpr :: AExpr TypeExpr -> AExpr TypeExpr   

binding2SMT :: Bool -> VerifyInfo -> (Int,AExpr TypeExpr) -> StateT TransState IO Term   

nonfailPreCondExpOf :: VerifyInfo -> (String,String) -> TypeExpr -> [(Int,TypeExpr)] -> StateT TransState IO Term   

nonfailCondExpOf :: VerifyInfo -> (String,String) -> TypeExpr -> [(Int,TypeExpr)] -> StateT TransState IO ([(Int,TypeExpr)],Term)   

preCondExpOf :: VerifyInfo -> (String,String) -> [(Int,TypeExpr)] -> StateT TransState IO Term   

postCondExpOf :: VerifyInfo -> (String,String) -> [(Int,TypeExpr)] -> StateT TransState IO Term   

applyFunc :: AFuncDecl TypeExpr -> [(Int,TypeExpr)] -> StateT TransState IO (AExpr TypeExpr)   

pred2SMT :: AExpr TypeExpr -> StateT TransState IO Term   

normalizeArgs :: [AExpr TypeExpr] -> StateT TransState IO ([(Int,AExpr TypeExpr)],[AExpr TypeExpr])   

getFreshVarsForTypes :: [TypeExpr] -> StateT TransState IO [(Int,TypeExpr)]   

renameLetVars :: [((Int,TypeExpr),AExpr TypeExpr)] -> AExpr TypeExpr -> StateT TransState IO ([((Int,TypeExpr),AExpr TypeExpr)],AExpr TypeExpr)   

renameFreeVars :: [(Int,TypeExpr)] -> AExpr TypeExpr -> StateT TransState IO ([(Int,TypeExpr)],AExpr TypeExpr)   

renamePatternVars :: ABranchExpr TypeExpr -> StateT TransState IO (ABranchExpr TypeExpr)   

checkImplicationWithSMT :: Options -> IORef VState -> String -> [(Int,TypeExpr)] -> Term -> Term -> Term -> IO (Maybe Bool)   

axiomatizedOps :: [String]   

Further infos:

• solution complete, i.e., able to compute all solutions

typedVar2SMT :: (Int,TypeExpr) -> Command   

tconsOfTypeExpr :: TypeExpr -> [(String,String)]   

testBoolCase :: [ABranchExpr TypeExpr] -> Maybe (AExpr TypeExpr,AExpr TypeExpr)   

Tests whether the given branches of a case expressions are a Boolean case distinction. If yes, the expressions of the False and True branch are returned.

showWithLineNums :: String -> String   

Shows a text with line numbers prefixed:

ilog :: Int -> Int   

The value of ilog n is the floor of the logarithm in the base 10 of n. Fails if n <= 0. For positive integers, the returned value is 1 less the number of digits in the decimal representation of n.

Example call:

(ilog n)

Parameters:

• n : The argument.

Returns:

the floor of the logarithm in the base 10 of n.