TheoremUsage.curry 3.73 KB
Newer Older
Michael Hanus 's avatar
Michael Hanus committed
1 2 3 4 5 6 7 8 9 10 11
------------------------------------------------------------------------
--- 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
12 13 14 15 16 17
---   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`.
Michael Hanus 's avatar
Michael Hanus committed
18 19 20 21 22 23
---
---  * 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
24
--- @version October 2018
Michael Hanus 's avatar
Michael Hanus committed
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
------------------------------------------------------------------------

module TheoremUsage
  ( determinismTheoremFor
  , getProofFiles, existsProofFor, isProofFileName, 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.
getProofFiles :: String -> IO [String]
getProofFiles dir = do
  files <- getDirectoryContents dir
  return (filter isProofFileName files)

--- Does the list of file names (second argument) contain a proof of the
60 61 62 63
--- qualified theorem name given as the first argument?
existsProofFor :: QName -> [String] -> Bool
existsProofFor qpropname filenames =
  any (isProofFileNameFor qpropname) filenames
Michael Hanus 's avatar
Michael Hanus committed
64 65 66 67 68 69

--- Is this a file name with a proof, i.e., start it with `proof`?
isProofFileName :: String -> Bool
isProofFileName fn = "proof" `isPrefixOf` (map toLower fn)

--- Is this the file name of a proof of property `prop`?
70 71
isProofFileNameFor :: QName -> String -> Bool
isProofFileNameFor (mn,prop) fname =
Michael Hanus 's avatar
Michael Hanus committed
72
  let lfname = map toLower (dropExtension fname)
73
      lprop  = map toLower (mn ++ prop)
Michael Hanus 's avatar
Michael Hanus committed
74 75 76 77 78 79 80 81 82 83 84 85 86
   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]
Michael Hanus 's avatar
Michael Hanus committed
87
getTheoremFunctions proofdir (CurryProg _ _ _ _ _ _ functions _) = do
Michael Hanus 's avatar
Michael Hanus committed
88 89
  let propfuncs = filter isProperty functions -- all properties
  prooffiles <- getProofFiles proofdir
90
  return $ filter (\fd -> existsProofFor (funcName fd) prooffiles)
Michael Hanus 's avatar
Michael Hanus committed
91 92 93
                  propfuncs

------------------------------------------------------------------------