tamarin-prover-utils 0.8.0.0 → 0.8.0.1
raw patch · 6 files changed
+103/−103 lines, 6 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- src/Control/Monad/Trans/FastFresh.hs +2/−2
- src/Control/Monad/Trans/PreciseFresh.hs +2/−2
- src/Data/Color.hs +18/−18
- src/Extension/Prelude.hs +11/−11
- src/Text/Dot.hs +69/−69
- tamarin-prover-utils.cabal +1/−1
src/Control/Monad/Trans/FastFresh.hs view
@@ -84,9 +84,9 @@ -- | Restrict the scope of the freshness requests. scopeFreshness :: Monad m => FreshT m a -> FreshT m a scopeFreshness scoped = do- state <- FreshT get -- save state before scoped action+ st <- FreshT get -- save state before scoped action x <- scoped- FreshT (put state) -- restore freshness state+ FreshT (put st) -- restore freshness state return x
src/Control/Monad/Trans/PreciseFresh.hs view
@@ -98,9 +98,9 @@ -- | Restrict the scope of the freshness requests. scopeFreshness :: Monad m => FreshT m a -> FreshT m a scopeFreshness scoped = do- state <- FreshT get -- save state before scoped action+ st <- FreshT get -- save state before scoped action x <- scoped- FreshT (put state) -- restore freshness state+ FreshT (put st) -- restore freshness state return x
src/Data/Color.hs view
@@ -4,7 +4,7 @@ -- | -- Copyright : (c) 2010 Simon Meier -- License : GPL v3 (see LICENSE)--- +-- -- Maintainer : Simon Meier <iridcode@gmail.com> -- -- A simple color module for handling RGB and HSV representations of colors.@@ -19,7 +19,7 @@ , red , green , blue- + -- ** Conversions , rgbToGray , hsvToGray@@ -91,7 +91,7 @@ | ub == g = 60 * (2 + (b-r)/(ub-lb)) | otherwise = 60 * (4 + (r-g)/(ub-lb)) - h' | h < 0 = h + 360 + h' | h < 0 = h + 360 | otherwise = h s | ub == 0 = 0@@ -132,9 +132,9 @@ rgbToHex :: RealFrac t => RGB t -> String rgbToHex (RGB r g b) = ('#':) . showHex' r . showHex' g . showHex' b $ "" where showHex' f- | i <= 15 = ('0':) . showHex i- | otherwise = showHex i- where + | i <= 15 = ('0':) . showHex i+ | otherwise = showHex i+ where i :: Int i = max 0 (min 255 (floor (256 * f))) @@ -161,23 +161,23 @@ -- | From a list of group sizes build a function assigning every element a -- unique color, nicely distributed such that they are well differentiated both -- using color and monochrome displays.-genColorGroups :: RealFrac t => - ColorParams t +genColorGroups :: RealFrac t =>+ ColorParams t -> [Int] -- ^ List of group sizes. -> [((Int,Int),(HSV t))]-genColorGroups (ColorParams { - cpScale = scale - , cpZeroHue = zeroHue - , cpVBottom = vBot, cpVRange = vRan- , cpSBottom = sBot, cpSRange = sRan- }) groups = +genColorGroups (ColorParams {+ cpScale = scale+ , cpZeroHue = zeroHue+ , cpVBottom = vBot, cpVRange = vRan+ , cpSBottom = sBot, cpSRange = sRan+ }) groups = do (groupIdx, groupSize) <- zip [0.. ] groups elemIdx <- [0..groupSize - 1] let h = toShiftedGroupHue groupIdx (fromIntegral elemIdx / fromIntegral groupSize) v = vBot + vRan * toGroupHue groupIdx (fromIntegral elemIdx / fromIntegral groupSize) s = sBot + sRan * toGroupHue groupIdx (fromIntegral elemIdx / fromIntegral groupSize)- color = HSV (360*h) s v + color = HSV (360*h) s v return ((groupIdx, elemIdx), color) where nGroups :: Int@@ -188,9 +188,9 @@ 0.5 * (1 - scale) + -- left margin (h * scale) -- position in margin ) / (fromIntegral nGroups)- + toShiftedGroupHue g h =- snd . properFraction $ toGroupHue g h + 1 + + snd . properFraction $ toGroupHue g h + 1 + (zeroHue/360) - toGroupHue 0 0.5 @@ -234,7 +234,7 @@ {- colorTable :: Double -> (HSV Double -> HSV Double) -> [Int] -> Html-colorTable zeroHue conv groups = +colorTable zeroHue conv groups = table . toHtml . besides $ map col [0..length groups-1] where col i = aboves [cell $ (td ! [getStyle i j]) (stringToHtml (show (i,j)))
src/Extension/Prelude.hs view
@@ -1,7 +1,7 @@ -- | -- Copyright : (c) 2010, 2011 Simon Meier -- License : GPL v3 (see LICENSE)--- +-- -- Maintainer : Simon Meier <iridcode@gmail.com> -- -- Functions that could/should have made it into the Prelude or one of the@@ -50,7 +50,7 @@ -- duplicates. {-# INLINABLE sortednubBy #-} sortednubBy :: (a -> a -> Ordering) -> [a] -> [a]-sortednubBy cmp = +sortednubBy cmp = -- Adapted from GHC's Data.List module -- Copyright: (c) The University of Glasgow 2001 mergeAll . sequences@@ -83,7 +83,7 @@ LT -> a : merge as' bs -- | //O(n*log n).// Sort list and remove duplicates with respect to a--- projection. +-- projection. {-# INLINE sortednubOn #-} sortednubOn :: Ord b => (a -> b) -> [a] -> [a] sortednubOn proj = sortednubBy (comparing proj)@@ -127,8 +127,8 @@ splitBy p = unfoldr split where split [] = Nothing split xs = let ~(w,r) = break p xs in case r of- [] -> Just $ (w,[])- (_:rest) -> Just $ (w,rest)+ [] -> Just $ (w,[])+ (_:rest) -> Just $ (w,rest) -- | the list of all permutations of a given list@@ -138,17 +138,17 @@ -- where aux [] _ = [] -- aux (x:xs) ys = [x:p | p <- permutations (xs++ys)] ++ aux xs (x:ys) --- | the list of all combinations of n elements of a list. +-- | the list of all combinations of n elements of a list. -- E.g. choose 2 [1,2,3] = [[1,2],[1,3],[2,3]] choose :: Int -> [a] -> [[a]] choose 0 _ = [[]] choose _ [] = [] choose n (x:xs) = [x:xs' | xs' <- choose (n-1) xs] ++ choose n xs --- | build the list of lists each leaving another element out. +-- | build the list of lists each leaving another element out. -- (From left to right) leaveOneOut :: [a] -> [[a]]-leaveOneOut xs = +leaveOneOut xs = zipWith (++) (map init . tail . inits $ xs) (map tail . init . tails $ xs) @@ -161,12 +161,12 @@ -- Pairs -- ----------- --- | These functions were inspired by the ML library accompanying the +-- | These functions were inspired by the ML library accompanying the -- Isabelle theorem prover (<http://isabelle.in.tum.de/>) -- | swap the elements of a pair swap :: (a, b) -> (b, a)-swap (x, y) = (y, x)+swap (x, y) = (y, x) -- | sort the elements of a pair sortPair :: Ord a => (a,a) -> (a,a)@@ -250,7 +250,7 @@ -- | Gather all error free computations. errorFree :: MonadPlus m => [m a] -> m [a]-errorFree ms = +errorFree ms = catMaybes `liftM` sequence [(Just `liftM` m) `mplus` return Nothing | m <- ms] -- | Gather all error free computations and ensure that at least one was error
src/Text/Dot.hs view
@@ -7,68 +7,68 @@ -- Stability: unstable -- Portability: portable ----- This module provides a simple interface for building .dot graph files, for input into the dot and graphviz tools. +-- This module provides a simple interface for building .dot graph files, for input into the dot and graphviz tools. -- It includes a monadic interface for building graphs. -module Text.Dot - ( - -- * Dot- Dot -- abstract- -- * Nodes- , node- , NodeId -- abstract- , userNodeId- , userNode- -- * Edges- , edge- -- * Showing a graph- , showDot- -- * Other combinators- , scope- , attribute- , nodeAttributes- , edgeAttributes- , graphAttributes- , share- , same- , cluster- -- * Record specification- , Record -- abstract- , field- , portField- , hcat- , hcat'- , vcat- , vcat'- -- * Record node construction- , record- , record'- , record_- - , mrecord- , mrecord'- , mrecord_- ) where+module Text.Dot+ (+ -- * Dot+ Dot -- abstract+ -- * Nodes+ , node+ , NodeId -- abstract+ , userNodeId+ , userNode+ -- * Edges+ , edge+ -- * Showing a graph+ , showDot+ -- * Other combinators+ , scope+ , attribute+ , nodeAttributes+ , edgeAttributes+ , graphAttributes+ , share+ , same+ , cluster+ -- * Record specification+ , Record -- abstract+ , field+ , portField+ , hcat+ , hcat'+ , vcat+ , vcat'+ -- * Record node construction+ , record+ , record'+ , record_ + , mrecord+ , mrecord'+ , mrecord_+ ) where+ import Data.Char (isSpace) import Data.List (intersperse) import Control.Monad (liftM, ap) import Control.Applicative (Applicative(..)) data NodeId = NodeId String- | UserNodeId Int+ | UserNodeId Int instance Show NodeId where show (NodeId str) = str- show (UserNodeId i) - | i < 0 = "u_" ++ show (negate i)- | otherwise = "u" ++ show i+ show (UserNodeId i)+ | i < 0 = "u_" ++ show (negate i)+ | otherwise = "u" ++ show i data GraphElement = GraphAttribute String String- | GraphNode NodeId [(String,String)]- | GraphEdge NodeId NodeId [(String,String)]- | Scope [GraphElement]- | SubGraph NodeId [GraphElement]+ | GraphNode NodeId [(String,String)]+ | GraphEdge NodeId NodeId [(String,String)]+ | Scope [GraphElement]+ | SubGraph NodeId [GraphElement] data Dot a = Dot { unDot :: Int -> ([GraphElement],Int,a) } @@ -82,13 +82,13 @@ instance Monad Dot where return a = Dot $ \ uq -> ([],uq,a) m >>= k = Dot $ \ uq -> case unDot m uq of- (g1,uq',r) -> case unDot (k r) uq' of- (g2,uq2,r2) -> (g1 ++ g2,uq2,r2)+ (g1,uq',r) -> case unDot (k r) uq' of+ (g2,uq2,r2) -> (g1 ++ g2,uq2,r2) -- | 'rawNode' takes a list of attributes, generates a new node, and gives a 'NodeId'. rawNode :: [(String,String)] -> Dot NodeId-rawNode attrs = Dot $ \ uq -> - let nid = NodeId $ "n" ++ show uq +rawNode attrs = Dot $ \ uq ->+ let nid = NodeId $ "n" ++ show uq in ( [ GraphNode nid attrs ],succ uq,nid) -- | 'node' takes a list of attributes, generates a new node, and gives a@@ -105,7 +105,7 @@ userNodeId :: Int -> NodeId userNodeId i = UserNodeId i --- | 'userNode' takes a NodeId, and adds some attributes to that node. +-- | 'userNode' takes a NodeId, and adds some attributes to that node. userNode :: NodeId -> [(String,String)] -> Dot () userNode nId attrs = Dot $ \ uq -> ( [GraphNode nId attrs ],uq,()) @@ -116,14 +116,14 @@ -- | 'scope' groups a subgraph together; in dot these are the subgraphs inside "{" and "}". scope :: Dot a -> Dot a scope (Dot fn) = Dot (\ uq -> case fn uq of- ( elems,uq',a) -> ([Scope elems],uq',a))+ ( elems,uq',a) -> ([Scope elems],uq',a)) -- | 'share' is when a set of nodes share specific attributes. Usually used for layout tweaking. share :: [(String,String)] -> [NodeId] -> Dot ()-share attrs nodeids = Dot $ \ uq -> +share attrs nodeids = Dot $ \ uq -> ( [ Scope ( [ GraphAttribute name val | (name,val) <- attrs]- ++ [ GraphNode nodeid [] | nodeid <- nodeids ]- ) + ++ [ GraphNode nodeid [] | nodeid <- nodeids ]+ ) ], uq, ()) -- | 'same' provides a combinator for a common pattern; a set of 'NodeId's with the same rank.@@ -131,12 +131,12 @@ same = share [("rank","same")] --- | 'cluster' builds an explicit, internally named subgraph (called cluster). +-- | 'cluster' builds an explicit, internally named subgraph (called cluster). cluster :: Dot a -> Dot (NodeId,a)-cluster (Dot fn) = Dot (\ uq -> - let cid = NodeId $ "cluster_" ++ show uq - in case fn (succ uq) of- (elems,uq',a) -> ([SubGraph cid elems],uq',(cid,a)))+cluster (Dot fn) = Dot (\ uq ->+ let cid = NodeId $ "cluster_" ++ show uq+ in case fn (succ uq) of+ (elems,uq',a) -> ([SubGraph cid elems],uq',(cid,a))) -- | 'attribute' gives a attribute to the current scope. attribute :: (String,String) -> Dot ()@@ -158,7 +158,7 @@ -- 'showDot' renders a dot graph as a 'String'. showDot :: Dot a -> String showDot (Dot dm) = case dm 0 of- (elems,_,_) -> "digraph G {\n" ++ unlines (map showGraphElement elems) ++ "\n}\n"+ (elems,_,_) -> "digraph G {\n" ++ unlines (map showGraphElement elems) ++ "\n}\n" showGraphElement :: GraphElement -> String showGraphElement (GraphAttribute name val) = showAttr (name,val) ++ ";"@@ -171,15 +171,15 @@ showAttrs [] = "" showAttrs xs = "[" ++ showAttrs' xs ++ "]" where- -- never empty list- showAttrs' [a] = showAttr a- showAttrs' (a:as) = showAttr a ++ "," ++ showAttrs' as+ -- never empty list+ showAttrs' [a] = showAttr a+ showAttrs' (a:as) = showAttr a ++ "," ++ showAttrs' as showAttrs' [] = error "showAttrs: the impossible happended" showAttr :: (String, String) -> String showAttr (name, val) = name ++ "=\"" ++ concatMap escape val ++ "\""- where + where escape '\n' = "\\l" escape '"' = "\\\"" escape c = [c]@@ -247,10 +247,10 @@ renderRecord = render True where render _ (Field Nothing l) = return (escape l, const [])- render _ (Field (Just p) l) = + render _ (Field (Just p) l) = Dot $ \uq -> let pid = "n" ++ show uq lbl = "<"++pid++"> "++escape l- in ([], succ uq, (lbl, \nId -> [(p,NodeId (show nId++":"++pid))]))+ in ([], succ uq, (lbl, \nId -> [(p,NodeId (show nId++":"++pid))])) render horiz (HCat rs) = do (lbls, ids) <- liftM unzip $ mapM (render True) rs let rawLbl = concat (intersperse "|" lbls)
tamarin-prover-utils.cabal view
@@ -2,7 +2,7 @@ cabal-version: >= 1.8 build-type: Simple-version: 0.8.0.0+version: 0.8.0.1 license: GPL license-file: LICENSE category: Theorem Provers