Module Verify.Files

Operations to write and read auxiliary files containing verification information.

The tool caches already computed analysis results about modules under the directory defined in getVerifyCacheDirectory which is usually ~/.curry_verify_cache/<CURRYSYSTEM>/....

Author: Michael Hanus

Version: July 2024

Summary of exported operations:

deleteVerifyCacheDirectory :: Options -> IO ()  Deterministic 
Delete the tool's cache directory (for the Curry system).
storeTypes :: TermDomain a => Options -> String -> [FuncDecl] -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [((String,String),Maybe [a])] -> [((String,String),Maybe [a])] -> [((String,String),([(Int,TypeExpr)],Expr))] -> [((String,String),InOutType a)] -> IO ()  Deterministic 
Stores constructores, call types, non-fail conditions and input/output types for a module.
typeFilesOutdated :: Options -> String -> IO Bool  Deterministic 
readCallCondTypes :: TermDomain a => Options -> String -> IO ([((String,String),Maybe [a])],[((String,String),([(Int,TypeExpr)],Expr))])  Deterministic 
readTypesOfModules :: TermDomain a => Options -> (Options -> String -> IO ()) -> [String] -> IO ([((String,String),(Int,ConsType,[((String,String),Int)]))],[((String,String),Maybe [a])],[((String,String),([(Int,TypeExpr)],Expr))],[((String,String),InOutType a)])  Deterministic 
Reads constructors, call types, non-fail conditions, and input/output types for a given list of modules.
readCallTypeFile :: TermDomain a => Options -> ClockTime -> String -> IO (Maybe [((String,String),Maybe [a])])  Deterministic 
Reads the possibly previously inferred abstract call types for a given module if it is up-to-date (where the modification time of the module is passed as the second argument).
readNonFailCondFile :: Options -> ClockTime -> String -> IO (Maybe [((String,String),([(Int,TypeExpr)],Expr))])  Deterministic 
Reads the possibly previously inferred non-fail conditions for a given module if it is up-to-date (where the modification time of the module is passed as the second argument).
readPublicCallTypeModule :: Options -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> ClockTime -> String -> IO [((String,String),[[CallType]])]  Non-deterministic 
Reads the public non-trivial call types (which have been already computed or explicitly specified) for a given module which are stored in the source directory of the module with module suffix _CALLTYPES.

Exported operations:

deleteVerifyCacheDirectory :: Options -> IO ()  Deterministic 

Delete the tool's cache directory (for the Curry system).

storeTypes :: TermDomain a => Options -> String -> [FuncDecl] -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [((String,String),Maybe [a])] -> [((String,String),Maybe [a])] -> [((String,String),([(Int,TypeExpr)],Expr))] -> [((String,String),InOutType a)] -> IO ()  Deterministic 

Stores constructores, call types, non-fail conditions and input/output types for a module.

typeFilesOutdated :: Options -> String -> IO Bool  Deterministic 

readCallCondTypes :: TermDomain a => Options -> String -> IO ([((String,String),Maybe [a])],[((String,String),([(Int,TypeExpr)],Expr))])  Deterministic 

readTypesOfModules :: TermDomain a => Options -> (Options -> String -> IO ()) -> [String] -> IO ([((String,String),(Int,ConsType,[((String,String),Int)]))],[((String,String),Maybe [a])],[((String,String),([(Int,TypeExpr)],Expr))],[((String,String),InOutType a)])  Deterministic 

Reads constructors, call types, non-fail conditions, and input/output types for a given list of modules. If some of the data files does not exist or is not newer than the module source, the operation provided as the second argument is applied before reading the files.

readCallTypeFile :: TermDomain a => Options -> ClockTime -> String -> IO (Maybe [((String,String),Maybe [a])])  Deterministic 

Reads the possibly previously inferred abstract call types for a given module if it is up-to-date (where the modification time of the module is passed as the second argument).

readNonFailCondFile :: Options -> ClockTime -> String -> IO (Maybe [((String,String),([(Int,TypeExpr)],Expr))])  Deterministic 

Reads the possibly previously inferred non-fail conditions for a given module if it is up-to-date (where the modification time of the module is passed as the second argument).

readPublicCallTypeModule :: Options -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> ClockTime -> String -> IO [((String,String),[[CallType]])]  Non-deterministic 

Reads the public non-trivial call types (which have been already computed or explicitly specified) for a given module which are stored in the source directory of the module with module suffix _CALLTYPES. If the file does not exist, try to read a file from the include directory (for standard libraries).