Fri Jul 27 11:53:34 WEST 2007 Miguel Vilaca <jmvilaca@di.uminho.pt>
* Checks
Machinery to add checks over nets, plus a simple operation that checks if every port is connected exactly once.
{
hunk ./Makefile 38
+ src/INChecks.hs src/INChecksUI.hs \
hunk ./Makefile 257
+src/INChecks.o : src/INChecks.hs
+src/INChecks.o : src/Common.hi
+src/INChecks.o : src/INRule.hi
+src/INChecks.o : src/Ports.hi
+src/INChecks.o : src/Network.hi
+src/INChecks.o : src/Document.hi
hunk ./Makefile 322
+src/GUIEvents.o : src/INReductionStrategies.hi
hunk ./Makefile 352
+src/INChecksUI.o : src/INChecksUI.hs
+src/INChecksUI.o : src/InfoKind.hi
+src/INChecksUI.o : src/CommonIO.hi
+src/INChecksUI.o : src/DocumentFile.hi
+src/INChecksUI.o : src/SafetyNet.hi
+src/INChecksUI.o : src/Document.hi
+src/INChecksUI.o : src/Constants.hi
+src/INChecksUI.o : src/Common.hi
+src/INChecksUI.o : src/PersistentDocument.hi
+src/INChecksUI.o : src/State.hi
+src/INChecksUI.o : src/INChecks.hi
hunk ./Makefile 365
+src/NetworkUI.o : src/INChecksUI.hi
hunk ./src/Common.hs 191
+indent :: Int -> String -> String
+indent n = unlines' . map (replicate n '\t' ++) . lines
+
+-- | Similar to 'unlines' but without an @'\n'@ in the end.
+unlines' :: [String] -> String
+unlines' = foldr1 (\str1 str2 -> str1 ++ '\n':str2)
+
+infix 9 !+!
+
+(!+!) :: [a] -> [Int] -> [a]
+(!+!) l li = map (l !!) li
+
+
hunk ./src/Constants.hs 59
+
+extensions,paletteExtensions :: [(String, [String])]
+extensions = [ (toolName ++ " files (." ++ netExt ++ ")", ["*." ++ netExt]) ]
+paletteExtensions = [ ("Shape palettes (." ++ paletteExt ++ ")", ["*." ++ paletteExt]) ]
+
hunk ./src/GUIEvents.hs 16
+import INReductionStrategies
addfile ./src/INChecks.hs
hunk ./src/INChecks.hs 1
+{- | To create new Checks simply:
+
+ 1. create an element of type 'Check g n e'
+
+ 2. add it to the list 'checksList'
+
+ If necessary create new 'INError' values and
+ extend the 'show' function definition.
+-}
+module INChecks
+ (
+ -- * Data-types
+ INError(..)
+ , ErrorLoc
+ , CheckOp
+ , Check
+
+ -- * List of available check operations
+ , checksList
+
+ -- * Check operations combinators
+ , join
+ , joins
+
+ ) where
+
+import Document
+import Network
+import Ports
+import INRule
+import Common
+
+import Data.Maybe
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+-- | Interaction Nets Errors
+data INError g n e
+ = DisconnectedPorts [(NodeNr, Node n, [Port])] -- ^ Disconnected ports
+ | ErrorString String -- ^ General error
+-- | NewError ... -- ^ [_$_]
+
+instance (Show g, Show n, Show e) => Show (INError g n e) where
+ showsPrec _ (DisconnectedPorts l) =
+ showString badPortMsg . showChar '\n' . showString (showBadPortsNet 1 l)
+ showsPrec _ (ErrorString str) = showString str
+-- showsPrec _ (NewError ...) = ...
+
+
+
+data Side = Lhs | Rhs deriving (Eq,Ord)
+instance Show Side where
+ show Lhs = "LHS"
+ show Rhs = "RHS"
+
+data ErrorLoc = PALETTE | NET | RULE RuleName (Maybe Side) deriving (Eq, Ord)
+
+instance Show ErrorLoc where
+ show PALETTE = "PALETTE"
+ show NET = "NET"
+ show (RULE ruleName mSide) =
+ showString "RULE \"" . showString ruleName . showChar '\"'
+ . maybe id (\v -> showChar ' ' . shows v) mSide $ ""
+
+
+type CheckOp g n e = Document g n e -> Map ErrorLoc [INError g n e] -- ^ errors by location
+type Check g n e =
+ ( String -- Check operation name to be displayed
+ , String -- Check description
+ , String -- Message when the check is passed successfully
+ , String -- Message when the check fails
+ , CheckOp g n e -- Check function
+ )
+
+-- | Join two check operations; concatenate errors.
+join :: CheckOp g n e -> CheckOp g n e -> CheckOp g n e
+join check1 check2 = uncurry (Map.unionWith (++)) . (check1 /\ check2)
+
+-- | Join a list of check operations.
+joins :: [CheckOp g n e] -> CheckOp g n e
+joins = foldr1 join
+
+-- | List of available checks.
+checksList :: [Check g n e]
+checksList =
+ [ badPortsCheck
+-- , newCheck
+ ]
+
+
+
+--------------------------------------------------------
+-- | Useful function that transverse a 'Document' in a very common way to collect 'INError's.
+doc2Errors :: (Network g n e -> [INError g n e])
+ -> (INRule g n e -> [(Maybe Side, [INError g n e])] )
+ -> CheckOp g n e
+doc2Errors funcNet funcRule =
+ uncurry (foldl updtAc)
+ . ( (empOrSing NET . funcNet . getNetwork)
+ /\
+ getRules)
+ where
+ empOrSing k l = if null l then Map.empty else Map.singleton k l
+ -- updtAc :: Map ErrorLoc [INError g n e] -> INRule g n e -> Map ErrorLoc [INError g n e]
+ updtAc mapp rule = foldl (aux $ INRule.getName rule) mapp $ funcRule rule
+
+ aux :: RuleName -> Map ErrorLoc [INError g n e] -> (Maybe Side, [INError g n e])
+ -> Map ErrorLoc [INError g n e]
+ aux _ mapp (_,[]) = mapp
+ aux ruleName mapp (mSide, errs) = Map.insertWith (++) (RULE ruleName mSide) errs mapp
+
+
+-- Bad Ports ------------------------------------------------------------------------------------------------
+
+badPortMsg = "Disconnected or with multiple connections ports found"
+
+badPortsCheck :: Check g n e
+badPortsCheck =
+ ( "Check bad ports"
+ , "Every port must be connected exactly once."
+ , "No disconnected or with multiple connections ports found."
+ , badPortMsg
+ , pureBadPorts
+ )
+
+-- | Every net in INblobs must have exactly one edge connected at each port.
+badPortsNet :: Network g n e -> [(NodeNr, Node n, [Port])]
+badPortsNet network =
+ filter f . map badPortsN $ getNodeAssocs network
+ where
+ f (_,_,t) = not $ null t
+ -- Gives list of bad ports for this node.
+ badPortsN :: (NodeNr, Node n) -> (NodeNr, Node n, [Port])
+ badPortsN (nNr, node) = (nNr, node, case getPorts node of
+ Nothing -> error "unexpected situation"
+ Just ports -> filter (g nNr) ports)
+ g :: NodeNr -> Port -> Bool
+ g nnr port = isNothing $ edgeConnectedOnPort network nnr port
+
+-- | Collects all bad ports by location.
+pureBadPorts :: CheckOp g n e
+pureBadPorts = doc2Errors funcNet funcRule
+ where funcNet :: Network g n e -> [INError g n e]
+ funcNet = insertIfN . badPortsNet
+
+ funcRule :: INRule g n e -> [(Maybe Side, [INError g n e])]
+ funcRule =
+ uncurry (++)
+ . ((insertIfR Lhs . badPortsNet . getLHS)
+ /\
+ (insertIfR Rhs . badPortsNet . getRHS))
+
+ insertIfN netCheck = if null netCheck then [] else [DisconnectedPorts netCheck]
+ insertIfR side netCheck = if null netCheck then [] else [(Just side, [DisconnectedPorts netCheck])]
+
+showBadPortsNet :: Int -> [(NodeNr, Node n, [Port])] -> String
+showBadPortsNet n l = unlines' $ map showNode l
+ where showNode (_, node, lPorts) = unlines' $ (replicate n '\t' ++ Network.getName node ++ " @ " ++ show (getPosition node) ++ " in port(s):") : map showPort lPorts
+ showPort (name,_) = replicate (n+1) '\t' ++ name
+------------------------------------------------------------------------------------------------------------------
+
addfile ./src/INChecksUI.hs
hunk ./src/INChecksUI.hs 1
+module INChecksUI
+ ( checksList
+ , singleCheckOverIN
+ , multipleChecksOverIN_UI
+ , multipleChecksOverINs_UI
+ ) where
+
+import INChecks
+import State
+import qualified PersistentDocument as PD
+import Common
+import Constants
+import Document
+import SafetyNet
+import DocumentFile
+import CommonIO
+import InfoKind
+
+import Text.XML.HaXml.XmlContent (XmlContent)
+
+import Graphics.UI.WXCore hiding (Document)
+import Graphics.UI.WX
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.List
+import Control.Monad
+
+
+------------------------------------------------------------------------------------------
+showINErrorList :: (Show g, Show n, Show e) => [INError g n e] -> String
+showINErrorList = unlines' . map show
+
+showError :: (Show g, Show n, Show e) => Map ErrorLoc [INError g n e] -> String
+showError = Map.foldWithKey aux ""
+ where -- aux :: ErrorLoc -> [INError g n e] -> String -> String
+ aux loc err str = '\t':show loc ++ '\n': indent 2 (showINErrorList err) ++ '\n':str
+
+showError2 :: (Show g, Show n, Show e) => Map ErrorLoc (Map String (String, [INError g n e])) -> String
+showError2 = Map.foldWithKey aux2 "" . Map.map (Map.foldWithKey aux "")
+ where -- aux :: String -> (String, [INError g n e]) -> String -> String
+ aux checkName (badMsg, err) str = checkName ++ " :\n"
+ ++ indent 1 (showINErrorList err) ++ '\n':str
+
+ aux2 :: ErrorLoc -> String -> String -> String
+ aux2 loc err str = '\t':show loc ++ '\n': indent 2 err ++ '\n':str
+
+
+-- | Run the check operation over current IN system.
+singleCheckOverIN :: (Show g, Show n, Show e) => Check g n e -> State g n e -> IO ()
+singleCheckOverIN (checkName, _, okMsg, badMsg, func) state =
+ do w <- getNetworkFrame state
+ pDoc <- getDocument state
+ doc <- PD.getDocument pDoc
+ wxcBeginBusyCursor
+ let l = func doc
+ wxcEndBusyCursor
+ if Map.null l
+ then infoDialog w (checkName ++ ": Passed") okMsg
+ else do logMessage $ badMsg ++ ": \n" ++ showError l
+ errorDialog w (checkName ++ ": Failed") (badMsg ++ ".\nSee report in the bottom area.")
+
+-- | Run multiple check operations over current IN system.
+multipleChecksOverIN :: (Show g, Show n, Show e) => [Check g n e] -> State g n e -> IO ()
+multipleChecksOverIN listChecks state =
+ do w <- getNetworkFrame state
+ pDoc <- getDocument state
+ doc <- PD.getDocument pDoc
+ wxcBeginBusyCursor
+
+ case runChecksOver doc listChecks of
+ (goodsStr, Nothing) ->
+ do
+ wxcEndBusyCursor
+ infoDialog w "All checks passed" goodsStr
+ (goodsStr, Just (badsStr,badsStrLong)) ->
+ do
+ wxcEndBusyCursor
+ logMessage $ goodsStr ++ badsStrLong
+ errorDialog w "Checks Failed"
+ $ goodsStr ++ badsStr
+ ++ "See report in the bottom area."
+
+-- | Runs multiple checks over a document.
+runChecksOver :: (Show g, Show n, Show e) =>
+ Document g n e -> [Check g n e] -> (String -- good checks
+ , Maybe (String -- bad checks
+ ,String -- long bag checks report
+ ))
+runChecksOver doc listChecks =
+ if null bads
+ then (goodsStr, Nothing)
+ else (goodsStr, Just (badsStr, badsStrLong))
+ where
+ (goods, bads) = partition passed $ map (calc doc) listChecks
+ goodsStr = unlines $ map showOK goods
+ badsStr = unlines $ map showBAD bads
+ badsStrLong = showError2 $ transf bads
+
+ calc doc (a,_,b,c,func) = (a,b,c, func doc)
+ passed (_,_,_, r) = Map.null r
+ showOK (name,okMsg,_,_) = name ++ ": Passed\n\t" ++ okMsg
+ showBAD (name,_,badMsg,_) = name ++ ": Failed\n\t" ++ badMsg
+
+
+-- | Change from errors by Check inner sorted by 'ErrorLoc' to errors by 'ErrorLoc', inner sorted by Check.
+transf :: [(String, String, String, Map ErrorLoc [INError g n e])] -> Map ErrorLoc (Map String (String, [INError g n e]))
+transf = Map.unionsWith Map.union . map aux1
+ where aux1 :: (String, String, String, Map ErrorLoc [INError g n e]) -> Map ErrorLoc (Map String (String, [INError g n e]))
+ aux1 (name,_, badMsg, mapp) = Map.map (\v -> Map.singleton name (badMsg,v)) mapp
+
+
+multipleChecksOverIN_UI :: (Show g, Show n, Show e) => Frame () -> State g n e -> IO ()
+multipleChecksOverIN_UI theFrame state =
+ do
+ mChecks <- chooseChecksDialog theFrame
+ case mChecks of
+ Nothing -> return ()
+ Just [] -> infoDialog theFrame "Zero checks" "Zero checks chosen, so nothing to do"
+ Just ks -> multipleChecksOverIN ks state
+
+chooseChecksDialog :: Frame () -> IO (Maybe [Check g n e])
+chooseChecksDialog theFrame =
+ do
+ dialog <- dialog theFrame
+ [ text := "Choose Checks"
+ ]
+ p <- panel dialog []
+
+ lChks <- mapM (\(name, desc,_,_,_) -> checkBox p [ text := name
+ , checked := False
+ , tooltip := desc
+ ]
+ ) checksList
+
+ ok <- button p [ text := "Check" ]
+ set dialog [ layout := container p $
+ margin 10 $
+ column 5 [ label "Apply the following checks:"
+ , margin 10 . column 5 $ map widget lChks
+ , hfloatCentre $ widget ok
+ ]
+ ]
+
+ showModal dialog $ \stop ->
+ do set ok [ on command :=
+ do
+ sels <- filterM isSelected $ zip lChks checksList
+ stop (Just $ map snd sels)
+ ]
+
+isSelected = checkBoxGetValue . fst
+fst5 (a,_,_,_,_) = a
+
+multipleChecksOverINs_UI :: (InfoKind n g, InfoKind e g, XmlContent g, Show g)
+ => State g n e -> IO ()
+multipleChecksOverINs_UI state =
+ do
+ newFrame <- frame [ text := "Multiple Checks Over Multiple INs"
+ , size := sz 900 600
+ ]
+ p <- panel newFrame []
+ txt <- textCtrlRich p []
+ textCtrlSetEditable txt False
+ okB <- button p [ text := "Exit"
+ , on command := close newFrame
+ ]
+ saveB <- button p [ text := "Save to file"
+ , on command := safetyNet newFrame $
+ do
+ mFile <- fileSaveDialog newFrame rememberCurrentDir False "File to save report to:" [("Any file", ["*","*.txt","*.log"])] directory filename
+ case mFile of
+ Nothing -> errorDialog newFrame "No File" "No file to write to.\n Report not saved."
+ Just file -> do str <- textCtrlGetValue txt
+ writeFile file str
+
+ ]
+ set newFrame [ layout := container p $
+ margin 10 $
+ column 5 [ fill $ widget txt
+ , hfloatRight $ row 5 [widget saveB, widget okB]
+ ]
+ ]
+
+ files <- filesOpenDialog newFrame rememberCurrentDir allowReadOnly message extensions directory filename
+ mlChecks <- chooseChecksDialog newFrame
+
+ case (files, mlChecks) of
+ (fs, Just cs) | not (null fs) && not (null cs) -> -- useful case
+ do
+ textCtrlAppendText txt "Checking ...\n"
+ wxcBeginBusyCursor
+ mapM_ (reportPerFile state txt cs) fs
+ wxcEndBusyCursor
+ x -> textCtrlAppendText txt "No files and/or no checks chosen, so nothing to do"
+
+ where
+ rememberCurrentDir = True
+ allowReadOnly = True
+ message = "Open " ++ toolName ++ " files"
+ directory = "examples"
+ filename = ""
+
+-- | For each INblobs file add some info to the report.
+reportPerFile :: (InfoKind n g, InfoKind e g, XmlContent g, Show g) =>
+ State g n e -> TextCtrl () -> [Check g n e] -> FilePath -> IO ()
+reportPerFile _ txt chks fname =
+ do
+ contents <- strictReadFile fname
+ let errorOrDocument = DocumentFile.fromString contents
+ textCtrlAppendText txt $ fname ++ "\n"
+ case errorOrDocument of
+ Left err -> addError2TextCtrl txt $ err ++ "\nChecks not performed.\n"
+ Right (doc, [], False) ->
+ case runChecksOver doc chks of
+ (goodsStr, Nothing) -> addGood2TextCtrl txt "All checks passed"
+ (goodsStr, Just (badsStr,badsStrLong)) ->
+ do
+ addGood2TextCtrl txt goodsStr
+ addTxtOfColor2TextCtrl (wxcolor orange) txt badsStrLong
+
+ Right (doc, warnings, True) ->
+ addError2TextCtrl txt $
+ "File read warning\n"
+ ++ "The file you opened has the old " ++ toolName
+ ++ " file format which will become obsolete in newer versions of "
+ ++ toolName ++ ".\nChecks not performed.\n"
+
+ Right (doc, warnings, False) ->
+ addError2TextCtrl txt $
+ "Warnings while reading file:\n\n"
+ ++ unlines ( map ("* " ++) (take 10 warnings)
+ ++ if length warnings > 10 then ["..."] else []
+ )
+ ++ "\n Most likely you are reading a file that is created by a newer version of "
+ ++ toolName ++ ".\nChecks not performed.\n"
+ textCtrlAppendText txt $ '\n': replicate 20 '#' ++ "\n\n"
+
+-- | Add text to a 'TextCtrl' putting it in the given 'Color'.
+addTxtOfColor2TextCtrl :: Color -> TextCtrl () -> String -> IO ()
+addTxtOfColor2TextCtrl color txt str =
+ do
+ start <- textCtrlGetInsertionPoint txt
+ textCtrlAppendText txt str
+ end <- textCtrlGetInsertionPoint txt
+ style <- textAttrCreateDefault
+ textAttrSetTextColour style color
+ textCtrlSetStyle txt start end style
+ return ()
+
+addError2TextCtrl, addGood2TextCtrl :: TextCtrl () -> String -> IO ()
+addError2TextCtrl = addTxtOfColor2TextCtrl red
+addGood2TextCtrl = addTxtOfColor2TextCtrl green
+
hunk ./src/INReduction.hs 2
- ( isActivePair
- , reduce
+ (
+ reduce
hunk ./src/INReduction.hs 167
- cleanJust = takeJust "A port were expected here."
+ cleanJust = takeJust "A port was expected here."
hunk ./src/INReductionStrategies.hs 2
--- 1. add a new entry in @strategiesList@ (e.g. @("New Strategy string", choose_NewStrategy_function)@)
+--
+-- 1. add a new entry in @strategiesList@ (e.g. @(\"New Strategy string\", choose_NewStrategy_function)@)
+--
hunk ./src/INReductionStrategies.hs 42
-strategiesList :: [(Strategy -- ^ strategy name
- , [EdgeNr] -- ^ none empty list of all active pairs in the network
- -> Document g n e -- ^ document
- -> PossibleResult EdgeNr -- ^ edgeNr to reduce or thrown error message
+strategiesList :: [(Strategy -- strategy name
+ , [EdgeNr] -- none empty list of all active pairs in the network
+ -> Document g n e -- document
+ -> PossibleResult EdgeNr -- edgeNr to reduce or thrown error message
hunk ./src/Network.hs 58
+ , showEdge
hunk ./src/Network.hs 87
+
+showEdge :: Edge e -> String
+showEdge edge =
+ "Node " ++ show (edgeFrom edge) ++ showPort (portFrom edge)
+ ++ " |-> " ++
+ "Node " ++ show (edgeTo edge) ++ showPort (portTo edge)
+ where showPort Nothing = ""
+ showPort (Just (name, _)) = "@" ++ name
hunk ./src/NetworkUI.hs 33
+import INChecksUI
hunk ./src/NetworkUI.hs 230
+ -- to debug purposes
+ ; textlog <- textCtrlRich sp [enabled := False, wrap := WrapNone]
+ -- use text control as logger
+ ; textCtrlMakeLogActiveTarget textlog
hunk ./src/NetworkUI.hs 385
+ -- Checks menu
+ ; chksMenu <- menuPane [text := "&Checks"]
+ ; mapM_ (\ chk@(name, desc,_,_,_) ->
+ menuItem chksMenu [ text := name
+ , on command := safeAndClear theFrame textlog $ singleCheckOverIN chk state
+ ]
+ ) checksList
+ ; menuLine chksMenu
+ ; menuItem chksMenu [ text := "Multiple checks at once"
+ , on command := safeAndClear theFrame textlog $ multipleChecksOverIN_UI theFrame state
+ ]
+ ; menuItem chksMenu [ text := "Checks over multiple files"
+ , on command := safeAndClear theFrame textlog $ multipleChecksOverINs_UI state
+ ]
+
hunk ./src/NetworkUI.hs 429
- -- to debug purposes [_$_]
- ; textlog <- textCtrl sp [enabled := False, wrap := WrapNone] [_$_]
- -- use text control as logger
- ; textCtrlMakeLogActiveTarget textlog
-
hunk ./src/NetworkUI.hs 478
- ; set reduceB [on command := do logMessage "Button Reduce pressed"
+ ; set reduceB [on command := do
hunk ./src/NetworkUI.hs 512
- [ menuBar := [ fileMenu, editMenu, viewMenu, opsMenu, palMenu, helpMenu ]
+ [ menuBar := [ fileMenu, editMenu, viewMenu, opsMenu, palMenu, chksMenu, helpMenu ]
hunk ./src/NetworkUI.hs 630
-extensions,paletteExtensions :: [(String, [String])]
-extensions = [ (toolName ++ " files (." ++ netExt ++ ")", ["*." ++ netExt]) ]
-paletteExtensions = [ ("Shape palettes (." ++ paletteExt ++ ")", ["*." ++ paletteExt]) ]
-
hunk ./src/NetworkUI.hs 1608
- ++ "************* Lambda Term Gramar: ***************\n\n"
+ ++ "************* Lambda Term Grammar: ***************\n\n"
hunk ./src/NetworkUI.hs 1623
+safeAndClear :: Window a -> TextCtrl b -> IO c -> IO ()
+safeAndClear theFrame textlog comp =
+ safetyNet theFrame $ textCtrlClear textlog >> comp
+
}