Commit f527776b by Michael Hanus

### Typeclass version packaged

parent 57be800b
 ... ... @@ -27,7 +27,7 @@ plusComm :: Int -> Int -> Prop plusComm x y = x + y -=- y + x -- We can even write a polymorphic test: rev_rev_is_id :: [a] -> Prop rev_rev_is_id :: (Eq a, Show a) => [a] -> Prop rev_rev_is_id xs = reverse (reverse xs) -=- xs -- A polymorphic test will be automatically transformed into the same -- test specialized to values of type Ordering. ... ...
 ... ... @@ -6,7 +6,7 @@ rev [] = [] rev (x:xs) = rev xs ++ [x] -- Unit tests: revNull = rev [] -=- [] revNull = rev [] -=- ([] :: [Int]) rev123 = rev [1,2,3] -=- [3,2,1] -- Property: reversing two times is the identity: ... ... @@ -69,6 +69,7 @@ neg_or b1 b2 = not (b1 || b2) -=- not b1 && not b2 -- Natural numbers defined by s-terms (Z=zero, S=successor): data Nat = Z | S Nat deriving (Eq,Show) -- addition on natural numbers: add :: Nat -> Nat -> Nat ... ... @@ -84,6 +85,7 @@ addIsAssociative x y z = add (add x y) z -=- add x (add y z) -- A general tree type: data Tree a = Leaf a | Node [Tree a] deriving (Eq,Show) -- The leaves of a tree: leaves (Leaf x) = [x] ... ... @@ -107,6 +109,7 @@ sumUpIsCorrect n = n>=0 ==> sumUp n -=- n * (n+1) `div` 2 -- To test sumUpIsCorrect explicitly on non-ngeative integers, -- we define a new data type to wrap integers: data NonNeg = NonNeg { nonNeg :: Int } deriving (Eq,Show) -- We define our own generator for producing only non-negative integers: genNonNeg = genCons1 NonNeg genNN ... ...
 ... ... @@ -8,33 +8,33 @@ import qualified List import Test.Prop nub :: [a] -> [a] nub :: Eq a => [a] -> [a] nub = List.nub nub'spec :: [a] ->DET [a] nub'spec :: Eq a => [a] ->DET [a] nub'spec (xs++[e]++ys++[e]++zs) = nub'spec (xs++[e]++ys++zs) nub'spec'default xs = xs isPrefixOf :: [a] -> [a] -> Bool isPrefixOf :: Eq a => [a] -> [a] -> Bool isPrefixOf = List.isPrefixOf isPrefixOf'spec :: [a] -> [a] ->DET Bool isPrefixOf'spec :: Eq a => [a] -> [a] ->DET Bool isPrefixOf'spec xs (xs ++ _) = True isPrefixOf'spec'default _ _ = False isSuffixOf :: [a] -> [a] -> Bool isSuffixOf :: Eq a => [a] -> [a] -> Bool isSuffixOf = List.isSuffixOf isSuffixOf'spec :: [a] -> [a] ->DET Bool isSuffixOf'spec :: Eq a => [a] -> [a] ->DET Bool isSuffixOf'spec xs (_ ++ xs) = True isSuffixOf'spec'default _ _ = False isInfixOf :: [a] -> [a] -> Bool isInfixOf :: Eq a => [a] -> [a] -> Bool isInfixOf = List.isInfixOf isInfixOf'spec :: [a] -> [a] ->DET Bool isInfixOf'spec :: Eq a => [a] -> [a] ->DET Bool isInfixOf'spec xs (_ ++ xs ++ _) = True isInfixOf'spec'default _ _ = False
 ... ... @@ -4,6 +4,7 @@ import Test.Prop -- Natural numbers defined by s-terms (Z=zero, S=successor): data Nat = Z | S Nat deriving (Eq,Show) -- addition on natural numbers: add :: Nat -> Nat -> Nat ... ...
 ... ... @@ -4,6 +4,7 @@ import Test.Prop -- A general tree type: data Tree a = Leaf a | Node [Tree a] deriving (Eq,Show) leaves (Leaf x) = [x] leaves (Node ts) = concatMap leaves ts ... ...
 { "name": "currycheck", "version": "1.0.1", "version": "2.0.0", "author": "Michael Hanus ", "synopsis": "A tool to support automatic testing of Curry programs", "category": [ "Testing" ], "dependencies": { "rewriting" : ">= 0.0.1" "rewriting" : ">= 2.0.0" }, "compilerCompatibility": { "pakcs": ">= 1.14.0, < 2.0.0", "kics2": ">= 0.5.0, < 2.0.0" "pakcs": ">= 2.0.0", "kics2": ">= 2.0.0" }, "configModule": "CurryCheckConfig", "executable": { ... ... @@ -18,6 +18,7 @@ }, "testsuite": [ { "src-dir": "examples", "options": "-m70", "modules": [ "DefaultRulesTest", "DetOperations", "ExampleTests", "ExamplesFromManual", "FloatTest", "ListSpecifications", "Nats", "SEBF", "Sum", "SortSpec", "Tree" ] ... ...
 ... ... @@ -7,7 +7,7 @@ --- See example program `Examples/UsageErrors.curry` for some examples. --- --- @author Michael Hanus --- @version May 2016 --- @version October 2016 --------------------------------------------------------------------------- module CheckDetUsage(containsDetOperations, checkDetUse) where ... ... @@ -18,25 +18,26 @@ import AbstractCurry.Select --------------------------------------------------------------------- --- Does a Curr program contains operations with DET annotations? containsDetOperations :: CurryProg -> Bool containsDetOperations (CurryProg _ _ _ fdecls _) = any (detInTopLevelType . funcType) fdecls containsDetOperations (CurryProg _ _ _ _ _ _ fdecls _) = any (detInTopLevelType . typeOfQualType . funcType) fdecls where detInTopLevelType (CTVar _) = False detInTopLevelType (CTCons tc _) = tc == pre "DET" detInTopLevelType (CTVar _) = False detInTopLevelType (CTCons _) = False detInTopLevelType (CFuncType _ rt) = detInTopLevelType rt detInTopLevelType (CTApply tc _) = tc == CTCons (pre "DET") --------------------------------------------------------------------- --- Returns messages about unintended uses of type synonym `DET` --- in a Curry program. checkDetUse :: CurryProg -> [(QName,String)] checkDetUse (CurryProg _ _ _ fdecls _) = checkDetUse (CurryProg _ _ _ _ _ _ fdecls _) = concatMap (map showDetError . checkDetUseInFDecl) fdecls where showDetError qf = (qf, "wrong use of DET type synonym!") checkDetUseInFDecl :: CFuncDecl -> [QName] checkDetUseInFDecl (CFunc qn _ _ t rs) = if checkDetInTopLevelType t || any detInRule rs if checkDetInTopLevelType (typeOfQualType t) || any detInRule rs then [qn] else [] checkDetUseInFDecl (CmtFunc _ qn ar vis t rs) = ... ... @@ -44,15 +45,16 @@ checkDetUseInFDecl (CmtFunc _ qn ar vis t rs) = checkDetInTopLevelType :: CTypeExpr -> Bool checkDetInTopLevelType (CTVar _) = False checkDetInTopLevelType (CTCons _ ts) = any detInTypeExpr ts checkDetInTopLevelType (CTCons _) = False checkDetInTopLevelType (CFuncType at rt) = detInTypeExpr at || checkDetInTopLevelType rt checkDetInTopLevelType (CTApply _ ta) = detInTypeExpr ta detInTypeExpr :: CTypeExpr -> Bool detInTypeExpr (CTVar _) = False detInTypeExpr (CTCons tc ts) = tc == pre "DET" || any detInTypeExpr ts detInTypeExpr (CTCons tc) = tc == pre "DET" detInTypeExpr (CFuncType at rt) = detInTypeExpr at || detInTypeExpr rt detInTypeExpr (CTApply tc ta) = detInTypeExpr tc || detInTypeExpr ta detInRule :: CRule -> Bool detInRule (CRule _ rhs) = detInRhs rhs ... ... @@ -64,9 +66,9 @@ detInRhs (CGuardedRhs gs ldcls) = any detInGuard gs || any detInLocalDecl ldcls detInLocalDecl :: CLocalDecl -> Bool detInLocalDecl (CLocalFunc (CFunc _ _ _ t rs)) = detInTypeExpr t || any detInRule rs detInTypeExpr (typeOfQualType t) || any detInRule rs detInLocalDecl (CLocalFunc (CmtFunc _ _ _ _ t rs)) = detInTypeExpr t || any detInRule rs detInTypeExpr (typeOfQualType t) || any detInRule rs detInLocalDecl (CLocalPat _ rhs) = detInRhs rhs detInLocalDecl (CLocalVars _) = False ... ... @@ -80,7 +82,7 @@ detInExp (CLetDecl ldecls e) = any detInLocalDecl ldecls || detInExp e detInExp (CDoExpr stmts) = any detInStatement stmts detInExp (CListComp e stmts) = detInExp e || any detInStatement stmts detInExp (CCase _ e branches) = detInExp e || any (detInRhs . snd) branches detInExp (CTyped e t) = detInExp e || detInTypeExpr t detInExp (CTyped e t) = detInExp e || detInTypeExpr (typeOfQualType t) detInExp (CRecConstr _ fields) = any (detInExp . snd) fields detInExp (CRecUpdate e fields) = detInExp e || any (detInExp . snd) fields ... ...
 ... ... @@ -5,7 +5,7 @@ --- and pre/postconditions. --- --- @author Michael Hanus --- @version May 2016 --- @version October 2016 ------------------------------------------------------------------------ module ContractUsage ... ... @@ -56,7 +56,7 @@ checkPrePostResultTypes prog = in preerrs ++ posterrs hasBoolResultType :: CFuncDecl -> Bool hasBoolResultType fd = resultType (funcType fd) == boolType hasBoolResultType fd = resultType (typeOfQualType (funcType fd)) == boolType -- Get function names from a Curry module with a name satisfying the predicate: funDeclsWithNameArity :: (String -> Bool) -> CurryProg -> [(String,Int)] ... ... @@ -66,7 +66,8 @@ funDeclsWithNameArity pred prog = -- Computes the unqualified name and the arity from the type of the function. nameArityOfFunDecl :: CFuncDecl -> (String,Int) nameArityOfFunDecl fd = (snd (funcName fd), length (argTypes (funcType fd))) nameArityOfFunDecl fd = (snd (funcName fd), length (argTypes (typeOfQualType (funcType fd)))) -- Is this the name of a specification? ... ...