Module TheoremUsage

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 name of the theorem, e.g., Proof-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-perserves-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: August 2016

Summary of exported operations:

determinismTheoremFor
                  :: String -> String

The name of a proof of a determinism annotation for the operation given as the argument.

getProofFiles
                  :: String -> IO [String]

Get the names of all files in the directory (first argument) containing proofs of theorems.

existsProofFor
                  :: String -> [String] -> Bool

Does the list of file names (second argument) contain a proof of the theorem given as the first argument?

isProofFileName
                  :: String -> Bool

Is this a file name with a proof, i.e., start it with proof?

isProofFileNameFor
                  :: String -> String -> Bool

Is this the file name of a proof of property prop?

getTheoremFunctions
                  :: String -> CurryProg -> IO [CFuncDecl]

Get all theorems which are contained in a given program.

Exported operations:

determinismTheoremFor :: String -> String

The name of a proof of a determinism annotation for the operation given as the argument.

Further infos:

solution complete, i.e., able to compute all solutions

getProofFiles :: String -> IO [String]

Get the names of all files in the directory (first argument) containing proofs of theorems.

existsProofFor :: String -> [String] -> Bool

Does the list of file names (second argument) contain a proof of the theorem given as the first argument?

isProofFileName :: String -> Bool

Is this a file name with a proof, i.e., start it with proof?

isProofFileNameFor :: String -> String -> Bool

Is this the file name of a proof of property prop?

getTheoremFunctions :: String -> CurryProg -> IO [CFuncDecl]

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.