PAKCS
Exported names: Imported modules:

Module Main

A tool to verify non-failure properties of Curry operations.

Author: Michael Hanus

Version: April 2018

Summary of exported operations:

test :: Int -> String -> IO ()   
testv :: String -> IO ()   
:: String   
main :: IO ()   
verifyNonFailingModules :: Options -> [String] -> [String] -> IO ()   
verifyNonFailingMod :: Options -> String -> IO ()   
loadAnalysisWithImports :: Analysis a -> AProg TypeExpr -> IO (ProgInfo a)   
initTransInfo :: Options -> TransInfo   
addFunsToTransInfo :: [AFuncDecl TypeExpr] -> TransInfo -> TransInfo   
isContractOp :: (String,String) -> Bool   
Is an operation name the name of a contract or similar?
isProperty :: AFuncDecl TypeExpr -> Bool   
Is a function declaration a property?
makeTransState :: Int -> [(Int,TypeExpr)] -> TransState   
incFreshVarIndex :: TransState -> TransState   
addVarTypes :: [(Int,TypeExpr)] -> TransState -> TransState   
proveNonFailingFuncs :: Options -> ProgInfo [((String,String),Int)] -> TransInfo -> [AFuncDecl TypeExpr] -> VState -> IO VState   
proveNonFailingFunc :: Options -> ProgInfo [((String,String),Int)] -> TransInfo -> IORef VState -> AFuncDecl TypeExpr -> IO ()   
proveNonFailingRule :: Options -> ProgInfo [((String,String),Int)] -> TransInfo -> (String,String) -> Int -> ARule TypeExpr -> IORef VState -> IO ()   
missingConsInBranch :: ProgInfo [((String,String),Int)] -> [ABranchExpr TypeExpr] -> [((String,String),Int)]   
simpExpr :: AExpr TypeExpr -> AExpr TypeExpr   
exp2bool :: Bool -> TransInfo -> (Int,AExpr TypeExpr) -> TransState -> (BoolExp,TransState)   
transSpecialName :: (String,String) -> (String,String)   
nonfailPreCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   
nonfailCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   
preCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   
postCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   
applyFunc :: AFuncDecl TypeExpr -> [Int] -> TransState -> (AExpr TypeExpr,TransState)   
pred2bool :: AExpr TypeExpr -> TransState -> (BoolExp,TransState)   
normalizeArgs :: [AExpr TypeExpr] -> TransState -> (([(Int,AExpr TypeExpr)],[AExpr TypeExpr]),TransState)   
renameLetVars :: TransState -> [((Int,TypeExpr),AExpr TypeExpr)] -> AExpr TypeExpr -> (([((Int,TypeExpr),AExpr TypeExpr)],AExpr TypeExpr),TransState)   
renameFreeVars :: TransState -> [(Int,TypeExpr)] -> AExpr TypeExpr -> (([(Int,TypeExpr)],AExpr TypeExpr),TransState)   
renamePatternVars :: TransState -> ABranchExpr TypeExpr -> (ABranchExpr TypeExpr,TransState)   
addSuffix :: (String,String) -> String -> (String,String)   
checkImplicationWithSMT :: Options -> IORef VState -> [(Int,TypeExpr)] -> BoolExp -> BoolExp -> BoolExp -> IO (Maybe Bool)   
axiomatizedOps :: [String]   
typedVars2SMT :: [(Int,TypeExpr)] -> String   
tconsOfTypeExpr :: TypeExpr -> [(String,String)]   
fileInPath :: String -> IO Bool   
Checks whether a file exists in one of the directories on the PATH.
testBoolCase :: [ABranchExpr TypeExpr] -> Maybe (AExpr TypeExpr,AExpr TypeExpr)   
Tests whether the given branches of a case expressions are a Boolean case distinction.

Exported datatypes:

TransInfo

Constructors:

TransState

Constructors:

Exported operations:

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

testv :: String -> IO ()   

main :: IO ()   

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

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

initTransInfo :: Options -> TransInfo   

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

isContractOp :: (String,String) -> Bool   

Is an operation name the name of a contract or similar?

isProperty :: AFuncDecl TypeExpr -> Bool   

Is a function declaration a property?

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

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

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

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

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

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

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

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

exp2bool :: Bool -> TransInfo -> (Int,AExpr TypeExpr) -> TransState -> (BoolExp,TransState)   

transSpecialName :: (String,String) -> (String,String)   

nonfailPreCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   

nonfailCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   

preCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   

postCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   

addSuffix :: (String,String) -> String -> (String,String)   

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

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

axiomatizedOps :: [String]   

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

typedVars2SMT :: [(Int,TypeExpr)] -> String   

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

fileInPath :: String -> IO Bool   

Checks whether a file exists in one of the directories on the PATH.

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.