Hoed 0.3.1 → 0.3.2
raw patch · 17 files changed
+472/−161 lines, 17 filesdep +QuickCheckdep ~libgraphnew-component:exe:hoed-examples-CNF_unsound_de_Morgan__with_propertiesnew-component:exe:hoed-examples-Digraph_not_data_invariant__with_propertiesnew-component:exe:hoed-examples-SummerSchool_compiler_does_not_terminate__with_propertiesnew-component:exe:hoed-examples-XMonad_changing_focus_duplicates_windows__with_propertiesbinary-added
Dependencies added: QuickCheck
Dependency ranges changed: libgraph
Files
- Debug/Hoed/Pure.hs +22/−10
- Debug/Hoed/Pure/CompTree.hs +36/−9
- Debug/Hoed/Pure/DemoGUI.hs +128/−38
- Debug/Hoed/Pure/Observe.lhs +2/−1
- Debug/Hoed/Pure/Prop.hs +154/−91
- Debug/Hoed/Pure/Render.hs +8/−0
- Hoed.cabal +57/−5
- changelog +13/−2
- examples/CNF_unsound_demorgan__with_properties/Main.hs +10/−0
- examples/Digraph_not_data_invariant__with_properties/Main.hs +12/−0
- examples/afp02Exercises/Compiler__with_properties/Main.hs +25/−0
- img/loading.gif binary
- tests/Prop/t0/Main.hs +1/−1
- tests/Prop/t1/Main.hs +1/−1
- tests/Prop/t2/Main.hs +1/−1
- tests/Prop/t3/Main.hs +1/−1
- tests/Prop/t4/Main.hs +1/−1
Debug/Hoed/Pure.hs view
@@ -92,6 +92,8 @@ 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 CPP #-}+ module Debug.Hoed.Pure ( -- * Basic annotations observe@@ -109,6 +111,8 @@ , Proposition(..) , PropositionType(..) , Module(..)+ , propVarError+ , propVarFresh -- * Experimental annotations , traceOnly@@ -198,7 +202,7 @@ runO :: IO a -> IO () runO program = do (trace,traceInfo,compTree,frt) <- runO' program- debugSession trace traceInfo compTree frt+ debugSession trace traceInfo compTree frt [] return () -- | Repeat and trace a failing testcase@@ -211,8 +215,10 @@ runOwp :: [Propositions] -> IO a -> IO () runOwp ps program = do (trace,traceInfo,compTree,frt) <- runO' program+ let compTree' = compTree+{- hPutStrLn stderr "\n=== Evaluating assigned properties ===\n"- compTree' <- judge trace ps compTree+ compTree' <- judge propVarError trace ps compTree let vs = filter (/= RootVertex) (vertices compTree') showLen p = show . length . (filter p) $ vs@@ -224,12 +230,15 @@ [] -> do hPutStrLn stderr "\n=== Starting interactive debug session ===\n" debugSession trace traceInfo compTree' frt (v:_) -> hPutStrLn stderr $ "Fault detected in:\n\n" ++ show (vertexStmt v)+-}+ debugSession trace traceInfo compTree' frt ps return () -- | Repeat and trace a failing testcase testOwp :: Show a => [Propositions] -> (a->Bool) -> a -> IO ()-testOwp ps p x = runOwp ps $ putStrLn $ if (p x) then "Passed 1 test."- else " *** Failed! Falsifiable: " ++ show x+testOwp ps p x = runOwp ps $ putStrLn $ + if (p x) then "Passed 1 test."+ else " *** Failed! Falsifiable: " ++ show x -- | Short for @runO . print@. printO :: (Show a) => a -> IO ()@@ -261,7 +270,9 @@ ct = mkCompTree eqs ds writeFile ".Hoed/Events" (unlines . map show . reverse $ events)+#if defined(TRANSCRIPT) writeFile ".Hoed/Transcript" (getTranscript events ti)+#endif hPutStrLn stderr "\n=== Statistics ===\n" let e = length events@@ -291,11 +302,11 @@ showCompStmt = show . vertexStmt -- | As logO, but with property-based judging.-logOwp :: FilePath -> [Propositions] -> IO a -> IO ()-logOwp filePath properties program = do+logOwp :: PropVarGen String -> FilePath -> [Propositions] -> IO a -> IO ()+logOwp unevalGen filePath properties program = do (trace,traceInfo,compTree,frt) <- runO' program hPutStrLn stderr "\n=== Evaluating assigned properties ===\n"- compTree' <- judge trace properties compTree+ compTree' <- judge unevalGen trace properties compTree writeFile filePath (showGraph compTree') return () @@ -308,13 +319,14 @@ ------------------------------------------------------------------------ -- Algorithmic Debugging -debugSession :: Trace -> TraceInfo -> CompTree -> EventForest -> IO ()-debugSession trace traceInfo tree frt+debugSession :: Trace -> TraceInfo -> CompTree -> EventForest -> [Propositions] -> IO ()+debugSession trace traceInfo tree frt ps = do createDirectoryIfMissing True ".Hoed/wwwroot/css" dataDir <- getDataDir system $ "cp " ++ dataDir ++ "/img/*png .Hoed/wwwroot/"+ system $ "cp " ++ dataDir ++ "/img/*gif .Hoed/wwwroot/" treeRef <- newIORef tree startGUI defaultConfig { jsPort = Just 10000 , jsStatic = Just "./.Hoed/wwwroot"- } (guiMain trace traceInfo treeRef frt)+ } (guiMain trace traceInfo treeRef frt ps)
Debug/Hoed/Pure/CompTree.hs view
@@ -2,6 +2,8 @@ -- -- Copyright (c) Maarten Faddegon, 2015 +{-# LANGUAGE CPP #-}+ module Debug.Hoed.Pure.CompTree ( CompTree , Vertex(..)@@ -18,8 +20,9 @@ , leafs , ConstantValue(..) , getLocation-, getMessage+#if defined(TRANSCRIPT) , getTranscript+#endif , TraceInfo(..) , traceInfo , Graph(..) -- re-export from LibGraph@@ -32,8 +35,8 @@ import Prelude hiding (Right) import Data.Graph.Libgraph import Data.List(nub,delete,(\\))-import Data.IntMap (IntMap)-import qualified Data.IntMap as IntMap+import Data.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IntMap import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet @@ -126,8 +129,10 @@ -- reference from parent UID and position to location , computations :: Nesting -- UIDs of active and paused computations of arguments/results of Fun events+#if defined(TRANSCRIPT) , messages :: IntMap String -- stored depth of the stack for every event+#endif , storedStack :: IntMap [UID] -- reference from parent UID and position to previous stack , dependencies :: [(UID,UID)]@@ -135,7 +140,7 @@ -------------------------------------------------------------------------------------------------------------------------+#if defined(TRANSCRIPT) addMessage :: Event -> String -> TraceInfo -> TraceInfo addMessage e msg s = s{ messages = (flip $ IntMap.insert i) (messages s) $ case IntMap.lookup i (messages s) of Nothing -> msg@@ -159,9 +164,7 @@ (Just msg) -> "\n " ++ msg ms = messages t---+#endif ------------------------------------------------------------------------------------------------------------------------ getLocation :: Event -> TraceInfo -> Bool@@ -228,7 +231,11 @@ where i = getTopLvlFun e s cs = Computing i : computations s+#if defined(TRANSCRIPT) m = addMessage e $ "Start computation " ++ show i ++ ": " ++ showCs cs+#else+ m = id+#endif stop :: Event -> TraceInfo -> TraceInfo@@ -236,10 +243,14 @@ where i = getTopLvlFun e s cs = deleteFirst (computations s)- m = addMessage e $ "Stop computation " ++ show i ++ ": " ++ showCs cs deleteFirst [] = [] deleteFirst (s:ss) | isSpan i s = ss | otherwise = s : deleteFirst ss+#if defined(TRANSCRIPT)+ m = addMessage e $ "Stop computation " ++ show i ++ ": " ++ showCs cs+#else+ m = id+#endif pause :: Event -> TraceInfo -> TraceInfo@@ -252,7 +263,11 @@ (cs_pre,cs_post) = break isComputingI (computations s) isComputingI (Computing j) = i == j isComputingI _ = False+#if defined(TRANSCRIPT) m = addMessage e $ "Pause computation " ++ show i ++ ": " ++ showCs cs+#else+ m = id+#endif resume :: Event -> TraceInfo -> TraceInfo resume e s = m s{computations=cs}@@ -264,7 +279,11 @@ (cs_pre,cs_post) = break isPausedI (computations s) isPausedI (Paused j) = i == j isPausedI _ = False+#if defined(TRANSCRIPT) m = addMessage e $ "Resume computation " ++ show i ++ ": " ++ showCs cs+#else+ m = id+#endif activeComputations :: TraceInfo -> [UID] activeComputations s = map getSpanUID . filter isActive $ computations s@@ -282,9 +301,13 @@ [n] -> Just (-1,n) -- top-level function detected (may later add dependency from Root) (n:m:_) -> Just (m,n) +#if defined(TRANSCRIPT) m = case d of Nothing -> addMessage e ("does not add dependency") (Just d') -> addMessage e ("adds dependency " ++ show (fst d') ++ " -> " ++ show (snd d'))+#else+ m = id+#endif ------------------------------------------------------------------------------------------------------------------------ @@ -313,7 +336,11 @@ traceInfo trc = foldl loop s0 trc where s0 :: TraceInfo- s0 = TraceInfo IntMap.empty IntMap.empty [] IntMap.empty IntMap.empty []+ s0 = TraceInfo IntMap.empty IntMap.empty [] +#if defined(TRANSCRIPT)+ IntMap.empty+#endif+ IntMap.empty [] cs :: ConsMap cs = mkConsMap trc
Debug/Hoed/Pure/DemoGUI.hs view
@@ -3,7 +3,7 @@ -- Copyright (c) Maarten Faddegon, 2014-2015 {-# LANGUAGE CPP #-} -module Debug.Hoed.Pure.DemoGUI (guiMain, noNewlines)+module Debug.Hoed.Pure.DemoGUI (guiMain) where import qualified Prelude@@ -12,6 +12,8 @@ import Debug.Hoed.Pure.CompTree import Debug.Hoed.Pure.EventForest import Debug.Hoed.Pure.Observe+import qualified Debug.Hoed.Pure.Prop as Prop+import Debug.Hoed.Pure.Prop(Propositions,propVarError,propVarFresh,lookupPropositions,judgeWithPropositions,PropVarGen) import Paths_Hoed (version) import Data.Version (showVersion) import Data.Graph.Libgraph@@ -40,8 +42,8 @@ -------------------------------------------------------------------------------- -- The tabbed layout from which we select the different views -guiMain :: Trace -> TraceInfo -> IORef CompTree -> EventForest -> Window -> UI ()-guiMain trace traceInfo compTreeRef frt window+guiMain :: Trace -> TraceInfo -> IORef CompTree -> EventForest -> [Propositions] -> Window -> UI ()+guiMain trace traceInfo compTreeRef frt propositions window = do return window # set UI.title "Hoed debugging session" -- Get a list of vertices from the computation graph@@ -57,12 +59,13 @@ tab1 <- UI.button # set UI.text "About Hoed" # set UI.style activeTab tab2 <- UI.button # set UI.text "Observe" # set UI.style otherTab tab3 <- UI.button # set UI.text "Algorithmic Debugging" # set UI.style otherTab- tab4 <- UI.button # set UI.text "Explore" # set UI.style otherTab+ tab4 <- UI.button # set UI.text "Assisted Debugging" # set UI.style otherTab+ tab5 <- UI.button # set UI.text "Explore" # set UI.style otherTab -- tab5 <- UI.button # set UI.text "Events" # set UI.style otherTab logo <- UI.img # set UI.src "static/hoed-logo.png" # set UI.style [("float","right"), ("height","2.2em")]- tabs <- UI.div # set UI.style [("background-color","#D3D3D3")] #+ (map return [tab1,tab2,tab3,tab4{-,tab5-},logo])+ tabs <- UI.div # set UI.style [("background-color","#D3D3D3")] #+ (map return [tab1,tab2,tab3,tab4,tab5,logo]) - let coloActive tab = do mapM_ (\t -> (return t) # set UI.style otherTab) [tab1,tab2,tab3,tab4{-,tab5-}]; return tab # set UI.style activeTab+ let coloActive tab = do mapM_ (\t -> (return t) # set UI.style otherTab) [tab1,tab2,tab3,tab4,tab5]; return tab # set UI.style activeTab help <- guiHelp # set UI.style [("margin-top","0.5em")] on UI.click tab1 $ \_ -> do@@ -78,12 +81,12 @@ UI.getBody window # set UI.children [tabs,pane] on UI.click tab4 $ \_ -> do coloActive tab4+ pane <- guiAssisted trace propositions compTreeRef currentVertexRef regexRef imgCountRef # set UI.style [("margin-top","0.5em")]+ UI.getBody window # set UI.children [tabs,pane]+ on UI.click tab5 $ \_ -> do+ coloActive tab5 pane <- guiExplore compTreeRef currentVertexRef regexRef imgCountRef # set UI.style [("margin-top","0.5em")] UI.getBody window # set UI.children [tabs,pane]- -- on UI.click tab5 $ \_ -> do- -- coloActive tab5- -- pane <- guiTrace trace traceInfo # set UI.style [("margin-top","0.5em")]- -- UI.getBody window # set UI.children [tabs,pane] UI.getBody window # set UI.style [("margin","0")] #+ (map return [tabs,help]) return ()@@ -171,6 +174,74 @@ drawR --------------------------------------------------------------------------------+-- The Assisted Debugging GUI++guiAssisted :: Trace -> [Propositions] -> IORef CompTree -> IORef Int -> IORef String -> IORef Int -> UI UI.Element+guiAssisted trace ps compTreeRef currentVertexRef regexRef imgCountRef = do++ forallRef <- UI.liftIO $ newIORef (False :: Bool)++ -- Get a list of vertices from the computation tree+ tree <- UI.liftIO $ readIORef compTreeRef++ -- Status+ status <- UI.span+ updateStatus status compTreeRef ++ -- Field to show current computation statement to the programmer+ compStmt <- UI.pre # set UI.style [("margin","0 2em")]+ 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+ j right Right+ j wrong Wrong+ testB <- UI.button # set UI.text "test" # set UI.height 30 # set UI.style [("margin-right","1em")]+ testAllB <- UI.button # set UI.text "test all" # set UI.height 30+ on UI.click testAllB $ \_ -> testAll compTreeRef trace ps status currentVertexRef compStmt forallRef+ on UI.click testB $ \_ -> testCurrent compTreeRef trace ps status currentVertexRef compStmt forallRef++ -- Checkbox to indicate if we want to use quickcheck over unevaluated values+ forall <- UI.input # set UI.type_ "checkbox" # set UI.checked False # set UI.style [("transform","scale(1.5)"),("-webkit-transform","scale(1.5)"),("margin-right","0.5em")]+ forallDiv <- UI.div #+ [return forall, UI.span # set UI.text "Try to find counterexamples using randomly generated values for unevaluated parts of a computation statement."]+ on UI.checkedChange forall $ \b -> UI.liftIO $ writeIORef forallRef b++ -- Populate the main screen+ top <- UI.center #+ [return status, UI.br, return right, return wrong, return testB, return testAllB, return forallDiv]+ UI.div #+ [return top, UI.hr, return compStmt]++testAll compTreeRef trace ps status currentVertexRef compStmt forallRef = do+ return status # UI.set UI.text "Evaluating propositions ..." #+ [UI.img # set UI.src "static/loading.gif" # set UI.height 30]+ UI.liftIO $ do+ handler <- UI.liftIO $ unevalHandler forallRef+ compTree <- readIORef compTreeRef+ compTree' <- Prop.judge handler trace ps compTree+ writeIORef compTreeRef compTree'+ advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef++testCurrent compTreeRef trace ps status currentVertexRef compStmt forallRef = do+ return status # UI.set UI.text "Evaluating propositions ..." #+ [UI.img # set UI.src "static/loading.gif" # set UI.height 30]+ mcv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef+ case mcv of+ (Just cv) -> do+ case lookupPropositions ps cv of + Nothing -> updateStatus status compTreeRef+ (Just p) -> do+ handler <- UI.liftIO $ unevalHandler forallRef+ cv' <- UI.liftIO $ judgeWithPropositions handler trace p cv + compTree <- UI.liftIO $ readIORef compTreeRef+ UI.liftIO $ writeIORef compTreeRef (replaceVertex compTree cv')+ advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef+ Nothing -> updateStatus status compTreeRef++unevalHandler :: IORef Bool -> IO (PropVarGen String)+unevalHandler forallRef = do+ forall <- readIORef forallRef+ return $ if forall then propVarFresh else propVarError++-------------------------------------------------------------------------------- -- The Algorithmic Debugging GUI guiAlgoDebug :: IORef CompTree -> IORef Int -> IORef String -> IORef Int -> UI UI.Element@@ -206,30 +277,42 @@ judge :: Advance -> UI.Element -> UI.Element -> Maybe UI.Element -> Maybe (UI.Element,IORef Int) -> IORef UID -> IORef CompTree -> UI.Element -> Judgement -> UI ()-judge advance status compStmt mMenu mImg currentVertexRef compTreeRef b j = +judge adv status compStmt mMenu mImg currentVertexRef compTreeRef b j = on UI.click b $ \_ -> do mv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef case mv of- (Just v) -> judge' status compStmt b j v+ (Just v) -> judge' v Nothing -> return () where - judge' status compStmt b j v = do+ judge' :: Vertex -> UI ()+ judge' v = do t' <- UI.liftIO $ readIORef compTreeRef- let t = markNode t' v j- v' = setJudgement v j- w = case (advance, next_step t getJudgement v') of- (DoNotAdvance,_) -> v'- (AdvanceToNext,RootVertex) -> v'+ UI.liftIO $ writeIORef compTreeRef (markNode t' v j)+ advance adv status compStmt mMenu mImg currentVertexRef compTreeRef++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+ mv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef+ case mv of+ Nothing -> do+ return ()+ (Just v) -> do+ t <- UI.liftIO $ readIORef compTreeRef+ let w = case (adv, next_step t getJudgement) of+ (DoNotAdvance,_) -> v+ (AdvanceToNext,RootVertex) -> v (AdvanceToNext,w') -> w'+ a = case getJudgement w of+ (Assisted msg) -> msg+ _ -> "" UI.liftIO $ writeIORef currentVertexRef (vertexUID w)- UI.liftIO $ writeIORef compTreeRef t- UI.element compStmt # UI.set UI.text (show . vertexStmt $ w)+ showStmt compStmt compTreeRef currentVertexRef updateStatus status compTreeRef case mMenu of Nothing -> return () (Just menu) -> updateMenu menu compTreeRef currentVertexRef case mImg of Nothing -> return () (Just (img,imgCountRef)) -> redraw img imgCountRef compTreeRef (Just w)- -------------------------------------------------------------------------------- -- Explore the computation tree@@ -279,8 +362,10 @@ showStmt e compTreeRef currentVertexRef = do mv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef let s = case mv of- Nothing -> "Select vertex above to show details."- (Just v) -> show . vertexStmt $ v+ Nothing -> "No computation statement selected."+ (Just v) -> let s = show . vertexStmt $ v in case getJudgement v of+ (Assisted s') -> "Results from testing computation statement:\n" ++ s' ++ "\n---\n\n" ++ s+ _ -> s UI.element e # set UI.text s return () @@ -294,7 +379,7 @@ Nothing -> 0 t <- UI.liftIO $ readIORef compTreeRef let fs = faultyVertices t- ops <- mapM (\s->UI.option # set UI.text s) $ map (summarizeVertex fs) vs+ ops <- mapM (\s->UI.option # set UI.text s) $ map (summarizeVertex fs) vs (UI.element menu) # set UI.children [] UI.element menu #+ (map UI.element ops) (UI.element menu) # set UI.selection (Just j)@@ -322,7 +407,7 @@ mcv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef let cv = case mcv of (Just v) -> v; Nothing -> RootVertex ps = preds t cv- sibl = if RootVertex `elem` ps then succs t RootVertex else []+ sibl = if RootVertex `elem` ps then succs t RootVertex else [cv] return $ filter (/= RootVertex) $ ps ++ sibl ++ (succs t cv) lookupCurrentVertex :: IORef Int -> IORef CompTree -> IO (Maybe Vertex)@@ -343,6 +428,12 @@ (===) :: Vertex -> Vertex -> Bool v1 === v2 = (vertexUID v1) == (vertexUID v2) +replaceVertex :: CompTree -> Vertex -> CompTree+replaceVertex g v = mapGraph f g+ where f RootVertex = RootVertex+ f v' | (vertexUID v') == (vertexUID v) = v+ | otherwise = v'+ data MaxStringLength = ShorterThan Int | Unlimited shorten :: MaxStringLength -> String -> String@@ -352,16 +443,10 @@ | l > 3 = take (l - 3) s ++ "..." | otherwise = take l s -noNewlines :: String -> String-noNewlines = noNewlines' False-noNewlines' _ [] = []-noNewlines' w (s:ss)- | w && (s == ' ' || s == '\n') = noNewlines' True ss- | (not w) && (s == ' ' || s == '\n') = ' ' : noNewlines' True ss- | otherwise = s : noNewlines' False ss+shorterThan60 = shorten (ShorterThan 60) summarizeVertex :: [Vertex] -> Vertex -> String-summarizeVertex fs v = shorten (ShorterThan 60) (noNewlines . show . vertexStmt $ v) ++ s+summarizeVertex fs v = shorterThan60 (noNewlines . show . vertexStmt $ v) ++ s where s = if v `elem` fs then " !!" else case getJudgement v of Wrong -> " :(" Right -> " :)"@@ -369,7 +454,7 @@ vertexGraphvizLabel :: [Vertex] -> Vertex -> String vertexGraphvizLabel fs v =- "<<TABLE BORDER=\"0\" CELLBORDER=\"0\"><TR><TD HEIGHT=\"30\" WIDTH=\"30\" FIXEDSIZE=\"true\"><IMG SCALE=\"true\" SRC=\"" ++ (vertexImg fs v) ++ "\"/></TD><TD><FONT POINT-SIZE=\"30\">" ++ (htmlEscape . noNewlines . show . vertexStmt $ v) ++ "</FONT></TD></TR></TABLE>>"+ "<<TABLE BORDER=\"0\" CELLBORDER=\"0\"><TR><TD HEIGHT=\"30\" WIDTH=\"30\" FIXEDSIZE=\"true\"><IMG SCALE=\"true\" SRC=\"" ++ (vertexImg fs v) ++ "\"/></TD><TD><FONT POINT-SIZE=\"30\">" ++ (htmlEscape . shorterThan60 . noNewlines . show . vertexStmt $ v) ++ "</FONT></TD></TR></TABLE>>" htmlEscape :: String -> String htmlEscape = foldr (\c acc -> replace c ++ acc) ""@@ -379,20 +464,25 @@ replace '{' = "{" replace '\\' = "\" replace '>' = ">"+ replace '<' = "<" replace '}' = "}" replace c = [c] vertexImg :: [Vertex] -> Vertex -> String vertexImg fs v = if v `elem` fs then ".Hoed/wwwroot/faulty.png" else case vertexJmt v of- Unassessed -> ".Hoed/wwwroot/unassessed.png"- Wrong -> ".Hoed/wwwroot/wrong.png"- Right -> ".Hoed/wwwroot/right.png"+ Unassessed -> ".Hoed/wwwroot/unassessed.png"+ (Assisted _) -> ".Hoed/wwwroot/unassessed.png"+ Wrong -> ".Hoed/wwwroot/wrong.png"+ Right -> ".Hoed/wwwroot/right.png" updateStatus :: UI.Element -> IORef CompTree -> UI () updateStatus e compGraphRef = do g <- UI.liftIO $ readIORef compGraphRef- let isJudged v = getJudgement v /= Unassessed+ let isJudged v = case getJudgement v of+ Right -> True+ Wrong -> True+ _ -> False -- Assisted does not count as judged slen = show . length ns = filter (not . isRootVertex) (preorder g) js = filter isJudged ns
Debug/Hoed/Pure/Observe.lhs view
@@ -1187,7 +1187,8 @@ ourCatchAllIO = Exception.catch handleExc :: Parent -> SomeException -> IO a-handleExc context exc = return (send "throw" (return throw << exc) context)+-- handleExc context exc = return (send "throw" (return throw << exc) context)+handleExc context exc = return (send (show exc) (return (throw exc)) context) \end{code} %************************************************************************
Debug/Hoed/Pure/Prop.hs view
@@ -9,14 +9,10 @@ -- , Propositions(..) -- ) where import Debug.Hoed.Pure.Observe(Trace(..),UID,Event(..),Change(..),ourCatchAllIO,evaluate)-import Debug.Hoed.Pure.Render(CompStmt(..))+import Debug.Hoed.Pure.Render(CompStmt(..),noNewlines) import Debug.Hoed.Pure.CompTree(CompTree,Vertex(..),Graph(..),vertexUID) import Debug.Hoed.Pure.EventForest(EventForest,mkEventForest,dfsChildren)-import Debug.Hoed.Pure.DemoGUI(noNewlines) import qualified Data.IntMap as M--import qualified Debug.Trace as Debug -- MF TODO- import Prelude hiding (Right) import Data.Graph.Libgraph(Judgement(..),mapGraph) import System.Directory(createDirectoryIfMissing)@@ -26,7 +22,7 @@ import System.IO.Unsafe(unsafePerformIO) import Data.Char(isAlpha) import Data.Maybe(isNothing,fromJust)-import Data.List(intersperse)+import Data.List(intersperse,isInfixOf) import GHC.Generics hiding (moduleName) --(Generic(..),Rep(..),from,(:+:)(..),(:*:)(..),U1(..),K1(..),M1(..)) ------------------------------------------------------------------------------------------------------------------------@@ -35,13 +31,13 @@ , extraModules :: [Module] } -data PropType = Specify | PropertiesOf+data PropType = Specify | PropertiesOf deriving Eq type Proposition = (PropositionType,Module,String,[Int]) -data PropositionType = BoolProposition | QuickCheckProposition+data PropositionType = BoolProposition | QuickCheckProposition deriving Show -data Module = Module {moduleName :: String, searchPath :: String}+data Module = Module {moduleName :: String, searchPath :: String} deriving Show propositionType :: Proposition -> PropositionType propositionType (x,_,_,_) = x@@ -61,6 +57,7 @@ buildFiles = ".Hoed/exe/Main.o .Hoed/exe/Main.hi" exeFile = ".Hoed/exe/Main" outFile = ".Hoed/exe/Main.out"+errFile = ".Hoed/exe/Main.compilerMessages" ------------------------------------------------------------------------------------------------------------------------ @@ -76,74 +73,91 @@ ------------------------------------------------------------------------------------------------------------------------ -judge :: Trace -> [Propositions] -> CompTree -> IO CompTree-judge trc ps compTree = do+judge :: PropVarGen String -> Trace -> [Propositions] -> CompTree -> IO CompTree+judge unevalGen trc ps compTree = do ws <- mapM j vs return $ foldl updateTree compTree ws where vs = vertices compTree j v = case lookupPropositions ps v of Nothing -> return v- (Just p) -> judgeWithPropositions trc p v+ (Just p) -> judgeWithPropositions unevalGen trc p v updateTree compTree w = mapGraph (\v -> if (vertexUID v) == (vertexUID w) then w else v) compTree - -- Use a property to judge a vertex-judgeWithPropositions :: Trace -> Propositions -> Vertex -> IO Vertex-judgeWithPropositions _ _ RootVertex = return RootVertex-judgeWithPropositions trc p v = do- mbs <- mapM (evalProposition trc v (extraModules p)) (propositions p)- let j = case (propType p, any isNothing mbs) of- (Specify,False) -> if any isJustFalse mbs then Wrong else Right- _ -> if any isJustFalse mbs then Wrong else Unassessed- j' = case (j, (map snd) . (filter (isJustTrue . fst)) $ zip mbs (propositions p)) of- (Unassessed, []) -> Unassessed- (Unassessed, ps) -> Assisted $ "With passing properties: " ++ commas (map propName ps)- _ -> j- hPutStrLn stderr $ "Judgement was " ++ (show . vertexJmt) v ++ ", and is now " ++ show j'- return v{vertexJmt=j'}+judgeWithPropositions :: PropVarGen String -> Trace -> Propositions -> Vertex -> IO Vertex+judgeWithPropositions unevalGen _ _ RootVertex = return RootVertex+judgeWithPropositions unevalGen trc p v = do+ putStrLn $ "\n================\n"+ pas <- mapM (evalProposition unevalGen trc v (extraModules p)) (propositions p)+ putStrLn $ "judgeWithPropositions: pas=" ++ show pas + let s = propType p == Specify && noAssumption unevalGen+ z = zip pas (propositions p)+ let a = case (map snd) . (filter (holds . fst)) $ z of+ [] -> errorMessages z+ ps -> "With passing properties: " ++ commas (map propName ps) ++ "\n" ++ (errorMessages z)+ j | s && all hasResult pas = if any disproves pas then Wrong else Right+ | any hasResult pas = if any disproves pas then Wrong else Assisted a+ | otherwise = Assisted a+ hPutStrLn stderr $ "Judgement was " ++ (show . vertexJmt) v ++ ", and is now " ++ show j+ return v{vertexJmt=j} where- isJustFalse (Just False) = True- isJustFalse _ = False- isJustTrue (Just True) = True- isJustTrue _ = False- commas :: [String] -> String commas = concat . (intersperse ", ") +data PropApp = Error String | Holds | Disproves deriving Show -evalProposition :: Trace -> Vertex -> [Module] -> Proposition -> IO (Maybe Bool)-evalProposition trc v ms prop = do+hasResult :: PropApp -> Bool+hasResult (Error _) = False+hasResult _ = True++holds :: PropApp -> Bool+holds Holds = True+holds _ = False++disproves :: PropApp -> Bool+disproves Disproves = True+disproves _ = False++errorMessages :: [(PropApp,Proposition)] -> String+errorMessages = foldl (\msgs (Error msg,p) -> msgs ++ "\n---\n\nApplying property " ++ propName p ++ " gives inconclusive result:\n\n" ++ msg) [] . filter (not . hasResult . fst)++evalProposition :: PropVarGen String -> Trace -> Vertex -> [Module] -> Proposition -> IO PropApp+evalProposition unevalGen trc v ms prop = do createDirectoryIfMissing True ".Hoed/exe"- hPutStrLn stderr $ "\nEvaluating proposition " ++ propName prop ++ " with statement " ++ (shorten . noNewlines . show . vertexStmt) v- -- let args = map (\(n,s) -> "Argument " ++ show n ++ ": " ++ s) $ zip [0..] (generateArgs trc getEvent i)- -- let args = map (\(n,s) -> "Argument " ++ show n ++ ": " ++ (shorten s)) $ zip [0..] (generateArgs trc getEvent i)- -- hPutStrLn stderr $ "Statement UID = " ++ show i- -- mapM (hPutStrLn stderr) args+ hPutStrLn stderr $ "Evaluating proposition " ++ propName prop ++ " with statement " ++ (shorten . noNewlines . show . vertexStmt) v clean- generateCode+ prgm <- generateCode compile exit' <- compile+ err <- readFile errFile+ hPutStrLn stderr $ err hPutStrLn stderr $ "Compilation exitted with " ++ show exit'- exit <- case exit' of (ExitFailure n) -> return (ExitFailure n)- ExitSuccess -> evaluate- out <- readFile outFile- hPutStrLn stderr $ "Evaluation exitted with " ++ show exit- hPutStrLn stderr $ "Output is " ++ show out- return $ case (exit, out) of- (ExitFailure _, _) -> Nothing -- TODO: Can we do better with a failing precondition?- (ExitSuccess , "True\n") -> Just True- (ExitSuccess , "False\n") -> Just False- (ExitSuccess , _) -> Nothing+ case exit' of + (ExitFailure _) -> return $ Error $ "Compilation of {{{\n" ++ prgm ++ "\n}}} failed with:\n" ++ err+ ExitSuccess -> do + exit <- evaluate+ out' <- readFile outFile+ let out = backspaces out'+ hPutStrLn stderr $ out+ hPutStrLn stderr $ "Evaluation exitted with " ++ show exit+ return $ case (exit,out) of+ (ExitFailure _, _) -> Error out+ (ExitSuccess , "True\n") -> Holds+ (ExitSuccess , "False\n") -> Disproves+ (ExitSuccess , _) -> if "Failed! Falsifiable" `isInfixOf` out+ then Disproves+ else Error out where clean = system $ "rm -f " ++ sourceFile ++ " " ++ exeFile ++ " " ++ buildFiles generateCode = do -- Uncomment the next line to dump generated program on screen -- hPutStrLn stderr $ "Generated the following program ***\n" ++ prgm ++ "\n***" writeFile sourceFile prgm+ return prgm where prgm :: String- prgm = (generate prop ms trc getEvent i)- compile = system $ "ghc -i" ++ (searchPath . propModule) prop ++ " -o " ++ exeFile ++ " " ++ sourceFile+ prgm = (generate unevalGen prop ms trc getEvent i)+ compile = system $ "ghc -i" ++ (searchPath . propModule) prop ++ " -o " ++ exeFile ++ " " ++ sourceFile ++ " > " ++ errFile ++ " 2>&1" evaluate = system $ exeFile ++ " > " ++ outFile ++ " 2>&1" i = (stmtIdentifier . vertexStmt) v @@ -155,6 +169,17 @@ getEvent j = fromJust $ M.lookup j m where m = M.fromList $ map (\e -> (eventUID e, e)) trc +backspaces :: String -> String+backspaces s = reverse (backspaces' [] s)+ where+ backspaces' s [] = s+ backspaces' s (c:t)+ | c == '\b' = backspaces' (safeTail s) t+ | otherwise = backspaces' (c:s) t++ safeTail [] = []+ safeTail (c:s) = s+ -- The actual logic that changes the judgement of a vertex. judge1' :: ExitCode -> String -> Judgement -> Judgement judge1' (ExitFailure _) _ j = j@@ -172,9 +197,49 @@ ------------------------------------------------------------------------------------------------------------------------ -generate :: Proposition -> [Module] -> Trace -> (UID->Event) -> UID -> String-generate prop ms trc getEvent i = generateHeading prop ms ++ generateMain prop trc getEvent i+type PropVars = ([String],[String]) -- A tuple of used variables, and a supply of fresh variables+type PropVarGen a = PropVars -> (a,PropVars) +comp :: PropVarGen a -> PropVarGen b -> (a -> b -> c) -> PropVarGen c+comp x y f vs = let (x', vs') = x vs+ (y', vs'') = y vs'+ in (f x' y', vs'')++-- MF TODO: this is exactly like liftM2+liftPV :: (a -> b -> c) -> PropVarGen a -> PropVarGen b -> PropVarGen c+liftPV f x y = comp x y f++propVars0 :: PropVars+propVars0 = ([], map (('x':) . show) [1..])++propVarError :: PropVarGen String+propVarError = propVarReturn "(error \"Request of value that was unevaluated in original program.\")"++propVarFresh :: PropVarGen String+propVarFresh (bvs,v:fvs) = (v, (v:bvs,fvs))++propVarReturn :: String -> PropVarGen String+propVarReturn s vs = (s,vs)++noAssumption :: PropVarGen a -> Bool+noAssumption unevalGen = (fst . snd . unevalGen) propVars0 == []++propVarBind :: (String,PropVars) -> Proposition -> String+propVarBind (propApp,([],_)) prop = generatePrint prop ++ " $ " ++ propApp+propVarBind (propApp,(bvs,_)) prop = "quickCheck (\\" ++ bvs' ++ " -> " ++ propApp ++ ")"+ where+ bvs' = concat (intersperse " " bvs)++generatePrint :: Proposition -> String+generatePrint p = case propositionType p of+ BoolProposition -> "print"+ QuickCheckProposition -> "do g <- newStdGen; print . fromJust . ok . (generate 1 g) . evaluate"++------------------------------------------------------------------------------------------------------------------------++generate :: PropVarGen String -> Proposition -> [Module] -> Trace -> (UID->Event) -> UID -> String+generate unevalGen prop ms trc getEvent i = generateHeading prop ms ++ generateMain unevalGen prop trc getEvent i+ generateHeading :: Proposition -> [Module] -> String generateHeading prop ms = "-- This file is generated by the Haskell debugger Hoed\n"@@ -184,51 +249,49 @@ generateImport :: Module -> String generateImport m = "import " ++ (moduleName m) ++ "\n" -generateMain :: Proposition -> Trace -> (UID->Event) -> UID -> String-generateMain prop trc getEvent i =- foldl (\acc x -> acc ++ " " ++ getArg x) ("main = " ++ generatePrint prop ++ " $ " ++ propName prop ++ " ") (reverse . argMap $ prop) ++ "\n"- where - getArg :: Int -> String- getArg x- | x < (length args) = args !! x- | otherwise = __-- args :: [String]- args = generateArgs trc getEvent i--generatePrint :: Proposition -> String-generatePrint p = case propositionType p of- BoolProposition -> "print"- QuickCheckProposition -> "do g <- newStdGen; print . fromJust . ok . (generate 1 g) . evaluate"+generateMain :: (PropVarGen String) -> Proposition -> Trace -> (UID->Event) -> UID -> String+generateMain unevalGen prop trc getEvent i+ = "main = " ++ propVarBind (foldl accArg ((propName prop),propVars0) (reverse . argMap $ prop)) prop ++ "\n"+ where + accArg :: (String,PropVars) -> Int -> (String,PropVars)+ accArg (acc,propVars) x = let (s,propVars') = getArg x propVars in (acc ++ " " ++ s, propVars')+ getArg :: Int -> PropVarGen String+ getArg x+ | x < (length args) = args !! x+ | otherwise = propVarError -generateArgs :: Trace -> (UID -> Event) -> UID -> [String]-generateArgs trc getEvent i = case dfsChildren frt e of- [_,ma,_,mr] -> generateExpr frt ma : moreArgs trc getEvent mr- xs -> error ("generateArgs: dfsChildren (" ++ show e ++ ") = " ++ show xs)+ args :: [PropVarGen String]+ args = generateArgs unevalGen trc getEvent i - where frt = (mkEventForest trc)- e = getEvent i -- (reverse trc) !! (i-1)+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 -- (reverse trc) !! (i-1) -moreArgs :: Trace -> (UID->Event) -> Maybe Event -> [String]-moreArgs trc getEvent Nothing = []-moreArgs trc getEvent (Just e)- | change e == Fun = generateArgs trc getEvent (eventUID e)+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 :: EventForest -> Maybe Event -> String-generateExpr _ Nothing = __-generateExpr frt (Just e) = -- uncomment next line to add events as comments to generated code: - -- "{- " ++ show e ++ " -}" ++- case change e of+generateExpr :: PropVarGen String -> EventForest -> Maybe Event -> PropVarGen String+generateExpr unevalGen _ Nothing = unevalGen+generateExpr unevalGen frt (Just e) = case change e of (Cons _ s) -> let s' = if isAlpha (head s) then s else "(" ++ s ++ ")"- in foldl (\acc c -> acc ++ " " ++ c) ("(" ++ s') cs ++ ") "- Enter -> ""- _ -> "error \"cannot represent\""-- where cs = map (generateExpr frt) (dfsChildren frt e)+ in liftPV (++) ( foldl (liftPV $ \acc c -> acc ++ " " ++ c)+ (propVarReturn ("(" ++ s')) cs+ ) + ( propVarReturn ") "+ )+ Enter -> propVarReturn ""+ _ -> propVarReturn "error \"cannot represent\"" -__ :: String-__ = "(error \"Request of value that was unevaluated in original program.\")"+ where cs :: [PropVarGen String]+ cs = map (generateExpr unevalGen frt) (dfsChildren frt e) ------------------------------------------------------------------------------------------------------------------------
Debug/Hoed/Pure/Render.hs view
@@ -10,6 +10,7 @@ ,eventsToCDS ,rmEntrySet ,simplifyCDSSet+,noNewlines ) where import Debug.Hoed.Pure.EventForest @@ -53,6 +54,13 @@ show = stmtRes showList eqs eq = unlines (map show eqs) ++ eq +noNewlines :: String -> String+noNewlines = noNewlines' False+noNewlines' _ [] = []+noNewlines' w (s:ss)+ | w && (s == ' ' || s == '\n') = noNewlines' True ss+ | (not w) && (s == ' ' || s == '\n') = ' ' : noNewlines' True ss+ | otherwise = s : noNewlines' False ss ------------------------------------------------------------------------ -- Render equations from CDS set
Hoed.cabal view
@@ -1,5 +1,5 @@ name: Hoed-version: 0.3.1+version: 0.3.2 synopsis: Lightweight algorithmic debugging. description: Hoed is a tracer and debugger for the programming language Haskell. You can trace a program by annotating functions in suspected modules and linking your program against standard profiling libraries.@@ -17,7 +17,7 @@ build-type: Simple cabal-version: >=1.10 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+data-files: img/*.png, img/*.gif flag buildExamples description: Build example executables.@@ -62,15 +62,20 @@ , process , threepenny-gui == 0.6.* , filepath- , libgraph == 1.7+ , libgraph == 1.9 , RBTree == 0.0.5 , regex-posix , mtl , directory , FPretty default-language: Haskell2010- -- ghc-options: -fwarn-unused-binds+ -- Enable to get some extra warnings.+ -- ghc-options: -fwarn-unused-binds + -- Enable to create a file .Hoed/Transcript that lists all steps taken to construct a+ -- computation tree from the list of events.+ -- cpp-options: -DTRANSCRIPT+ --------------------------------------------------------------------------- -- -- A list of example-programs that bind to a debugging session after the@@ -164,7 +169,7 @@ hs-source-dirs: examples/XMonad_changing_focus_duplicates_windows__CC default-language: Haskell2010 -Executable hoed-examples-XMonad_changing_focus_duplicates_windows__using_properties+Executable hoed-examples-XMonad_changing_focus_duplicates_windows__with_properties if flag(buildExamples) build-depends: base >= 4 && < 5, Hoed, X11>=1.5 && < 1.7, mtl, unix,@@ -191,6 +196,38 @@ hs-source-dirs: examples/afp02Exercises/Compiler/ default-language: Haskell2010 +Executable hoed-examples-SummerSchool_compiler_does_not_terminate__with_properties+ 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,+ array,QuickCheck+ else+ buildable: False+ main-is: Main.hs+ hs-source-dirs: examples/afp02Exercises/Compiler__with_properties/+ default-language: Haskell2010++Executable hoed-examples-CNF_unsound_de_Morgan__with_properties+ if flag(buildExamples)+ build-depends: base >= 4 && < 5, Hoed+ else+ buildable: False+ main-is: Main.hs+ hs-source-dirs: examples/CNF_unsound_demorgan__with_properties/+ default-language: Haskell2010++Executable hoed-examples-Digraph_not_data_invariant__with_properties+ if flag(buildExamples)+ build-depends: base >= 4 && < 5, Hoed, lazysmallcheck+ else+ buildable: False+ main-is: Main.hs+ hs-source-dirs: examples/Digraph_not_data_invariant__with_properties/+ default-language: Haskell2010+ Executable hoed-examples-Simple_higher-order_function if flag(buildExamples) build-depends: base >= 4 && < 5, Hoed, @@ -204,6 +241,21 @@ main-is: SimpleHO.hs hs-source-dirs: examples/ default-language: Haskell2010++-- MF TODO: add source to repository and re-enable this again+-- Executable hoed-examples-Exception+-- 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,+-- array+-- else+-- buildable: False+-- main-is: Exception.hs+-- hs-source-dirs: examples/+-- default-language: Haskell2010 Executable hoed-examples-Parity_test if flag(buildExamples)
changelog view
@@ -1,5 +1,17 @@-0.2.2 Maarten Faddegon 14 2015+0.3.2 Maarten Faddegon 6 Dec 2015 + * Add experimental combinators for property-assisted algorithmic debugging.++0.3.1 Maarten Faddegon 20 Nov 2015++ * Some performance improvements in Debug.Hoed.Pure; add several extra examples.++0.3.0 Maarten Faddegon 3 Sep 2015++ * Add Debug.Hoed.Pure, allowing computation tree tracing with higher precision without depending on the cost centre stack extension.++0.2.2 Maarten Faddegon 14 July 2015+ * Use a preprocessor to make the library work with GHC 7.10, but also for older versions of GHC. This is related to the "The Applicative Monad Proposal" and the changes to Template Haskell in GHC 7.10 that are not backward compatibility with earlier versions of GHC. 0.2.1 Maarten Faddegon 1 May 2015@@ -10,7 +22,6 @@ * A threepenny-gui algorithmic debugger. * Construction of computation trees with just local annotations. Existing algorithmic debuggers for Haskell require a transformation of all modules in a program, even libraries that the user does not want to debug and which may use language features not supported by the debugger. This is a pity, because a promising approach to debugging is therefore not applicable to many real-world programs. We use the cost centre stack from the Glasgow Haskell Compiler profiling environment together with runtime value observations to collect enough information for algorithmic debugging.- 0.1.0.1 Maarten Faddegon 24 May 2014
+ examples/CNF_unsound_demorgan__with_properties/Main.hs view
@@ -0,0 +1,10 @@+-- A program with unexpected output.+import CNF+import Debug.Hoed.Pure++main = runOwp properties $ print (prop_negin_correct eg)+ where+ properties = [Propositions [(BoolProposition,cnfModule,"prop_negin_complete",[0]), (BoolProposition,cnfModule,"prop_negin_sound",[0])] Specify "negin" [modQuickCheck]+ ]+ cnfModule = Module "CNF" "../examples/CNF_unsound_demorgan__with_properties/"+ modQuickCheck = Module "Test.QuickCheck" ""
+ examples/Digraph_not_data_invariant__with_properties/Main.hs view
@@ -0,0 +1,12 @@+-- A program with unexpected output.+import Digraph+import Debug.Hoed.Pure++main = runOwp properties $ print (prop_assoc1toNdigraph eg)+ where+ properties = [ Propositions [(BoolProposition,digraphModule,"prop_assoc1toNdigraph",[0])] Specify "assoc1toNdigraph" [modQuickCheck]+ , Propositions [(BoolProposition,digraphModule,"prop_mergeAndSortTargets",[0])] Specify "mergeAndSortTargets" [modQuickCheck]+ , Propositions [(BoolProposition,digraphModule,"prop_addMissingSources",[0])] Specify "addMissingSources" [modQuickCheck]+ ]+ digraphModule = Module "Digraph" "../examples/Digraph_not_data_invariant__with_properties/"+ modQuickCheck = Module "Test.QuickCheck" ""
+ examples/afp02Exercises/Compiler__with_properties/Main.hs view
@@ -0,0 +1,25 @@+module Main where++import Debug.Hoed.Pure+import Syntax+import Parser+import Interpreter+import Machine+import Compiler++main = runOwp properties $ do+ let prog = parse gcdSource+ putStrLn "interpreted:"+ print (obey prog)+ putStrLn "compiled:"+ print (exec (compile prog))+ where+ properties = [Propositions [(BoolProposition,modInterpreter,"prop_ifT",[1,0])] PropertiesOf "run" [modSyntax,modValue,modQuickCheck]+ ]+ modInterpreter = Module "Interpreter" "../examples/afp02Exercises/Compiler__with_properties/"+ modValue = Module "Value" "../examples/afp02Exercises/Compiler__with_properties/"+ modSyntax = Module "Syntax" "../examples/afp02Exercises/Compiler__with_properties/"+ modQuickCheck = Module "Test.QuickCheck" ""++gcdSource :: String+gcdSource = "x := 148; y := 58;\nwhile ~(x=y) do\n if x < y then y := y - x\n else x := x - y\n fi\nod;\nprint x\n"
+ img/loading.gif view
binary file changed (absent → 22954 bytes)
tests/Prop/t0/Main.hs view
@@ -4,7 +4,7 @@ import Debug.Hoed.Pure -- main = quickcheck prop_idemSimplify-main = logOwp "hoed-tests-Prop-t0.graph" properties $ print $ prop_idemSimplify (Mul (Const 1) (Const 2))+main = logOwp propVarError "hoed-tests-Prop-t0.graph" properties $ print $ prop_idemSimplify (Mul (Const 1) (Const 2)) where properties = [ Propositions [(BoolProposition,myModule,"prop_idemOne",[0])] PropertiesOf "one" [] , Propositions [(BoolProposition,myModule,"prop_idemZero",[0])] PropertiesOf "zero" []
tests/Prop/t1/Main.hs view
@@ -3,7 +3,7 @@ import Debug.Hoed.Pure -- main = quickcheck prop_idem_negin_sound-main = logOwp "hoed-tests-Prop-t1.graph" properties $ print (prop_negin_correct eg)+main = logOwp propVarError "hoed-tests-Prop-t1.graph" properties $ print (prop_negin_correct eg) -- main = logOwp "hoed-tests-Prop-t1.graph" properties $ print (negin eg, prop_negin_correct eg) where properties = [Propositions [(BoolProposition,cnfModule,"prop_negin_complete",[0]), (BoolProposition,cnfModule,"prop_negin_sound",[0])] Specify "negin" []
tests/Prop/t2/Main.hs view
@@ -3,7 +3,7 @@ import Debug.Hoed.Pure -- main = quickcheck prop_idem_negin_sound-main = logOwp "hoed-tests-Prop-t2.graph" properties $ print (prop_assoc1toNdigraph eg)+main = logOwp propVarError "hoed-tests-Prop-t2.graph" properties $ print (prop_assoc1toNdigraph eg) where properties = [ Propositions [(BoolProposition,digraphModule,"prop_assoc1toNdigraph",[0])] Specify "assoc1toNdigraph" [] , Propositions [(BoolProposition,digraphModule,"prop_mergeAndSortTargets",[0])] Specify "mergeAndSortTargets" []
tests/Prop/t3/Main.hs view
@@ -13,7 +13,7 @@ main :: IO ()-main = logOwp "hoed-tests-Prop-t3.graph" propositions $ do+main = logOwp propVarError "hoed-tests-Prop-t3.graph" propositions $ do -- main = do {- Running all tests
tests/Prop/t4/Main.hs view
@@ -24,7 +24,7 @@ -} main :: IO ()-main = logOwp "hoed-tests-Prop-t4.graph" propositions $ do+main = logOwp propVarError "hoed-tests-Prop-t4.graph" propositions $ do g <- newStdGen print . fromJust . ok . (generate 1 g) . evaluate $ prop_shift_win_I 1 'd' myStackSet where