------------------------------------------------------------------------
--- 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 October 2018
------------------------------------------------------------------------
module TheoremUsage
( determinismTheoremFor
, getModuleProofFiles, existsProofFor, isProofFileNameFor
, getTheoremFunctions
) where
import AbstractCurry.Types
import AbstractCurry.Select
import Char
import Directory
import Distribution (lookupModuleSourceInLoadPath, modNameToPath)
import FilePath (dropExtension, takeDirectory)
import List
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
------------------------------------------------------------------------