TheoremUsage.curry 3.96 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
------------------------------------------------------------------------

module TheoremUsage
  ( determinismTheoremFor
29
  , getModuleProofFiles, existsProofFor, isProofFileNameFor
Michael Hanus 's avatar
Michael Hanus committed
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
  , 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:

52 53 54 55 56 57 58
--- 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)

Michael Hanus 's avatar
Michael Hanus committed
59
--- 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 70 71
--- 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)

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

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