1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 |
------------------------------------------------------------------------ --- This module contains some operations to access and check proof --- for theorems formulated as properties in Curry programs. --- --- Current assumptions: --- * A theorem is represented in a source file as a EasyCheck property, e.g.: --- --- sortPreservesLength xs = length xs -=- length (sort xs) --- --- * A theorem is considered as proven and, thus, not be checked --- by CurryCheck or the contract wrapper (see `currypp`), if there exists --- a file named with prefix "Proof" and the qualified name of the theorem, --- e.g., `Proof-Sort-sortPreservesLength.agda`. --- The name is not case sensitive, the file name extension is arbitrary --- and the special characters in the name are ignored. --- Hence, a proof for `sortlength` could be also stored in --- a file named `PROOF_Sort_sort_preserves_length.smt`. --- --- * A proof that some operation `f` is deterministic has the name --- `fIsDeterministic` so that a proof for `last` can be stored in --- `proof-last-is-deterministic.agda` (and also in some other files). --- --- @author Michael Hanus --- @version December 2018 ------------------------------------------------------------------------ module TheoremUsage ( determinismTheoremFor , getModuleProofFiles, existsProofFor, isProofFileNameFor , getTheoremFunctions ) where import AbstractCurry.Types import AbstractCurry.Select import Char import Directory import FilePath ( dropExtension, takeDirectory ) import List import System.CurryPath ( lookupModuleSourceInLoadPath, modNameToPath ) import PropertyUsage ------------------------------------------------------------------------ --- The name of a proof of a determinism annotation for the operation --- given as the argument. determinismTheoremFor :: String -> String determinismTheoremFor funcname = funcname ++ "isdeterministic" ------------------------------------------------------------------------ -- Operations for proof files: --- Get the names of all files in the directory (first argument) containing --- proofs of theorems of the module (second argument). getModuleProofFiles :: String -> String -> IO [String] getModuleProofFiles dir mod = do files <- getDirectoryContents dir return (filter (isModuleProofFileName mod) files) --- Does the list of file names (second argument) contain a proof of the --- qualified theorem name given as the first argument? existsProofFor :: QName -> [String] -> Bool existsProofFor qpropname filenames = any (isProofFileNameFor qpropname) filenames --- Is the second argument a file name with a proof of some theorem of a module --- (first argument), i.e., start it with `proof` and the module name? isModuleProofFileName :: String -> String -> Bool isModuleProofFileName mn fn = deleteNonAlphanNum ("proof" ++ map toLower mn) `isPrefixOf` deleteNonAlphanNum (map toLower fn) --- Is this the file name of a proof of property `prop`? isProofFileNameFor :: QName -> String -> Bool isProofFileNameFor (mn,prop) fname = let lfname = map toLower (dropExtension fname) lprop = map toLower (mn ++ prop) in if "proof" `isPrefixOf` lfname then deleteNonAlphanNum (drop 5 lfname) == deleteNonAlphanNum lprop else False --- Delete non alphanumeric characters. deleteNonAlphanNum :: String -> String deleteNonAlphanNum = filter isAlphaNum ------------------------------------------------------------------------ --- Get all theorems which are contained in a given program. --- A theorem is a property for which a proof file exists in the --- directory provided as first argument. getTheoremFunctions :: String -> CurryProg -> IO [CFuncDecl] getTheoremFunctions proofdir (CurryProg mn _ _ _ _ _ functions _) = do let propfuncs = filter isProperty functions -- all properties prooffiles <- getModuleProofFiles proofdir mn return $ filter (\fd -> existsProofFor (funcName fd) prooffiles) propfuncs ------------------------------------------------------------------------ |