Module Verify.NonFailConditions

nfcFalse :: ([(Int,TypeExpr)],Expr)   

The always unsatisfiable non-fail condition.

Further infos:

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

genNonFailCond :: [(Int,TypeExpr)] -> Expr -> ([(Int,TypeExpr)],Expr)   

Generate a non-fail condition from a list of variables types and a list of Boolean expressions.

combineNonFailConds :: ([(Int,TypeExpr)],Expr) -> ([(Int,TypeExpr)],Expr) -> ([(Int,TypeExpr)],Expr)   

Combine two non-fail conditions.

expandExpr :: [(Int,TypeExpr,Expr)] -> Expr -> Expr   

renameAllVars :: [(Int,Int)] -> Expr -> Expr   

nonfailSuffix :: String   

The suffix of functions specifying non-fail conditions.

Further infos:

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

nonFailCondsOfModule :: Prog -> [((String,String),([(Int,TypeExpr)],Expr))]   

Extracts explicit non-fail conditions specified in a module as operations with suffix 'nonfail.

lookupPredefinedNonFailCond :: (String,String) -> Maybe ([(Int,TypeExpr)],Expr)   

Returns the non-fail condition for particular predefined operations with non-trivial non-fail conditions.

predefinedNonFailConds :: [((String,String),([(Int,TypeExpr)],Expr))]   

intDivOps :: [(String,String)]   

Integer division operators defined in the prelude.

floatDivOps :: [(String,String)]   

Float division operators defined in the prelude.

showConditions :: [FuncDecl] -> [((String,String),([(Int,TypeExpr)],Expr))] -> String   

Prints a list of conditions for operations (if not empty). The first argument contains all function declarations of the current module.

genNonFailFunction :: [FuncDecl] -> ((String,String),([(Int,TypeExpr)],Expr)) -> (String,FuncDecl)   

Generates the function representing the non-fail condition for a given function and non-fail condition. The first argument is the list of all functions of the module.

transTester :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> Expr -> Expr   

allFreeVars :: Expr -> [Int]   

Gets all free variables (i.e., without let/free/pattern bound variables) occurring in an expression.