packages feed

Hoed 0.3.4 → 0.3.5

raw patch · 26 files changed

+811/−383 lines, 26 filesdep +bytestringdep +cerealdep ~libgraphdep ~threepenny-guinew-component:exe:hoed-examples-Queens__with_properties

Dependencies added: bytestring, cereal

Dependency ranges changed: libgraph, threepenny-gui

Files

Debug/Hoed/Pure.hs view
@@ -97,29 +97,41 @@   ( -- * Basic annotations     observe   , runO-  , testO   , printO-  , logO+  , testO -  -- * Property-based judging+  -- * Property-assisted algorithmic debugging   , runOwp   , testOwp-  , logOwp   , Propositions(..)   , PropType(..)   , Proposition(..)   , PropositionType(..)   , Module(..)-  , UnevalHandler(..)+  , Signature(..)+  , ParEq(..)+  , runOstore+  , conAp -    -- * Experimental annotations-  , traceOnly+  -- * Build your own debugger with Hoed+  , runO'+  , judge+  , unjudgedCharacterCount+  , CompTree(..)+  , Vertex(..)+  , CompStmt(..)+  , Judge(..)+  , Verbosity(..)++  -- * Alternative template Haskell annotations   , observeTempl   , observedTypes-  , observeCC -   -- * Parallel equality-  , ParEq(..)+  -- * API to test Hoed itself+  , logO+  , logOwp+  , traceOnly+  , UnevalHandler(..)     -- * The Observable class   , Observer(..)@@ -128,8 +140,9 @@   , thunk   , nothunk   , send-  , observeBase   , observeOpaque+  , observeBase+  , constrainBase   , debugO   , CDS(..)   , Generic@@ -142,6 +155,7 @@ import Debug.Hoed.Pure.CompTree import Debug.Hoed.Pure.DemoGUI import Debug.Hoed.Pure.Prop+import Debug.Hoed.Pure.Serialize import Paths_Hoed(getDataDir)  import Prelude hiding (Right)@@ -175,10 +189,22 @@  -- Run the observe ridden code. ++runOnce :: IO ()+runOnce = do+  f <- readIORef firstRun+  case f of True  -> writeIORef firstRun False+            False -> error "It is best not to run Hoed more that once (maybe you want to restart GHCI?)"++firstRun :: IORef Bool+firstRun = unsafePerformIO $ newIORef True++ -- | run some code and return the Trace debugO :: IO a -> IO Trace debugO program =-     do { initUniq+     do { runOnce+        ; initUniq         ; startEventStream         ; let errorMsg e = "[Escaping Exception in Code : " ++ show e ++ "]"         ; ourCatchAllIO (do { program ; return () })@@ -199,10 +225,18 @@  runO :: IO a -> IO () runO program = do-  (trace,traceInfo,compTree,frt) <- runO' program+  (trace,traceInfo,compTree,frt) <- runO' Verbose program   debugSession trace traceInfo compTree frt []   return () ++-- | Hoed internal function that stores a serialized version of the tree on disk (assisted debugging spawns new instances of Hoed).+runOstore :: String -> IO a -> IO ()+runOstore tag program = do +  (trace,traceInfo,compTree,frt) <- runO' Silent program+  storeTree (treeFilePath ++ tag) compTree+  storeTrace (traceFilePath ++ tag) trace+ -- | Repeat and trace a failing testcase testO :: Show a => (a->Bool) -> a -> IO () testO p x = runO $ putStrLn $ if (p x) then "Passed 1 test."@@ -212,23 +246,8 @@  runOwp :: [Propositions] -> IO a -> IO () runOwp ps program = do-  (trace,traceInfo,compTree,frt) <- runO' program+  (trace,traceInfo,compTree,frt) <- runO' Verbose program   let compTree' = compTree-{--  hPutStrLn stderr "\n=== Evaluating assigned properties ===\n"-  compTree' <- judge propVarError trace ps compTree--  let vs = filter (/= RootVertex) (vertices compTree')-      showLen p = show . length . (filter p) $ vs-  hPutStrLn stderr "\n=== Evaluated assigned properties for all computation statements ==="-  hPutStrLn stderr $ showLen isWrong    ++ " statements are now wrong because they fail a property."-  hPutStrLn stderr $ showLen isAssisted ++ " statements satisfy some properties and violate no properties."-  hPutStrLn stderr $ showLen isRight    ++ " statements are right because they satisfy their specification."-  case (findFaulty_dag getJudgement compTree') of-    []    -> 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 () @@ -249,13 +268,20 @@   return ()  -runO' :: IO a -> IO (Trace,TraceInfo,CompTree,EventForest)-runO' program = do+data Verbosity = Verbose | Silent++condPutStrLn :: Verbosity -> String -> IO ()+condPutStrLn Silent _  = return ()+condPutStrLn Verbose msg = hPutStrLn stderr msg++-- |Entry point giving you access to the internals of Hoed. Also see: runO.+runO' :: Verbosity -> IO a -> IO (Trace,TraceInfo,CompTree,EventForest)+runO' verbose program = do   createDirectoryIfMissing True ".Hoed/"-  putStrLn "=== program output ===\n"+  condPutStrLn verbose "=== program output ===\n"   events <- debugO program-  putStrLn "\n=== program terminated ==="-  putStrLn "Please wait while the computation tree is constructed..."+  condPutStrLn verbose"\n=== program terminated ==="+  condPutStrLn verbose"Please wait while the computation tree is constructed..."    let cdss = eventsToCDS events   let cdss1 = rmEntrySet cdss@@ -272,24 +298,23 @@   writeFile ".Hoed/Transcript" (getTranscript events ti) #endif   -  hPutStrLn stderr "\n=== Statistics ===\n"+  condPutStrLn verbose "\n=== Statistics ===\n"   let e  = length events       n  = length eqs-      -- d  = treeDepth ct       b  = fromIntegral (length . arcs $ ct ) / fromIntegral ((length . vertices $ ct) - (length . leafs $ ct))-  hPutStrLn stderr $ "e = " ++ show e-  hPutStrLn stderr $ "n = " ++ show n-  hPutStrLn stderr $ "d' = " ++ (show . length $ ds)-  -- hPutStrLn stderr $ "d = " ++ show d-  hPutStrLn stderr $ "b = " ++ show b+  condPutStrLn verbose $ show e ++ " events"+  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)" -  -- hPutStrLn stderr "\n=== Debug Session ===\n"+  condPutStrLn verbose "\n=== Debug Session ===\n"   return (events, ti, ct, frt)  -- | Trace and write computation tree to file. Useful for regression testing. logO :: FilePath -> IO a -> IO () logO filePath program = {- SCC "logO" -} do-  (_,_,compTree,_) <- runO' program+  (_,_,compTree,_) <- runO' Verbose program   writeFile filePath (showGraph compTree)   return () @@ -302,9 +327,9 @@ -- | As logO, but with property-based judging. logOwp :: UnevalHandler -> FilePath -> [Propositions] -> IO a -> IO () logOwp handler filePath properties program = do-  (trace,traceInfo,compTree,frt) <- runO' program+  (trace,traceInfo,compTree,frt) <- runO' Verbose program   hPutStrLn stderr "\n=== Evaluating assigned properties ===\n"-  compTree' <- judge handler trace properties compTree+  compTree' <- judgeAll handler unjudgedCharacterCount trace properties compTree   writeFile filePath (showGraph compTree')   return () @@ -323,8 +348,7 @@        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 ps)+           } (guiMain trace tree frt ps)
Debug/Hoed/Pure/CompTree.hs view
@@ -2,7 +2,7 @@ -- -- Copyright (c) Maarten Faddegon, 2015 -{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP, DeriveGeneric #-}  module Debug.Hoed.Pure.CompTree ( CompTree@@ -11,15 +11,19 @@ , isRootVertex , vertexUID , vertexRes+, replaceVertex , getJudgement , setJudgement , isRight , isWrong , isUnassessed , isAssisted+, isInconclusive+, isPassing , leafs , ConstantValue(..) , getLocation+, unjudgedCharacterCount #if defined(TRANSCRIPT) , getTranscript #endif@@ -39,9 +43,10 @@ import qualified Data.IntMap.Strict as IntMap import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet+import GHC.Generics  data Vertex = RootVertex | Vertex {vertexStmt :: CompStmt, vertexJmt :: Judgement}-  deriving (Eq,Show,Ord)+  deriving (Eq,Show,Ord,Generic)  getJudgement :: Vertex -> Judgement getJudgement RootVertex = Right@@ -56,6 +61,18 @@ isUnassessed v = getJudgement v == Unassessed isAssisted v   = case getJudgement v of (Assisted _) -> True; _ -> False +isInconclusive v = case getJudgement v of+  (Assisted ms) -> any isInconclusive' ms+  _             -> False+isInconclusive' (InconclusiveProperty _) = True+isInconclusive' _                        = False++isPassing v = case getJudgement v of+  (Assisted ms) -> any isPassing' ms+  _             -> False+isPassing' (PassingProperty _) = True+isPassing' _                        = False+ vertexUID :: Vertex -> UID vertexUID RootVertex   = -1 vertexUID (Vertex s _) = stmtIdentifier s@@ -64,6 +81,7 @@ vertexRes RootVertex = "RootVertex" vertexRes v          = stmtRes . vertexStmt $ v +-- | The forest of computation trees. Also see the Libgraph library. type CompTree = Graph Vertex ()  isRootVertex :: Vertex -> Bool@@ -72,6 +90,21 @@  leafs :: CompTree -> [Vertex] leafs g = filter (\v -> succs g v == []) (vertices g)++-- | Approximates the complexity of a computation tree by summing the length+-- of the unjudged computation statements (i.e not Right or Wrong) in the tree.+unjudgedCharacterCount :: CompTree -> Int+unjudgedCharacterCount = sum . (map characterCount) . (filter unjudged) . vertices+  where characterCount = length . stmtLabel . vertexStmt++unjudged = not . judged+judged v = (isRight v || isWrong v)++replaceVertex :: CompTree -> Vertex -> CompTree+replaceVertex g v = mapGraph f g+  where f RootVertex = RootVertex+        f v' | (vertexUID v') == (vertexUID v) = v+             | otherwise                       = v'  -------------------------------------------------------------------------------- -- Computation Tree
Debug/Hoed/Pure/DemoGUI.hs view
@@ -3,7 +3,7 @@ -- Copyright (c) Maarten Faddegon, 2014-2015 {-# LANGUAGE CPP #-} -module Debug.Hoed.Pure.DemoGUI (guiMain)+module Debug.Hoed.Pure.DemoGUI (guiMain,treeFilePath) where  import qualified Prelude@@ -12,8 +12,9 @@ import Debug.Hoed.Pure.CompTree import Debug.Hoed.Pure.EventForest import Debug.Hoed.Pure.Observe+import Debug.Hoed.Pure.Serialize import qualified Debug.Hoed.Pure.Prop as Prop-import Debug.Hoed.Pure.Prop(Propositions,lookupPropositions,judgeWithPropositions,UnevalHandler(..))+import Debug.Hoed.Pure.Prop(Propositions,lookupPropositions,UnevalHandler(..),Judge(..),treeFilePath) import Paths_Hoed (version) import Data.Version (showVersion) import Data.Graph.Libgraph@@ -42,12 +43,15 @@ -------------------------------------------------------------------------------- -- The tabbed layout from which we select the different views -guiMain :: Trace -> TraceInfo -> IORef CompTree -> EventForest -> [Propositions] -> Window -> UI ()-guiMain trace traceInfo compTreeRef frt propositions window+guiMain :: Trace -> CompTree -> EventForest -> [Propositions] -> Window -> UI ()+guiMain trace tree frt propositions window   = do return window # set UI.title "Hoed debugging session" +       -- memory shared between the different views+       compTreeRef <- UI.liftIO $ newIORef tree+       traceRef    <- UI.liftIO $ newIORef trace+        -- Get a list of vertices from the computation graph-       tree <- UI.liftIO $ readIORef compTreeRef        let ns = filter (not . isRootVertex) (preorder tree)         -- Shared memory@@ -56,16 +60,16 @@        imgCountRef         <- UI.liftIO $ newIORef (0 :: Int)         -- Tabs to select which pane to display-       tab1 <- UI.button # set UI.text "About Hoed"            # set UI.style activeTab+       tab1 <- UI.button # set UI.text "About"                 # 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 "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+       tab6 <- UI.button # set UI.text "Stats"                 # 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,tab6,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,tab6]; return tab # set UI.style activeTab         help <- guiHelp # set UI.style [("margin-top","0.5em")]        on UI.click tab1 $ \_ -> do@@ -81,12 +85,16 @@             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")]+            pane <- guiAssisted traceRef 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 tab6 $ \_ -> do+            coloActive tab6+            pane <- guiStats compTreeRef+            UI.getBody window # set UI.children [tabs,pane]         UI.getBody window # set UI.style [("margin","0")] #+ (map return [tabs,help])        return ()@@ -112,6 +120,31 @@   ]   --------------------------------------------------------------------------------+-- The statistics GUI++guiStats :: IORef CompTree -> UI UI.Element+guiStats compTreeRef = do+  (Graph _ vs as) <- UI.liftIO $ readIORef compTreeRef++  sec1   <- UI.h3 # set UI.text "Computation Tree Statistics"+  -- Minus 1 for the root node+  vcount <- UI.div # set UI.text (show ((length vs) - 1) ++ " computation statements")+  -- TODO: Should we subtract the dependencies from the root node?+  acount <- UI.div # set UI.text (show (length as) ++ " dependencies")++  sec2   <- UI.h3 # set UI.text "Judgements"+  -- Minus 1 for the root node that is always considered as right+  rightCount <- UI.div # set UI.text ((show $ (length . filter isRight $ vs) - 1) ++ " Right")+  wrongCount <- UI.div # set UI.text ((show . length . filter isWrong      $ vs) ++ " Wrong")+  assCount   <- UI.div # set UI.text ((show . length . filter isAssisted   $ vs) ++ " Assisted")+  incon      <- UI.div # set UI.text ((show . length . filter isInconclusive $ vs) ++ " Inconclusive") # set UI.style [("margin-left","2em")]++  passing    <- UI.div # set UI.text ((show . length . filter isPassing $ vs) ++ " Passing") # set UI.style [("margin-left","2em")]+  unassCount <- UI.div # set UI.text ((show . length . filter isUnassessed $ vs) ++ " Unassessed")++  UI.div # set UI.style [("margin-left", "20%"),("margin-right", "20%")] #+ (map return [sec1,vcount,acount, sec2, rightCount, wrongCount, assCount, incon, passing, unassCount])++-------------------------------------------------------------------------------- -- The observe GUI  guiObserve :: IORef CompTree -> IORef Int -> UI UI.Element@@ -166,8 +199,12 @@     i <- UI.liftIO $ readIORef currentVertexRef     s <- UI.span # set UI.text (vertexRes v)     r <- UI.input # set UI.type_ "radio" # set UI.checked (i == vertexUID v)+    let src | isRight v = "static/right.png"+            | isWrong v = "static/wrong.png"+            | otherwise = "static/unassessed.png"+    j <- UI.img # set UI.src src # set UI.height 20 # set UI.style [("margin-left","1em")]     on UI.checkedChange r $ \_ -> checked v-    UI.div #+ [return r, return s]+    UI.div #+ map return [r,s,j]    checked v = do     UI.liftIO $ writeIORef currentVertexRef (vertexUID v)@@ -176,10 +213,10 @@ -------------------------------------------------------------------------------- -- 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+guiAssisted :: IORef Trace -> [Propositions] -> IORef CompTree -> IORef Int -> IORef String -> IORef Int -> UI UI.Element+guiAssisted traceRef ps compTreeRef currentVertexRef regexRef imgCountRef = do -       handlerRef <- UI.liftIO $ newIORef Abort+       handlerRef <- UI.liftIO $ newIORef Bottom         -- Get a list of vertices from the computation tree        tree <- UI.liftIO $ readIORef compTreeRef@@ -199,12 +236,13 @@        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")]+       -- testAllB  <- UI.button # set UI.text "test all"                                         # set UI.height 30 # set UI.style [("margin-right","1em")]        resetB <- UI.button # set UI.text "clear all judgements"                                # set UI.height 30-       on UI.click testAllB $ \_ -> testAll compTreeRef trace ps status currentVertexRef compStmt handlerRef-       on UI.click testB $ \_ -> testCurrent compTreeRef trace ps status currentVertexRef compStmt handlerRef+       -- on UI.click 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 +       -- 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@@ -217,12 +255,12 @@             UI.liftIO $ writeIORef handlerRef h             return a # set UI.checked False             return b # set UI.checked False-       onCheck r1 r2 r3 Abort+       onCheck r1 r2 r3 Bottom        onCheck r2 r1 r3 Forall-       onCheck r3 r1 r2 TrustForall+       -- onCheck r3 r1 r2 TrustForall         -- Populate the main screen-       top <- UI.center #+ [return status, UI.br, return right, return wrong, return testB, return testAllB, return resetB]+       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]  resetTree compTreeRef ps status currentVertexRef compStmt = do@@ -231,6 +269,7 @@   advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef   where resetVertex = flip setJudgement Unassessed +{- testAll compTreeRef trace ps status currentVertexRef compStmt handlerRef = do   return status # UI.set UI.text "Evaluating propositions ..." #+ [UI.img # set UI.src "static/loading.gif" # set UI.height 30]   UI.liftIO $ do@@ -239,8 +278,9 @@     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 handlerRef = do+testCurrent compTreeRef traceRef ps status currentVertexRef compStmt handlerRef = do   return status # UI.set UI.text "Evaluating propositions ..." #+ [UI.img # set UI.src "static/loading.gif" # set UI.height 30]   mcv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef   case mcv of@@ -248,10 +288,16 @@       case lookupPropositions ps cv of          Nothing  -> updateStatus status compTreeRef         (Just p) -> do-          handler <- UI.liftIO $ readIORef handlerRef-          cv' <- UI.liftIO $ judgeWithPropositions handler trace p cv            compTree <- UI.liftIO $ readIORef compTreeRef-          UI.liftIO $ writeIORef compTreeRef (replaceVertex compTree cv')+          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 @@ -310,24 +356,27 @@   mv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef   case mv of     Nothing  -> do-      return ()+      t <- UI.liftIO $ readIORef compTreeRef+      case next_step 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-      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)-      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)+      case (adv, next_step 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+  updateStatus status compTreeRef  +advanceTo w status compStmt mMenu mImg currentVertexRef compTreeRef = do+  UI.liftIO $ writeIORef currentVertexRef (vertexUID w)+  showStmt compStmt compTreeRef currentVertexRef+  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 @@ -346,7 +395,7 @@        compStmt <- UI.pre         -- Menu to select which statement to show-       menu <- UI.select+       menu <- UI.select # set UI.style [("margin-right","1em")]        showStmt compStmt compTreeRef currentVertexRef        updateMenu menu compTreeRef currentVertexRef         let selectVertex' = selectVertex compStmt menu compTreeRef currentVertexRef (redrawWith img imgCountRef compTreeRef)@@ -357,18 +406,41 @@        updateStatus status compTreeRef          -- 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 20]-       wrong <- UI.button # set UI.text "wrong "    #+ [UI.img # set UI.src "static/wrong.png" # set UI.height 20]+       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        j right Right        j wrong Wrong +       -- Store and restore buttons+       storeb   <- UI.button # UI.set UI.text "store" # set UI.style [("margin-right","1em")]+       restoreb <- UI.button # UI.set UI.text "restore" +       on UI.click storeb $ \_ -> UI.liftIO $ store compTreeRef+       on UI.click restoreb $ \_ -> do UI.liftIO $ restore compTreeRef+                                       updateStatus status compTreeRef+                                       v <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef+                                       redraw img imgCountRef compTreeRef v+        -- Populate the main screen        hr <- UI.hr        br <- UI.br-       UI.div #+ (map UI.element [menu, right, wrong, br, img', br, status, hr, compStmt])+       UI.div #+ (map UI.element [menu, right, wrong, storeb, restoreb, br, hr, img', br, status, hr, compStmt]) +judgementFilePath :: FilePath+judgementFilePath = ".Hoed/savedJudgements" +store :: IORef CompTree -> IO ()+store compTreeRef = do+  t <- readIORef compTreeRef+  storeJudgements judgementFilePath t++restore :: IORef CompTree -> IO ()+restore compTreeRef = do+  t  <- readIORef compTreeRef+  t' <- restoreJudgements judgementFilePath t+  writeIORef compTreeRef t'+ preorder :: CompTree -> [Vertex] preorder = getPreorder . getDfs @@ -378,11 +450,16 @@   let s = case mv of                 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+                              (Assisted s') -> "Results from testing computation statement:\n" ++ (getMessage s') ++ "\n---\n\n" ++ s                               _             -> s   UI.element e # set UI.text s   return () +getMessage :: [AssistedMessage] -> String+getMessage = foldl (\acc m -> acc ++ getMessage' m) ""+getMessage' (InconclusiveProperty msg) = msg+getMessage' (PassingProperty msg) = msg ++ " holds for this statement's values"+ -- populate the exploration menu with the current vertex, its predecessor and its successors updateMenu :: UI.Element -> IORef CompTree -> IORef Int -> UI () updateMenu menu compTreeRef currentVertexRef = do@@ -441,12 +518,6 @@          (===) :: 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
Debug/Hoed/Pure/Observe.lhs view
@@ -144,19 +144,38 @@         default observer :: (Generic a, GObservable (Rep a)) => a -> Parent -> a         observer x c = to (gdmobserver (from x) c) +        constrain :: a -> a -> a+        default constrain :: (Generic a, GConstrain (Rep a)) => a -> a -> a+        constrain x c = to (gconstrain (from x) (from c))+ class GObservable f where         gdmobserver :: f a -> Parent -> f a         gdmObserveChildren :: f a -> ObserverM (f a)         gdmShallowShow :: f a -> String++constrainBase :: Eq a => a -> a -> a+constrainBase x c | x == c = x \end{code} -Creating a shallow representation for types of the Data class.+A type generic definition of constrain  \begin{code}---- shallowShow :: Constructor c => t c (f :: * -> *) a -> [Char]--- shallowShow = conName-+class GConstrain f where gconstrain :: f a -> f a -> f a+instance (GConstrain a, GConstrain b) => GConstrain (a :+: b) where+  gconstrain (L1 x) (L1 c) = L1 (gconstrain x c)+  gconstrain (R1 x) (R1 c) = R1 (gconstrain x c)+instance (GConstrain a, GConstrain b) => GConstrain (a :*: b) where+  gconstrain (x :*: y) (c :*: d) = (gconstrain x c) :*: (gconstrain y d)+instance GConstrain U1 where+  gconstrain x c = x+instance (Observable a) => GConstrain (K1 i a) where+  gconstrain (K1 x) (K1 c) = K1 (constrain x c)+instance (GConstrain a) => GConstrain (M1 D d a) where+  gconstrain (M1 x) (M1 c) = M1 (gconstrain x c)+instance (GConstrain a, Selector s) => GConstrain (M1 S s a) where+  gconstrain m@(M1 x) n@(M1 c) | selName m ==  selName n = M1 (gconstrain x c)+instance (GConstrain a, Constructor c) => GConstrain (M1 C c a) where+  gconstrain m@(M1 x) n@(M1 c) | conName m == conName n = M1 (gconstrain x c) \end{code}  Observing the children of Data types of kind *.@@ -222,6 +241,7 @@ \begin{code} instance (Observable a,Observable b) => Observable (a -> b) where   observer fn cxt arg = gdmFunObserver cxt fn arg+  constrain = error "how to constrain the function type?" \end{code}  Observing the children of Data types of kind *->*.@@ -249,7 +269,7 @@ observeTempl s = do n  <- methodName s                     let f  = return $ VarE n                         s' = stringE s-                    [| (\x-> fst (gobserve $f DoNotTraceThreadId $s' x)) |]+                    [| (\x-> fst (gobserve $f $s' x)) |] \end{code}  Generate class definition and class instances for list of types.@@ -715,14 +735,20 @@  The Haskell Base types  \begin{code}-instance Observable Int         where { observer = observeBase }-instance Observable Bool        where { observer = observeBase }-instance Observable Integer     where { observer = observeBase }-instance Observable Float       where { observer = observeBase }-instance Observable Double      where { observer = observeBase }-instance Observable Char        where { observer = observeBase }--instance Observable ()          where { observer = observeOpaque "()" }+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  = observeOpaque "()"+                                  constrain = constrainBase  -- utilities for base types. -- The strictness (by using seq) is the same @@ -773,6 +799,7 @@   observer arr = send "array" (return Array.array << Array.bounds arr                                                    << Array.assocs arr                               )+  constrain = undefined \end{code}  IO monad.@@ -782,6 +809,7 @@   observer fn cxt =          do res <- fn            send "<IO>" (return return << res) cxt+  constrain = undefined \end{code}  @@ -791,12 +819,15 @@ \begin{code} instance Observable SomeException where   observer e = send ("<Exception> " ++ show e) (return e)+  constrain = undefined  -- instance Observable ErrorCall where --   observer (ErrorCall a)        = send "ErrorCall"   (return ErrorCall << a)  -instance Observable Dynamic where { observer = observeOpaque "<Dynamic>" }+instance Observable Dynamic where+  observer = observeOpaque "<Dynamic>"+  constrain = undefined \end{code}  @@ -903,8 +934,8 @@ -- 'observe' can also observe functions as well a structural values. --  {-# NOINLINE gobserve #-}-gobserve :: (a->Parent->a) -> TraceThreadId -> String -> a -> (a,Int)-gobserve f tti name a = generateContext f tti name a+gobserve :: (a->Parent->a) -> String -> a -> (a,Int)+gobserve f name a = generateContext f name a  {- |  Functions which you suspect of misbehaving are annotated with observe and@@ -937,11 +968,7 @@ -} {-# NOINLINE observe #-} observe ::  (Observable a) => String -> a -> a-observe lbl = fst . (gobserve observer DoNotTraceThreadId lbl)--{-# NOINLINE observeCC #-}-observeCC ::  (Observable a) => String -> a -> a-observeCC lbl = fst . (gobserve observer TraceThreadId lbl)+observe lbl = fst . (gobserve observer lbl)  {- This gets called before observer, allowing us to mark  - we are entering a, before we do case analysis on@@ -972,22 +999,14 @@ \end{code}  \begin{code}-data TraceThreadId = TraceThreadId | DoNotTraceThreadId--generateContext :: (a->Parent->a) -> TraceThreadId -> String -> a -> (a,Int)-generateContext f tti label orig = unsafeWithUniq $ \node ->-     do { t <- myThreadId-        ; sendEvent node (Parent 0 0) (Observe label t node)-        ; return (observer_ f orig (Parent-                        { parentUID      = node-                        , parentPosition = 0-                        })-                 , node)-        }-  where myThreadId = case tti of-          DoNotTraceThreadId -> return ThreadIdUnknown-          TraceThreadId      -> do t <- Concurrent.myThreadId-                                   return (ThreadId t)+generateContext :: (a->Parent->a) -> String -> a -> (a,Int)+generateContext f {- tti -} label orig = unsafeWithUniq $ \node ->+     do sendEvent node (Parent 0 0) (Observe label node)+        return (observer_ f orig (Parent+                      { parentUID      = node+                      , parentPosition = 0+                      })+               , node)  send :: String -> ObserverM a -> Parent -> a send consLabel fn context = unsafeWithUniq $ \ node ->@@ -1046,22 +1065,22 @@                 , eventParent  :: !Parent                 , change       :: !Change                 }-        deriving (Eq)+        deriving (Eq,Generic)  data Change-        = Observe       !String         !ThreadId        !Int+        = Observe       !String        !Int         | Cons    !Int  !String         | Enter         | NoEnter         | Fun-        deriving (Eq, Show)+        deriving (Eq, Show,Generic)  type ParentPosition = Int  data Parent = Parent         { parentUID      :: !UID            -- my parents UID         , parentPosition :: !ParentPosition -- my branch number (e.g. the field of a data constructor)-        } deriving (Eq)+        } deriving (Eq,Generic)  instance Show Event where   show e = (show . eventUID $ e) ++ ": " ++ (show . change $ e) ++ " (" ++ (show . eventParent $ e) ++ ")"@@ -1070,10 +1089,6 @@   show p = "P " ++ (show . parentUID $ p) ++ " " ++ (show . parentPosition $ p)  root = Parent 0 0--data ThreadId = ThreadIdUnknown | ThreadId Concurrent.ThreadId-        deriving (Show,Eq,Ord)-  isRootEvent :: Event -> Bool isRootEvent e = case change e of Observe{} -> True; _ -> False
Debug/Hoed/Pure/Prop.hs view
@@ -8,13 +8,14 @@ -- ( judge -- , Propositions(..) -- ) where-import Debug.Hoed.Pure.Observe(Trace(..),UID,Event(..),Change(..),ourCatchAllIO,evaluate)+import Debug.Hoed.Pure.Observe(Observable(..),Trace(..),UID,Event(..),Change(..),ourCatchAllIO,evaluate) import Debug.Hoed.Pure.Render(CompStmt(..),noNewlines)-import Debug.Hoed.Pure.CompTree(CompTree,Vertex(..),Graph(..),vertexUID)+import Debug.Hoed.Pure.CompTree(CompTree,Vertex(..),Graph(..),vertexUID,vertexRes,replaceVertex,getJudgement,setJudgement) import Debug.Hoed.Pure.EventForest(EventForest,mkEventForest,dfsChildren)+import Debug.Hoed.Pure.Serialize import qualified Data.IntMap as M import Prelude hiding (Right)-import Data.Graph.Libgraph(Judgement(..),mapGraph)+import Data.Graph.Libgraph(Judgement(..),AssistedMessage(..),mapGraph) import System.Directory(createDirectoryIfMissing) import System.Process(system) import System.Exit(ExitCode(..))@@ -24,40 +25,63 @@ import Data.Maybe(isNothing,fromJust) import Data.List(intersperse,isInfixOf) import GHC.Generics hiding (moduleName) --(Generic(..),Rep(..),from,(:+:)(..),(:*:)(..),U1(..),K1(..),M1(..))+import Control.Monad(foldM)  ------------------------------------------------------------------------------------------------------------------------  data Propositions = Propositions { propositions :: [Proposition], propType :: PropType, funName :: String                                  , extraModules :: [Module]-                                 } +                                 } -data PropType     = Specify | PropertiesOf deriving Eq+data PropType = Specify | PropertiesOf deriving Eq -type Proposition  = (PropositionType,Module,String,[Int])+data Signature +  = Argument Int+  | SubjectFunction+  | Random+  deriving Show -data PropositionType = BoolProposition | LegacyQuickCheckProposition | QuickCheckProposition deriving Show+type Proposition = (PropositionType,Module,String,[Signature]) -data Module       = Module {moduleName :: String, searchPath :: String} deriving Show+data PropositionType +  = IOProposition+  | BoolProposition+  | LegacyQuickCheckProposition+  | QuickCheckProposition +  deriving Show +data Module = Module {moduleName :: String, searchPath :: String} +  deriving Show++data PropRes +  = Error Proposition String +  | Hold Proposition +  | HoldWeak Proposition+  | Disprove Proposition+  | DisproveBy Proposition [String] +  deriving Show+ propositionType :: Proposition -> PropositionType propositionType (x,_,_,_) = x  propName :: Proposition -> String propName (_,_,x,_) = x -argMap :: Proposition -> [Int]-argMap (_,_,_,x) = x+signature :: Proposition -> [Signature]+signature (_,_,_,x) = x  propModule :: Proposition -> Module propModule (_,x,_,_) = x  ------------------------------------------------------------------------------------------------------------------------ -sourceFile = ".Hoed/exe/Main.hs"-buildFiles = ".Hoed/exe/Main.o .Hoed/exe/Main.hi"-exeFile    = ".Hoed/exe/Main"-outFile    = ".Hoed/exe/Main.out"-errFile    = ".Hoed/exe/Main.compilerMessages"+sourceFile   = ".Hoed/exe/Main.hs"+buildFiles   = ".Hoed/exe/Main.o .Hoed/exe/Main.hi"+exeFile      = ".Hoed/exe/Main"+outFile      = ".Hoed/exe/Main.out"+errFile      = ".Hoed/exe/Main.compilerMessages"+treeFilePath = ".Hoed/savedCompTree."+traceFilePath = ".Hoed/savedTrace."  ------------------------------------------------------------------------------------------------------------------------ @@ -73,135 +97,216 @@  ------------------------------------------------------------------------------------------------------------------------ -judge :: UnevalHandler -> Trace -> [Propositions] -> CompTree -> IO CompTree-judge handler trc ps compTree = do-  ws <- mapM j vs-  return $ foldl updateTree compTree ws-  where -  vs  = vertices compTree-  j v = case lookupPropositions ps v of -    Nothing  -> return v-    (Just p) -> judgeWithPropositions handler trc p v-  updateTree compTree w = mapGraph (\v -> if (vertexUID v) == (vertexUID w) then w else v) compTree --- Use a property to judge a vertex-judgeWithPropositions :: UnevalHandler -> Trace -> Propositions -> Vertex -> IO Vertex-judgeWithPropositions _ _ _ RootVertex = return RootVertex-judgeWithPropositions handler trc p v = do-  putStrLn $ "\n================\n"-  pas' <- mapM (evalProposition unevalGen trc v (extraModules p)) (propositions p)-  putStrLn $ "judgeWithPropositions: pas=" ++ show pas'-  let pas = if handler == TrustForall then trustWeak pas' else weaken pas'-      z = zip pas (propositions p)-      a = case (map snd) . (filter (holds . fst)) $ z of-            [] -> errorMessages z-            ps -> "With passing properties: " ++ commas (map propName ps) ++ "\n" ++ (errorMessages z)-      j' | propType p == Specify && all hasResult pas-                                       = if any disproves pas then Wrong else Right-         | any hasResult pas           = if any disproves pas then Wrong else Assisted a-         | otherwise                   = Assisted a-      j  | j' `moreInfo` (vertexJmt v) = j'-         | otherwise                   = vertexJmt v+data Judge +  = Judge Judgement+    -- ^ Returns a Judgement (see Libgraph library).+  | AlternativeTree CompTree Trace+    -- ^ Found counter example with simpler computation tree. -  hPutStrLn stderr $ "Judgement was " ++ (show . vertexJmt) v ++ ", and is now " ++ show j-  return v{vertexJmt=j}+judgeAll :: UnevalHandler -> (CompTree -> Int) -> Trace -> [Propositions] -> CompTree -> IO CompTree+judgeAll handler complexity trc ps compTree = foldM f compTree (vertices compTree)   where-  unevalGen = unevalHandler handler-  commas :: [String] -> String-  commas = concat . (intersperse ", ")+  c = complexity compTree+  f :: CompTree -> Vertex -> IO CompTree+  f curTree v = do+    putStrLn $ take 50 (cycle "-")+    putStrLn $ "Evaluating properties to judge statement: " ++ vertexRes v+    putStrLn $ take 50 (cycle "-")+    case lookupPropositions ps v of+      Nothing  -> do+        putStrLn "*** no propositions"+        return curTree+      (Just p) -> do+        j <- judge' Bottom trc p v complexity curTree+        case j of+          (Judge jmt)            -> do+            putStrLn $ "*** judgement is " ++ show jmt+            return $ replaceVertex curTree (setJudgement v jmt)+          (AlternativeTree t' _) -> do+             let msg = "Simpler tree suggested with complexity " ++ show (complexity t') +                       ++ "(current tree has complexity of " ++ show c ++ ")"+             putStrLn $ "*** " ++ msg+             return $ replaceVertex curTree (setJudgement v (Assisted [InconclusiveProperty msg])) -  moreInfo _          Unassessed   = True-  moreInfo Unassessed (Assisted _) = False-  moreInfo _          (Assisted _) = True-  moreInfo _          Right        = False-  moreInfo _          Wrong        = False+-- 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. -data UnevalHandler = Abort | Forall | TrustForall deriving (Eq, Show)+-- |Use propositions to judge a computation statement.+-- First tries restricted and bottom for unevaluated expressions,+-- then unrestricted and random 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 -unevalHandler :: UnevalHandler -> PropVarGen String-unevalHandler Abort = propVarError-unevalHandler _     = propVarFresh+judge' Bottom trc p v complexity curTree = do+  pas <- evalPropositions Bottom trc p v+  let j | propType p == Specify && all holds pas  = (Judge Right)+        | any disproves pas                       = (Judge Wrong)+        | otherwise                               = advice pas+  return j -data PropApp = Error String | Holds | HoldsWeak | Disproves deriving Show+judge' Forall trc p v complexity curTree = do+  pas <- evalPropositions Forall trc p v+  let j | propType p == Specify && all holds pas  = return (Judge Right)+        | any disproves pas                       = do +            let curComplexity = complexity curTree+            (bestComplexity,bestTree,bestTrace) <- simplestTree complexity (extraModules p) pas (curComplexity,curTree,[]) trc v+            if bestComplexity == curComplexity+              then return $ Judge $ Assisted $ [InconclusiveProperty $ "We found values for the unevaluated "+                                                ++ "expressions in the current statement that falsify\n"+                                                ++ "a property, however the resulting tree is not simpler."]+              else return (AlternativeTree bestTree bestTrace)+        | otherwise = return (advice pas)+  j -trustWeak :: [PropApp] -> [PropApp]-trustWeak = map f-  where f HoldsWeak = Holds -- A possible unsafe assumption-        f p         = p+holds :: PropRes -> Bool+holds (Hold _) = True+holds (HoldWeak _) = True+holds _         = False -weaken :: [PropApp] -> [PropApp]-weaken = map f-  where f HoldsWeak = Error "Holds for all randomly generated values we tried."-        f p         = p+disproves :: PropRes -> Bool+disproves (Disprove _)     = True+disproves (DisproveBy _ _) = True+disproves _                = False -hasResult :: PropApp -> Bool-hasResult (Error _) = False-hasResult HoldsWeak = False-hasResult _         = True+disprovesBy :: PropRes -> Bool+disprovesBy (DisproveBy _ _) = True+disprovesBy _                = False -hasWeakResult :: PropApp -> Bool-hasWeakResult (Error _)     = False-hasWeakResult _             = True+-- 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) -holds :: PropApp -> Bool-holds Holds = True-holds _     = False+-- 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.+-- Return whichever of these two trees is simplest.+simple2 :: (CompTree -> Int)  -> Trace -> Vertex -> [Module] -> (Int,CompTree,Trace) -> PropRes -> IO (Int,CompTree,Trace)+simple2 complexity trc v ms (curComplexity,curTree,curTrace) propRes = do+  reEvalProposition propRes trc v ms+  maybeCandTree  <- restoreTree  $ treeFilePath  ++ resOf propRes+  maybeCandTrace <- restoreTrace $ traceFilePath ++ resOf propRes+  case (maybeCandTree,maybeCandTrace) of+    (Just candTree, Just candTrace) -> do +      let candComplexity = complexity candTree+      return $ if candComplexity < curComplexity +                 then (candComplexity,candTree,candTrace)+                 else (curComplexity,curTree,curTrace)+    _ -> do+      putStrLn $ "FAILED to to restore computation tree of " ++ resOf propRes+      return (curComplexity,curTree,curTrace) -disproves :: PropApp -> Bool-disproves Disproves = True-disproves _         = False+advice :: [PropRes] -> Judge+advice rs' = case filter holds rs' of+  [] -> Judge $ Assisted $ errorMessages rs'+  rs -> Judge $ Assisted $ PassingProperty (commas (map resOf rs)) : errorMessages rs' -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)+commas :: [String] -> String+commas = concat . (intersperse ", ") -evalProposition :: PropVarGen String -> Trace -> Vertex -> [Module] -> Proposition -> IO PropApp-evalProposition unevalGen trc v ms prop = do+errorMessages :: [PropRes] -> [AssistedMessage]+errorMessages = foldl (\acc (Error prop msg) -> InconclusiveProperty ("\n---\n\nApplying property " ++ propName prop ++ " gives inconclusive result:\n\n" ++ msg) : acc) [] . filter isError++isError (Error _ _) = True+isError _           = False++data UnevalHandler = Bottom | Forall | FromList [String] deriving (Eq, Show)++unevalHandler :: UnevalHandler -> PropVarGen String+unevalHandler Bottom       = propVarError+unevalHandler Forall       = propVarFresh+unevalHandler (FromList _) = propVarFresh++unevalState :: UnevalHandler -> PropVars+unevalState Bottom            = propVars0+unevalState Forall            = propVars0+-- unevalState (FromList _)      = propVars0+-- Replace last line with +unevalState (FromList values) = ([],values)+-- to directly substitute unevaluated expressions with the FromList values.+-- This is only valid when all randomly generated values are actually substituting+-- unevaluated expressions (this is not always the case, consider e.g. testing f in+-- quickCheck p where p f x y = f x == g x y)++resOf :: PropRes -> String+resOf (Error p _)      = propName p+resOf (Hold p)         = propName p+resOf (HoldWeak p)     = propName p+resOf (Disprove p)     = propName p+resOf (DisproveBy p _) = propName p++evalPropositions :: UnevalHandler -> Trace -> Propositions -> Vertex -> IO [PropRes]+evalPropositions _ _ _ RootVertex = return []+evalPropositions handler trc p v = mapM (evalProposition handler trc v (extraModules p)) (propositions p)++evalProposition :: UnevalHandler -> Trace -> Vertex -> [Module] -> Proposition -> IO PropRes+evalProposition handler trc v ms prop = do+  putStrLn $ "property " ++ propName prop   createDirectoryIfMissing True ".Hoed/exe"-  hPutStrLn stderr $ "Evaluating proposition " ++ propName prop ++ " with statement " ++ (shorten . noNewlines . show . vertexStmt) v   clean-  prgm <- generateCode-  compile-  exit' <- compile-  err  <- readFile errFile-  hPutStrLn stderr $ err-  hPutStrLn stderr $ "Compilation exitted with " ++ show exit'-  case exit' of -    (ExitFailure _) -> return $ Error $ "Compilation of {{{\n" ++ prgm ++ "\n}}} failed with:\n" ++ err+  prgm <- generateCode handler trc v prop ms+  compile prop+  exit <- compile prop+  case exit of +    (ExitFailure _) -> do+        err  <- readFile errFile+        putStrLn $ "failed to compile: " ++ err+        return $ Error prop $ "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  , "+++ OK, passed 100 tests.\n") -> HoldsWeak-        (ExitSuccess  , "False\n") -> Disproves-        (ExitSuccess  , _)         -> if "Failed! Falsifiable" `isInfixOf` out-                                        then Disproves-                                        else Error out+      exit <- run+      out <- readFile outFile+      putStrLn $ "evaluated to: " ++ out+      return $ mkPropRes prop exit (backspaces 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 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 -    shorten s-      | length s < 120 = s-      | otherwise    = (take 117 s) ++ "..."+reEvalProposition :: PropRes -> Trace -> Vertex -> [Module] -> IO PropRes+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"+  return (Disprove p) -    getEvent :: UID -> Event-    getEvent j = fromJust $ M.lookup j m-      where m = M.fromList $ map (\e -> (eventUID e, e)) trc+clean = system $ "rm -f " ++ sourceFile ++ " " ++ exeFile ++ " " ++ buildFiles +compile prop = system $ "ghc  -i" ++ (searchPath . propModule) prop ++ " -o " ++ exeFile ++ " " ++ sourceFile ++ " > " ++ errFile ++ " 2>&1"++run = system $ exeFile ++ " > " ++ outFile ++ " 2>&1"++generateCode :: UnevalHandler -> Trace -> Vertex -> Proposition -> [Module] -> IO String+generateCode handler trc v prop ms = 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 = generate handler prop ms trc (getEventFromMap $ eventMap trc) i f+  i    = (stmtIdentifier . vertexStmt) v+  f    = (stmtLabel . vertexStmt) v+++getEventFromMap m j = fromJust $ M.lookup j m++eventMap trc = M.fromList $ map (\e -> (eventUID e, e)) trc++mkPropRes :: Proposition -> ExitCode -> String -> PropRes+mkPropRes prop (ExitFailure _) out        = Error prop out+mkPropRes prop ExitSuccess out+  | out == "True\n"                       = Hold prop+  | out == "+++ OK, passed 100 tests.\n"  = HoldWeak prop+  | out == "False\n"                      = Disprove prop+  | "Failed! Falsifiable" `isInfixOf` out = DisproveBy prop (reverse . tail . lines $ out)+  | otherwise                             = Error prop out++shorten s+  | length s < 120 = s+  | otherwise    = (take 117 s) ++ "..."+ backspaces :: String -> String backspaces s = reverse (backspaces' [] s)   where@@ -213,21 +318,6 @@   safeTail []    = []   safeTail (c:s) = s --- The actual logic that changes the judgement of a vertex.-judge1' :: ExitCode -> String -> Judgement -> Judgement-judge1' (ExitFailure _) _   j = j-judge1' ExitSuccess     out j-  | out == "False\n" = Wrong-  | out == "True\n"  = j-  | otherwise     = j--judge1_spec :: ExitCode -> String -> Judgement -> Judgement-judge1_spec (ExitFailure _) _   j = j-judge1_spec ExitSuccess     out j-  | out == "False\n" = Wrong-  | out == "True\n"  = Right-  | otherwise     = j- ------------------------------------------------------------------------------------------------------------------------  type PropVars = ([String],[String]) -- A tuple of used variables, and a supply of fresh variables@@ -254,33 +344,36 @@ propVarReturn :: String -> PropVarGen String propVarReturn s vs = (s,vs) -propVarBind :: (String,PropVars) -> Proposition -> String-propVarBind (propApp,([],_))  prop = generatePrint prop ++ " $ " ++ propApp-propVarBind (propApp,(bvs,_)) prop = "quickCheck (\\" ++ bvs' ++ " -> " ++ propApp ++ ")"+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 ++ ")"   where   bvs' = concat (intersperse " " bvs)  generatePrint :: Proposition -> String generatePrint p = case propositionType p of-  BoolProposition       -> "print"-  QuickCheckProposition -> "(\\q -> do MkRose res ts <- protectRose .reduceRose .  unProp . (\\p->unGen p  (mkQCGen 1) 1) . unProperty $ q; print . fromJust . ok $ res)"-  LegacyQuickCheckProposition -> "do g <- newStdGen; print . fromJust . ok . (generate 1 g) . evaluate"+  IOProposition         -> ""+  BoolProposition       -> "print $ "+  QuickCheckProposition -> "(\\q -> do MkRose res ts <- reduceRose .  unProp . (\\p->unGen p  (mkQCGen 1) 1) . unProperty $ q; print . fromJust . ok $ res) $ "+  LegacyQuickCheckProposition -> "do g <- newStdGen; print . fromJust . ok . (generate 1 g) . evaluate $ "  ------------------------------------------------------------------------------------------------------------------------ -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+generate :: UnevalHandler -> Proposition -> [Module ] -> Trace -> (UID->Event) -> UID -> String -> String+generate handler prop ms trc getEvent i f = generateHeading prop ms ++ generateMain handler prop trc getEvent i f  generateHeading :: Proposition -> [Module] -> String generateHeading prop ms =   "-- This file is generated by the Haskell debugger Hoed\n"   ++ generateImport (propModule prop)+  ++ generateImport (Module "qualified Debug.Hoed.Pure as Hoed" [])   ++ qcImports   ++ foldl (\acc m -> acc ++ generateImport m) "" ms-   where   qcImports = case propositionType prop of-        BoolProposition -> []+        BoolProposition -> generateImport (Module "Test.QuickCheck" [])+        IOProposition   -> generateImport (Module "Test.QuickCheck" [])         LegacyQuickCheckProposition -> qcImports'         QuickCheckProposition -> qcImports'                                  ++ generateImport (Module "Test.QuickCheck.Property" [])@@ -289,24 +382,59 @@   qcImports'     = generateImport (Module "System.Random" [])             -- newStdGen       ++ generateImport (Module "Data.Maybe" [])             -- fromJust+      ++ generateImport (Module "Test.QuickCheck" [])  generateImport :: Module -> String generateImport m =  "import " ++ (moduleName m) ++ "\n" -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"+generateMain :: UnevalHandler -> Proposition -> Trace -> (UID->Event) -> UID -> String -> String+generateMain handler prop trc getEvent i f+  = "main = Hoed.runOstore \"" ++ (propName prop) ++"\" $ "+            ++ propVarBind handler (foldl accSig ((propName prop) ++ " ",unevalState handler) (signature prop)) prop+            -- ++ appValues handler+            ++ "\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+    -- appValues (FromList values) = concat (map (" "++) values)+    -- appValues _                 = ""+    accSig :: (String,PropVars) -> Signature -> (String,PropVars)+    accSig (acc,propVars) x = let (s,propVars') = getSig x propVars in (acc ++ " " ++ s, propVars')+    getSig :: Signature -> PropVarGen String+    getSig SubjectFunction = cf+    getSig (Argument i) | i < length args = args !! i+    -- MF TODO: should we do something better when user gives index that is out of bounds?+    getSig Random = propVarFresh+    getSig _ = propVarError      args :: [PropVarGen String]-    args = generateArgs unevalGen trc getEvent i+    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 $ ")"+                            ]+       | 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' :: 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)+ 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@@ -314,7 +442,7 @@   xs             -> error ("generateArgs: dfsChildren (" ++ show e ++ ") = " ++ show xs)   where   frt = (mkEventForest trc)-  e   = getEvent i -- (reverse trc) !! (i-1)+  e   = getEvent i  moreArgs :: PropVarGen String -> Trace -> (UID->Event) -> Maybe Event -> [PropVarGen String] moreArgs _ trc getEvent Nothing = []@@ -337,7 +465,20 @@   where cs :: [PropVarGen String]         cs = map (generateExpr unevalGen frt) (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)"+  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 ...  class ParEq a where   (===) :: a -> a -> Maybe Bool
Debug/Hoed/Pure/Render.hs view
@@ -1,7 +1,7 @@ -- This file is part of the Haskell debugger Hoed. -- -- Copyright (c) Maarten Faddegon, 2014-{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP, DeriveGeneric #-}  module Debug.Hoed.Pure.Render (CompStmt(..)@@ -25,6 +25,7 @@ import Data.Graph.Libgraph import Data.Array as Array import Data.Char(isAlpha)+import GHC.Generics  #if __GLASGOW_HASKELL__ < 710 sortOn :: Ord b => (a -> b) -> [a] -> [a]@@ -48,7 +49,7 @@                          , stmtIdentifier :: UID                          , stmtRes        :: String                          }-                deriving (Eq, Ord)+                deriving (Eq,Ord,Generic)  instance Show CompStmt where   show = stmtRes@@ -72,7 +73,7 @@ -- is rendered to a computation statement  renderCompStmt :: CDS -> [CompStmt]-renderCompStmt (CDSNamed name threadId dependsOn set)+renderCompStmt (CDSNamed name dependsOn set)   = map mkStmt statements   where statements :: [(String,UID)]         statements   = map (\(d,i) -> (pretty 70 d,i)) doc@@ -103,7 +104,7 @@ -- %************************************************************************  -data CDS = CDSNamed      String ThreadId UID CDSSet+data CDS = CDSNamed      String UID CDSSet          | CDSCons       UID    String   [CDSSet]          | CDSFun        UID             CDSSet CDSSet          | CDSEntered    UID@@ -134,8 +135,8 @@      getNode'' ::  Int -> Event -> Change -> CDS      getNode'' node e change =        case change of-        (Observe str t i) -> let chd = getChild node 0-                               in CDSNamed str t (getId chd i) chd+        (Observe str i) -> let chd = getChild node 0+                               in CDSNamed str (getId chd i) chd         (Enter)             -> CDSEntered node         (NoEnter)           -> CDSTerminated node         Fun                 -> CDSFun node (getChild node 0) (getChild node 1)@@ -243,11 +244,11 @@ findFn' other rest = ([],[other], Nothing) : rest  rmEntry :: CDS -> CDS-rmEntry (CDSNamed str t i set)= CDSNamed str t i (rmEntrySet set)-rmEntry (CDSCons i str sets)       = CDSCons i str (map rmEntrySet sets)-rmEntry (CDSFun i a b)             = CDSFun i (rmEntrySet a) (rmEntrySet b)-rmEntry (CDSTerminated i)          = CDSTerminated i-rmEntry (CDSEntered i)             = error "found bad CDSEntered"+rmEntry (CDSNamed str i set) = CDSNamed str i (rmEntrySet set)+rmEntry (CDSCons i str sets) = CDSCons i str (map rmEntrySet sets)+rmEntry (CDSFun i a b)       = CDSFun i (rmEntrySet a) (rmEntrySet b)+rmEntry (CDSTerminated i)    = CDSTerminated i+rmEntry (CDSEntered i)       = error "found bad CDSEntered"  rmEntrySet = map rmEntry . filter noEntered   where@@ -255,7 +256,7 @@         noEntered _              = True  simplifyCDS :: CDS -> CDS-simplifyCDS (CDSNamed str t i set) = CDSNamed str t i (simplifyCDSSet set)+simplifyCDS (CDSNamed str i set) = CDSNamed str i (simplifyCDSSet set) simplifyCDS (CDSCons _ "throw"                   [[CDSCons _ "ErrorCall" set]]             ) = simplifyCDS (CDSCons 0 "error" set)@@ -296,7 +297,7 @@ cdssToOutput :: CDSSet -> [Output] cdssToOutput =  map cdsToOutput -cdsToOutput (CDSNamed name _ _ cdsset)+cdsToOutput (CDSNamed name _ cdsset)             = OutLabel name res1 res2   where       res1 = [ cdss | (OutData cdss) <- res ]
+ Debug/Hoed/Pure/Serialize.hs view
@@ -0,0 +1,105 @@+-- This file is part of the Haskell debugger Hoed.+--+-- Copyright (c) Maarten Faddegon, 2016+{-# LANGUAGE DeriveGeneric #-}++module Debug.Hoed.Pure.Serialize+( storeJudgements+, restoreJudgements+, storeTree+, restoreTree+, storeTrace+, restoreTrace+) where+import Debug.Hoed.Pure.Observe+import Prelude hiding (lookup,Right)+import qualified Prelude as Prelude+import Debug.Hoed.Pure.CompTree+import Debug.Hoed.Pure.Render(CompStmt(..))+import Data.Serialize+import Data.ByteString (ByteString)+import qualified Data.ByteString as BS+import GHC.Generics+import Data.Graph.Libgraph(Judgement(..),AssistedMessage(..),mapGraph,Graph(..),Arc(..))++--------------------------------------------------------------------------------+-- Derive Serialize instances++instance (Serialize a, Serialize b) => Serialize (Graph a b)+instance (Serialize a, Serialize b) => Serialize (Arc a b)+instance Serialize Vertex+instance Serialize Judgement+instance Serialize AssistedMessage+instance Serialize CompStmt+instance Serialize Parent+instance Serialize Event+instance Serialize Change++--------------------------------------------------------------------------------+-- Tree++storeTree :: FilePath -> CompTree -> IO ()+storeTree fp = (BS.writeFile fp) . encode++restoreTree :: FilePath -> IO (Maybe CompTree)+restoreTree fp = do+        bs <- BS.readFile fp+        case decode bs of+          (Prelude.Left _)   -> return Nothing+          (Prelude.Right x) -> return (Just x)++--------------------------------------------------------------------------------+-- Trace++storeTrace :: FilePath -> Trace -> IO ()+storeTrace fp = (BS.writeFile fp) . encode++restoreTrace :: FilePath -> IO (Maybe Trace)+restoreTrace fp = do+        bs <- BS.readFile fp+        case decode bs of+          (Prelude.Left _)   -> return Nothing+          (Prelude.Right x) -> return (Just x)++--------------------------------------------------------------------------------+-- Judgements++storeJudgements :: FilePath -> CompTree -> IO ()+storeJudgements fp = (BS.writeFile fp) . encode . (foldl insert empty) . vertices++restoreJudgements :: FilePath -> CompTree -> IO CompTree+restoreJudgements fp ct = do+        bs <- BS.readFile fp+        case decode bs of+          (Prelude.Left _)   -> return ct+          (Prelude.Right db) -> return $ mapGraph (restore db) ct++restore :: DB -> Vertex -> Vertex+restore db v = case lookup db v of+  (Just Right) -> setJudgement v Right+  (Just Wrong) -> setJudgement v Wrong+  _            -> v++data DB = DB [(String, Judgement)] deriving (Generic)+instance Serialize DB++empty :: DB+empty = DB []++lookup :: DB -> Vertex -> Maybe Judgement+lookup (DB db) v = Prelude.lookup (key v) db++insert :: DB -> Vertex -> DB+insert (DB db) v = case judgement v of+  Nothing  -> DB db+  (Just j) -> DB ((key v, j) : db)++key :: Vertex -> String+key = vertexRes++judgement :: Vertex -> Maybe Judgement+judgement RootVertex = Nothing+judgement v = case vertexJmt v of+  Right -> Just Right+  Wrong -> Just Wrong+  _     -> Nothing
Debug/Hoed/Stk.hs view
@@ -151,13 +151,12 @@   hPutStrLn stderr "\n=== Statistics ===\n"   let e  = length events       n  = length eqs-      d  = treeDepth ct       b  = fromIntegral (length . arcs $ ct ) / fromIntegral ((length . vertices $ ct) - (length . leafs $ ct))-  hPutStrLn stderr $ "e = " ++ show e-  hPutStrLn stderr $ "n = " ++ show n-  hPutStrLn stderr $ "arc = " ++ show (length . arcs $ ct)-  hPutStrLn stderr $ "d = " ++ show d-  hPutStrLn stderr $ "b = " ++ show b+  hPutStrLn stderr $ show e ++ " events"+  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 "\n=== Debug session === \n"   -- hPutStrLn stderr (showWithStack eqs)
Hoed.cabal view
@@ -1,5 +1,5 @@ name:                Hoed-version:             0.3.4+version:             0.3.5 synopsis:            Lightweight algorithmic debugging. description:     Hoed is a tracer and debugger for the programming language Haskell.@@ -56,6 +56,7 @@                        , Debug.Hoed.Pure.Render                        , Debug.Hoed.Pure.DemoGUI                        , Debug.Hoed.Pure.Prop+                       , Debug.Hoed.Pure.Serialize                        , Paths_Hoed   build-depends:       base >= 4 && <5                        , template-haskell@@ -63,12 +64,13 @@                        , process                        , threepenny-gui == 0.6.*                        , filepath-                       , libgraph == 1.9+                       , libgraph == 1.10                        , RBTree == 0.0.5                        , regex-posix                        , mtl                        , directory                        , FPretty+                       , cereal, bytestring   default-language:    Haskell2010   -- Enable to get some extra warnings.   --   ghc-options:         -fwarn-unused-binds@@ -132,6 +134,23 @@ --   hs-source-dirs:      examples/FPretty__with_properties --   default-language:    Haskell2010 +Executable hoed-examples-Queens__with_properties+  if flag(buildExamples)+    build-depends:       base >= 4 && < 5+                         , Hoed+                         , threepenny-gui+                         , filepath+                         , containers+                         , deepseq+                         , array+                         , QuickCheck+                         , mtl+  else+    buildable: False+  main-is:             Main.hs+  hs-source-dirs:      examples/Queens__with_properties+  default-language:    Haskell2010+ Executable hoed-examples-Rot13   if flag(buildExamples)     build-depends:       base >= 4 && < 5@@ -740,12 +759,14 @@                          , process                          , threepenny-gui == 0.6.*                          , filepath-                         , libgraph == 1.9+                         , libgraph == 1.10                          , RBTree == 0.0.5                          , regex-posix                          , mtl                          , directory                          , FPretty+                         , cereal+                         , bytestring   else     buildable: False   main-is:             Debug/Hoed/Pure/TestParEq.hs
changelog view
@@ -1,3 +1,11 @@+0.3.5 Maarten Faddegon 9 Feb 2016++  * Give more control to restrict properties when used for judging to make approach sound.++0.3.4 Maarten Faddegon 8 Jan 2016++  * Added beta functionality of using properties to judge statements.+ 0.3.3 Maarten Faddegon 6 Dec 2015    * Documentation and additional examples.
examples/CNF_unsound_demorgan__with_properties/Main.hs view
@@ -2,9 +2,10 @@ import CNF import Debug.Hoed.Pure -main = runOwp properties $ print (prop_negin_correct eg)+main = runOwp properties $ print (prop_negin_correct negin eg)   where-  properties = [Propositions [(BoolProposition,cnfModule,"prop_negin_complete",[0]), (BoolProposition,cnfModule,"prop_negin_sound",[0])] Specify "negin" [modQuickCheck]+  properties = [Propositions [ (BoolProposition,cnfModule,"prop_negin_complete",[Argument (-1),Argument 0])+                             , (BoolProposition,cnfModule,"prop_negin_sound",[Argument (-1),Argument 0])]+                             Specify "negin" []                ]   cnfModule     = Module "CNF" "../examples/CNF_unsound_demorgan__with_properties/"-  modQuickCheck = Module "Test.QuickCheck"         ""
examples/Digraph_not_data_invariant__with_properties/Main.hs view
@@ -4,9 +4,11 @@  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]+  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" []                ]   digraphModule = Module "Digraph" "../examples/Digraph_not_data_invariant__with_properties/"-  modQuickCheck = Module "Test.QuickCheck" ""
examples/ExpressionSimplifier/Main2.hs view
@@ -6,8 +6,8 @@ -- main = quickcheck prop_idemSimplify main = testOwp properties 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" []-               , Propositions [(BoolProposition,myModule,"prop_idemSimplify",[0])] PropertiesOf "simplify" []+  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" []                ]   myModule = Module "MyModule" "../examples/ExpressionSimplifier"
examples/Nubsort/Main.hs view
@@ -3,16 +3,16 @@  main = testOwp ps prop_nub_idempotent [2,1,1]   where-  ps = [ Propositions [ (BoolProposition,nubsortModule,"prop_nub_idempotent",[0])-                      , (BoolProposition,nubsortModule,"prop_nub_unique",[0])-                      , (BoolProposition,nubsortModule,"prop_nub_complete",[0])+  ps = [ Propositions [ (BoolProposition,nubsortModule,"prop_nub_idempotent",[Argument 0])+                      , (BoolProposition,nubsortModule,"prop_nub_unique",[Argument 0])+                      , (BoolProposition,nubsortModule,"prop_nub_complete",[Argument 0])                       ] PropertiesOf "nub" []-       , Propositions [ (QuickCheckProposition,nubsortModule,"prop_nubord'_idempotent",[1,0])-                      , (QuickCheckProposition,nubsortModule,"prop_nubord'_unique",[1,0])-                      , (QuickCheckProposition,nubsortModule,"prop_nubord'_complete",[1,0])+       , 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])                       ] PropertiesOf "nubord'" [modQuickCheck]-       , Propositions [ (QuickCheckProposition,nubsortModule,"prop_insert_ordered",[1,0])-                      , (QuickCheckProposition,nubsortModule,"prop_insert_complete",[1,0])+       , Propositions [ (QuickCheckProposition,nubsortModule,"prop_insert_ordered",[Argument 1,Argument 0])+                      , (QuickCheckProposition,nubsortModule,"prop_insert_complete",[Argument 1,Argument 0])                       ] PropertiesOf "insert" [modQuickCheck]        ]   nubsortModule = Module "Nubsort" "../examples/Nubsort/"
+ examples/Queens__with_properties/Main.hs view
@@ -0,0 +1,3 @@+import Queens++main = doit
examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs view
@@ -29,25 +29,25 @@   print . fromJust . ok . (generate 1 g) . evaluate $  prop_shift_win_I 1 'd' myStackSet   where     propositions =-        [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[0])-                      ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0])+        [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[Argument 0])+                      ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[Argument 0])                       ]                       PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] -        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[1,0])+        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[Argument 1,Argument 0])                        ]                         PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] -        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[1,0])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[1,0])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[0,1])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[0,1])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[0,1])+        , 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])                        ]                         PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] -        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[1,0])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[0,1])+        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[Argument 1,Argument 0])+                       , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[Argument 0,Argument 1])                        ]                         PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
examples/afp02Exercises/Compiler__with_properties/Main.hs view
@@ -14,7 +14,7 @@   putStrLn "compiled:"   print (exec (compile prog))   where-  properties = [Propositions [(BoolProposition,modInterpreter,"prop_ifT",[1,0])] PropertiesOf "run" [modSyntax,modValue,modQuickCheck]+  properties = [Propositions [(BoolProposition,modInterpreter,"prop_ifT",[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/"
tests/Generic/r0.hs view
@@ -5,6 +5,7 @@  instance Observable D where   observer (D x) = send "D" $ return D << x+  constrain = undefined  f = observe "f" f' f' x = D x
tests/Generic/r1.hs view
@@ -6,6 +6,7 @@ instance Observable D where   observer (D x) = send "D" $ return D << x   observer (C i) = send "C" $ return C << i+  constrain = undefined  f :: D -> Int f = observe "f" f'
tests/Generic/r2.hs view
@@ -6,6 +6,7 @@ instance Observable D where   observer (D x) = send "D" $ return D << x   observer T     = send "T" $ return T+  constrain = undefined  f :: D -> Int f = observe "f" f'
tests/Generic/r3.hs view
@@ -7,6 +7,7 @@   observer (Mul e1 e2) = send "Mul"   $ return Mul << e1 << e2   observer (Const v)   = send "Const" $ return Const << v   observer Exc         = send "Exc"   $ return Exc+  constrain = undefined  one = observe "one" one' one' (Mul expr (Const 1)) = expr
tests/Prop/t0/Main.hs view
@@ -4,10 +4,10 @@ import Debug.Hoed.Pure  -- main = quickcheck prop_idemSimplify-main = logOwp Abort "hoed-tests-Prop-t0.graph" properties $ print $ prop_idemSimplify (Mul (Const 1) (Const 2))+main = logOwp Bottom "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" []-               , Propositions [(BoolProposition,myModule,"prop_idemSimplify",[0])] PropertiesOf "simplify" []+  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" []                ]   myModule = Module "MyModule" "../Prop/t0/"
tests/Prop/t1/Main.hs view
@@ -3,9 +3,9 @@ import Debug.Hoed.Pure  -- main = quickcheck prop_idem_negin_sound-main = logOwp Abort "hoed-tests-Prop-t1.graph" properties $ print (prop_negin_correct eg)+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",[0]), (BoolProposition,cnfModule,"prop_negin_sound",[0])] Specify "negin" []+  properties = [Propositions [(BoolProposition,cnfModule,"prop_negin_complete",[Argument 0]), (BoolProposition,cnfModule,"prop_negin_sound",[Argument 0])] Specify "negin" []                ]   cnfModule  = Module "CNF" "../Prop/t1/"
tests/Prop/t2/Main.hs view
@@ -3,10 +3,10 @@ import Debug.Hoed.Pure  -- main = quickcheck prop_idem_negin_sound-main = logOwp Abort "hoed-tests-Prop-t2.graph" properties $ print (prop_assoc1toNdigraph eg)+main = logOwp Bottom "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" []-               , Propositions [(BoolProposition,digraphModule,"prop_addMissingSources",[0])]   Specify "addMissingSources" []+  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" []                ]   digraphModule = Module "Digraph" "../Prop/t2/"
tests/Prop/t3/Main.hs view
@@ -13,7 +13,7 @@   main :: IO ()-main = logOwp Abort "hoed-tests-Prop-t3.graph" propositions $ do+main = logOwp Bottom "hoed-tests-Prop-t3.graph" propositions $ do -- main = do  {- Running all tests@@ -39,21 +39,21 @@   where     propositions =-        [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[0])-                      ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_generic",[0])+        [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])                       ]                       PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] -        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[1,0])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[1,0])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[0,1])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[0,1])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[0,1])+        , 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])                        ]                         PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]-        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[1,0])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[0,1])+        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[Argument 1,Argument 0])+                       , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[Argument 0,Argument 1])                        ]                         PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
tests/Prop/t4/Main.hs view
@@ -24,12 +24,12 @@ -}  main :: IO ()-main = logOwp Abort "hoed-tests-Prop-t4.graph" propositions $ do+main = logOwp Bottom "hoed-tests-Prop-t4.graph" propositions $ do   g <- newStdGen   print . fromJust . ok . (generate 1 g) . evaluate $  prop_shift_win_I 1 'd' myStackSet   where     propositions =-        [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[0])+        [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[Argument 0])                       -- ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0])                       ]                       PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]@@ -38,16 +38,16 @@         --                ]          --                PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] -        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[1,0])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[1,0])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[0,1])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[0,1])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[0,1])+        , 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])                        ]                         PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe] -        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[1,0])-                       , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[0,1])+        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[Argument 1,Argument 0])+                       , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[Argument 0,Argument 1])                        ]                         PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]