diff --git a/Debug/Hoed/Pure.hs b/Debug/Hoed/Pure.hs --- a/Debug/Hoed/Pure.hs +++ b/Debug/Hoed/Pure.hs @@ -110,8 +110,7 @@ , Proposition(..) , PropositionType(..) , Module(..) - , propVarError - , propVarFresh + , UnevalHandler(..) -- * Experimental annotations , traceOnly @@ -301,11 +300,11 @@ showCompStmt = show . vertexStmt -- | As logO, but with property-based judging. -logOwp :: PropVarGen String -> FilePath -> [Propositions] -> IO a -> IO () -logOwp unevalGen filePath properties program = do +logOwp :: UnevalHandler -> FilePath -> [Propositions] -> IO a -> IO () +logOwp handler filePath properties program = do (trace,traceInfo,compTree,frt) <- runO' program hPutStrLn stderr "\n=== Evaluating assigned properties ===\n" - compTree' <- judge unevalGen trace properties compTree + compTree' <- judge handler trace properties compTree writeFile filePath (showGraph compTree') return () diff --git a/Debug/Hoed/Pure/DemoGUI.hs b/Debug/Hoed/Pure/DemoGUI.hs --- a/Debug/Hoed/Pure/DemoGUI.hs +++ b/Debug/Hoed/Pure/DemoGUI.hs @@ -13,7 +13,7 @@ import Debug.Hoed.Pure.EventForest import Debug.Hoed.Pure.Observe import qualified Debug.Hoed.Pure.Prop as Prop -import Debug.Hoed.Pure.Prop(Propositions,propVarError,propVarFresh,lookupPropositions,judgeWithPropositions,PropVarGen) +import Debug.Hoed.Pure.Prop(Propositions,lookupPropositions,judgeWithPropositions,UnevalHandler(..)) import Paths_Hoed (version) import Data.Version (showVersion) import Data.Graph.Libgraph @@ -179,7 +179,7 @@ guiAssisted :: Trace -> [Propositions] -> IORef CompTree -> IORef Int -> IORef String -> IORef Int -> UI UI.Element guiAssisted trace ps compTreeRef currentVertexRef regexRef imgCountRef = do - forallRef <- UI.liftIO $ newIORef (False :: Bool) + handlerRef <- UI.liftIO $ newIORef Abort -- Get a list of vertices from the computation tree tree <- UI.liftIO $ readIORef compTreeRef @@ -199,29 +199,48 @@ j right Right j wrong Wrong testB <- UI.button # set UI.text "test" # set UI.height 30 # set UI.style [("margin-right","1em")] - testAllB <- UI.button # set UI.text "test all" # set UI.height 30 - on UI.click testAllB $ \_ -> testAll compTreeRef trace ps status currentVertexRef compStmt forallRef - on UI.click testB $ \_ -> testCurrent compTreeRef trace ps status currentVertexRef compStmt forallRef + testAllB <- UI.button # set UI.text "test all" # set UI.height 30 # set UI.style [("margin-right","1em")] + resetB <- UI.button # set UI.text "clear all judgements" # set UI.height 30 + on UI.click testAllB $ \_ -> testAll compTreeRef trace ps status currentVertexRef compStmt handlerRef + on UI.click testB $ \_ -> testCurrent compTreeRef trace ps status currentVertexRef compStmt handlerRef + on UI.click resetB $ \_ -> resetTree compTreeRef ps status currentVertexRef compStmt - -- Checkbox to indicate if we want to use quickcheck over unevaluated values - forall <- UI.input # set UI.type_ "checkbox" # set UI.checked False # set UI.style [("transform","scale(1.5)"),("-webkit-transform","scale(1.5)"),("margin-right","0.5em")] - forallDiv <- UI.div #+ [return forall, UI.span # set UI.text "Try to find counterexamples using randomly generated values for unevaluated parts of a computation statement."] - on UI.checkedChange forall $ \b -> UI.liftIO $ writeIORef forallRef b + -- Radio buttons to indicate how unevaluated expressions are handled + r1 <- UI.input # set UI.type_ "radio" # set UI.checked True + r2 <- UI.input # set UI.type_ "radio" # set UI.checked False + r3 <- UI.input # set UI.type_ "radio" # set UI.checked False + d1 <- UI.div #+ [return r1, UI.span # set UI.text "Abort when property depends on an unevaluated expression."] + d2 <- UI.div #+ [return r2, UI.span # set UI.text "Try to find counterexamples using randomly generated values for unevaluated parts of a computation statement."] + d3 <- UI.div #+ [return r3, UI.span # set UI.text "Accept specification without counter examples as enough to judge as right (use with caution)."] + radioButtons <- UI.div #+ map return [d1,d2,d3] + let onCheck r a b h = on UI.checkedChange r $ \_ -> do + UI.liftIO $ writeIORef handlerRef h + return a # set UI.checked False + return b # set UI.checked False + onCheck r1 r2 r3 Abort + onCheck r2 r1 r3 Forall + onCheck r3 r1 r2 TrustForall -- Populate the main screen - top <- UI.center #+ [return status, UI.br, return right, return wrong, return testB, return testAllB, return forallDiv] - UI.div #+ [return top, UI.hr, return compStmt] + top <- UI.center #+ [return status, UI.br, return right, return wrong, return testB, return testAllB, return resetB] + UI.div #+ [return top, return radioButtons, UI.hr, return compStmt] -testAll compTreeRef trace ps status currentVertexRef compStmt forallRef = do +resetTree compTreeRef ps status currentVertexRef compStmt = do + t <- UI.liftIO $ readIORef compTreeRef + UI.liftIO $ writeIORef compTreeRef (mapGraph resetVertex t) + advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef + where resetVertex = flip setJudgement Unassessed + +testAll compTreeRef trace ps status currentVertexRef compStmt handlerRef = do return status # UI.set UI.text "Evaluating propositions ..." #+ [UI.img # set UI.src "static/loading.gif" # set UI.height 30] UI.liftIO $ do - handler <- UI.liftIO $ unevalHandler forallRef + handler <- UI.liftIO $ readIORef handlerRef compTree <- readIORef compTreeRef compTree' <- Prop.judge handler trace ps compTree writeIORef compTreeRef compTree' advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef -testCurrent compTreeRef trace ps status currentVertexRef compStmt forallRef = do +testCurrent compTreeRef trace ps status currentVertexRef compStmt handlerRef = do return status # UI.set UI.text "Evaluating propositions ..." #+ [UI.img # set UI.src "static/loading.gif" # set UI.height 30] mcv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef case mcv of @@ -229,18 +248,13 @@ case lookupPropositions ps cv of Nothing -> updateStatus status compTreeRef (Just p) -> do - handler <- UI.liftIO $ unevalHandler forallRef + handler <- UI.liftIO $ readIORef handlerRef cv' <- UI.liftIO $ judgeWithPropositions handler trace p cv compTree <- UI.liftIO $ readIORef compTreeRef UI.liftIO $ writeIORef compTreeRef (replaceVertex compTree cv') advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef Nothing -> updateStatus status compTreeRef -unevalHandler :: IORef Bool -> IO (PropVarGen String) -unevalHandler forallRef = do - forall <- readIORef forallRef - return $ if forall then propVarFresh else propVarError - -------------------------------------------------------------------------------- -- The Algorithmic Debugging GUI @@ -491,6 +505,7 @@ else " Judged " ++ slen js ++ "/" ++ slen ns UI.element e # set UI.text txt return () + redrawWith :: UI.Element -> IORef Int -> IORef CompTree -> IORef Int -> UI () redrawWith img imgCountRef compTreeRef currentVertexRef = do diff --git a/Debug/Hoed/Pure/Prop.hs b/Debug/Hoed/Pure/Prop.hs --- a/Debug/Hoed/Pure/Prop.hs +++ b/Debug/Hoed/Pure/Prop.hs @@ -2,7 +2,7 @@ -- -- Copyright (c) Maarten Faddegon, 2015 -{-# LANGUAGE DefaultSignatures, TypeOperators, FlexibleContexts, FlexibleInstances, StandaloneDeriving, CPP #-} +{-# LANGUAGE DefaultSignatures, TypeOperators, FlexibleContexts, FlexibleInstances, StandaloneDeriving, CPP, DeriveGeneric #-} module Debug.Hoed.Pure.Prop where -- ( judge @@ -35,7 +35,7 @@ type Proposition = (PropositionType,Module,String,[Int]) -data PropositionType = BoolProposition | QuickCheckProposition deriving Show +data PropositionType = BoolProposition | LegacyQuickCheckProposition | QuickCheckProposition deriving Show data Module = Module {moduleName :: String, searchPath :: String} deriving Show @@ -73,44 +73,76 @@ ------------------------------------------------------------------------------------------------------------------------ -judge :: PropVarGen String -> Trace -> [Propositions] -> CompTree -> IO CompTree -judge unevalGen trc ps compTree = do +judge :: UnevalHandler -> Trace -> [Propositions] -> CompTree -> IO CompTree +judge handler trc ps compTree = do ws <- mapM j vs return $ foldl updateTree compTree ws where vs = vertices compTree j v = case lookupPropositions ps v of Nothing -> return v - (Just p) -> judgeWithPropositions unevalGen trc p v + (Just p) -> judgeWithPropositions handler trc p v updateTree compTree w = mapGraph (\v -> if (vertexUID v) == (vertexUID w) then w else v) compTree -- Use a property to judge a vertex -judgeWithPropositions :: PropVarGen String -> Trace -> Propositions -> Vertex -> IO Vertex -judgeWithPropositions unevalGen _ _ RootVertex = return RootVertex -judgeWithPropositions unevalGen trc p v = do +judgeWithPropositions :: UnevalHandler -> Trace -> Propositions -> Vertex -> IO Vertex +judgeWithPropositions _ _ _ RootVertex = return RootVertex +judgeWithPropositions handler trc p v = do putStrLn $ "\n================\n" - pas <- mapM (evalProposition unevalGen trc v (extraModules p)) (propositions p) - putStrLn $ "judgeWithPropositions: pas=" ++ show pas - let s = propType p == Specify && noAssumption unevalGen + pas' <- mapM (evalProposition unevalGen trc v (extraModules p)) (propositions p) + putStrLn $ "judgeWithPropositions: pas=" ++ show pas' + let pas = if handler == TrustForall then trustWeak pas' else weaken pas' z = zip pas (propositions p) - let a = case (map snd) . (filter (holds . fst)) $ z of + a = case (map snd) . (filter (holds . fst)) $ z of [] -> errorMessages z ps -> "With passing properties: " ++ commas (map propName ps) ++ "\n" ++ (errorMessages z) - j | s && all hasResult pas = if any disproves pas then Wrong else Right - | any hasResult pas = if any disproves pas then Wrong else Assisted a - | otherwise = Assisted a + j' | propType p == Specify && all hasResult pas + = if any disproves pas then Wrong else Right + | any hasResult pas = if any disproves pas then Wrong else Assisted a + | otherwise = Assisted a + j | j' `moreInfo` (vertexJmt v) = j' + | otherwise = vertexJmt v + hPutStrLn stderr $ "Judgement was " ++ (show . vertexJmt) v ++ ", and is now " ++ show j return v{vertexJmt=j} where + unevalGen = unevalHandler handler commas :: [String] -> String commas = concat . (intersperse ", ") -data PropApp = Error String | Holds | Disproves deriving Show + moreInfo _ Unassessed = True + moreInfo Unassessed (Assisted _) = False + moreInfo _ (Assisted _) = True + moreInfo _ Right = False + moreInfo _ Wrong = False +data UnevalHandler = Abort | Forall | TrustForall deriving (Eq, Show) + +unevalHandler :: UnevalHandler -> PropVarGen String +unevalHandler Abort = propVarError +unevalHandler _ = propVarFresh + +data PropApp = Error String | Holds | HoldsWeak | Disproves deriving Show + +trustWeak :: [PropApp] -> [PropApp] +trustWeak = map f + where f HoldsWeak = Holds -- A possible unsafe assumption + f p = p + +weaken :: [PropApp] -> [PropApp] +weaken = map f + where f HoldsWeak = Error "Holds for all randomly generated values we tried." + f p = p + hasResult :: PropApp -> Bool hasResult (Error _) = False +hasResult HoldsWeak = False hasResult _ = True +hasWeakResult :: PropApp -> Bool +hasWeakResult (Error _) = False +hasWeakResult _ = True + holds :: PropApp -> Bool holds Holds = True holds _ = False @@ -144,6 +176,7 @@ return $ case (exit,out) of (ExitFailure _, _) -> Error out (ExitSuccess , "True\n") -> Holds + (ExitSuccess , "+++ OK, passed 100 tests.\n") -> HoldsWeak (ExitSuccess , "False\n") -> Disproves (ExitSuccess , _) -> if "Failed! Falsifiable" `isInfixOf` out then Disproves @@ -221,9 +254,6 @@ propVarReturn :: String -> PropVarGen String propVarReturn s vs = (s,vs) -noAssumption :: PropVarGen a -> Bool -noAssumption unevalGen = (fst . snd . unevalGen) propVars0 == [] - propVarBind :: (String,PropVars) -> Proposition -> String propVarBind (propApp,([],_)) prop = generatePrint prop ++ " $ " ++ propApp propVarBind (propApp,(bvs,_)) prop = "quickCheck (\\" ++ bvs' ++ " -> " ++ propApp ++ ")" @@ -233,7 +263,8 @@ generatePrint :: Proposition -> String generatePrint p = case propositionType p of BoolProposition -> "print" - QuickCheckProposition -> "do g <- newStdGen; print . fromJust . ok . (generate 1 g) . evaluate" + QuickCheckProposition -> "(\\q -> do MkRose res ts <- protectRose .reduceRose . unProp . (\\p->unGen p (mkQCGen 1) 1) . unProperty $ q; print . fromJust . ok $ res)" + LegacyQuickCheckProposition -> "do g <- newStdGen; print . fromJust . ok . (generate 1 g) . evaluate" ------------------------------------------------------------------------------------------------------------------------ @@ -244,7 +275,20 @@ generateHeading prop ms = "-- This file is generated by the Haskell debugger Hoed\n" ++ generateImport (propModule prop) + ++ qcImports ++ foldl (\acc m -> acc ++ generateImport m) "" ms + + where + qcImports = case propositionType prop of + BoolProposition -> [] + LegacyQuickCheckProposition -> qcImports' + QuickCheckProposition -> qcImports' + ++ generateImport (Module "Test.QuickCheck.Property" []) + ++ generateImport (Module "Test.QuickCheck.Gen" []) + ++ generateImport (Module "Test.QuickCheck.Random" []) + qcImports' + = generateImport (Module "System.Random" []) -- newStdGen + ++ generateImport (Module "Data.Maybe" []) -- fromJust generateImport :: Module -> String generateImport m = "import " ++ (moduleName m) ++ "\n" diff --git a/Debug/Hoed/Pure/TestParEq.hs b/Debug/Hoed/Pure/TestParEq.hs new file mode 100644 --- /dev/null +++ b/Debug/Hoed/Pure/TestParEq.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE DefaultSignatures, TypeOperators, FlexibleContexts, FlexibleInstances, StandaloneDeriving, CPP, DeriveGeneric #-} + +import Debug.Hoed.Pure.Prop +import GHC.Generics hiding (moduleName) + +data A = A deriving (Eq, Generic) +instance ParEq A +data B = C B | D | E A A A | F Int Int | G B B deriving (Eq, Generic) +instance ParEq B +data H = I B B B | J Int B deriving (Eq, Generic) +instance ParEq H + +main = print $ all (==True) [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11, + s1,s2,s3,s4,s5,s6] + +t1 = pareq_equiv A A +t2 = pareq_equiv D D +t3 = pareq_equiv (C D) D +t4 = pareq_equiv D (C D) +t5 = pareq_equiv (C (C D)) D +t6 = pareq_equiv (E A A A) D +t7 = pareq_equiv e e where e = E A A A +t8 = pareq_equiv (C (C D)) (C (C (E A A A))) +t9 = pareq_equiv (C (C D)) (C (F 4 2)) +t10 = pareq_equiv c c where c = (C (F 4 2)) +t11 = pareq_equiv c c where c = (C (F 4 2)) + +s1 = ((G (error "oeps") D) === (G D (F 4 2))) == Just False +s2 = ((G D (F 4 2) === (G (error "oeps") D))) == Just False +s3 = ((G (error "oeps") D) === (G D D)) == Nothing +s4 = (I D (E A A A) D) === (I (error "oeps") D D) == Just False +s5 = (I D D (E A A A)) === (I D (error "oeps") D) == Just False +s6 = (I (E A A A) D D) === (I D D (error "oeps")) == Just False + +-- pareq should be equivalent to normal equality when the +-- latter is conclusive +pareq_equiv x y = (x == y) == b + where (Just b) = x === y diff --git a/Hoed.cabal b/Hoed.cabal --- a/Hoed.cabal +++ b/Hoed.cabal @@ -1,5 +1,5 @@ name: Hoed -version: 0.3.3 +version: 0.3.4 synopsis: Lightweight algorithmic debugging. description: Hoed is a tracer and debugger for the programming language Haskell. @@ -8,12 +8,12 @@ . Hoed comes in two flavours: Hoed.Pure and Hoed.Stk. Hoed.Stk uses the cost-centre stacks of the GHC profiling environment to construct the information needed for debugging. Hoed.Pure is recommended over Hoed.Stk: to debug your program with Hoed.Pure you can optimize your program and do not need to enable profiling. . -homepage: http://maartenfaddegon.nl +homepage: https://wiki.haskell.org/Hoed license: BSD3 license-file: LICENSE author: Maarten Faddegon maintainer: hoed@maartenfaddegon.nl -copyright: (c) 2000 Andy Gill, (c) 2010 University of Kansas, (c) 2013-2015 Maarten Faddegon +copyright: (c) 2000 Andy Gill, (c) 2010 University of Kansas, (c) 2013-2016 Maarten Faddegon category: Debug, Trace build-type: Simple cabal-version: >=1.10 @@ -156,6 +156,33 @@ hs-source-dirs: examples default-language: Haskell2010 +Executable hoed-examples-ZLang_Defect-1 + if flag(buildExamples) + build-depends: base >= 4 && < 5, Hoed, threepenny-gui, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions + else + buildable: False + main-is: Main.hs + hs-source-dirs: examples/ZLang/1 + default-language: Haskell2010 + +Executable hoed-examples-ZLang_Defect-2 + if flag(buildExamples) + build-depends: base >= 4 && < 5, Hoed, threepenny-gui, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions + else + buildable: False + main-is: Main.hs + hs-source-dirs: examples/ZLang/2 + default-language: Haskell2010 + +Executable hoed-examples-ZLang_Defect-3 + if flag(buildExamples) + build-depends: base >= 4 && < 5, Hoed, threepenny-gui, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions + else + buildable: False + main-is: Main.hs + hs-source-dirs: examples/ZLang/3 + default-language: Haskell2010 + Executable hoed-examples-Nub-defective-sort__with_properties if flag(buildExamples) build-depends: base >= 4 && < 5, Hoed, threepenny-gui, filepath, QuickCheck @@ -700,6 +727,31 @@ -- default-language: Haskell2010 --------------------------------------------------------------------------- +-- Validate derivation of Observable and ParEq for Generic types +-- +--------------------------------------------------------------------------- + + +Executable hoed-tests-ParEq + if flag(validateGeneric) + build-depends: base >= 4 && <5 + , template-haskell + , array, containers + , process + , threepenny-gui == 0.6.* + , filepath + , libgraph == 1.9 + , RBTree == 0.0.5 + , regex-posix + , mtl + , directory + , FPretty + else + buildable: False + main-is: Debug/Hoed/Pure/TestParEq.hs + default-language: Haskell2010 + + Executable hoed-tests-Generic-r0 if flag(validateGeneric) diff --git a/examples/Nubsort/Main.hs b/examples/Nubsort/Main.hs --- a/examples/Nubsort/Main.hs +++ b/examples/Nubsort/Main.hs @@ -7,12 +7,12 @@ , (BoolProposition,nubsortModule,"prop_nub_unique",[0]) , (BoolProposition,nubsortModule,"prop_nub_complete",[0]) ] PropertiesOf "nub" [] - , Propositions [ (QuickCheckProposition,nubsortModule,"prop_nubord_idempotent",[0]) - , (QuickCheckProposition,nubsortModule,"prop_nubord_unique",[0]) - , (QuickCheckProposition,nubsortModule,"prop_nubord_complete",[0]) - ] PropertiesOf "nubord" [modQuickCheck] - , Propositions [ (QuickCheckProposition,nubsortModule,"prop_insert_ordered",[0]) - , (QuickCheckProposition,nubsortModule,"prop_insert_complete",[0]) + , Propositions [ (QuickCheckProposition,nubsortModule,"prop_nubord'_idempotent",[1,0]) + , (QuickCheckProposition,nubsortModule,"prop_nubord'_unique",[1,0]) + , (QuickCheckProposition,nubsortModule,"prop_nubord'_complete",[1,0]) + ] PropertiesOf "nubord'" [modQuickCheck] + , Propositions [ (QuickCheckProposition,nubsortModule,"prop_insert_ordered",[1,0]) + , (QuickCheckProposition,nubsortModule,"prop_insert_complete",[1,0]) ] PropertiesOf "insert" [modQuickCheck] ] nubsortModule = Module "Nubsort" "../examples/Nubsort/" diff --git a/examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs b/examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs --- a/examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs +++ b/examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs @@ -29,25 +29,25 @@ print . fromJust . ok . (generate 1 g) . evaluate $ prop_shift_win_I 1 'd' myStackSet where propositions = - [Propositions [(QuickCheckProposition,module_Properties,"prop_focus_all_l",[0]) - ,(QuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0]) + [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[0]) + ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0]) ] PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (QuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[1,0]) + , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[1,0]) ] PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (QuickCheckProposition,module_Properties,"prop_view_reversible",[1,0]) - , (QuickCheckProposition,module_Properties,"prop_view_I",[1,0]) - , (QuickCheckProposition,module_Properties,"prop_view_current",[0,1]) - , (QuickCheckProposition,module_Properties,"prop_view_idem",[0,1]) - , (QuickCheckProposition,module_Properties,"prop_view_local",[0,1]) + , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[1,0]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[1,0]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[0,1]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[0,1]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[0,1]) ] PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (QuickCheckProposition,module_Properties,"prop_greedyView_reversible",[1,0]) - , (QuickCheckProposition,module_Properties,"prop_greedyView_idem",[0,1]) + , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[1,0]) + , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[0,1]) ] PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] diff --git a/examples/ZLang/1/Main.hs b/examples/ZLang/1/Main.hs new file mode 100644 --- /dev/null +++ b/examples/ZLang/1/Main.hs @@ -0,0 +1,39 @@ +import Parser as P +import TypeInfer as T +import MatchCheck as MC +import Control.Monad.Trans.Writer.Lazy +import qualified Data.List as List + +-- TEST RELATED BEGIN +import Types +import TypedAst +import qualified Data.Map as Map +import Debug.Hoed.Pure + +failType = Record False [("a",IntType),("b",StringType)] + +m1 = (TRecordMatchExpr [("a",(TIntMatchExpr 42,IntType)),("b",(TStringMatchExpr "abc",StringType))],Record False [("a",IntType),("b",StringType)]) +m2 = (TRecordMatchExpr [("a",(TVarMatch "n",IntType)),("b",(TStringMatchExpr "def",StringType))],Record False [("a",IntType),("b",StringType)]) +m3 = (TRecordMatchExpr [("a",(TVarMatch "n",IntType)),("b",(TVarMatch "s",StringType))],Record False [("a",IntType),("b",StringType)]) + +testCovering ty matches = covering Map.empty (ideal Map.empty ty) matches == [Covered] +-- TEST RELATED END + +concreteTest = testCovering failType [m1, m2, m3] + +main = printO $ concreteTest + +{- +main :: IO () +main = let path = "../test.z" + in do content <- readFile path + case P.parse content of + Left err -> print err + Right ast -> do + (typed, env, subst) <- T.infer ast + let (b, badMatches) = runWriter (MC.matchCheck env typed) + mapM putStrLn (List.map MC.formatMatchWarning badMatches) + case b of + True -> return () --Continue compilation + False -> return () --Abort compilation +-} diff --git a/examples/ZLang/2/Main.hs b/examples/ZLang/2/Main.hs new file mode 100644 --- /dev/null +++ b/examples/ZLang/2/Main.hs @@ -0,0 +1,39 @@ +import Parser as P +import TypeInfer as T +import MatchCheck as MC +import Control.Monad.Trans.Writer.Lazy +import qualified Data.List as List + +-- TEST RELATED BEGIN +import Types +import TypedAst +import qualified Data.Map as Map +import Debug.Hoed.Pure + +failType = Record False [("a",IntType),("b",StringType)] + +m1 = (TRecordMatchExpr [("a",(TIntMatchExpr 42,IntType)),("b",(TStringMatchExpr "abc",StringType))],Record False [("a",IntType),("b",StringType)]) +m2 = (TRecordMatchExpr [("a",(TVarMatch "n",IntType)),("b",(TStringMatchExpr "def",StringType))],Record False [("a",IntType),("b",StringType)]) +m3 = (TRecordMatchExpr [("a",(TVarMatch "n",IntType)),("b",(TVarMatch "s",StringType))],Record False [("a",IntType),("b",StringType)]) + +testCovering ty matches = covering Map.empty (ideal Map.empty ty) matches == [Covered] +-- TEST RELATED END + +concreteTest = testCovering failType [m1, m2, m3] + +main = printO $ concreteTest + +{- +main :: IO () +main = let path = "../test.z" + in do content <- readFile path + case P.parse content of + Left err -> print err + Right ast -> do + (typed, env, subst) <- T.infer ast + let (b, badMatches) = runWriter (MC.matchCheck env typed) + mapM putStrLn (List.map MC.formatMatchWarning badMatches) + case b of + True -> return () --Continue compilation + False -> return () --Abort compilation +-} diff --git a/examples/ZLang/3/Main.hs b/examples/ZLang/3/Main.hs new file mode 100644 --- /dev/null +++ b/examples/ZLang/3/Main.hs @@ -0,0 +1,39 @@ +import Parser as P +import TypeInfer as T +import MatchCheck as MC +import Control.Monad.Trans.Writer.Lazy +import qualified Data.List as List + +-- TEST RELATED BEGIN +import Types +import TypedAst +import qualified Data.Map as Map +import Debug.Hoed.Pure + +failType = Record False [("a",IntType),("b",StringType)] + +m1 = (TRecordMatchExpr [("a",(TIntMatchExpr 42,IntType)),("b",(TStringMatchExpr "abc",StringType))],Record False [("a",IntType),("b",StringType)]) +m2 = (TRecordMatchExpr [("a",(TVarMatch "n",IntType)),("b",(TStringMatchExpr "def",StringType))],Record False [("a",IntType),("b",StringType)]) +m3 = (TRecordMatchExpr [("a",(TVarMatch "n",IntType)),("b",(TVarMatch "s",StringType))],Record False [("a",IntType),("b",StringType)]) + +testCovering ty matches = covering Map.empty (ideal Map.empty ty) matches == [Covered] +-- TEST RELATED END + +concreteTest = testCovering failType [m1, m2, m3] + +main = printO $ concreteTest + +{- +main :: IO () +main = let path = "../test.z" + in do content <- readFile path + case P.parse content of + Left err -> print err + Right ast -> do + (typed, env, subst) <- T.infer ast + let (b, badMatches) = runWriter (MC.matchCheck env typed) + mapM putStrLn (List.map MC.formatMatchWarning badMatches) + case b of + True -> return () --Continue compilation + False -> return () --Abort compilation +-} diff --git a/test.Generic b/test.Generic --- a/test.Generic +++ b/test.Generic @@ -3,6 +3,23 @@ TESTS="0 1 2 3" FAIL=0 + +echo "Testing parallel equality for Generic types" +echo + +x=`./dist/build/hoed-tests-ParEq/hoed-tests-ParEq` +echo "x is $x" +if [ $x = "True" ]; then + echo -n "[OK" +else + FAIL=1 + echo -n "[" + echo -en '\E[37;31m'"\033[1m!!\033[0m" # red "!!" on white background + tput sgr0 # reset colour +fi + echo "] Generic.ParEq" + + echo "Testing events produced for Observable derived for Generic types" echo diff --git a/tests/Prop/t0/Main.hs b/tests/Prop/t0/Main.hs --- a/tests/Prop/t0/Main.hs +++ b/tests/Prop/t0/Main.hs @@ -4,7 +4,7 @@ import Debug.Hoed.Pure -- main = quickcheck prop_idemSimplify -main = logOwp propVarError "hoed-tests-Prop-t0.graph" properties $ print $ prop_idemSimplify (Mul (Const 1) (Const 2)) +main = logOwp Abort "hoed-tests-Prop-t0.graph" properties $ print $ prop_idemSimplify (Mul (Const 1) (Const 2)) where properties = [ Propositions [(BoolProposition,myModule,"prop_idemOne",[0])] PropertiesOf "one" [] , Propositions [(BoolProposition,myModule,"prop_idemZero",[0])] PropertiesOf "zero" [] diff --git a/tests/Prop/t1/Main.hs b/tests/Prop/t1/Main.hs --- a/tests/Prop/t1/Main.hs +++ b/tests/Prop/t1/Main.hs @@ -3,7 +3,7 @@ import Debug.Hoed.Pure -- main = quickcheck prop_idem_negin_sound -main = logOwp propVarError "hoed-tests-Prop-t1.graph" properties $ print (prop_negin_correct eg) +main = logOwp Abort "hoed-tests-Prop-t1.graph" properties $ print (prop_negin_correct eg) -- main = logOwp "hoed-tests-Prop-t1.graph" properties $ print (negin eg, prop_negin_correct eg) where properties = [Propositions [(BoolProposition,cnfModule,"prop_negin_complete",[0]), (BoolProposition,cnfModule,"prop_negin_sound",[0])] Specify "negin" [] diff --git a/tests/Prop/t2/Main.hs b/tests/Prop/t2/Main.hs --- a/tests/Prop/t2/Main.hs +++ b/tests/Prop/t2/Main.hs @@ -3,7 +3,7 @@ import Debug.Hoed.Pure -- main = quickcheck prop_idem_negin_sound -main = logOwp propVarError "hoed-tests-Prop-t2.graph" properties $ print (prop_assoc1toNdigraph eg) +main = logOwp Abort "hoed-tests-Prop-t2.graph" properties $ print (prop_assoc1toNdigraph eg) where properties = [ Propositions [(BoolProposition,digraphModule,"prop_assoc1toNdigraph",[0])] Specify "assoc1toNdigraph" [] , Propositions [(BoolProposition,digraphModule,"prop_mergeAndSortTargets",[0])] Specify "mergeAndSortTargets" [] diff --git a/tests/Prop/t3/Main.hs b/tests/Prop/t3/Main.hs --- a/tests/Prop/t3/Main.hs +++ b/tests/Prop/t3/Main.hs @@ -13,7 +13,7 @@ main :: IO () -main = logOwp propVarError "hoed-tests-Prop-t3.graph" propositions $ do +main = logOwp Abort "hoed-tests-Prop-t3.graph" propositions $ do -- main = do {- Running all tests @@ -39,21 +39,21 @@ where propositions = - [Propositions [(QuickCheckProposition,module_Properties,"prop_focus_all_l",[0]) - ,(QuickCheckProposition,module_Properties,"prop_focus_all_l_generic",[0]) + [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[0]) + ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_generic",[0]) -- ,(QuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0]) ] PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (QuickCheckProposition,module_Properties,"prop_view_reversible",[1,0]) - , (QuickCheckProposition,module_Properties,"prop_view_I",[1,0]) - , (QuickCheckProposition,module_Properties,"prop_view_current",[0,1]) - , (QuickCheckProposition,module_Properties,"prop_view_idem",[0,1]) - , (QuickCheckProposition,module_Properties,"prop_view_local",[0,1]) + , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[1,0]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[1,0]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[0,1]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[0,1]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[0,1]) ] PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (QuickCheckProposition,module_Properties,"prop_greedyView_reversible",[1,0]) - , (QuickCheckProposition,module_Properties,"prop_greedyView_idem",[0,1]) + , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[1,0]) + , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[0,1]) ] PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] diff --git a/tests/Prop/t4/Main.hs b/tests/Prop/t4/Main.hs --- a/tests/Prop/t4/Main.hs +++ b/tests/Prop/t4/Main.hs @@ -24,30 +24,30 @@ -} main :: IO () -main = logOwp propVarError "hoed-tests-Prop-t4.graph" propositions $ do +main = logOwp Abort "hoed-tests-Prop-t4.graph" propositions $ do g <- newStdGen print . fromJust . ok . (generate 1 g) . evaluate $ prop_shift_win_I 1 'd' myStackSet where propositions = - [Propositions [(QuickCheckProposition,module_Properties,"prop_focus_all_l",[0]) - -- ,(QuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0]) + [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[0]) + -- ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0]) ] PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - -- , Propositions [ (QuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[1,0]) + -- , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[1,0]) -- ] -- PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (QuickCheckProposition,module_Properties,"prop_view_reversible",[1,0]) - , (QuickCheckProposition,module_Properties,"prop_view_I",[1,0]) - , (QuickCheckProposition,module_Properties,"prop_view_current",[0,1]) - , (QuickCheckProposition,module_Properties,"prop_view_idem",[0,1]) - , (QuickCheckProposition,module_Properties,"prop_view_local",[0,1]) + , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[1,0]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[1,0]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[0,1]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[0,1]) + , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[0,1]) ] PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (QuickCheckProposition,module_Properties,"prop_greedyView_reversible",[1,0]) - , (QuickCheckProposition,module_Properties,"prop_greedyView_idem",[0,1]) + , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[1,0]) + , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[0,1]) ] PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]