Commit d414a3b9 authored by Michael Hanus 's avatar Michael Hanus

Updates w.r.t. currycheck updates

parent fae5a11c
*~
cdoc
docs/*.aux
docs/*.pdf
docs/*.toc
docs/*.log
docs/*.out
docs/*.synctex.gz
.curry
.cpm
......@@ -3,7 +3,7 @@
--- and deterministic functions.
---
--- @author Michael Hanus
--- @version May 2016
--- @version October 2018
-----------------------------------------------------------------------------
import AbstractCurry.Types
......@@ -81,11 +81,12 @@ transDefaultRules verb moreopts _ prog = do
-- of proof files:
filterProofObligation :: Int -> [String] -> [QName] -> IO [QName]
filterProofObligation _ _ [] = return []
filterProofObligation verb prooffiles (qf@(_,fn) : qfs) = do
let hasdetproof = existsProofFor (determinismTheoremFor fn) prooffiles
filterProofObligation verb prooffiles (qf@(mn,fn) : qfs) = do
let dettheoname = (mn, determinismTheoremFor fn)
hasdetproof = existsProofFor dettheoname prooffiles
when (hasdetproof && verb>0) $ putStrLn $
"Proofs for determinism property of " ++ showQName qf ++ " found:\n" ++
unlines (filter (isProofFileNameFor (determinismTheoremFor fn)) prooffiles)
unlines (filter (isProofFileNameFor dettheoname) prooffiles)
filterqfs <- filterProofObligation verb prooffiles qfs
return (if hasdetproof then filterqfs else qf : filterqfs)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment