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_verifycache/....

Author: Michael Hanus

Version: October 2023

Summary of exported operations:

deleteVerifyCacheDirectory :: Options -> IO ()  Deterministic 
Delete the tool's cache directory (for the Curry system).
storeTypes :: TermDomain a => Options -> String -> [[((String,String),Int)]] -> [((String,String),Maybe [a])] -> [((String,String),InOutType a)] -> IO ()  Non-deterministic 
readTypesOfModules :: TermDomain a => Options -> (Options -> String -> IO ()) -> [String] -> IO ([[((String,String),Int)]],[((String,String),Maybe [a])],[((String,String),InOutType a)])  Non-deterministic 
Reads constructors, call types, and input/output types for a given list of modules.
readCallTypeFile :: TermDomain a => Options -> ClockTime -> String -> IO (Maybe [((String,String),Maybe [a])])  Non-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).
readPublicCallTypeModule :: Options -> [[((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 -> [[((String,String),Int)]] -> [((String,String),Maybe [a])] -> [((String,String),InOutType a)] -> IO ()  Non-deterministic 

readTypesOfModules :: TermDomain a => Options -> (Options -> String -> IO ()) -> [String] -> IO ([[((String,String),Int)]],[((String,String),Maybe [a])],[((String,String),InOutType a)])  Non-deterministic 

Reads constructors, call types, and input/output types for a given list of modules. If some of the data files do not exists or are 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])])  Non-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).

readPublicCallTypeModule :: Options -> [[((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).