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 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

Summary of exported operations:

determinismTheoremFor
                  ::  String -> String

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

getModuleProofFiles
                  ::  String -> String -> IO [String]

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

existsProofFor
                  ::  (String,String) -> [String] -> Bool

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

isProofFileNameFor
                  ::  (String,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

getModuleProofFiles :: String -> String -> IO [String]

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

existsProofFor :: (String,String) -> [String] -> Bool

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

isProofFileNameFor :: (String,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.