makeTransInfo
:: Options -> [AFuncDecl TypeExpr] -> TransInfo
|
initVState
:: TransInfo -> VState
|
readTransInfoRef
:: IORef VState -> IO TransInfo
Reads TransInfo from VState IORef. |
showStats
:: VState -> String
Shows the statistics in human-readable format. |
areContractsAdded
:: VState -> Bool
Is the program transformed so that some contracts are added? |
addPreCondToStats
:: String -> Bool -> VState -> VState
Increments the number of preconditions. |
addPostCondToStats
:: String -> Bool -> VState -> VState
Adds an operation to the already processed operations with postconditions. |
addProgToState
:: AProg TypeExpr -> VState -> VState
Adds a new typed FlatCurry program to the state. |
Constructors:
TransInfo
:: Options -> [AFuncDecl TypeExpr] -> [AFuncDecl TypeExpr] -> [AFuncDecl TypeExpr] -> TransInfo
Fields:
Constructors:
VState
:: TransInfo -> [String] -> [String] -> [String] -> [String] -> [AProg TypeExpr] -> VState
Fields:
|
|
Reads TransInfo from VState IORef. |
Is the program transformed so that some contracts are added?
|
Increments the number of preconditions. If the first argument is true, a precondition has been verified. |
Adds an operation to the already processed operations with postconditions. If the second argument is true, the postcondition of this operation has been verified. |
Adds a new typed FlatCurry program to the state.
|