Hoed 0.3.5 → 0.3.6
raw patch · 34 files changed
+1288/−511 lines, 34 filesdep +GLUTdep +OpenGLdep +SDLdep ~basedep ~libgraphdep ~threepenny-guinew-component:exe:hoed-examples-Queens_v1__with_propertiesnew-component:exe:hoed-examples-Queens_v2__with_propertiesnew-component:exe:hoed-examples-Queens_v3__with_propertiesnew-component:exe:hoed-examples-Queens_v4_defect_in_filter__with_propertiesnew-component:exe:hoed-examples-Raincatnew-component:exe:hoed-examples-Stern-Brocotnew-component:exe:hoed-examples-XMonad_changing_focus_duplicates_windows__test_onlynew-component:exe:hoed-examples-filter__with_propertiesnew-component:exe:hoed-tests-Prop-t5binary-added
Dependencies added: GLUT, OpenGL, SDL, SDL-image, SDL-mixer, time
Dependency ranges changed: base, libgraph, threepenny-gui
Files
- Debug/Hoed/NoTrace.hs +128/−0
- Debug/Hoed/Pure.hs +13/−1
- Debug/Hoed/Pure/CompTree.hs +8/−0
- Debug/Hoed/Pure/DemoGUI.hs +143/−61
- Debug/Hoed/Pure/Observe.lhs +39/−33
- Debug/Hoed/Pure/Prop.hs +219/−82
- Debug/Hoed/Pure/Render.hs +17/−7
- Debug/Hoed/Pure/TestParEq.hs +7/−7
- Debug/Hoed/Stk.hs +1/−1
- Debug/Hoed/Stk/Render.hs +36/−41
- Hoed.cabal +166/−39
- README.md +5/−1
- examples/CNF_unsound_demorgan__with_properties/Main.hs +8/−3
- examples/Digraph_not_data_invariant__with_properties/Main.hs +3/−3
- examples/ExpressionSimplifier/Main2.hs +6/−3
- examples/Nubsort/Main.hs +24/−8
- examples/Queens__with_properties/Main2.hs +3/−0
- examples/Queens__with_properties/Main3.hs +3/−0
- examples/Queens_defective_filter__with_properties/Main.hs +3/−0
- examples/Raincat/src/Main.hs +30/−0
- examples/SternBrocot.lhs +97/−0
- examples/XMonad_changing_focus_duplicates_windows__test_only/Main.hs +171/−0
- examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs +56/−188
- examples/afp02Exercises/Compiler__with_properties/Main.hs +4/−1
- examples/filter__with_properties/Main.hs +3/−0
- img/test.png binary
- run +3/−0
- test.Generic +2/−3
- tests/Prop/t0/Main.hs +9/−3
- tests/Prop/t1/Main.hs +6/−1
- tests/Prop/t2/Main.hs +6/−3
- tests/Prop/t3/Main.hs +34/−10
- tests/Prop/t4/Main.hs +32/−12
- tests/Prop/t5/Main.hs +3/−0
+ Debug/Hoed/NoTrace.hs view
@@ -0,0 +1,128 @@+{-|+Module : Debug.Hoed.Notrace+Description : Lighweight algorithmic debugging based on observing intermediate values.+Copyright : (c) 2016 Maarten Faddegon+License : BSD3+Maintainer : hoed@maartenfaddegon.nl+Stability : experimental+Portability : POSIX++Hoed is a tracer and debugger for the programming language Haskell.++This is a drop-in replacement of the Debug.Hoed.Pure or Debug.Hoed.Stk modules and disables tracing (all functions are variations of id).++Read more about Hoed on its project homepage <https://wiki.haskell.org/Hoed>.++Papers on the theory behind Hoed can be obtained via <http://maartenfaddegon.nl/#pub>.++I am keen to hear about your experience with Hoed: where did you find it useful and where would you like to see improvement? You can send me an e-mail at hoed@maartenfaddegon.nl, or use the github issue tracker <https://github.com/MaartenFaddegon/hoed/issues>.+-}++{-# LANGUAGE DefaultSignatures, CPP #-}++module Debug.Hoed.NoTrace+( observe+, runO+, printO+, testO+, observeBase+, Observable(..)+, Parent(..)+, Generic(..)+, send+, ObserverM(..)+, (<<)+) where+import GHC.Generics+import System.IO.Unsafe+import Control.Monad++observe :: String -> a -> a+observe _ = id++runO :: IO a -> IO ()+runO program = do+ program+ return ()++printO :: (Show a) => a -> IO ()+printO expr = print expr++testO :: Show a => (a->Bool) -> a -> IO ()+testO p x = putStrLn $ if (p x) then "Passed 1 test."+ else " *** Failed! Falsifiable: " ++ show x++data Parent = Parent+class Observable a where+ observer :: a -> Parent -> a + default observer :: (Generic a) => a -> Parent -> a+ observer x _ = x++ constrain :: a -> a -> a+ default constrain :: (Generic a) => a -> a -> a+ constrain x _ = x++observeBase :: a -> Parent -> a +observeBase x _ = x++constrainBase :: a -> a -> a+constrainBase x _ = x++newtype ObserverM a = ObserverM { runMO :: Int -> Int -> (a,Int) }++instance Functor ObserverM where+ fmap = liftM++#if __GLASGOW_HASKELL__ >= 710+instance Applicative ObserverM where+ pure = return+ (<*>) = ap+#endif++instance Monad ObserverM where+ return a = ObserverM (\ c i -> (a,i))+ fn >>= k = ObserverM (\ c i ->+ case runMO fn c i of+ (r,i2) -> runMO (k r) c i2+ )++(<<) :: (Observable a) => ObserverM (a -> b) -> a -> ObserverM b+fn << a = do {fn' <- fn; return (fn' a)}++send :: String -> ObserverM a -> Parent -> a+send _ fn context =+ unsafePerformIO $ do { let (r,portCount) = runMO fn 0 0+ ; return r+ }++instance Observable Int where+ observer = observeBase+ constrain = constrainBase+ +instance Observable Bool where+ observer = observeBase+ constrain = constrainBase+ +instance Observable Integer where+ observer = observeBase+ constrain = constrainBase+ +instance Observable Float where+ observer = observeBase+ constrain = constrainBase+ +instance Observable Double where+ observer = observeBase+ constrain = constrainBase+ +instance Observable Char where+ observer = observeBase+ constrain = constrainBase+ +instance Observable () where+ observer = observeBase+ constrain = constrainBase++instance (Observable a) => Observable [a] where+ observer = observeBase+ constrain = constrainBase
Debug/Hoed/Pure.hs view
@@ -102,14 +102,22 @@ -- * Property-assisted algorithmic debugging , runOwp+ , printOwp , testOwp , Propositions(..) , PropType(..) , Proposition(..)+ , mkProposition+ , ofType+ , withSignature+ , sizeHint+ , withTestGen+ , TestGen(..) , PropositionType(..) , Module(..) , Signature(..) , ParEq(..)+ , (===) , runOstore , conAp @@ -261,6 +269,10 @@ printO :: (Show a) => a -> IO () printO expr = runO (print expr) ++printOwp :: (Show a) => [Propositions] -> a -> IO ()+printOwp ps expr = runOwp ps (print expr)+ -- | Only produces a trace. Useful for performance measurements. traceOnly :: IO a -> IO () traceOnly program = do@@ -306,7 +318,7 @@ condPutStrLn verbose $ show n ++ " computation statements" condPutStrLn verbose $ show ((length . vertices $ ct) - 1) ++ " nodes + 1 virtual root node in the computation tree" condPutStrLn verbose $ show (length . arcs $ ct) ++ " edges in computation tree"- condPutStrLn verbose $ "computation tree has a branch factor of " ++ show b ++ "(i.e the average number of children of non-leaf nodes)"+ condPutStrLn verbose $ "computation tree has a branch factor of " ++ show b ++ " (i.e the average number of children of non-leaf nodes)" condPutStrLn verbose "\n=== Debug Session ===\n" return (events, ti, ct, frt)
Debug/Hoed/Pure/CompTree.hs view
@@ -393,9 +393,17 @@ $ start e s False -> pause e s + NoEnter{} -> if not . corToCons cs $ e then s else cpyTopLvlFun e+ $ case loc of+ True -> addDependency e+ $ start e s+ False -> pause e s+ -- Span end Cons{} -> cpyTopLvlFun e . setLocation e (\_->loc) $ case loc of True -> stop e s False -> resume e s++ evnt -> error $ "traceInfo.loop cannot handle " ++ show evnt
Debug/Hoed/Pure/DemoGUI.hs view
@@ -24,6 +24,7 @@ import Data.IORef import Text.Regex.Posix import Text.Regex.Posix.String+import Data.Time.Clock import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap import Data.List(findIndex,intersperse,nub,sort,sortBy@@ -40,6 +41,8 @@ sortOn' f = sortBy (\x y -> compare (f x) (f y)) #endif +type Next = CompTree -> (Vertex -> Judgement) -> Vertex+ -------------------------------------------------------------------------------- -- The tabbed layout from which we select the different views @@ -217,6 +220,7 @@ guiAssisted traceRef ps compTreeRef currentVertexRef regexRef imgCountRef = do handlerRef <- UI.liftIO $ newIORef Bottom+ nextRef <- UI.liftIO $ newIORef (next_step :: Next) -- Get a list of vertices from the computation tree tree <- UI.liftIO $ readIORef compTreeRef@@ -230,82 +234,158 @@ showStmt compStmt compTreeRef currentVertexRef -- Buttons to judge the current statement- right <- UI.button # UI.set UI.text "right " #+ [UI.img # set UI.src "static/right.png" # set UI.height 30] # set UI.style [("margin-right","1em")]- wrong <- UI.button # set UI.text "wrong " #+ [UI.img # set UI.src "static/wrong.png" # set UI.height 30] # set UI.style [("margin-right","1em")]- let j = judge AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef+ right <- UI.button # UI.set UI.text "right " #+ [UI.img # set UI.src "static/right.png" # set UI.height 20] # set UI.style [("margin-right","1em")]+ wrong <- UI.button # set UI.text "wrong " #+ [UI.img # set UI.src "static/wrong.png" # set UI.height 20] # set UI.style [("margin-right","1em")]+ let j = judge AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef 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 # 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 traceRef ps status currentVertexRef compStmt handlerRef- on UI.click testB $ \_ -> testCurrent compTreeRef traceRef ps status currentVertexRef compStmt handlerRef- on UI.click resetB $ \_ -> resetTree compTreeRef ps status currentVertexRef compStmt+ let lightBulbs n = take n . repeat $ UI.img # set UI.src "static/test.png" # set UI.height 20 - -- MF TODO: remove radio buttons !?- -- 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 Bottom- onCheck r2 r1 r3 Forall- -- onCheck r3 r1 r2 TrustForall+ test1B <- UI.button # set UI.text "test" #+ lightBulbs 1 # set UI.style [("margin-right","1em")]+ testChB <- UI.button # set UI.text "test" #+ lightBulbs 2 # set UI.style [("margin-right","1em")]+ testAllB <- UI.button # set UI.text "test" #+ lightBulbs 3 # set UI.style [("margin-right","1em")]+ resetB <- UI.button # set UI.text "clear all" # set UI.height 20+ on UI.click test1B $ \_ -> testCurrent compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef+ on UI.click testChB $ \_ -> testCurrentAndChildren compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef+ on UI.click testAllB $ \_ -> testAll compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef+ on UI.click resetB $ \_ -> resetTree compTreeRef ps status currentVertexRef compStmt nextRef + -- strategy buttons+ singleStep <- UI.input # set UI.type_ "radio" # set UI.checked True+ divideQuery <- UI.input # set UI.type_ "radio" # set UI.checked False+ on UI.checkedChange singleStep $ \_ -> do+ return divideQuery # set UI.checked False+ UI.liftIO $ writeIORef nextRef next_step+ advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef+ on UI.checkedChange divideQuery $ \_ -> do+ return singleStep # set UI.checked False+ UI.liftIO $ writeIORef nextRef next_daq+ advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef+ -- Populate the main screen- 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]+ top <- UI.center #+ [return status, UI.br, return right, return wrong, return test1B, return testChB, return testAllB, return resetB]+ top2 <- UI.center #+ [ UI.span # set UI.text "strategy: " # set UI.style [("margin-right","1em")]+ , return singleStep, UI.span # set UI.text "single step" # set UI.style [("margin-right","1em")]+ , return divideQuery, UI.span # set UI.text "divide & query"]+ UI.div #+ [return top, return top2, UI.hr, return compStmt] -resetTree compTreeRef ps status currentVertexRef compStmt = do+resetTree compTreeRef ps status currentVertexRef compStmt nextRef = do t <- UI.liftIO $ readIORef compTreeRef UI.liftIO $ writeIORef compTreeRef (mapGraph resetVertex t)- advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef+ advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef where resetVertex = flip setJudgement Unassessed -{--testAll compTreeRef trace ps status currentVertexRef compStmt handlerRef = do+testCurrent :: IORef CompTree -> IORef Trace -> [Propositions] -> UI.Element -> IORef Int -> UI.Element -> t -> IORef Next -> UI ()+testCurrent compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef= 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 $ readIORef handlerRef- compTree <- readIORef compTreeRef- compTree' <- Prop.judge handler trace ps compTree- writeIORef compTreeRef compTree'- advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef--}+ mcv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef+ case mcv of+ Nothing -> updateStatus status compTreeRef+ (Just cv) -> do+ time1 <- UI.liftIO getCurrentTime+ test1 cv compTreeRef traceRef ps handlerRef (onNoProps cv) onJudge onTreeSwitch+ time2 <- UI.liftIO getCurrentTime+ UI.liftIO $ putStrLn ("tested computation statement in " ++ show (diffUTCTime time2 time1))+ where+ onNoProps cv = do+ UI.element status # set UI.text ("Cannot test: no propositions associated with function " ++ (stmtLabel . vertexStmt) cv ++ "!")+ return ()+ onJudge =+ advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef+ onTreeSwitch :: CompTree -> Trace -> UI ()+ onTreeSwitch newCompTree newTrace = do+ UI.liftIO $ writeIORef compTreeRef newCompTree+ UI.liftIO $ writeIORef traceRef newTrace + advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef+ return status # UI.set UI.text "Discovered and switched to a simpler computatation tree!" #+ [UI.img # set UI.src "static/test.png" # set UI.height 30]+ return () -testCurrent compTreeRef traceRef ps status currentVertexRef compStmt handlerRef = do+testCurrentAndChildren compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef = 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+ compTree <- UI.liftIO $ readIORef compTreeRef case mcv of+ Nothing -> updateStatus status compTreeRef (Just cv) -> do- case lookupPropositions ps cv of - Nothing -> updateStatus status compTreeRef+ let vs = cv : succs compTree cv+ time1 <- UI.liftIO getCurrentTime+ switchedTree <- testMany vs compTreeRef traceRef ps handlerRef+ time2 <- UI.liftIO getCurrentTime+ UI.liftIO $ putStrLn ("tested " ++ show (length vs) ++ " computation statements in " ++ show (diffUTCTime time2 time1))+ advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef+ if switchedTree + then do+ return status # UI.set UI.text "Discovered and switched to a simpler computatation tree!" #+ [UI.img # set UI.src "static/test.png" # set UI.height 30]+ return ()+ else+ return ()++testAll compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef = 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+ compTree <- UI.liftIO $ readIORef compTreeRef+ let vs = vertices compTree+ time1 <- UI.liftIO getCurrentTime+ switchedTree <- testMany vs compTreeRef traceRef ps handlerRef+ time2 <- UI.liftIO getCurrentTime+ UI.liftIO $ putStrLn ("tested " ++ show (length vs) ++ " computation statements in " ++ show (diffUTCTime time2 time1))+ advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef+ if switchedTree + then do+ return status # UI.set UI.text "Discovered and switched to a simpler computatation tree!" #+ [UI.img # set UI.src "static/test.png" # set UI.height 30]+ return ()+ else+ return ()++testMany :: [Vertex] -> IORef CompTree -> IORef Trace -> [Propositions] -> t -> UI Bool+testMany vs compTreeRef traceRef ps handlerRef = case vs of+ [] -> return False+ (v:vs') -> do+ continue <- test1 v compTreeRef traceRef ps handlerRef (onNoProps v) onJudge onTreeSwitch+ if continue then testMany vs' compTreeRef traceRef ps handlerRef+ else return True+ where+ onNoProps _ =+ return True+ onJudge = + return True+ onTreeSwitch newCompTree newTrace = do+ UI.liftIO $ writeIORef compTreeRef newCompTree+ UI.liftIO $ writeIORef traceRef newTrace + UI.liftIO $ putStrLn $ "Switched to a simpler computation tree!"+ return False++test1 :: Vertex -> IORef CompTree -> IORef Trace -> [Propositions] -> t -> UI b -> UI b -> (CompTree -> Trace -> UI b) -> UI b+test1 vertex compTreeRef traceRef ps handlerRef onNoProps onJudge onTreeSwitch = do+ compTree <- UI.liftIO $ readIORef compTreeRef+ mj <- test1' vertex compTree traceRef ps handlerRef+ case mj of+ Nothing -> onNoProps+ (Just j) -> case j of + (Judge jmt) -> do+ UI.liftIO $ putStrLn $ "conclusion: statement is " ++ show jmt+ UI.liftIO $ writeIORef compTreeRef (replaceVertex compTree (setJudgement vertex jmt))+ onJudge+ (AlternativeTree compTree' trace') -> do+ onTreeSwitch compTree' trace'++test1' :: Vertex -> CompTree -> IORef Trace -> [Propositions] -> t -> UI (Maybe Judge)+test1' v compTree traceRef ps handlerRef = do+ case lookupPropositions ps v of + Nothing ->+ return Nothing (Just p) -> do- compTree <- UI.liftIO $ readIORef compTreeRef trace <- UI.liftIO $ readIORef traceRef- j <- UI.liftIO $ Prop.judge trace p cv unjudgedCharacterCount compTree- case j of - (Judge jmt) -> - UI.liftIO $ writeIORef compTreeRef (replaceVertex compTree (setJudgement cv jmt))- (AlternativeTree compTree' trace') -> do- UI.liftIO $ writeIORef compTreeRef compTree'- UI.liftIO $ writeIORef traceRef trace'- UI.liftIO $ putStrLn $ "Switched to a simpler computation tree!" -- MF TODO: need to properly tell (or better: ask) user- advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef- Nothing -> updateStatus status compTreeRef+ j <- UI.liftIO $ Prop.judge trace p v unjudgedCharacterCount compTree+ return (Just j) + -------------------------------------------------------------------------------- -- The Algorithmic Debugging GUI guiAlgoDebug :: IORef CompTree -> IORef Int -> IORef String -> IORef Int -> UI UI.Element guiAlgoDebug compTreeRef currentVertexRef regexRef imgCountRef = do+ nextRef <- UI.liftIO $ newIORef (next_step :: Next) -- Get a list of vertices from the computation tree tree <- UI.liftIO $ readIORef compTreeRef@@ -321,7 +401,7 @@ -- Buttons to judge the current statement right <- UI.button # UI.set UI.text "right " #+ [UI.img # set UI.src "static/right.png" # set UI.height 30] # set UI.style [("margin-right","1em")] wrong <- UI.button # set UI.text "wrong " #+ [UI.img # set UI.src "static/wrong.png" # set UI.height 30]- let j = judge AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef+ let j = judge AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef j right Right j wrong Wrong @@ -336,8 +416,8 @@ data Advance = AdvanceToNext | DoNotAdvance judge :: Advance -> UI.Element -> UI.Element -> Maybe UI.Element -> Maybe (UI.Element,IORef Int) - -> IORef UID -> IORef CompTree -> UI.Element -> Judgement -> UI ()-judge adv status compStmt mMenu mImg currentVertexRef compTreeRef b j = + -> IORef UID -> IORef CompTree -> IORef Next -> UI.Element -> Judgement -> UI ()+judge adv status compStmt mMenu mImg currentVertexRef compTreeRef nextRef b j = on UI.click b $ \_ -> do mv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef case mv of@@ -348,21 +428,22 @@ judge' v = do t' <- UI.liftIO $ readIORef compTreeRef UI.liftIO $ writeIORef compTreeRef (markNode t' v j)- advance adv status compStmt mMenu mImg currentVertexRef compTreeRef+ advance adv status compStmt mMenu mImg currentVertexRef compTreeRef nextRef advance :: Advance -> UI.Element -> UI.Element -> Maybe UI.Element -> Maybe (UI.Element,IORef Int) - -> IORef UID -> IORef CompTree -> UI ()-advance adv status compStmt mMenu mImg currentVertexRef compTreeRef = do+ -> IORef UID -> IORef CompTree -> IORef Next -> UI ()+advance adv status compStmt mMenu mImg currentVertexRef compTreeRef nextRef = do mv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef+ next <- UI.liftIO $ readIORef nextRef case mv of Nothing -> do t <- UI.liftIO $ readIORef compTreeRef- case next_step t getJudgement of+ case next t getJudgement of RootVertex -> return () -- when does this happen ... ? w -> advanceTo w status compStmt mMenu mImg currentVertexRef compTreeRef (Just v) -> do t <- UI.liftIO $ readIORef compTreeRef- case (adv, next_step t getJudgement) of+ case (adv, next t getJudgement) of (DoNotAdvance,_) -> advanceTo v status compStmt mMenu mImg currentVertexRef compTreeRef (AdvanceToNext,RootVertex) -> advanceTo v status compStmt mMenu mImg currentVertexRef compTreeRef (AdvanceToNext,w) -> advanceTo w status compStmt mMenu mImg currentVertexRef compTreeRef@@ -409,7 +490,8 @@ right <- UI.button # UI.set UI.text "right " #+ [UI.img # set UI.src "static/right.png" # set UI.height 20] # set UI.style [("margin-right","1em")] wrong <- UI.button # set UI.text "wrong " #+ [UI.img # set UI.src "static/wrong.png" # set UI.height 20] # set UI.style [("margin-right","1em")] - let j = judge DoNotAdvance status compStmt (Just menu) (Just (img, imgCountRef)) currentVertexRef compTreeRef+ nextRef <- UI.liftIO $ newIORef (next_step :: Next)+ let j = judge DoNotAdvance status compStmt (Just menu) (Just (img, imgCountRef)) currentVertexRef compTreeRef nextRef j right Right j wrong Wrong
Debug/Hoed/Pure/Observe.lhs view
@@ -123,6 +123,7 @@ ) as Exception -} import Data.Dynamic ( Dynamic )+ \end{code} \begin{code}@@ -150,7 +151,7 @@ class GObservable f where gdmobserver :: f a -> Parent -> f a- gdmObserveChildren :: f a -> ObserverM (f a)+ gdmObserveArgs :: f a -> ObserverM (f a) gdmShallowShow :: f a -> String constrainBase :: Eq a => a -> a -> a@@ -184,54 +185,52 @@ -- Meta: data types instance (GObservable a) => GObservable (M1 D d a) where- gdmobserver m@(M1 x) cxt = M1 (gdmobserver x cxt)- gdmObserveChildren = gthunk- gdmShallowShow = error "gdmShallowShow not defined on <<Meta: data types>>"+ gdmobserver m@(M1 x) cxt = M1 (gdmobserver x cxt)+ gdmObserveArgs = gthunk+ gdmShallowShow = error "gdmShallowShow not defined on the <<data meta type>>" -- Meta: Selectors instance (GObservable a, Selector s) => GObservable (M1 S s a) where- gdmobserver m@(M1 x) cxt- = M1 (gdmobserver x cxt)- -- Uncomment next two lines to record selector names- -- selName m == "" = M1 (gdmobserver x cxt)- -- otherwise = M1 (send (selName m ++ " =") (gdmObserveChildren x) cxt)- gdmObserveChildren = gthunk- gdmShallowShow = error "gdmShallowShow not defined on <<Meta: selectors>>"+ gdmobserver (M1 x) cxt = M1 (gdmobserver x cxt)+ gdmObserveArgs = gthunk+ gdmShallowShow = error "gdmShallowShow not defined on the <<selector meta type>>" -- Meta: Constructors instance (GObservable a, Constructor c) => GObservable (M1 C c a) where- gdmobserver m1 = send (gdmShallowShow m1) (gdmObserveChildren m1)- gdmObserveChildren (M1 x) = do {x' <- gdmObserveChildren x; return (M1 x')}- gdmShallowShow = conName+ gdmobserver m1 = send (gdmShallowShow m1) (gdmObserveArgs m1)+ gdmObserveArgs (M1 x) = do {x' <- gdmObserveArgs x; return (M1 x')}+ gdmShallowShow = conName -- Unit: used for constructors without arguments instance GObservable U1 where- gdmobserver x _ = x- gdmObserveChildren = return- gdmShallowShow = error "gdmShallowShow not defined on <<the unit type>>"+ gdmobserver x _ = x+ gdmObserveArgs = return+ gdmShallowShow = error "gdmShallowShow not defined on <<the unit type>>" -- Sums: encode choice between constructors instance (GObservable a, GObservable b) => GObservable (a :+: b) where- gdmobserver (L1 x) = send (gdmShallowShow x) (gdmObserveChildren $ L1 x)- gdmobserver (R1 x) = send (gdmShallowShow x) (gdmObserveChildren $ R1 x)- gdmShallowShow (L1 x) = gdmShallowShow x- gdmShallowShow (R1 x) = gdmShallowShow x- gdmObserveChildren (L1 x) = do {x' <- gdmObserveChildren x; return (L1 x')}- gdmObserveChildren (R1 x) = do {x' <- gdmObserveChildren x; return (R1 x')}+ gdmobserver (L1 x) = send (gdmShallowShow x) (gdmObserveArgs $ L1 x)+ gdmobserver (R1 x) = send (gdmShallowShow x) (gdmObserveArgs $ R1 x)+ gdmShallowShow (L1 x) = gdmShallowShow x+ gdmShallowShow (R1 x) = gdmShallowShow x+ gdmObserveArgs (L1 x) = do {x' <- gdmObserveArgs x; return (L1 x')}+ gdmObserveArgs (R1 x) = do {x' <- gdmObserveArgs x; return (R1 x')} -- Products: encode multiple arguments to constructors instance (GObservable a, GObservable b) => GObservable (a :*: b) where- gdmobserver (a :*: b) cxt = (gdmobserver a cxt) :*: (gdmobserver b cxt)- gdmObserveChildren (a :*: b) = do a' <- gdmObserveChildren a- b' <- gdmObserveChildren b- return (a' :*: b')- gdmShallowShow = error "gdmShallowShow not defined on <<the product type>>"+ gdmobserver (a :*: b) cxt = (gdmobserver a cxt) :*: (gdmobserver b cxt)+ gdmObserveArgs (a :*: b) = do + a' <- gdmObserveArgs a+ b' <- gdmObserveArgs b+ return (a' :*: b')+ gdmShallowShow = error "gdmShallowShow not defined on <<the product type>>" -- Constants: additional parameters and recursion of kind * instance (Observable a) => GObservable (K1 i a) where- gdmobserver (K1 x) cxt = K1 $ observer x cxt- gdmObserveChildren = gthunk- gdmShallowShow = error "gdmShallowShow not defined on <<constant types>>"+ gdmobserver (K1 x) cxt = K1 $ observer x cxt+ gdmObserveArgs = gthunk+ gdmShallowShow = error "gdmShallowShow not defined on <<the constant type>>"+ \end{code} Observing functions is done via the ad-hoc mechanism, because@@ -547,11 +546,18 @@ \begin{code} +-- MF TODO: the eqType and isObservable' definitions feel a bit "hacky",+-- can we do better? isObservable :: TyVarMap -> Type -> Type -> Q Bool--- MF TODO: if s == t then return True else isObservable' bs t+isObservable bs s t | s `eqType` t = return True isObservable bs s t = isObservable' bs t --- MF TODO this is a hack+eqType (ForallT _ _ t1) t2 = t1 `eqType` t2+eqType (AppT t1 s1) (AppT t2 s2) = (t1 `eqType` t2) && (s1 `eqType` s2)+eqType (VarT _) (VarT _) = True -- dodgy ...+eqType (ConT n1) (ConT n2) = n1 == n2+eqType _ _ = False+ isObservable' bs (AppT ListT _) = return True isObservable' bs (VarT n) = case lookupBinding bs n of
Debug/Hoed/Pure/Prop.hs view
@@ -1,6 +1,6 @@ -- This file is part of the Haskell debugger Hoed. ----- Copyright (c) Maarten Faddegon, 2015+-- Copyright (c) Maarten Faddegon 2015-2016 {-# LANGUAGE DefaultSignatures, TypeOperators, FlexibleContexts, FlexibleInstances, StandaloneDeriving, CPP, DeriveGeneric #-} @@ -8,7 +8,7 @@ -- ( judge -- , Propositions(..) -- ) where-import Debug.Hoed.Pure.Observe(Observable(..),Trace(..),UID,Event(..),Change(..),ourCatchAllIO,evaluate)+import Debug.Hoed.Pure.Observe(Observable(..),Trace(..),UID,Event(..),Change(..),ourCatchAllIO,evaluate,eventParent,parentPosition) import Debug.Hoed.Pure.Render(CompStmt(..),noNewlines) import Debug.Hoed.Pure.CompTree(CompTree,Vertex(..),Graph(..),vertexUID,vertexRes,replaceVertex,getJudgement,setJudgement) import Debug.Hoed.Pure.EventForest(EventForest,mkEventForest,dfsChildren)@@ -22,14 +22,16 @@ import System.IO(hPutStrLn,stderr) import System.IO.Unsafe(unsafePerformIO) import Data.Char(isAlpha)-import Data.Maybe(isNothing,fromJust)-import Data.List(intersperse,isInfixOf)+import Data.Maybe(isNothing,fromJust,isJust)+import Data.List(intersperse,isInfixOf,foldl1) import GHC.Generics hiding (moduleName) --(Generic(..),Rep(..),from,(:+:)(..),(:*:)(..),U1(..),K1(..),M1(..)) import Control.Monad(foldM) ------------------------------------------------------------------------------------------------------------------------ -data Propositions = Propositions { propositions :: [Proposition], propType :: PropType, funName :: String+data Propositions = Propositions { propositions :: [Proposition]+ , propType :: PropType+ , funName :: String , extraModules :: [Module] } @@ -39,10 +41,40 @@ = Argument Int | SubjectFunction | Random+ deriving (Show,Eq)++data TestGen = TestGenQuickCheck | TestGenLegacyQuickCheck -- TestGenSmallCheck deriving Show -type Proposition = (PropositionType,Module,String,[Signature])+data Proposition = Proposition { propositionType :: PropositionType+ , propModule :: Module+ , propName :: String+ , signature :: [Signature]+ , maxSize :: Maybe Int+ , testgen :: TestGen+ } deriving Show +mkProposition :: Module -> String -> Proposition+mkProposition m f = Proposition { propositionType = BoolProposition+ , propModule = m+ , propName = f+ , signature = [SubjectFunction,Argument 0]+ , maxSize = Nothing+ , testgen = TestGenQuickCheck+ }++ofType :: Proposition -> PropositionType -> Proposition+ofType p t = p{propositionType = t}++withSignature :: Proposition -> [Signature] -> Proposition+withSignature p s = p{signature = s}++sizeHint :: Proposition -> Int -> Proposition+sizeHint p n = p{maxSize = Just n}++withTestGen :: Proposition -> TestGen -> Proposition+withTestGen p f = p{testgen=f}+ data PropositionType = IOProposition | BoolProposition@@ -61,18 +93,6 @@ | DisproveBy Proposition [String] deriving Show -propositionType :: Proposition -> PropositionType-propositionType (x,_,_,_) = x--propName :: Proposition -> String-propName (_,_,x,_) = x--signature :: Proposition -> [Signature]-signature (_,_,_,x) = x--propModule :: Proposition -> Module-propModule (_,x,_,_) = x- ------------------------------------------------------------------------------------------------------------------------ sourceFile = ".Hoed/exe/Main.hs"@@ -104,6 +124,7 @@ | AlternativeTree CompTree Trace -- ^ Found counter example with simpler computation tree. +-- TODO: review this function, not sure if complexity suggestion actually makes sense there... judgeAll :: UnevalHandler -> (CompTree -> Int) -> Trace -> [Propositions] -> CompTree -> IO CompTree judgeAll handler complexity trc ps compTree = foldM f compTree (vertices compTree) where@@ -118,7 +139,7 @@ putStrLn "*** no propositions" return curTree (Just p) -> do- j <- judge' Bottom trc p v complexity curTree+ j <- judge' handler trc p v complexity curTree case j of (Judge jmt) -> do putStrLn $ "*** judgement is " ++ show jmt@@ -129,30 +150,39 @@ putStrLn $ "*** " ++ msg return $ replaceVertex curTree (setJudgement v (Assisted [InconclusiveProperty msg])) --- MF TODO. We should in function judge also try in between restricted and forall to use the unrestricted subject function with bottom for unevaluated expressions. Note that also in that case we need to switch trees if Wrong. -- |Use propositions to judge a computation statement. -- First tries restricted and bottom for unevaluated expressions,--- then unrestricted and random values for unevaluated expressions.+-- then unrestricted, and finally with randomly generated values +-- for unevaluated expressions. judge :: Trace -> Propositions -> Vertex -> (CompTree -> Int) -> CompTree -> IO Judge judge trc p v complexity curTree = do putStrLn $ take 50 (cycle "-") putStrLn $ "Evaluating properties to judge statement: " ++ vertexRes v putStrLn $ take 50 (cycle "-")- judgeBottom <- judge' Bottom trc p v complexity curTree- case judgeBottom of- (Judge (Assisted _)) -> judge' Forall trc p v complexity curTree- (Judge _) -> return judgeBottom+ putStrLn "### ATTEMPT 1: with a restricted subject function\n"+ res1 <- judge' RestrictedBottom trc p v complexity curTree+ case res1 of+ (Judge (Assisted _)) -> do + putStrLn "### ATTEMPT 2: with an unrestricted subject function\n"+ res2 <- judge' Bottom trc p v complexity curTree+ case res2 of+ (Judge (Assisted _)) -> do + putStrLn "### ATTEMPT 3: with randomly generated values\n"+ judge' Forall trc p v complexity curTree+ _ -> return res2+ (Judge _) -> return res1+ return res1 -judge' Bottom trc p v complexity curTree = do- pas <- evalPropositions Bottom trc p v+judge' RestrictedBottom trc p v complexity curTree = do+ pas <- evalPropositions RestrictedBottom trc p v let j | propType p == Specify && all holds pas = (Judge Right) | any disproves pas = (Judge Wrong) | otherwise = advice pas return j -judge' Forall trc p v complexity curTree = do- pas <- evalPropositions Forall trc p v+judge' handler trc p v complexity curTree = do+ pas <- evalPropositions handler trc p v let j | propType p == Specify && all holds pas = return (Judge Right) | any disproves pas = do let curComplexity = complexity curTree@@ -182,7 +212,7 @@ -- Using the given complexity function, compare the computation trees of the list of -- property results and select the simplest tree. simplestTree :: (CompTree -> Int) -> [Module] -> [PropRes] -> (Int,CompTree,Trace) -> Trace -> Vertex -> IO (Int,CompTree,Trace)-simplestTree complexity ms rs cur trc v = foldM (simple2 complexity trc v ms) cur (filter disprovesBy rs)+simplestTree complexity ms rs cur trc v = foldM (simple2 complexity trc v ms) cur (filter disproves rs) -- Using the given complexity function, read the computation tree of the given property -- into memory and compare its complexity with the complexity of the currently best tree.@@ -195,6 +225,8 @@ case (maybeCandTree,maybeCandTrace) of (Just candTree, Just candTrace) -> do let candComplexity = complexity candTree+ putStrLn $ "Discovered new tree with complexity " ++ show candComplexity + ++ " (current tree is " ++ show curComplexity ++ ")" return $ if candComplexity < curComplexity then (candComplexity,candTree,candTrace) else (curComplexity,curTree,curTrace)@@ -216,14 +248,16 @@ isError (Error _ _) = True isError _ = False -data UnevalHandler = Bottom | Forall | FromList [String] deriving (Eq, Show)+data UnevalHandler = RestrictedBottom | Bottom | Forall | FromList [String] deriving (Eq, Show) unevalHandler :: UnevalHandler -> PropVarGen String-unevalHandler Bottom = propVarError-unevalHandler Forall = propVarFresh-unevalHandler (FromList _) = propVarFresh+unevalHandler RestrictedBottom = propVarError+unevalHandler Bottom = propVarError+unevalHandler Forall = propVarFresh+unevalHandler (FromList _) = propVarFresh unevalState :: UnevalHandler -> PropVars+unevalState RestrictedBottom = propVars0 unevalState Bottom = propVars0 unevalState Forall = propVars0 -- unevalState (FromList _) = propVars0@@ -246,6 +280,9 @@ evalPropositions handler trc p v = mapM (evalProposition handler trc v (extraModules p)) (propositions p) evalProposition :: UnevalHandler -> Trace -> Vertex -> [Module] -> Proposition -> IO PropRes+evalProposition RestrictedBottom trc v ms prop | not (SubjectFunction `elem` (signature prop)) = do+ putStrLn $ "property " ++ propName prop ++ ": Cannot restrict subject function!"+ return $ Error prop "Cannot restrict subject function!" evalProposition handler trc v ms prop = do putStrLn $ "property " ++ propName prop createDirectoryIfMissing True ".Hoed/exe"@@ -266,11 +303,14 @@ reEvalProposition :: PropRes -> Trace -> Vertex -> [Module] -> IO PropRes+reEvalProposition (Disprove prop) _ _ _ = return (Disprove prop) -- no need to re-evaluate reEvalProposition (DisproveBy prop values) trc v ms = do- putStrLn $ "RE-EVALUATE with " ++ concat (intersperse " " values) ++ " {"- (Disprove p) <- evalProposition (FromList values) trc v ms prop+ putStrLn $ "RE-EVALUATE with " ++ concat valuesInBrackets ++ " {"+ (Disprove p) <- evalProposition (FromList valuesInBrackets) trc v ms prop putStrLn $ "} RE-EVALUATE" return (Disprove p)+ where+ valuesInBrackets = map (\s -> " (" ++ s ++ ") ") values clean = system $ "rm -f " ++ sourceFile ++ " " ++ exeFile ++ " " ++ buildFiles @@ -347,9 +387,18 @@ propVarBind :: UnevalHandler -> (String,PropVars) -> Proposition -> String propVarBind (FromList _) (propApp,_) prop = generatePrint prop ++ propApp propVarBind _ (propApp,([],_)) prop = generatePrint prop ++ propApp-propVarBind _ (propApp,(bvs,_)) prop = "quickCheck (\\" ++ bvs' ++ " -> " ++ propApp ++ ")"+propVarBind _ (propApp,(bvs,_)) prop = qc ++ " (\\" ++ bvs' ++ " -> " ++ propApp ++ ")" where bvs' = concat (intersperse " " bvs)+ qc = case (testgen prop, maxSize prop) of+ (TestGenQuickCheck, Nothing) + -> "quickCheckWith stdArgs{maxDiscardRatio=50}"+ (TestGenQuickCheck, Just n)+ -> "quickCheckWith stdArgs{maxDiscardRatio=50,maxSize=" ++ show n ++ "}"+ (TestGenLegacyQuickCheck, Nothing)+ -> "check defaultConfig{configMaxFail=5000}"+ (TestGenLegacyQuickCheck, Just n)+ -> "check defaultConfig{configMaxFail=5000,configSize=(+" ++ show n ++ ") . (`div` 2)}" generatePrint :: Proposition -> String generatePrint p = case propositionType p of@@ -409,50 +458,133 @@ args = generateArgs (unevalHandler handler) trc getEvent i cf :: PropVarGen String- cf | handler == Bottom = foldl1 (liftPV $ \acc c -> acc ++ " " ++ c)- [ propVarReturn $ "(" ++ genConAp (length args) f- , generateRes (unevalHandler handler) trc getEvent i- , propVarReturn $ ")"- ]+ cf | handler == RestrictedBottom + = foldl1 (liftPV $ \acc c -> acc ++ " " ++ c)+ [ propVarReturn $ "(" ++ genConAp (length args) f+ , generateRes (unevalHandler handler) trc getEvent i+ , propVarReturn $ ")"+ ] | otherwise = propVarReturn f generateRes :: (PropVarGen String) -> Trace -> (UID -> Event) -> UID -> PropVarGen String-generateRes unevalGen trc getEvent i = case dfsChildren frt e of- [_,_,_,Nothing] -> unevalGen- [_,_,_,mr] -> generateRes' unevalGen trc getEvent mr- where- frt = (mkEventForest trc)- e = getEvent i+generateRes unevalGen trc getEvent i+ | areFun mres = (propVarReturn " {- generateRes -} ") `pvCat`+ (generateRes unevalGen trc getEvent (eventUID . head . justFuns $ mres)) -- (*)+ | otherwise = case mres of [_,mr] -> generateRes' unevalGen trc getEvent mr+ --+ -- (*) MF TODO: can there be multiple funs in mres? what then?+ --+ where+ mres = filter isJustRes children+ mr = case mres of [_,e] -> e; _ -> Nothing+ children = dfsChildren frt e+ frt = (mkEventForest trc)+ e = getEvent i generateRes' :: PropVarGen String -> Trace -> (UID->Event) -> Maybe Event -> PropVarGen String generateRes' unevalGen trc getEvent Nothing = unevalGen generateRes' unevalGen trc getEvent (Just e)- | change e == Fun = case dfsChildren frt e of [_,_ ,_,mr] -> generateRes' unevalGen trc getEvent mr- [Nothing,_,mr] -> generateRes' unevalGen trc getEvent mr- as -> error $ "generateRes': event " ++ show (eventUID e) ++ ":FUN has " - ++ show (length as) ++ " children!\nnamely: " ++ commas (map show as)- | otherwise = generateExpr unevalGen frt (Just e)- where- frt = (mkEventForest trc)+ | change e == Fun = + case dfsChildren frt e of + [_,_ ,_,mr] -> + generateRes' unevalGen trc getEvent mr+ [Nothing,_,mr] -> + generateRes' unevalGen trc getEvent mr+ as -> + error $ "generateRes': event " ++ show (eventUID e) + ++ ":FUN has " ++ show (length as) ++ " children!\nnamely: " ++ commas (map show as)+ | otherwise = generateExpr unevalGen trc getEvent frt (Just e)+ where+ frt = (mkEventForest trc) generateArgs :: (PropVarGen String) -> Trace -> (UID -> Event) -> UID -> [PropVarGen String]-generateArgs unevalGen trc getEvent i = case dfsChildren frt e of- [_,ma,_,mr] -> generateExpr unevalGen frt ma : moreArgs unevalGen trc getEvent mr- [Nothing,_,mr] -> unevalGen : moreArgs unevalGen trc getEvent mr- xs -> error ("generateArgs: dfsChildren (" ++ show e ++ ") = " ++ show xs)- where- frt = (mkEventForest trc)- e = getEvent i+generateArgs unevalGen trc getEvent i =+ (propVarReturn " {- generateArgs -} ") `pvCat`+ pvArg `pvCat` (propVarReturn $ " {- more: " ++ show mres ++ " -} ") + : moreArgs unevalGen trc getEvent mr+ where+ pvArg | areFun marg = generateFunMap unevalGen trc getEvent (justFuns marg)+ | otherwise = case marg of+ [Nothing] -> unevalGen+ [_,ma] -> generateExpr unevalGen trc getEvent frt ma+ e = getEvent i+ marg = filter nothingOrArg children+ mres = filter isJustRes children+ mr = case mres of [_,e] -> e; _ -> Nothing+ children = dfsChildren frt e+ frt = (mkEventForest trc) +nothingOrArg Nothing = True+nothingOrArg (Just e) = isArg e++noArg [Nothing] = True+noArg _ = False++areFun :: [Maybe Event] -> Bool+areFun (_:e:_) = isJustFun e+areFun _ = False++justFuns :: [Maybe Event] -> [Event]+justFuns = map fromJust . filter isJustFun ++isJustFun :: Maybe Event -> Bool+isJustFun (Just e) = change e == Fun+isJustFun Nothing = False++generateFunMap :: (PropVarGen String) -> Trace -> (UID -> Event) -> [Event] -> PropVarGen String+generateFunMap unevalGen trc getEvent funs + | length funs > 0 = caseOf `pvCat` (pvConcat cases') `pvCat` esac+ | otherwise = propVarReturn "{- a fun without applications? -}"+ where + caseOf = propVarReturn $ " {- funmap with " ++ (show . length $ funs ) ++ " cases -} " + ++ "(\\y -> case y of "+ esac = propVarReturn ")"+ cases, cases' :: [PropVarGen String]+ cases = map (\fun -> generateCase unevalGen trc getEvent fun) funs+ cases' = intersperse (propVarReturn "; ") cases++generateCase :: (PropVarGen String) -> Trace -> (UID -> Event) -> Event -> PropVarGen String+generateCase unevalGen trc getEvent fun =+ (propVarReturn $ " {- CASE " ++ show fun ++ " -} ") `pvCat`+ case args of + [] -> (propVarReturn "{- catchall -} _") --> res+ _ -> (foldl1 (liftPV $ \acc c -> acc ++ " " ++ c) args) --> res+ where+ args :: [PropVarGen String]+ args = map (generateExpr (propVarReturn "_") trc getEvent frt)+ . filter (\(Just e) -> isArg e) . filter isJust . dfsChildren frt $ fun+ res :: PropVarGen String+ res = generateRes unevalGen trc getEvent (eventUID fun)+ (-->) :: PropVarGen String -> PropVarGen String -> PropVarGen String + (-->) = liftPV $ \x y -> x ++ " -> " ++ y+ frt = mkEventForest trc -- MF TODO: create just once and share?++isArg = hasParentPos 0++isRes = hasParentPos 1++isJustRes (Just e) = isRes e+isJustRes Nothing = False++hasParentPos i = (==i) . parentPosition . eventParent++pvCat :: PropVarGen String -> PropVarGen String -> PropVarGen String+pvCat = liftPV (++)++pvConcat :: [PropVarGen String] -> PropVarGen String+pvConcat = foldl pvCat (propVarReturn "")+ moreArgs :: PropVarGen String -> Trace -> (UID->Event) -> Maybe Event -> [PropVarGen String] moreArgs _ trc getEvent Nothing = [] moreArgs unevalGen trc getEvent (Just e) | change e == Fun = generateArgs unevalGen trc getEvent (eventUID e) | otherwise = [] -generateExpr :: PropVarGen String -> EventForest -> Maybe Event -> PropVarGen String-generateExpr unevalGen _ Nothing = unevalGen-generateExpr unevalGen frt (Just e) = case change e of+generateExpr :: PropVarGen String -> Trace -> (UID -> Event) -> EventForest -> Maybe Event -> PropVarGen String+generateExpr unevalGen _ _ _ Nothing = unevalGen+generateExpr unevalGen trc getEvent frt (Just e) = + -- (propVarReturn $ "{- generateExpr " ++ show e ++ "-}") `pvCat` + case change e of (Cons _ s) -> let s' = if isAlpha (head s) then s else "(" ++ s ++ ")" in liftPV (++) ( foldl (liftPV $ \acc c -> acc ++ " " ++ c) (propVarReturn ("(" ++ s')) cs@@ -460,30 +592,35 @@ ( propVarReturn ") " ) Enter -> propVarReturn ""- _ -> propVarReturn "error \"cannot represent\""+ -- Fun -> generateFunMap unevalGen trc getEvent (justFuns xs)+ evnt -> propVarReturn $ "error \"cannot represent: " ++ show evnt ++ "\"" - where cs :: [PropVarGen String]- cs = map (generateExpr unevalGen frt) (dfsChildren frt e)+ where cs :: [PropVarGen String]+ cs = map (generateExpr unevalGen trc getEvent frt) xs+ xs = (dfsChildren frt e) -------------------------------------------------------------------------------------------------------------------------- -- only works if there is 1 argument conAp :: Observable b => (a -> b) -> b -> a -> b conAp f r x = constrain (f x) r genConAp :: Int -> String -> String-genConAp n f = "(\\r " ++ args ++ " -> Hoed.constrain (" ++ f ++ " " ++ args ++ ") r)"+genConAp n f | n > 0 = "(\\r " ++ args ++ " -> Hoed.constrain (" ++ f ++ " " ++ args ++ ") r)" where args = foldl1 (\a x -> a ++ " " ++ x) xs xs = map (\i -> "x" ++ show i) [1..n] -------------------------------------------------------------------------------------------------------------------------+-------------------------------------------------------------------------------- -- MF TODO: this should probably be part of the Observable class ... ++(===) :: ParEq a => a -> a -> Bool+x === y = case parEq x y of (Just b) -> b+ Nothing -> error "might be equal"+ class ParEq a where- (===) :: a -> a -> Maybe Bool- default (===) :: (Generic a, GParEq (Rep a)) => a -> a -> Maybe Bool- x === y = gParEq (from x) (from y)+ parEq :: a -> a -> Maybe Bool+ default parEq :: (Generic a, GParEq (Rep a)) => a -> a -> Maybe Bool+ parEq x y = gParEq (from x) (from y) class GParEq rep where gParEq :: rep a -> rep a -> Maybe Bool@@ -521,7 +658,7 @@ -- Constants: additional parameters and recursion of kind * instance (ParEq a) => GParEq (K1 i a) where gParEq x y = let r = gParEq_ x y in r- where gParEq_ (K1 x) (K1 y) = x === y+ where gParEq_ (K1 x) (K1 y) = x `parEq` y -- Meta: data types instance (GParEq a) => GParEq (M1 D d a) where@@ -541,9 +678,9 @@ instance (ParEq a) => ParEq [a] instance (ParEq a, ParEq b) => ParEq (a,b) instance (ParEq a) => ParEq (Maybe a)-instance ParEq Int where x === y = Just (x == y)-instance ParEq Bool where x === y = Just (x == y)-instance ParEq Integer where x === y = Just (x == y)-instance ParEq Float where x === y = Just (x == y)-instance ParEq Double where x === y = Just (x == y)-instance ParEq Char where x === y = Just (x == y)+instance ParEq Int where parEq x y = Just (x == y)+instance ParEq Bool where parEq x y = Just (x == y)+instance ParEq Integer where parEq x y = Just (x == y)+instance ParEq Float where parEq x y = Just (x == y)+instance ParEq Double where parEq x y = Just (x == y)+instance ParEq Char where parEq x y = Just (x == y)
Debug/Hoed/Pure/Render.hs view
@@ -66,6 +66,8 @@ ------------------------------------------------------------------------ -- Render equations from CDS set +statementWidth = 110 -- 110 is good for papers (maybe make this configurable from the GUI?)+ renderCompStmts :: CDSSet -> [CompStmt] renderCompStmts = foldl (\acc set -> acc ++ renderCompStmt set) [] @@ -73,20 +75,22 @@ -- is rendered to a computation statement renderCompStmt :: CDS -> [CompStmt]-renderCompStmt (CDSNamed name dependsOn set)+renderCompStmt (CDSNamed name uid set) = map mkStmt statements where statements :: [(String,UID)]- statements = map (\(d,i) -> (pretty 70 d,i)) doc- doc = foldl (\a b -> a ++ renderNamedTop name b) [] output+ statements = map (\(d,i) -> (pretty statementWidth d,i)) doc+ doc = foldl (\a b -> a ++ renderNamedTop name uid b) [] output output = cdssToOutput set mkStmt :: (String,UID) -> CompStmt mkStmt (s,i) = CompStmt name i s -renderNamedTop :: String -> Output -> [(Doc,UID)]-renderNamedTop name (OutData cds)- = map (\(args,res,Just i) -> (renderNamedFn name (args,res), i)) pairs- where pairs = (nubSorted . sortOn argAndRes) pairs'+renderNamedTop :: String -> UID -> Output -> [(Doc,UID)]+renderNamedTop name observeUid(OutData cds)+ = map f pairs+ where f (args,res,Just i) = (renderNamedFn name (args,res), i)+ f (_,cons,Nothing) = (renderNamedCons name cons, observeUid)+ pairs = (nubSorted . sortOn argAndRes) pairs' pairs' = findFn [cds] argAndRes (arg,res,_) = (arg,res) @@ -226,6 +230,12 @@ text "-> " <> renderSet' 0 False res ) )++renderNamedCons :: String -> CDSSet -> Doc+renderNamedCons name cons+ = text name <> nest 2+ ( sep <> linebreak <> grp (text "= " <> renderSet' 0 False cons)+ ) renderNamedFn :: String -> ([CDSSet],CDSSet) -> Doc renderNamedFn name (args,res)
Debug/Hoed/Pure/TestParEq.hs view
@@ -25,14 +25,14 @@ 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+s1 = ((G (error "oeps") D) === (G D (F 4 2))) == False+s2 = ((G D (F 4 2) === (G (error "oeps") D))) == False+s3 = ((G (error "oeps") D) `parEq` (G D D)) == Nothing+s4 = (I D (E A A A) D) === (I (error "oeps") D D) == False+s5 = (I D D (E A A A)) === (I D (error "oeps") D) == False+s6 = (I (E A A A) D D) === (I D D (error "oeps")) == 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+ where (Just b) = x `parEq` y
Debug/Hoed/Stk.hs view
@@ -156,7 +156,7 @@ hPutStrLn stderr $ show n ++ " computation statements" hPutStrLn stderr $ show ((length . vertices $ ct) - 1) ++ " nodes + 1 virtual root node in the computation tree" hPutStrLn stderr $ show (length . arcs $ ct) ++ " edges in computation tree"- hPutStrLn stderr $ "computation tree has a branch factor of " ++ show b ++ "(i.e the average number of children of non-leaf nodes)"+ hPutStrLn stderr $ "computation tree has a branch factor of " ++ show b ++ " (i.e the average number of children of non-leaf nodes)" hPutStrLn stderr "\n=== Debug session === \n" -- hPutStrLn stderr (showWithStack eqs)
Debug/Hoed/Stk/Render.hs view
@@ -118,6 +118,9 @@ -- Truncate -> nextStack_truncate nextStack = nextStack_truncate +nextStackVertex (Vertex (c:_) _) = nextStack c+vertexStack (Vertex (c:_) _) = equStack c+ -- Always push onto top of stack -- nextStack_vanilla :: CompStmt -> CallStack -- nextStack_vanilla (CompStmt cc _ _ _ _ ccs) = cc:ccs@@ -161,19 +164,19 @@ ------------------------------------------------------------------------ -- Bags are collections of computation statements with the same stack -data Bag = Bag {bagStack :: CallStack, bagStmts :: [CompStmt]}+data Bag = Bag {bagStack :: CallStack, bagStmts :: [Vertex]} instance Eq Bag where b1 == b2 = {-# SCC "Bag.==" #-} bagStack b1 == bagStack b2 instance Ord Bag where compare b1 b2 = cmpStk (bagStack b1) (bagStack b2) -bag :: (CompStmt -> CallStack) -> CompStmt -> Bag+bag :: (Vertex -> CallStack) -> Vertex -> Bag bag s c = Bag (s c) [c] -(+++) :: CompStmt -> Bag -> Bag+(+++) :: Vertex -> Bag -> Bag c +++ b = b{bagStmts = c : bagStmts b} -mkBags :: (CompStmt -> CallStack) -> [CompStmt] -> [Bag]+mkBags :: (Vertex -> CallStack) -> [Vertex] -> [Bag] mkBags _ [] = [] mkBags s cs = mkBags' (bag s fc) [] ocs @@ -189,12 +192,11 @@ type Tree = RBTree Bag -mkTree :: (CompStmt -> CallStack) -> [CompStmt] -> Tree+mkTree :: (Vertex -> CallStack) -> [Vertex] -> Tree mkTree s cs = foldl insertOrd emptyRB (mkBags s cs) -mkTrees :: [CompStmt] -> (Tree,Tree)-mkTrees cs = (mkTree equStack cs, mkTree nextStack cs)-+mkTrees :: [Vertex] -> (Tree,Tree)+mkTrees cs = (mkTree vertexStack cs, mkTree nextStackVertex cs) cmpStk :: CallStack -> CallStack -> Ordering cmpStk [] [] = EQ@@ -202,7 +204,7 @@ EQ -> compare (head s1) (head s2) ord -> ord -lookup :: Tree -> CallStack -> [CompStmt]+lookup :: Tree -> CallStack -> [Vertex] lookup t s = case search (\s b -> cmpStk s (bagStack b)) t s of (Just b) -> bagStmts b Nothing -> []@@ -210,7 +212,7 @@ ------------------------------------------------------------------------ -- Inverse call -stmts :: Tree -> (CallStack,CallStack) -> [(CompStmt,CompStmt)]+stmts :: Tree -> (CallStack,CallStack) -> [(Vertex,Vertex)] stmts t (s1,s2) = flattenStmts (lookup t s1, lookup t s2) flattenStmts :: ([a],[b]) -> [(a,b)]@@ -252,53 +254,38 @@ isRoot Root = True isRoot _ = False -pushDeps :: (Tree,Tree) -> [CompStmt] -> [Arc CompStmt ()]+pushDeps :: (Tree,Tree) -> [Vertex] -> [Arc Vertex ()] pushDeps ts cs = concat (map (pushArcs ts) cs) -pushArcs :: (Tree,Tree) -> CompStmt -> [Arc CompStmt ()]+pushArcs :: (Tree,Tree) -> Vertex -> [Arc Vertex ()] pushArcs t p = map (\c -> p ==> c) (pushers t p) where src ==> tgt = Arc src tgt () -pushers :: (Tree,Tree) -> CompStmt -> [CompStmt]-pushers (ts,tn) c = lookup ts (nextStack c)+pushers :: (Tree,Tree) -> Vertex -> [Vertex]+pushers (ts,tn) c = lookup ts (nextStackVertex c) -callDeps :: (Tree,Tree) -> [CompStmt] -> [Arc CompStmt ()]+callDeps :: (Tree,Tree) -> [Vertex] -> [Arc Vertex ()] callDeps (_,t) cs = concat (map (callDep t) cs) -callDep :: Tree -> CompStmt -> [Arc CompStmt ()]+callDep :: Tree -> Vertex -> [Arc Vertex ()] callDep t c3 = foldl (\as (c2,c1) -> c1 ==> c2 : c2 ==> c3 : as) []- (concat (map (stmts t) (lacc $ equStack c3)))+ (concat (map (stmts t) (lacc $ vertexStack c3))) where src ==> tgt = Arc src tgt () mkGraph :: [CompStmt] -> CompGraph mkGraph cs = (dagify merge) . addRoot- . toVertices - -- . sameThread - -- . filterDependsJustOn- -- . addSequenceDependencies . nubArcs $ g- where g :: Graph CompStmt ()- g = let ts = mkTrees cs in Graph (head' msg cs) cs (pushDeps ts cs ++ callDeps ts cs)+ where g :: Graph Vertex ()+ g = Graph (head' msg vs) vs (pushDeps ts vs ++ callDeps ts vs) msg = "mkGraph: No computation statements to construct graph from!" - nubArcs :: Graph CompStmt () -> Graph CompStmt ()- nubArcs (Graph r vs as) = Graph r vs (nub as)-- -- sameThread :: Graph CompStmt () -> Graph CompStmt ()- -- sameThread (Graph r vs as) = Graph r vs (filter (sameThread') as)- -- sameThread' (Arc v w _)- -- | equThreadId v == ThreadIdUnknown - -- || equThreadId w == ThreadIdUnknown- -- || equThreadId v == equThreadId w = True- -- | otherwise = False+ ts = mkTrees vs+ vs = mergeEquivalent cs - -- filterDependsJustOn :: Graph CompStmt () -> Graph CompStmt ()- -- filterDependsJustOn (Graph r vs as) = Graph r vs (filter (filterDependsJustOn') as)- -- filterDependsJustOn' (Arc v w _) = case equDependsOn w of- -- (DependsJustOn i) -> i == equIdentifier v- -- _ -> True+ nubArcs :: Graph Vertex () -> Graph Vertex ()+ nubArcs (Graph r vs as) = Graph r vs (nub as) addSequenceDependencies :: Graph CompStmt () -> Graph CompStmt () addSequenceDependencies (Graph r vs as) = Graph r vs (seqDeps vs ++ as)@@ -307,9 +294,6 @@ (InSequenceAfter i) -> i == equIdentifier v _ -> False - toVertices :: Graph CompStmt () -> CompGraph- toVertices = mapGraph (\s->Vertex [s] Unassessed)- addRoot :: CompGraph -> CompGraph addRoot (Graph _ vs as) = let rs = filter (\(Vertex (s:_) _) -> equStack s == []) vs@@ -322,6 +306,17 @@ msgvs = "mkGraph.merge: No vertices to merge." src ==> tgt = Arc src tgt ()++mergeEquivalent :: [CompStmt] -> [Vertex]+mergeEquivalent [] = []+mergeEquivalent (c:cs) = mkVertex (c:e) : mergeEquivalent n+ where+ equivalent x y = equLabel x == equLabel y && equStack x == equStack y+ (e,n) = partition (equivalent c) cs++mkVertex :: [CompStmt] -> Vertex+mkVertex s = Vertex s Unassessed+ -- %************************************************************************ -- %* *
Hoed.cabal view
@@ -1,5 +1,5 @@ name: Hoed-version: 0.3.5+version: 0.3.6 synopsis: Lightweight algorithmic debugging. description: Hoed is a tracer and debugger for the programming language Haskell.@@ -20,6 +20,11 @@ extra-source-files: changelog, README.md, configure.Demo, configure.Generic, configure.Profiling, configure.Prop, configure.Pure, configure.Stk, run, test.Generic, test.Pure, test.Stk data-files: img/*.png, img/*.gif ++flag buildPropExamples+ description: Build example executables.+ default: False+ flag buildExamples description: Build example executables. default: False@@ -47,6 +52,7 @@ library exposed-modules: Debug.Hoed.Stk , Debug.Hoed.Pure+ , Debug.Hoed.NoTrace other-modules: Debug.Hoed.Stk.Observe , Debug.Hoed.Stk.Render , Debug.Hoed.Stk.DemoGUI@@ -62,15 +68,16 @@ , template-haskell , array, containers , process- , threepenny-gui == 0.6.*+ , threepenny-gui == 0.6.0.5 , filepath- , libgraph == 1.10+ , libgraph == 1.11 , RBTree == 0.0.5 , regex-posix , mtl , directory , FPretty , cereal, bytestring+ , time default-language: Haskell2010 -- Enable to get some extra warnings. -- ghc-options: -fwarn-unused-binds@@ -87,11 +94,31 @@ -- --------------------------------------------------------------------------- +Executable hoed-examples-Raincat+ if flag(buildExamples)+ build-depends: base >= 3 && < 5,+ containers,+ extensible-exceptions,+ mtl,+ random,+ time,+ GLUT,+ OpenGL,+ SDL,+ SDL-image,+ SDL-mixer,+ Hoed+ else+ buildable: False+ main-is: Main.hs+ hs-source-dirs: examples/Raincat/src+ default-language: Haskell2010+ Executable hoed-examples-FPretty_indents_too_much if flag(buildExamples) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath , containers , deepseq@@ -106,7 +133,7 @@ if flag(buildExamples) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath , containers , deepseq@@ -134,15 +161,31 @@ -- hs-source-dirs: examples/FPretty__with_properties -- default-language: Haskell2010 -Executable hoed-examples-Queens__with_properties+Executable hoed-examples-Stern-Brocot if flag(buildExamples) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath , containers , deepseq , array+ else+ buildable: False+ main-is: SternBrocot.lhs+ hs-source-dirs: examples/+ default-language: Haskell2010++Executable hoed-examples-Queens_v1__with_properties+ -- if flag(buildExamples) ||+ if flag (buildPropExamples)+ build-depends: base >= 4 && < 5+ , Hoed+ , threepenny-gui == 0.6.0.5+ , filepath+ , containers+ , deepseq+ , array , QuickCheck , mtl else@@ -151,11 +194,80 @@ hs-source-dirs: examples/Queens__with_properties default-language: Haskell2010 +Executable hoed-examples-Queens_v2__with_properties+ if flag(buildPropExamples)+ build-depends: base >= 4 && < 5+ , Hoed+ , threepenny-gui == 0.6.0.5+ , filepath+ , containers+ , deepseq+ , array+ , QuickCheck+ , mtl+ else+ buildable: False+ main-is: Main2.hs+ hs-source-dirs: examples/Queens__with_properties+ default-language: Haskell2010++Executable hoed-examples-Queens_v3__with_properties+ if flag(buildPropExamples)+ build-depends: base >= 4 && < 5+ , Hoed+ , threepenny-gui == 0.6.0.5+ , filepath+ , containers+ , deepseq+ , array+ , QuickCheck+ , mtl+ else+ buildable: False+ main-is: Main3.hs+ hs-source-dirs: examples/Queens__with_properties+ default-language: Haskell2010++Executable hoed-examples-Queens_v4_defect_in_filter__with_properties+ if flag(buildPropExamples)+ build-depends: base >= 4 && < 5+ , Hoed+ , threepenny-gui == 0.6.0.5+ , filepath+ , containers+ , deepseq+ , array+ , QuickCheck+ , mtl+ else+ buildable: False+ main-is: Main.hs+ hs-source-dirs: examples/Queens_defective_filter__with_properties+ default-language: Haskell2010++Executable hoed-examples-filter__with_properties+ if flag(buildPropExamples)+ build-depends: base >= 4 && < 5+ , Hoed+ , threepenny-gui == 0.6.0.5+ , filepath+ , containers+ , deepseq+ , array+ , QuickCheck+ , mtl+ else+ buildable: False+ main-is: Main.hs+ hs-source-dirs: examples/filter__with_properties+ default-language: Haskell2010++ Executable hoed-examples-Rot13 if flag(buildExamples) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath else buildable: False@@ -167,7 +279,7 @@ if flag(buildExamples) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath else buildable: False@@ -177,7 +289,7 @@ 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+ build-depends: base >= 4 && < 5, Hoed, threepenny-gui == 0.6.0.5, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions else buildable: False main-is: Main.hs@@ -186,7 +298,7 @@ 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+ build-depends: base >= 4 && < 5, Hoed, threepenny-gui == 0.6.0.5, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions else buildable: False main-is: Main.hs@@ -195,7 +307,7 @@ 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+ build-depends: base >= 4 && < 5, Hoed, threepenny-gui == 0.6.0.5, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions else buildable: False main-is: Main.hs@@ -203,8 +315,8 @@ default-language: Haskell2010 Executable hoed-examples-Nub-defective-sort__with_properties- if flag(buildExamples)- build-depends: base >= 4 && < 5, Hoed, threepenny-gui, filepath, QuickCheck+ if flag(buildPropExamples)+ build-depends: base >= 4 && < 5, Hoed, threepenny-gui == 0.6.0.5, filepath, QuickCheck else buildable: False main-is: Main.hs@@ -215,7 +327,7 @@ if flag(buildExamples) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath else buildable: False@@ -236,6 +348,19 @@ hs-source-dirs: examples/XMonad_changing_focus_duplicates_windows default-language: Haskell2010 +Executable hoed-examples-XMonad_changing_focus_duplicates_windows__test_only+ if flag(buildExamples)+ build-depends: base >= 4 && < 5, Hoed, + X11>=1.5 && < 1.7, mtl, unix,+ utf8-string,+ extensible-exceptions, random,+ containers, filepath, process, directory+ else+ buildable: False+ main-is: Main.hs+ hs-source-dirs: examples/XMonad_changing_focus_duplicates_windows__test_only+ default-language: Haskell2010+ Executable hoed-examples-XMonad_changing_focus_duplicates_windows__CC if flag(buildExamples) build-depends: base >= 4 && < 5, Hoed, @@ -250,7 +375,8 @@ default-language: Haskell2010 Executable hoed-examples-XMonad_changing_focus_duplicates_windows__with_properties- if flag(buildExamples)+ --if flag(buildExamples)+ if flag (buildPropExamples) build-depends: base >= 4 && < 5, Hoed, X11>=1.5 && < 1.7, mtl, unix, utf8-string,@@ -277,7 +403,7 @@ default-language: Haskell2010 Executable hoed-examples-SummerSchool_compiler_does_not_terminate__with_properties- if flag(buildExamples)+ if flag(buildPropExamples) build-depends: base >= 4 && < 5, Hoed, X11>=1.5 && < 1.7, mtl, unix, utf8-string,@@ -291,7 +417,7 @@ default-language: Haskell2010 Executable hoed-examples-CNF_unsound_de_Morgan__with_properties- if flag(buildExamples)+ if flag(buildPropExamples) build-depends: base >= 4 && < 5, Hoed else buildable: False@@ -300,7 +426,7 @@ default-language: Haskell2010 Executable hoed-examples-Digraph_not_data_invariant__with_properties- if flag(buildExamples)+ if flag(buildPropExamples) build-depends: base >= 4 && < 5, Hoed, lazysmallcheck else buildable: False@@ -732,18 +858,19 @@ hs-source-dirs: tests/Prop/t4 default-language: Haskell2010 --- Executable hoed-tests-Prop-t5--- if flag(validateProp)--- build-depends: base >= 4 && < 5, Hoed, --- X11>=1.5 && < 1.7, mtl, unix,--- utf8-string >= 0.3 && < 0.4,--- extensible-exceptions, random,--- containers, filepath, process, directory--- else--- buildable: False--- main-is: Main.hs--- hs-source-dirs: tests/Prop/t5--- default-language: Haskell2010+Executable hoed-tests-Prop-t5+ if flag(validateProp)+ build-depends: base >= 4 && < 5, Hoed, + X11>=1.5 && < 1.7, mtl, unix,+ utf8-string,+ extensible-exceptions, random,+ containers, filepath, process, directory,+ QuickCheck+ else+ buildable: False+ main-is: Main.hs+ hs-source-dirs: tests/Prop/t5+ default-language: Haskell2010 --------------------------------------------------------------------------- -- Validate derivation of Observable and ParEq for Generic types@@ -757,9 +884,9 @@ , template-haskell , array, containers , process- , threepenny-gui == 0.6.*+ , threepenny-gui == 0.6.0.5 , filepath- , libgraph == 1.10+ , libgraph == 1.11 , RBTree == 0.0.5 , regex-posix , mtl@@ -925,7 +1052,7 @@ if flag(validateStk) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath , network else@@ -939,7 +1066,7 @@ if flag(validateStk) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath else buildable: False@@ -952,7 +1079,7 @@ if flag(validateStk) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath else buildable: False@@ -965,7 +1092,7 @@ if flag(validateStk) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath else buildable: False@@ -978,7 +1105,7 @@ if flag(validateStk) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath else buildable: False@@ -991,7 +1118,7 @@ if flag(validateStk) build-depends: base >= 4 && < 5 , Hoed- , threepenny-gui+ , threepenny-gui == 0.6.0.5 , filepath else buildable: False
README.md view
@@ -1,7 +1,11 @@-# Hoed - A Lightweight Haskell Tracer and Debugger [](https://travis-ci.org/MaartenFaddegon/Hoed)+# Hoed - A Lightweight Haskell Tracer and Debugger Hoed is a tracer and debugger for the programming language Haskell. To locate a defect with Hoed you annotate suspected functions and compile as usual. Then you run your program, information about the annotated functions is collected. Finally you connect to a debugging session using a webbrowser. See the [**Project homepage**](http://wiki.haskell.org/Hoed) for more information on what it does and how you can use it to find bugs in your code.++Submit feature requests or contribute code on the++ [**Github projectpage**](https://github.com/MaartenFaddegon/Hoed) [](https://travis-ci.org/MaartenFaddegon/Hoed)
examples/CNF_unsound_demorgan__with_properties/Main.hs view
@@ -4,8 +4,13 @@ main = runOwp properties $ print (prop_negin_correct negin eg) where- properties = [Propositions [ (BoolProposition,cnfModule,"prop_negin_complete",[Argument (-1),Argument 0])- , (BoolProposition,cnfModule,"prop_negin_sound",[Argument (-1),Argument 0])]- Specify "negin" []+ properties = [Propositions + [ mkProposition cnfModule "prop_negin_complete"+ `ofType` BoolProposition+ `withSignature` [SubjectFunction,Argument 0]+ , mkProposition cnfModule "prop_negin_sound"+ `ofType` BoolProposition+ `withSignature` [SubjectFunction,Argument 0]+ ] Specify "negin" [] ] cnfModule = Module "CNF" "../examples/CNF_unsound_demorgan__with_properties/"
examples/Digraph_not_data_invariant__with_properties/Main.hs view
@@ -4,11 +4,11 @@ main = runOwp properties $ print (prop_assoc1toNdigraph eg) where- properties = [ Propositions [(BoolProposition,digraphModule,"prop_assoc1toNdigraph",[Argument 0])]+ properties = [ Propositions [mkProposition digraphModule "prop_assoc1toNdigraph" `ofType` BoolProposition `withSignature` [Argument 0]] Specify "assoc1toNdigraph" []- , Propositions [(BoolProposition,digraphModule,"prop_mergeAndSortTargets",[Argument 0])]+ , Propositions [mkProposition digraphModule "prop_mergeAndSortTargets" `ofType` BoolProposition `withSignature` [Argument 0]] Specify "mergeAndSortTargets" []- , Propositions [(BoolProposition,digraphModule,"prop_addMissingSources",[Argument 0])]+ , Propositions [mkProposition digraphModule "prop_addMissingSources" `ofType` BoolProposition `withSignature` [Argument 0]] Specify "addMissingSources" [] ] digraphModule = Module "Digraph" "../examples/Digraph_not_data_invariant__with_properties/"
examples/ExpressionSimplifier/Main2.hs view
@@ -6,8 +6,11 @@ -- main = quickcheck prop_idemSimplify main = testOwp properties prop_idemSimplify (Mul (Const 1) (Const 2)) where- properties = [ Propositions [(BoolProposition,myModule,"prop_idemOne",[Argument 0])] PropertiesOf "one" []- , Propositions [(BoolProposition,myModule,"prop_idemZero",[Argument 0])] PropertiesOf "zero" []- , Propositions [(BoolProposition,myModule,"prop_idemSimplify",[Argument 0])] PropertiesOf "simplify" []+ properties = [ Propositions [mkProposition myModule "prop_idemOne" `ofType` BoolProposition `withSignature` [Argument 0]+ ] PropertiesOf "one" []+ , Propositions [ mkProposition myModule "prop_idemZero" `ofType` BoolProposition `withSignature` [Argument 0]+ ] PropertiesOf "zero" []+ , Propositions [ mkProposition myModule "prop_idemSimplify" `ofType` BoolProposition `withSignature` [Argument 0]+ ] PropertiesOf "simplify" [] ] myModule = Module "MyModule" "../examples/ExpressionSimplifier"
examples/Nubsort/Main.hs view
@@ -3,16 +3,32 @@ main = testOwp ps prop_nub_idempotent [2,1,1] where- ps = [ Propositions [ (BoolProposition,nubsortModule,"prop_nub_idempotent",[Argument 0])- , (BoolProposition,nubsortModule,"prop_nub_unique",[Argument 0])- , (BoolProposition,nubsortModule,"prop_nub_complete",[Argument 0])+ ps = [ Propositions [ mkProposition nubsortModule "prop_nub_idempotent" + `ofType` BoolProposition + `withSignature`[Argument 0]+ , mkProposition nubsortModule "prop_nub_unique"+ `ofType` BoolProposition + `withSignature`[Argument 0]+ , mkProposition nubsortModule "prop_nub_complete"+ `ofType` BoolProposition + `withSignature`[Argument 0] ] PropertiesOf "nub" []- , Propositions [ (QuickCheckProposition,nubsortModule,"prop_nubord'_idempotent",[Argument 1,Argument 0])- , (QuickCheckProposition,nubsortModule,"prop_nubord'_unique",[Argument 1,Argument 0])- , (QuickCheckProposition,nubsortModule,"prop_nubord'_complete",[Argument 1,Argument 0])+ , Propositions [ mkProposition nubsortModule "prop_nubord'_idempotent"+ `ofType` QuickCheckProposition+ `withSignature`[Argument 1, Argument 0]+ , mkProposition nubsortModule "prop_nubord'_unique"+ `ofType` QuickCheckProposition+ `withSignature`[Argument 1, Argument 0]+ , mkProposition nubsortModule "prop_nubord'_complete"+ `ofType` QuickCheckProposition+ `withSignature`[Argument 1, Argument 0] ] PropertiesOf "nubord'" [modQuickCheck]- , Propositions [ (QuickCheckProposition,nubsortModule,"prop_insert_ordered",[Argument 1,Argument 0])- , (QuickCheckProposition,nubsortModule,"prop_insert_complete",[Argument 1,Argument 0])+ , Propositions [ mkProposition nubsortModule "prop_insert_ordered"+ `ofType` QuickCheckProposition+ `withSignature`[Argument 1, Argument 0]+ , mkProposition nubsortModule "prop_insert_complete"+ `ofType` QuickCheckProposition+ `withSignature`[Argument 1, Argument 0] ] PropertiesOf "insert" [modQuickCheck] ] nubsortModule = Module "Nubsort" "../examples/Nubsort/"
+ examples/Queens__with_properties/Main2.hs view
@@ -0,0 +1,3 @@+import Queens++main = doit2
+ examples/Queens__with_properties/Main3.hs view
@@ -0,0 +1,3 @@+import Queens3++main = doit
+ examples/Queens_defective_filter__with_properties/Main.hs view
@@ -0,0 +1,3 @@+import Queens++main = doit
+ examples/Raincat/src/Main.hs view
@@ -0,0 +1,30 @@+module Main (main) where++import Graphics.UI.GLUT+import System.Exit+import Game.GameInput+import Game.GameInit+import World.World+import Settings.DisplaySettings as DisplaySettings+import qualified Nxt.Graphics as NG+import Data.IORef+import Program.Program+import Debug.Hoed.Pure++main :: IO ()+main = runO $ do+ NG.initWindow screenRes "Raincat"+ NG.initGraphics screenResWidth screenResHeight++ worldState <- gameInit+ worldStateRef <- newIORef worldState++ displayCallback $= programDraw worldStateRef++ keyboardMouseCallback $= Just (gameInput (keysStateRef worldState))+ motionCallback $= Just (gameMotion (mousePosRef worldState))+ passiveMotionCallback $= Just (gameMotion (mousePosRef worldState))++ addTimerCallback 1 (programMain worldStateRef)++ mainLoop
+ examples/SternBrocot.lhs view
@@ -0,0 +1,97 @@+We need the Template Haskell extension to splice in the generated+Observable instances. We need the Rank2Types extionsion to be able+to specify parametrized types such as 'Tree a' with forall a.++> {-# LANGUAGE TemplateHaskell, Rank2Types #-}++We need the Derive Generic extention to derive the Generic representation+used for the non spliced in observe (see the Cache data type).++> {-# LANGUAGE DeriveGeneric #-}++> import Debug.Hoed.Pure++We use the Stern–Brocot tree as example. The Stern-Brocot tree is a+binary tree containing all rational numbers. The tree is infinit and+is therefore a nice example to demonstrate how laziness is handled.++To store the tree we use the following datatype, note that because+our definition is endless we do not actually use Leaf.++> data Tree a = Node a (Tree a) (Tree a) deriving Generic++The values in the tree will be fractional numbers:++> data Frac = Frac Int Int deriving (Show,Generic)++We use cache to store what the last seen up and to the left, and up and+to the right values are.++> data Cache = Cache { v :: Frac+> , l :: Frac+> , r :: Frac+> } deriving Generic++Make Cache and Frac Observable for gdmobserve.++> instance Observable Cache+> instance Observable Frac++The mediant is used to find which new number to insert between 2 exisiting+numbers.++> mediant :: Frac -> Frac -> Frac+> mediant (Frac p1 q1) (Frac p2 q2) = Frac (p1+p2) (q1+q2)++Definition of the sternbrocot tree:++> sternbrocot :: Tree Frac+> sternbrocot = sternbrocot' mediant+>+> sternbrocot' :: (Frac -> Frac -> Frac) -> Tree Frac+> sternbrocot' m = w_sternbrocot m Cache{v=(Frac 1 1), l=(Frac 0 1), r=(Frac 1 0)}+>+> w_sternbrocot :: (Frac -> Frac -> Frac) -> Cache -> Tree Frac+> w_sternbrocot m cache+> = let Cache{v=v, l=l, r=r} = cache -- observe "cache" cache+> in Node v (w_sternbrocot m Cache{v=m v l, l=l, r=v})+> (w_sternbrocot m Cache{v=m v r, l=v, r=r})++The Stern-Brocot tree is sorted: all values in the left subtree are+smaller than the value of the current node and all values in the right subtree+are greater than the value in the current node.+This can be used to approximate a Float value by doing a binary search where+each next rational number is a better aproximation of the Float.++> toFrac :: Float -> Tree Frac -> Frac+> toFrac val (Node frac@(Frac p q) left right)+> = case compare ((fromIntegral p) / (fromIntegral q)) val of+> LT -> toFrac val right +> GT -> toFrac val left+> EQ -> frac++We use template-haskell to observe Tree and the values stored in Tree.++> $(observedTypes "sternbrocot1" [ [t| forall a . Observable a => Tree a |]+> , [t| Frac |]+> ]+> )+>+> frac1 = toFrac 0.6 ($(observeTempl "sternbrocot1") sternbrocot)++Or to only observe which part of the tree is walked while ignoring+the values stored in the tree.++> $(observedTypes "sternbrocot2" [ [t| forall a . Tree a |]])+>+> frac2 = toFrac 0.6 ($(observeTempl "sternbrocot2") sternbrocot)++> instance (Observable a) => Observable (Tree a)+>+> frac3 = toFrac 0.6 (observe "sternbrocot3" sternbrocot)++Example main function:++> main = runO $ do -- print frac1+> -- print frac2+> print frac3
+ examples/XMonad_changing_focus_duplicates_windows__test_only/Main.hs view
@@ -0,0 +1,171 @@+import Properties+import Debug.Hoed.NoTrace+import System.Environment+import Text.Printf+import Control.Monad+import System.Random+import Test.QuickCheck+import Data.Maybe+import XMonad.StackSet+import qualified Data.Map as M++myStackSet :: T+myStackSet = StackSet {current = Screen {workspace = Workspace {tag = NonNegative 2, layout = -2, stack = Just (Stack {focus = 'c', up = "", down = "z"})}, screen = 2, screenDetail = 1}, visible = [Screen {workspace = Workspace {tag = NonNegative 0, layout = -2, stack = Just (Stack {focus = 'd', up = "", down = ""})}, screen = 1, screenDetail = -2},Screen {workspace = Workspace {tag = NonNegative 3, layout = -2, stack = Just (Stack {focus = 'v', up = "", down = ""})}, screen = 3, screenDetail = -1},Screen {workspace = Workspace {tag = NonNegative 4, layout = -2, stack = Just (Stack {focus = 'w', up = "", down = "i"})}, screen = 0, screenDetail = -2}], hidden = [Workspace {tag = NonNegative 1, layout = -2, stack = Just (Stack {focus = 'n', up = "", down = ""})},Workspace {tag = NonNegative 0, layout = -2, stack = Nothing},Workspace {tag = NonNegative 4, layout = -2, stack = Nothing}], floating = M.fromList []}++++main = do+ args <- fmap (drop 1) getArgs+ let n = if null args then 100 else read (head args)+ (results, passed) <- liftM unzip $ mapM (\(s,a) -> printf "%-40s: " s >> a n) tests+ printf "Passed %d tests!\n" (sum passed)+ when (not . and $ results) $ fail "Not all tests passed!"++ where++ tests = zipWith (\(name,test) number -> (show number ++ ": " ++ name,test)) tests' [1..]++ tests' =+ [("prop_invariant" , mytest prop_invariant)++ ,("prop_empty_I" , mytest prop_empty_I)+ ,("prop_empty" , mytest prop_empty)+ ,("prop_empty_current" , mytest prop_empty_current)+ ,("prop_member_empty" , mytest prop_member_empty)++ ,("prop_view_I" , mytest prop_view_I)+ ,("prop_view_current" , mytest prop_view_current)+ ,("prop_view_idem" , mytest prop_view_idem)+ ,("prop_view_reversible" , mytest prop_view_reversible)+ ,("prop_view_local" , mytest prop_view_local)++ ,("prop_view_greedyView_I" , mytest prop_greedyView_I)+ ,("prop_greedyView_current" , mytest prop_greedyView_current)+ ,("prop_greedyView_current_id" , mytest prop_greedyView_current_id)+ ,("prop_greedyView_idem" , mytest prop_greedyView_idem)+ ,("prop_greedyView_reversible" , mytest prop_greedyView_reversible)+ ,("prop_greedyView_local" , mytest prop_greedyView_local)++ ,("prop_member_peek" , mytest prop_member_peek)++ ,("prop_index_length" , mytest prop_index_length)++ ,("prop_focusUp_I", mytest prop_focusUp_I)+ ,("prop_focusMaster_I", mytest prop_focusMaster_I)+ ,("prop_focusDown_I", mytest prop_focusDown_I)+ ,("prop_focus_I", mytest prop_focus_I)+ ,("prop_focus_left_master" , mytest prop_focus_left_master)+ ,("prop_focus_right_master" , mytest prop_focus_right_master)+ ,("prop_focus_master_master" , mytest prop_focus_master_master)+ ,("prop_focusWindow_master" , mytest prop_focusWindow_master)+ ,("prop_focus_left" , mytest prop_focus_left)+ ,("prop_focus_right" , mytest prop_focus_right)+ ,("prop_focus_all_l" , mytest prop_focus_all_l)+ ,("prop_focus_all_r" , mytest prop_focus_all_r)+ ,("prop_focus_down_local" , mytest prop_focus_down_local)+ ,("prop_focus_up_local" , mytest prop_focus_up_local)+ ,("prop_focus_master_local" , mytest prop_focus_master_local)+ ,("prop_focusMaster_idem" , mytest prop_focusMaster_idem)++ ,("prop_focusWindow_local", mytest prop_focusWindow_local)+ ,("prop_focusWindow_works" , mytest prop_focusWindow_works)+ ,("prop_focusWindow_identity", mytest prop_focusWindow_identity)++ ,("prop_findIndex" , mytest prop_findIndex)+ ,("prop_allWindowsMember" , mytest prop_allWindowsMember)+ ,("prop_currentTag" , mytest prop_currentTag)++ ,("prop_insertUp_I" , mytest prop_insertUp_I)+ ,("prop_insert_empty/new" , mytest prop_insert_empty)+ ,("prop_insert_idem", mytest prop_insert_idem)+ ,("prop_insert_delete", mytest prop_insert_delete)+ ,("prop_insert_local" , mytest prop_insert_local)+ ,("prop_insert_duplicate" , mytest prop_insert_duplicate)+ ,("prop_insert_peek" , mytest prop_insert_peek)+ ,("prop_size_insert" , mytest prop_size_insert)++ ,("prop_delete_I" , mytest prop_delete_I)+ ,("prop_empty" , mytest prop_empty)+ ,("prop_delete" , mytest prop_delete)+ ,("prop_delete_insert", mytest prop_delete_insert)+ ,("prop_delete_local" , mytest prop_delete_local)+ ,("prop_delete_focus" , mytest prop_delete_focus)+ ,("prop_delete_focus_end", mytest prop_delete_focus_end)+ ,("prop_delete_focus_not_end", mytest prop_delete_focus_not_end)++ ,("prop_filter_order", mytest prop_filter_order)++ ,("prop_swap_master_I", mytest prop_swap_master_I)+ ,("prop_swap_left_I" , mytest prop_swap_left_I)+ ,("prop_swap_right_I", mytest prop_swap_right_I)+ ,("prop_swap_master_focus", mytest prop_swap_master_focus)+ ,("prop_swap_left_focus", mytest prop_swap_left_focus)+ ,("prop_swap_right_focus", mytest prop_swap_right_focus)+ ,("prop_swap_master_idempotent", mytest prop_swap_master_idempotent)+ ,("prop_swap_all_l" , mytest prop_swap_all_l)+ ,("prop_swap_all_r" , mytest prop_swap_all_r)+ ,("prop_swap_master_local" , mytest prop_swap_master_local)+ ,("prop_swap_left_local" , mytest prop_swap_left_local)+ ,("prop_swap_right_local" , mytest prop_swap_right_local)++ ,("prop_shift_master_focus", mytest prop_shift_master_focus)+ ,("prop_shift_master_local", mytest prop_shift_master_local)+ ,("prop_shift_master_idempotent", mytest prop_shift_master_idempotent)+ ,("prop_shift_master_ordering", mytest prop_shift_master_ordering)++ ,("prop_shift_I" , mytest prop_shift_I)+ ,("prop_shift_reversible" , mytest prop_shift_reversible)+ ,("prop_shift_win_I" , mytest prop_shift_win_I)+ ,("prop_shift_win_focus" , mytest prop_shift_win_focus)+ ,("prop_shift_win_fix_current" , mytest prop_shift_win_fix_current)++ ,("prop_float_reversible" , mytest prop_float_reversible)+ ,("prop_float_geometry" , mytest prop_float_geometry)+ ,("prop_float_delete", mytest prop_float_delete)+ ,("prop_screens", mytest prop_screens)++ ,("prop_differentiate", mytest prop_differentiate)+ ,("prop_lookup_current", mytest prop_lookup_current)+ ,("prop_lookup_visible", mytest prop_lookup_visible)+ ,("prop_screens_works", mytest prop_screens_works)+ ,("prop_rename1", mytest prop_rename1)+ ,("prop_ensure", mytest prop_ensure)+ ,("prop_ensure_append", mytest prop_ensure_append)++ ,("prop_mapWorkspaceId", mytest prop_mapWorkspaceId)+ ,("prop_mapWorkspaceInverse", mytest prop_mapWorkspaceInverse)+ ,("prop_mapLayoutId", mytest prop_mapLayoutId)+ ,("prop_mapLayoutInverse", mytest prop_mapLayoutInverse)++ -- testing for failure:+ ,("prop_abort", mytest prop_abort)+ ,("prop_new_abort", mytest prop_new_abort)+ ,("prop_shift_win_indentity", mytest prop_shift_win_indentity)++ -- tall layout++ ,("prop_tile_fullscreen", mytest prop_tile_fullscreen)+ ,("prop_tile_non_overlap", mytest prop_tile_non_overlap)+ ,("prop_split_hoziontal", mytest prop_split_hoziontal)+ ,("prop_splitVertically", mytest prop_splitVertically)++ ,("prop_purelayout_tall", mytest prop_purelayout_tall)+ ,("prop_shrink_tall", mytest prop_shrink_tall)+ ,("prop_expand_tall", mytest prop_expand_tall)+ ,("prop_incmaster_tall", mytest prop_incmaster_tall)++ -- full layout++ ,("prop_purelayout_full", mytest prop_purelayout_full)+ ,("prop_sendmsg_full", mytest prop_sendmsg_full)+ ,("prop_desc_full", mytest prop_desc_full)++ ,("prop_desc_mirror", mytest prop_desc_mirror)++ -- resize hints+ ,("prop_resize_inc", mytest prop_resize_inc)+ ,("prop_resize_inc_extra", mytest prop_resize_inc_extra)+ ,("prop_resize_max", mytest prop_resize_max)+ ,("prop_resize_max_extra", mytest prop_resize_max_extra)++ ]
examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs view
@@ -13,213 +13,81 @@ myStackSet = StackSet {current = Screen {workspace = Workspace {tag = NonNegative 2, layout = -2, stack = Just (Stack {focus = 'c', up = "", down = "z"})}, screen = 2, screenDetail = 1}, visible = [Screen {workspace = Workspace {tag = NonNegative 0, layout = -2, stack = Just (Stack {focus = 'd', up = "", down = ""})}, screen = 1, screenDetail = -2},Screen {workspace = Workspace {tag = NonNegative 3, layout = -2, stack = Just (Stack {focus = 'v', up = "", down = ""})}, screen = 3, screenDetail = -1},Screen {workspace = Workspace {tag = NonNegative 4, layout = -2, stack = Just (Stack {focus = 'w', up = "", down = "i"})}, screen = 0, screenDetail = -2}], hidden = [Workspace {tag = NonNegative 1, layout = -2, stack = Just (Stack {focus = 'n', up = "", down = ""})},Workspace {tag = NonNegative 0, layout = -2, stack = Nothing},Workspace {tag = NonNegative 4, layout = -2, stack = Nothing}], floating = M.fromList []} --{- Running all tests-main = do- args <- fmap (drop 1) getArgs- let n = if null args then 100 else read (head args)- (results, passed) <- liftM unzip $ mapM (\(s,a) -> printf "%-40s: " s >> a n) tests- printf "Passed %d tests!\n" (sum passed)- when (not . and $ results) $ fail "Not all tests passed!"--}- main :: IO () main = runOwp propositions $ do g <- newStdGen- print . fromJust . ok . (generate 1 g) . evaluate $ prop_shift_win_I 1 'd' myStackSet+ print . fromJust . ok . (generate 1 g) . evaluate $ prop_shift_win_I shiftWin 1 'd' myStackSet where propositions =- [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[Argument 0])- ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[Argument 0])+ [ Propositions [mkProposition module_Properties "prop_shift_win_I"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [SubjectFunction, Argument 0, Argument 1, Argument 2]+ `withTestGen` TestGenLegacyQuickCheck+ ]+ PropertiesOf "shiftWin" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]+ , Propositions [mkProposition module_Properties "prop_focus_all_l"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0]+ `withTestGen` TestGenLegacyQuickCheck+ ,mkProposition module_Properties "prop_focus_all_l_weak"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0]+ `withTestGen` TestGenLegacyQuickCheck ] PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[Argument 1,Argument 0])+ , Propositions [ mkProposition module_Properties "prop_insert_duplicate_weak"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0, Argument 1]+ `withTestGen` TestGenLegacyQuickCheck ] PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[Argument 1,Argument 0])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[Argument 1,Argument 0])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[Argument 0,Argument 1])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[Argument 0,Argument 1])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[Argument 0,Argument 1])+ , Propositions [ mkProposition module_Properties "prop_view_reversible"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0, Argument 1]+ `withTestGen` TestGenLegacyQuickCheck+ , mkProposition module_Properties "prop_view_I"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [SubjectFunction, Argument 0, Argument 1]+ `withTestGen` TestGenLegacyQuickCheck+ , mkProposition module_Properties "prop_view_current"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ `withTestGen` TestGenLegacyQuickCheck+ , mkProposition module_Properties "prop_view_idem"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ `withTestGen` TestGenLegacyQuickCheck+ , mkProposition module_Properties "prop_view_local"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ `withTestGen` TestGenLegacyQuickCheck ] PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[Argument 1,Argument 0])- , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[Argument 0,Argument 1])+ , Propositions [ mkProposition module_Properties "prop_greedyView_reversible"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0, Argument 1]+ `withTestGen` TestGenLegacyQuickCheck+ , mkProposition module_Properties "prop_greedyView_idem"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ `withTestGen` TestGenLegacyQuickCheck ] PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]+ , Propositions [ mkProposition module_Properties "prop_findIndex"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1]+ `withTestGen` TestGenLegacyQuickCheck+ ]+ PropertiesOf "findTag" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] ] - module_Properties = Module "Properties" "../examples/XMonad_changing_focus_duplicates_windows/"- module_StackSet = Module "XMonad.StackSet" "../examples/XMonad_changing_focus_duplicates_windows/"- module_QuickCheck = Module "Test.QuickCheck" "../examples/XMonad_changing_focus_duplicates_windows/"+ module_Properties = Module "Properties" "../examples/XMonad_changing_focus_duplicates_windows__using_properties/"+ module_StackSet = Module "XMonad.StackSet" "../examples/XMonad_changing_focus_duplicates_windows__using_properties/"+ module_QuickCheck = Module "Test.QuickCheck" "../examples/XMonad_changing_focus_duplicates_windows__using_properties/" module_Map = Module "qualified Data.Map as M" "" module_Random = Module "System.Random" "" module_Maybe = Module "Data.Maybe" ""-- tests =- [("shiftMaster id on focus", mytest prop_shift_master_focus)- -- ,("shiftMaster is local", mytest prop_shift_master_local)- -- ,("shiftMaster is idempotent", mytest prop_shift_master_idempotent)- -- ,("shiftMaster preserves ordering", mytest prop_shift_master_ordering)-- -- ,("shift: invariant" , mytest prop_shift_I)- -- ,("shift is reversible" , mytest prop_shift_reversible)- ,("shiftWin: invariant" , mytest prop_shift_win_I)- ,("shiftWin is shift on focus" , mytest prop_shift_win_focus)- ,("shiftWin fix current" , mytest prop_shift_win_fix_current)- ]--{-- [("StackSet invariants" , mytest prop_invariant)-- ,("empty: invariant" , mytest prop_empty_I)- ,("empty is empty" , mytest prop_empty)- ,("empty / current" , mytest prop_empty_current)- ,("empty / member" , mytest prop_member_empty)-- ,("view : invariant" , mytest prop_view_I)- ,("view sets current" , mytest prop_view_current)- ,("view idempotent" , mytest prop_view_idem)- ,("view reversible" , mytest prop_view_reversible)--- ,("view / xinerama" , mytest prop_view_xinerama)- ,("view is local" , mytest prop_view_local)-- ,("greedyView : invariant" , mytest prop_greedyView_I)- ,("greedyView sets current" , mytest prop_greedyView_current)- ,("greedyView is safe " , mytest prop_greedyView_current_id)- ,("greedyView idempotent" , mytest prop_greedyView_idem)- ,("greedyView reversible" , mytest prop_greedyView_reversible)- ,("greedyView is local" , mytest prop_greedyView_local)------ ,("valid workspace xinerama", mytest prop_lookupWorkspace)-- ,("peek/member " , mytest prop_member_peek)-- ,("index/length" , mytest prop_index_length)-- ,("focus left : invariant", mytest prop_focusUp_I)- ,("focus master : invariant", mytest prop_focusMaster_I)- ,("focus right: invariant", mytest prop_focusDown_I)- ,("focusWindow: invariant", mytest prop_focus_I)- ,("focus left/master" , mytest prop_focus_left_master)- ,("focus right/master" , mytest prop_focus_right_master)- ,("focus master/master" , mytest prop_focus_master_master)- ,("focusWindow master" , mytest prop_focusWindow_master)- ,("focus left/right" , mytest prop_focus_left)- ,("focus right/left" , mytest prop_focus_right)- ,("focus all left " , mytest prop_focus_all_l)- ,("focus all right " , mytest prop_focus_all_r)- ,("focus down is local" , mytest prop_focus_down_local)- ,("focus up is local" , mytest prop_focus_up_local)- ,("focus master is local" , mytest prop_focus_master_local)- ,("focus master idemp" , mytest prop_focusMaster_idem)-- ,("focusWindow is local", mytest prop_focusWindow_local)- ,("focusWindow works" , mytest prop_focusWindow_works)- ,("focusWindow identity", mytest prop_focusWindow_identity)-- ,("findTag" , mytest prop_findIndex)- ,("allWindows/member" , mytest prop_allWindowsMember)- ,("currentTag" , mytest prop_currentTag)-- ,("insert: invariant" , mytest prop_insertUp_I)- ,("insert/new" , mytest prop_insert_empty)- ,("insert is idempotent", mytest prop_insert_idem)- ,("insert is reversible", mytest prop_insert_delete)- ,("insert is local" , mytest prop_insert_local)- ,("insert duplicates" , mytest prop_insert_duplicate)- ,("insert/peek " , mytest prop_insert_peek)- ,("insert/size" , mytest prop_size_insert)-- ,("delete: invariant" , mytest prop_delete_I)- ,("delete/empty" , mytest prop_empty)- ,("delete/member" , mytest prop_delete)- ,("delete is reversible", mytest prop_delete_insert)- ,("delete is local" , mytest prop_delete_local)- ,("delete/focus" , mytest prop_delete_focus)- ,("delete last/focus up", mytest prop_delete_focus_end)- ,("delete ~last/focus down", mytest prop_delete_focus_not_end)-- ,("filter preserves order", mytest prop_filter_order)-- ,("swapMaster: invariant", mytest prop_swap_master_I)- ,("swapUp: invariant" , mytest prop_swap_left_I)- ,("swapDown: invariant", mytest prop_swap_right_I)- ,("swapMaster id on focus", mytest prop_swap_master_focus)- ,("swapUp id on focus", mytest prop_swap_left_focus)- ,("swapDown id on focus", mytest prop_swap_right_focus)- ,("swapMaster is idempotent", mytest prop_swap_master_idempotent)- ,("swap all left " , mytest prop_swap_all_l)- ,("swap all right " , mytest prop_swap_all_r)- ,("swapMaster is local" , mytest prop_swap_master_local)- ,("swapUp is local" , mytest prop_swap_left_local)- ,("swapDown is local" , mytest prop_swap_right_local)-- ,("shiftMaster id on focus", mytest prop_shift_master_focus)- ,("shiftMaster is local", mytest prop_shift_master_local)- ,("shiftMaster is idempotent", mytest prop_shift_master_idempotent)- ,("shiftMaster preserves ordering", mytest prop_shift_master_ordering)-- ,("shift: invariant" , mytest prop_shift_I)- ,("shift is reversible" , mytest prop_shift_reversible)- ,("shiftWin: invariant" , mytest prop_shift_win_I)- ,("shiftWin is shift on focus" , mytest prop_shift_win_focus)- ,("shiftWin fix current" , mytest prop_shift_win_fix_current)-- ,("floating is reversible" , mytest prop_float_reversible)- ,("floating sets geometry" , mytest prop_float_geometry)- ,("floats can be deleted", mytest prop_float_delete)- ,("screens includes current", mytest prop_screens)-- ,("differentiate works", mytest prop_differentiate)- ,("lookupTagOnScreen", mytest prop_lookup_current)- ,("lookupTagOnVisbleScreen", mytest prop_lookup_visible)- ,("screens works", mytest prop_screens_works)- ,("renaming works", mytest prop_rename1)- ,("ensure works", mytest prop_ensure)- ,("ensure hidden semantics", mytest prop_ensure_append)-- ,("mapWorkspace id", mytest prop_mapWorkspaceId)- ,("mapWorkspace inverse", mytest prop_mapWorkspaceInverse)- ,("mapLayout id", mytest prop_mapLayoutId)- ,("mapLayout inverse", mytest prop_mapLayoutInverse)-- -- testing for failure:- ,("abort fails", mytest prop_abort)- ,("new fails with abort", mytest prop_new_abort)- ,("shiftWin identity", mytest prop_shift_win_indentity)-- -- tall layout-- ,("tile 1 window fullsize", mytest prop_tile_fullscreen)- ,("tiles never overlap", mytest prop_tile_non_overlap)- ,("split hozizontally", mytest prop_split_hoziontal)- ,("split verticalBy", mytest prop_splitVertically)-- ,("pure layout tall", mytest prop_purelayout_tall)- ,("send shrink tall", mytest prop_shrink_tall)- ,("send expand tall", mytest prop_expand_tall)- ,("send incmaster tall", mytest prop_incmaster_tall)-- -- full layout-- ,("pure layout full", mytest prop_purelayout_full)- ,("send message full", mytest prop_sendmsg_full)- ,("describe full", mytest prop_desc_full)-- ,("describe mirror", mytest prop_desc_mirror)-- -- resize hints- ,("window hints: inc", mytest prop_resize_inc)- ,("window hints: inc all", mytest prop_resize_inc_extra)- ,("window hints: max", mytest prop_resize_max)- ,("window hints: max all ", mytest prop_resize_max_extra)-- ]--}--
examples/afp02Exercises/Compiler__with_properties/Main.hs view
@@ -14,7 +14,10 @@ putStrLn "compiled:" print (exec (compile prog)) where- properties = [Propositions [(BoolProposition,modInterpreter,"prop_ifT",[Argument 1,Argument 0])] PropertiesOf "run" [modSyntax,modValue,modQuickCheck]+ properties = [Propositions [mkProposition modInterpreter "prop_ifT"+ `ofType` BoolProposition + `withSignature`[Argument 1, Argument 0]+ ]PropertiesOf "run" [modSyntax,modValue,modQuickCheck] ] modInterpreter = Module "Interpreter" "../examples/afp02Exercises/Compiler__with_properties/" modValue = Module "Value" "../examples/afp02Exercises/Compiler__with_properties/"
+ examples/filter__with_properties/Main.hs view
@@ -0,0 +1,3 @@+import Even++main = doit
+ img/test.png view
binary file changed (absent → 3876 bytes)
run view
@@ -42,6 +42,9 @@ # else # ../dist/build/$EXE/$EXE +RTS -p -h -L80 # fi+ eval ../dist/build/$EXE/$EXE +# profile ....+#../dist/build/$EXE/$EXE +RTS -hd -L80
test.Generic view
@@ -3,12 +3,11 @@ TESTS="0 1 2 3" FAIL=0 -+echo 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@@ -19,7 +18,7 @@ fi echo "] Generic.ParEq" -+echo echo "Testing events produced for Observable derived for Generic types" echo
tests/Prop/t0/Main.hs view
@@ -6,8 +6,14 @@ -- main = quickcheck prop_idemSimplify main = logOwp Bottom "hoed-tests-Prop-t0.graph" properties $ print $ prop_idemSimplify (Mul (Const 1) (Const 2)) where- properties = [ Propositions [(BoolProposition,myModule,"prop_idemOne",[Argument 0])] PropertiesOf "one" []- , Propositions [(BoolProposition,myModule,"prop_idemZero",[Argument 0])] PropertiesOf "zero" []- , Propositions [(BoolProposition,myModule,"prop_idemSimplify",[Argument 0])] PropertiesOf "simplify" []+ properties = [ Propositions [mkProposition myModule "prop_idemOne"+ `ofType` BoolProposition+ `withSignature` [Argument 0]] PropertiesOf "one" []+ , Propositions [mkProposition myModule "prop_idemZero"+ `ofType` BoolProposition+ `withSignature` [Argument 0]] PropertiesOf "zero" []+ , Propositions [mkProposition myModule "prop_idemSimplify"+ `ofType` BoolProposition+ `withSignature` [Argument 0]] PropertiesOf "simplify" [] ] myModule = Module "MyModule" "../Prop/t0/"
tests/Prop/t1/Main.hs view
@@ -6,6 +6,11 @@ main = logOwp Bottom "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",[Argument 0]), (BoolProposition,cnfModule,"prop_negin_sound",[Argument 0])] Specify "negin" []+ properties = [Propositions + [ mkProposition cnfModule "prop_negin_complete"+ `ofType` BoolProposition `withSignature` [Argument 0]+ , mkProposition cnfModule "prop_negin_sound"+ `ofType` BoolProposition `withSignature` [Argument 0]+ ] Specify "negin" [] ] cnfModule = Module "CNF" "../Prop/t1/"
tests/Prop/t2/Main.hs view
@@ -5,8 +5,11 @@ -- main = quickcheck prop_idem_negin_sound main = logOwp Bottom "hoed-tests-Prop-t2.graph" properties $ print (prop_assoc1toNdigraph eg) where- properties = [ Propositions [(BoolProposition,digraphModule,"prop_assoc1toNdigraph",[Argument 0])] Specify "assoc1toNdigraph" []- , Propositions [(BoolProposition,digraphModule,"prop_mergeAndSortTargets",[Argument 0])] Specify "mergeAndSortTargets" []- , Propositions [(BoolProposition,digraphModule,"prop_addMissingSources",[Argument 0])] Specify "addMissingSources" []+ properties = [ Propositions [mkProposition digraphModule "prop_assoc1toNdigraph" + `ofType` BoolProposition `withSignature` [Argument 0]] Specify "assoc1toNdigraph" []+ , Propositions [mkProposition digraphModule "prop_mergeAndSortTargets"+ `ofType` BoolProposition `withSignature` [Argument 0]] Specify "mergeAndSortTargets" []+ , Propositions [mkProposition digraphModule "prop_addMissingSources" + `ofType` BoolProposition `withSignature` [Argument 0]] Specify "addMissingSources" [] ] digraphModule = Module "Digraph" "../Prop/t2/"
tests/Prop/t3/Main.hs view
@@ -39,21 +39,45 @@ where propositions =- [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[Argument 0])- ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_generic",[Argument 0])- -- ,(QuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0])+ [Propositions [mkProposition module_Properties "prop_focus_all_l"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0]+ ,mkProposition module_Properties "prop_focus_all_l_weak"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0] ] PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[Argument 1,Argument 0])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[Argument 1,Argument 0])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[Argument 0,Argument 1])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[Argument 0,Argument 1])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[Argument 0,Argument 1])+ , Propositions [ mkProposition module_Properties "prop_insert_duplicate_weak"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0] ] + PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]++ , Propositions [ mkProposition module_Properties "prop_view_reversible"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ , mkProposition module_Properties "prop_view_I"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ , mkProposition module_Properties "prop_view_current"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ , mkProposition module_Properties "prop_view_idem"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0, Argument 1]+ , mkProposition module_Properties "prop_view_local"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0, Argument 1]+ ] PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]- , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[Argument 1,Argument 0])- , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[Argument 0,Argument 1])++ , Propositions [ mkProposition module_Properties "prop_greedyView_reversible"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ , mkProposition module_Properties "prop_greedyView_idem"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0, Argument 1] ] PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
tests/Prop/t4/Main.hs view
@@ -29,25 +29,45 @@ print . fromJust . ok . (generate 1 g) . evaluate $ prop_shift_win_I 1 'd' myStackSet where propositions =- [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[Argument 0])- -- ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0])+ [Propositions [mkProposition module_Properties "prop_focus_all_l"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0]+ ,mkProposition module_Properties "prop_focus_all_l_weak"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0] ] PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - -- , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[1,0])- -- ] - -- PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]+ , Propositions [ mkProposition module_Properties "prop_insert_duplicate_weak"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ ] + PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[Argument 0,Argument 1])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[Argument 0,Argument 1])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[Argument 1,Argument 0])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[Argument 1,Argument 0])- , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[Argument 1,Argument 0])+ , Propositions [ mkProposition module_Properties "prop_view_reversible"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ , mkProposition module_Properties "prop_view_I"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ , mkProposition module_Properties "prop_view_current"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ , mkProposition module_Properties "prop_view_idem"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0, Argument 1]+ , mkProposition module_Properties "prop_view_local"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0, Argument 1] ] PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] - , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[Argument 1,Argument 0])- , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[Argument 0,Argument 1])+ , Propositions [ mkProposition module_Properties "prop_greedyView_reversible"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 1, Argument 0]+ , mkProposition module_Properties "prop_greedyView_idem"+ `ofType` LegacyQuickCheckProposition+ `withSignature` [Argument 0, Argument 1] ] PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
+ tests/Prop/t5/Main.hs view
@@ -0,0 +1,3 @@+import Even++main = doit