Module Verify.NonFailConditions

Definition and some operations for non-fail conditions.

Author: Michael Hanus

Version: March 2024

Summary of exported operations:

nfcFalse :: ([(Int,TypeExpr)],Expr)  Deterministic 
The always unsatisfiable non-fail condition.
genNonFailCond :: [(Int,TypeExpr)] -> Expr -> ([(Int,TypeExpr)],Expr)  Deterministic 
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)  Deterministic 
Combine two non-fail conditions.
expandExpr :: [(Int,TypeExpr,Expr)] -> Expr -> Expr  Deterministic 
renameAllVars :: [(Int,Int)] -> Expr -> Expr  Deterministic 
nonfailSuffix :: String  Deterministic 
The suffix of functions specifying non-fail conditions.
nonFailCondsOfModule :: Prog -> [((String,String),([(Int,TypeExpr)],Expr))]  Deterministic 
Extracts explicit non-fail conditions specified in a module as operations with suffix 'nonfail.
lookupPredefinedNonFailCond :: (String,String) -> Maybe ([(Int,TypeExpr)],Expr)  Deterministic 
Returns the non-fail condition for particular predefined operations with non-trivial non-fail conditions.
predefinedNonFailConds :: [((String,String),([(Int,TypeExpr)],Expr))]  Deterministic 
intDivOps :: [(String,String)]  Deterministic 
Integer division operators defined in the prelude.
floatDivOps :: [(String,String)]  Deterministic 
Float division operators defined in the prelude.
showConditions :: [FuncDecl] -> [((String,String),([(Int,TypeExpr)],Expr))] -> String  Deterministic 
Prints a list of conditions for operations (if not empty).
genNonFailFunction :: [FuncDecl] -> ((String,String),([(Int,TypeExpr)],Expr)) -> (String,FuncDecl)  Deterministic 
Generates the function representing the non-fail condition for a given function and non-fail condition.
transTester :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> Expr -> Expr  Deterministic 
allFreeVars :: Expr -> [Int]  Deterministic 
Gets all free variables (i.e., without let/free/pattern bound variables) occurring in an expression.

Exported datatypes:


NonFailCond

Non-fail conditions are represented as a pair of typed variables occurring in the conditions and a Boolean expression (in FlatCurry representation).

Type synonym: NonFailCond = ([(Int,TypeExpr)],Expr)


Exported operations:

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

The always unsatisfiable non-fail condition.

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

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

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)  Deterministic 

Combine two non-fail conditions.

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

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

nonfailSuffix :: String  Deterministic 

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))]  Deterministic 

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

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

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

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

intDivOps :: [(String,String)]  Deterministic 

Integer division operators defined in the prelude.

floatDivOps :: [(String,String)]  Deterministic 

Float division operators defined in the prelude.

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

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)  Deterministic 

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  Deterministic 

allFreeVars :: Expr -> [Int]  Deterministic 

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