Commit 5f6ebaa9 authored by Michael Hanus's avatar Michael Hanus
Browse files

Theorem usage modified. Theorems are just properties and do not require prefix theorem'

parent 2e3a1f8f
......@@ -17,10 +17,12 @@ module ContractUsage
import AbstractCurry.Types
import AbstractCurry.Select
import AbstractCurry.Build (boolType)
import List
checkContractUse :: CurryProg -> IO [(QName,String)]
checkContractUse prog = do
--- Checks the intended usage of contracts.
checkContractUse :: CurryProg -> [(QName,String)]
checkContractUse prog =
let mn = progName prog
allops = map nameArityOfFunDecl (functions prog)
specops = map (\ (n,a) -> (fromSpecName n, a))
......@@ -39,7 +41,22 @@ checkContractUse prog = do
onlypostcond
specerrs = map (\ (n,_) -> ((mn, n++"'spec"), errmsg ++ "specification"))
onlyspec
return (preerrs ++ posterrs ++ specerrs)
in preerrs ++ posterrs ++ specerrs ++ checkPrePostResultTypes prog
checkPrePostResultTypes :: CurryProg -> [(QName,String)]
checkPrePostResultTypes prog =
let allops = functions prog
preops = filter (isPreCondName . snd . funcName) allops
postops = filter (isPostCondName . snd . funcName) allops
errmsg c = c ++ " has illegal type"
preerrs = map (\fd -> (funcName fd, errmsg "Precondition"))
(filter (not . hasBoolResultType) preops)
posterrs = map (\fd -> (funcName fd, errmsg "Postcondition"))
(filter (not . hasBoolResultType) postops)
in preerrs ++ posterrs
hasBoolResultType :: CFuncDecl -> Bool
hasBoolResultType fd = resultType (funcType fd) == boolType
-- Get function names from a Curry module with a name satisfying the predicate:
funDeclsWithNameArity :: (String -> Bool) -> CurryProg -> [(String,Int)]
......
......@@ -39,8 +39,9 @@ import System (system, exitWith, getArgs, getPID)
import CheckDetUsage (checkDetUse, containsDetOperations)
import ContractUsage
import DefaultRuleUsage (checkDefaultRules, containsDefaultRules)
import TheoremUsage
import PropertyUsage
import SimplifyPostConds (simplifyPostConditionsWithTheorems)
import TheoremUsage
import UsageCheck (checkBlacklistUse, checkSetUse)
--- Maximal arity of check functions and tuples currently supported:
......@@ -381,23 +382,6 @@ makeAllPublic (CurryProg modname imports typedecls functions opdecls) =
makePublic (CmtFunc cmt name arity _ typeExpr rules) =
CmtFunc cmt name arity Public typeExpr rules
-- Check if a function definition is a property that should be tested,
-- i.e., if the result type is Prop (= [Test]) or PropIO.
isTest :: CFuncDecl -> Bool
isTest = isTestType . funcType
where
isTestType :: CTypeExpr -> Bool
isTestType ct = isPropIOType ct || resultType ct == propType
-- The type of EasyCheck properties.
propType :: CTypeExpr
propType = baseType (easyCheckModule,"Prop")
isPropIOType :: CTypeExpr -> Bool
isPropIOType texp = case texp of
CTCons tcons [] -> tcons == (easyCheckModule,"PropIO")
_ -> False
-- classify the tests as either PropTest or IOTest
classifyTests :: [CFuncDecl] -> [Test]
classifyTests = map makeProperty
......@@ -412,7 +396,7 @@ classifyTests = map makeProperty
-- all ignored tests, and the public version of the original module.
transformTests :: Options -> CurryProg -> IO ([CFuncDecl],[CFuncDecl],CurryProg)
transformTests opts prog@(CurryProg mname imps typeDecls functions opDecls) = do
theofuncs <- getTheoremFunctions prog
theofuncs <- getTheoremFunctions prog
simpfuncs <- simplifyPostConditionsWithTheorems (optVerb opts) theofuncs funcs
let preCondOps = preCondOperations simpfuncs
postCondOps = map ((\ (mn,fn) -> (mn, fromPostCondName fn)) . funcName)
......@@ -428,7 +412,9 @@ transformTests opts prog@(CurryProg mname imps typeDecls functions opDecls) = do
if not (optProp opts)
then []
else concatMap (poly2default (optDefType opts)) $
filter (\fd -> funcName fd `notElem` map funcName theofuncs) usertests ++
-- ignore already proved properties:
filter (\fd -> funcName fd `notElem` map funcName theofuncs)
usertests ++
(if optSpec opts then postCondTests ++ specOpTests else [])
return (map snd realtests,
map snd ignoredtests,
......@@ -438,7 +424,7 @@ transformTests opts prog@(CurryProg mname imps typeDecls functions opDecls) = do
(simpfuncs ++ map snd (realtests ++ ignoredtests))
opDecls)
where
(usertests, funcs) = partition isTest functions
(usertests, funcs) = partition isProperty functions
-- Extracts all determinism tests from a given Curry module and
......@@ -488,10 +474,9 @@ funDeclsWith pred = filter (pred . snd . funcName)
-- Transforms a function type into a property type, i.e.,
-- t1 -> ... -> tn -> t is transformed into t1 -> ... -> tn -> Prop
propResultType :: CTypeExpr -> CTypeExpr
propResultType (CTVar _) = propType
propResultType (CTCons _ _) = propType
propResultType (CFuncType from to) = CFuncType from (propResultType to)
propResultType te = case te of
CFuncType from to -> CFuncType from (propResultType to)
_ -> baseType (easyCheckModule,"Prop")
-- Transforms a function declaration into a post condition test if
-- there is a post condition for this function (i.e., a relation named
......@@ -648,10 +633,10 @@ staticProgAnalysis opts modname progtxt prog = do
else return []
let defruleerrs = if optSource opts then checkDefaultRules prog else []
untypedprog <- readUntypedCurry modname
let detuseerrs = if optSource opts then checkDetUse untypedprog else []
contracterrs <- checkContractUse prog
let staticerrs = concat [seterrs,useerrs,defruleerrs,detuseerrs,contracterrs]
let missingCPP =
let detuseerrs = if optSource opts then checkDetUse untypedprog else []
contracterrs = checkContractUse prog
staticerrs = concat [seterrs,useerrs,defruleerrs,detuseerrs,contracterrs]
missingCPP =
if (containsDefaultRules prog || containsDetOperations untypedprog)
&& not (containsPPOptionLine progtxt)
then ["'" ++ modname ++
......@@ -911,18 +896,6 @@ modNameToId = intercalate "_" . split (=='.')
arityOfType :: CTypeExpr -> Int
arityOfType = length . argTypes
--- Name of the Test.Prop module (the clone of the EasyCheck module).
propModule :: String
propModule = "Test.Prop"
--- Name of the EasyCheck module.
easyCheckModule :: String
easyCheckModule = "Test.EasyCheck"
--- Name of the EasyCheckExec module.
easyCheckExecModule :: String
easyCheckExecModule = "Test.EasyCheckExec"
--- Name of the SearchTree module.
searchTreeModule :: String
searchTreeModule = "SearchTree"
......
-- Examples for problems to be detected by CurryCheck:
---------------------------------------------------------------------------
-- Here are some examples for problems to be detected by CurryCheck
---------------------------------------------------------------------------
import SetFunctions
---------------------------------------------------------------------------
-- Detection of unintended uses of set functions and functional pattern unif.
test1 x | 3 =:<= x = True -- not allowed!
test2 = set2 (++) [] [42] -- ok
......@@ -48,4 +53,12 @@ some'spec x = x
k'spec x = x
k x _ = x
inc :: Int -> Int
inc n = n + 1
-- Illegal contract types:
inc'pre x = x
inc'post x y = x+y
---------------------------------------------------------------------------
------------------------------------------------------------------------
--- This module contains some operations to handle properties in
--- a Curry program.
---
--- @author Michael Hanus
--- @version Augsut 2016
------------------------------------------------------------------------
module PropertyUsage
( isProperty, isPropType, isPropIOType
, propModule, easyCheckModule, easyCheckExecModule
) where
import AbstractCurry.Types
import AbstractCurry.Select (funcType, resultType)
------------------------------------------------------------------------
-- Check whether a function definition is a property,
-- i.e., if the result type is `Prop` or `PropIO`.
isProperty :: CFuncDecl -> Bool
isProperty = isPropertyType . funcType
where
isPropertyType ct = isPropIOType ct || isPropType (resultType ct)
-- Is the type expression the type Test.EasyCheck.Prop?
isPropType :: CTypeExpr -> Bool
isPropType texp = case texp of
CTCons (mn,tc) [] -> tc == "Prop" && isCheckModule mn
_ -> False
-- Is the type expression the type Test.EasyCheck.PropIO?
isPropIOType :: CTypeExpr -> Bool
isPropIOType texp = case texp of
CTCons (mn,tc) [] -> tc == "PropIO" && isCheckModule mn
_ -> False
-- Is the module name Test.Prop or Test.EasyCheck?
isCheckModule :: String -> Bool
isCheckModule mn = mn == propModule || mn == easyCheckModule
--- Name of the Test.Prop module (the clone of the EasyCheck module).
propModule :: String
propModule = "Test.Prop"
--- Name of the EasyCheck module.
easyCheckModule :: String
easyCheckModule = "Test.EasyCheck"
--- Name of the EasyCheckExec module.
easyCheckExecModule :: String
easyCheckExecModule = "Test.EasyCheckExec"
......@@ -82,6 +82,7 @@ simplifyPostCondition verb simprules fdecl@(CmtFunc cmt qn ar vis texp rules) =
else [CmtFunc cmt qn ar vis texp redrules]
else return [fdecl]
-- Translate property theorem into simplification rules.
theoremToSimpRules :: Rule QName -> [Rule QName]
theoremToSimpRules (_, TermVar _) =
error $ "theoremToSimpRules: variable in rhs"
......
------------------------------------------------------------------------
--- This module contains some operations to access and check theorems
--- attached to Curry program.
--- 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 by the prefix
--- `theorem`, e.g.:
--- * A theorem is represented in a source file as a EasyCheck property, e.g.:
---
--- theorem'sortlength xs = length xs -=- length (sort xs)
--- 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-sortlength.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-length.smt`.
--- `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 May 2016
--- @version August 2016
------------------------------------------------------------------------
module TheoremUsage
( isTheoremFunc, isTheoremName, fromTheoremName, determinismTheoremFor
( determinismTheoremFor
, getProofFiles, existsProofFor, isProofFileName, isProofFileNameFor
, getTheoremFunctions
) where
......@@ -38,21 +37,9 @@ import Distribution (modNameToPath)
import FilePath (dropExtension, takeDirectory)
import List
------------------------------------------------------------------------
-- Operations for proof names:
--- Is this function a theorem?
isTheoremFunc :: CFuncDecl -> Bool
isTheoremFunc = isTheoremName . snd . funcName
--- Is this the name of a theorem?
isTheoremName :: String -> Bool
isTheoremName f = "theorem'" `isPrefixOf` f
--- Drop the default rule prefix "theorem'" from the name:
fromTheoremName :: String -> String
fromTheoremName f = drop (if take 8 f == "theorem'" then 8 else 0) f
import PropertyUsage
------------------------------------------------------------------------
--- The name of a proof of a determinism annotation for the operation
--- given as the argument.
determinismTheoremFor :: String -> String
......@@ -71,36 +58,34 @@ getProofFiles dir = do
--- Does the list of file names (second argument) contain a proof of the
--- theorem given as the first argument?
existsProofFor :: String -> [String] -> Bool
existsProofFor thmname filenames =
any (isProofFileNameFor thmname) filenames
existsProofFor propname filenames =
any (isProofFileNameFor propname) filenames
--- Is this a file name with a proof, i.e., start it with `proof`?
isProofFileName :: String -> Bool
isProofFileName fn = "proof" `isPrefixOf` (map toLower fn)
--- Is this the file name of a proof of theorem `thm`?
--- Is this the file name of a proof of property `prop`?
isProofFileNameFor :: String -> String -> Bool
isProofFileNameFor tn thm =
let lthm = map toLower thm
in if "proof" `isPrefixOf` lthm
then deleteNonAlphanNum (drop 5 lthm) == deleteNonAlphanNum tn
isProofFileNameFor prop fname =
let lfname = map toLower (dropExtension fname)
lprop = map toLower prop
in if "proof" `isPrefixOf` lfname
then deleteNonAlphanNum (drop 5 lfname) == deleteNonAlphanNum lprop
else False
--- Delete non alphanumeric characters
--- Delete non alphanumeric characters.
deleteNonAlphanNum :: String -> String
deleteNonAlphanNum s = filter isAlphaNum (dropExtension s)
deleteNonAlphanNum = filter isAlphaNum
------------------------------------------------------------------------
-- Get all theorems which are contained in a given program
-- and for which proof files exist.
--- Get all theorems which are contained in a given program.
--- A theorem is a property for which a proof file exists.
getTheoremFunctions :: CurryProg -> IO [CFuncDecl]
getTheoremFunctions (CurryProg mname _ _ functions _) = do
let dcltheofuncs = funDeclsWith isTheoremName functions -- declared theorems
let propfuncs = filter isProperty functions -- all properties
prooffiles <- getProofFiles (takeDirectory (modNameToPath mname))
return $ filter (\fd -> existsProofFor (fromTheoremName (snd (funcName fd)))
prooffiles)
dcltheofuncs
where
funDeclsWith pred = filter (pred . snd . funcName)
return $ filter (\fd -> existsProofFor (snd (funcName fd)) prooffiles)
propfuncs
------------------------------------------------------------------------
......@@ -158,7 +158,7 @@ transformCProg :: Int -> Options -> String -> CurryProg -> String
transformCProg verb opts srctxt orgprog outmodname = do
let -- to avoid constructor CFunc and references to Test.Prop
prog = addCmtFuncInProg (renameProp2EasyCheck orgprog)
usageerrors <- checkContractUse prog
usageerrors = checkContractUse prog
unless (null usageerrors) $ do
putStr (unlines $ "ERROR: ILLEGAL USE OF CONTRACTS:" :
map (\ ((mn,fn),err) -> fn ++ " (module " ++ mn ++ "): " ++ err)
......
......@@ -9,5 +9,5 @@ even Z = True
even (S Z) = False
even (S (S n)) = even n
theorem'evendoublecoin x = always (even (double (coin x)))
evendoublecoin x = always (even (double (coin x)))
......@@ -15,6 +15,6 @@ odd :: Nat -> Bool
odd Z = False
odd (S n) = even n
theorem'odddoublecoin x = odd (double (coin x)) <~> False
odddoublecoin x = odd (double (coin x)) <~> False
......@@ -37,4 +37,4 @@ solve2 (S x) (S y) = L : solve2 x (S y) ? R : solve2 (S x) y
-- and prove:
theorem'gamelength x y = len (solve2 x y) -=- add x y
gamelength x y = len (solve2 x y) -=- add x y
......@@ -5,4 +5,4 @@ data List a = Empty | Cons a (List a)
append Empty ys = ys
append (Cons x xs) ys = Cons x (append xs ys)
theorem'assoc xs ys zs = append (append xs ys) zs -=- append xs (append ys zs)
appendIsAssoc xs ys zs = append (append xs ys) zs -=- append xs (append ys zs)
......@@ -8,4 +8,4 @@ insert x (y:ys) = (x : y : ys) ? (y : insert x ys)
perm [] = []
perm (x:xs) = insert x (perm xs)
theorem'permlength xs = length xs <~> length (perm xs)
permPreservesLength xs = length xs <~> length (perm xs)
......@@ -25,7 +25,7 @@ rm -f TO-PROVE-* $LOGFILE
# execute all tests:
# Check whether the Agda compiler compiles the generated programs.
AGDA=`which agda`
AGDAIMPORTS="-i . -i /home/mh/home/languages_systems/agda/ial -i /usr/share/agda-stdlib"
AGDAIMPORTS="-i . -i /net/medoc/home/mh/home/languages_systems/agda/ial_org -i /usr/share/agda-stdlib"
AGDAOPTS="--allow-unsolved-metas"
if [ -z "$AGDA" ] ; then
......
......@@ -4,9 +4,10 @@ TOOL=$(BINDIR)/curry2verify
# for determinism analysis and for module TheoremUsage:
TOOLDIR=..
CVPATH = $(TOOLDIR)/analysis:$(TOOLDIR)/CASS:$(TOOLDIR)/currycheck
CCPATH = $(TOOLDIR)/currycheck
CVPATH = $(TOOLDIR)/analysis:$(TOOLDIR)/CASS:$(CCPATH)
DEPS = *.curry
DEPS = *.curry $(CCPATH)/PropertyUsage.curry
.PHONY: all compile install clean uninstall
......
......@@ -19,8 +19,9 @@ import Rewriting.Files
import Rewriting.Term
import Rewriting.Rules
import Rewriting.CriticalPairs
import TheoremUsage
import Time
import PropertyUsage
import VerifyOptions
-- to access the determinism analysis:
......@@ -33,14 +34,13 @@ import TotallyDefined (Completeness(..))
--- Generate an Agda program file for a given theorem name and the
--- list of all functions involved in this theorem.
theoremToAgda :: Options -> QName -> [CFuncDecl] -> [CTypeDecl] -> IO ()
theoremToAgda opts qtheoname allfuncs alltypes = do
theoremToAgda opts qtheo@(_,theoname) allfuncs alltypes = do
let (rename, orgtypedrules) = funcDeclsToTypedRules allfuncs
transform = if optScheme opts == "nondet" then transformRuleWithNondet
else transformRuleWithChoices
typedrules = concatMap (transform opts) orgtypedrules
(theorules,funcrules) = partition (\ (fn,_,_,_) -> isTheoremName (snd fn))
(theorules,funcrules) = partition (\ (fn,_,_,_) -> fn == qtheo)
typedrules
theoname = fromTheoremName (snd qtheoname)
mname = "TO-PROVE-" ++ theoname
hrule = take 75 (repeat '-')
agdaprog = unlines $
......@@ -339,8 +339,6 @@ transformRuleWithNondet opts (fn,cmt,texp,trs)
[TermCons (mn,"failing") args, agdaTrue]
_ -> t
isOp f = lookupProgInfo (stripRuleName f) detinfo /= Nothing
isNondetOp f = lookupProgInfo (stripRuleName f) detinfo == Just NDet
addNondetInTerm v@(TermVar _) = agdaVal v
......@@ -540,9 +538,12 @@ ruleFunc rl@(TermVar _,_) = error $ "Rule with variable lhs: " ++
showRule showQName rl
ruleFunc (TermCons f _,_) = f
-- Is this rule a theorem of the source program?
-- Is this rule of a property of the source program?
isTheoremRule :: Rule QName -> Bool
isTheoremRule rule = isTheoremName (snd (ruleFunc rule))
isTheoremRule (_,rhs) =
case rhs of
TermVar _ -> False
TermCons f _ -> snd f `elem` ["-=-","<~>","always","eventually","failing"]
fst4 :: (a,b,c,d) -> a
fst4 (x,_,_,_) = x
......
......@@ -17,7 +17,8 @@ import List
import Maybe (fromJust)
import SCC (scc)
import System (exitWith, getArgs)
import TheoremUsage
import PropertyUsage
import ToAgda
import VerifyOptions
......@@ -32,7 +33,7 @@ cvBanner :: String
cvBanner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText =
"curry2verify: Curry programs -> Verifiers (version of 14/06/2016)"
"curry2verify: Curry programs -> Verifiers (version of 15/08/2016)"
bannerLine = take (length bannerText) (repeat '-')
-- Help text
......@@ -56,20 +57,20 @@ main = do
generateTheorems :: Options -> String -> IO ()
generateTheorems opts mname = do
prog <- readCurry mname
let theorems = filter (isTheoremName . snd . funcName) (functions prog)
if null theorems
then putStrLn "No theorems found!"
else mapIO_ (generateTheorem opts) (map funcName theorems)
let properties = filter isProperty (functions prog)
if null properties
then putStrLn "No properties found!"
else mapIO_ (generateTheorem opts) (map funcName properties)
-- Generate a file for a given theorem name.
-- Generate a file for a given property name.
generateTheorem :: Options -> QName -> IO ()
generateTheorem opts qtheoname = do
(newopts, allprogs, allfuncs) <- getAllFunctions opts [] [] [qtheoname]
generateTheorem opts qpropname = do
(newopts, allprogs, allfuncs) <- getAllFunctions opts [] [] [qpropname]
let alltypenames = foldr union []
(map (\fd -> tconsOfType (funcType fd)) allfuncs)
alltypes <- getAllTypeDecls opts allprogs alltypenames []
case optTarget opts of
"agda" -> theoremToAgda newopts qtheoname allfuncs alltypes
"agda" -> theoremToAgda newopts qpropname allfuncs alltypes
t -> error $ "Unknown translation target: " ++ t
-------------------------------------------------------------------------
......
Supports Markdown
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