semantic labelling: CPF output (to check JFP_Ex31)

[jwaldmann]

We should really output CPF documents, so the termination "proofs" like https://github.com/jwaldmann/co4/blob/5ba7181ddad0a5b880e529f3ab30e61d1d216fe6/JFP_Ex31.proof can be verified by CeTA.

This needs some (trivial, I hope) extensions in tpdb, see jwaldmann/haskell-tpdb#4 , and a rewrite of the termcomp2014 main program.

I don't see whether tpdb-8.0/TRS/AProVE_04/JFP_Ex31.xml is supposed to be terminating. The problem is from Ex 31 (see also Ex 15) in http://verify.rwth-aachen.de/giesl/papers/JFP-distribute.ps

[jwaldmann]

the current Main module should export a function with roughly this type:

step :: DP -> IO (Maybe (DP, CPF -> CPF))

with specification

• if step dp returns Just (dp',f), and p is any proof for termination of dp', then f p is a proof of termination of dp
• for each call of step dp , there is at least one marked rule in dp

As a first approximation (as long as jwaldmann/haskell-tpdb#4 is open), use String or Doc instead of CPF (and CPF is actually TPDB.CPF.Proof.Type.DpProof)

[jwaldmann]

Note: I am working on CPF output for everything outside semantic labelling. See recent commits in haskell-tpdb and co4.

[jwaldmann]

I think this works now. It's not in the nicest form, because we don't see details of the proof steps in the semantic labelling, because the output uses TPDB.CPF.* functions directly, while it should should use tc/MB/Proof. I'm closing this here, and refer to Issue #94