tamarin-prover-utils 0.1.0.0 → 0.4.0.0
raw patch · 19 files changed
+772/−531 lines, 19 filesdep +dlistdep ~SHAdep ~containersdep ~deepseqsetup-changed
Dependencies added: dlist
Dependency ranges changed: SHA, containers, deepseq, fclabels, time
Files
- Setup.hs +91/−0
- src/Control/Monad/Bind.hs +7/−1
- src/Control/Monad/Fresh.hs +2/−2
- src/Control/Monad/Fresh/Class.hs +25/−9
- src/Control/Monad/Trans/FastFresh.hs +114/−0
- src/Control/Monad/Trans/Fresh.hs +0/−110
- src/Control/Monad/Trans/PreciseFresh.hs +129/−0
- src/Data/DAG/Simple.hs +84/−10
- src/Extension/Data/Bounded.hs +8/−3
- src/Extension/Data/ByteString.hs +15/−0
- src/Extension/Data/Monoid.hs +44/−0
- src/Extension/Prelude.hs +41/−3
- src/Text/Dot.hs +49/−13
- src/Text/Isar.hs +0/−319
- src/Text/PrettyPrint/Class.hs +129/−29
- src/Text/PrettyPrint/Highlight.hs +1/−2
- src/Text/PrettyPrint/Html.hs +7/−4
- src/Utils/Misc.hs +11/−17
- tamarin-prover-utils.cabal +15/−9
Setup.hs view
@@ -1,2 +1,93 @@ import Distribution.Simple main = defaultMain++{- Inferring the package version from git. Posted by https://github.com/hvr+ -+ - https://gist.github.com/656738++import Control.Exception+import Control.Monad+import Data.Maybe+import Data.Version+import Distribution.PackageDescription (PackageDescription(..), HookedBuildInfo, GenericPackageDescription(..))+import Distribution.Package (PackageIdentifier(..))+import Distribution.Simple (defaultMainWithHooks, simpleUserHooks, UserHooks(..))+import Distribution.Simple.LocalBuildInfo (LocalBuildInfo(..))+import Distribution.Simple.Setup (BuildFlags(..), ConfigFlags(..))+import Distribution.Simple.Utils (die)+import System.Process (readProcess)+import Text.ParserCombinators.ReadP (readP_to_S)++main :: IO ()+main = defaultMainWithHooks simpleUserHooks+ { confHook = myConfHook+ , buildHook = myBuildHook+ }++-- configure hook+myConfHook :: (GenericPackageDescription, HookedBuildInfo)+ -> ConfigFlags+ -> IO LocalBuildInfo+myConfHook (gpdesc, hbinfo) cfg = do+ let GenericPackageDescription {+ packageDescription = pdesc@PackageDescription {+ package = pkgIden }} = gpdesc++ gitVersion <- inferVersionFromGit (pkgVersion (package pdesc))++ let gpdesc' = gpdesc {+ packageDescription = pdesc {+ package = pkgIden { pkgVersion = gitVersion } } }++ -- putStrLn $ showVersion gitVersion++ confHook simpleUserHooks (gpdesc', hbinfo) cfg+++-- build hook+myBuildHook :: PackageDescription+ -> LocalBuildInfo+ -> UserHooks+ -> BuildFlags+ -> IO ()+myBuildHook pdesc lbinfo uhooks bflags = do+ let lastVersion = pkgVersion $ package pdesc++ gitVersion <- inferVersionFromGit lastVersion ++ when (gitVersion /= lastVersion) $+ die("The version reported by git '" ++ showVersion gitVersion +++ "' has changed since last time this package was configured (version was '" +++ showVersion lastVersion ++ "' back then), please re-configure package")++ buildHook simpleUserHooks pdesc lbinfo uhooks bflags++-- |Infer package version from Git tags. Uses `git describe` to infer 'Version'.+inferVersionFromGit :: Version -> IO Version+inferVersionFromGit version0 = do+ ver_line <- init `liftM` readProcess "git"+ [ "describe"+ , "--abbrev=5"+ , "--tags"+ , "--match=v[0-9].[0-9][0-9]"+ , "--dirty"+ , "--long"+ , "--always"+ ] ""++ -- ver_line <- return "v0.1-42-gf9f4eb3-dirty"+ putStrLn ver_line+ -- let versionStr = ver_line -- (head ver_line == 'v') `assert` replaceFirst '-' '.' (tail ver_line)+ -- Just version = listToMaybe [ p | (p, "") <- readP_to_S parseVersion versionStr ]++ return version0++{-+-- | Helper for replacing first occurence of character by another one.+replaceFirst :: Eq a => a -> a -> [a] -> [a]+replaceFirst _ _ [] = []+replaceFirst o r (x:xs) | o == x = r : xs+ | otherwise = x : replaceFirst o r xs+-}++-}
src/Control/Monad/Bind.hs view
@@ -45,6 +45,8 @@ import Control.Monad.State import Control.Monad.Fresh +import qualified Control.Monad.Trans.PreciseFresh as Precise+ ------------------------------------------------------------------------------ -- Bindings ------------------------------------------------------------------------------@@ -64,6 +66,9 @@ instance Monad m => MonadBind k v (StateT (Bindings k v) m) where +instance MonadBind k v m => MonadBind k v (FreshT m) where+instance MonadBind k v m => MonadBind k v (Precise.FreshT m) where+ ------------------------------------------------------------------------------ -- Type synonym for the StateT monad transformer ------------------------------------------------------------------------------@@ -121,8 +126,9 @@ -- | @importBinding mkR d n@ checks if there is already a binding registered -- for the value @d@ and if not it generates a fresh identifier using the name -- @n@ as a hint and converting name and identifier to a value using $mkR$.+{-# INLINE importBinding #-} importBinding :: (MonadBind k v m, MonadFresh m, Show v, Show k, Ord k) - => (String -> Int -> v) + => (String -> Integer -> v) -> k -> String -> m v importBinding mkR k n = do
src/Control/Monad/Fresh.hs view
@@ -18,7 +18,7 @@ , evalFresh , execFresh - -- * The FreshT monad transformer+ -- * The fast FreshT monad transformer , FreshT(..) , freshT , runFreshT@@ -40,5 +40,5 @@ import Control.Monad.Trans import Control.Monad.Fresh.Class-import Control.Monad.Trans.Fresh hiding (freshIdent)+import Control.Monad.Trans.FastFresh hiding (freshIdents)
src/Control/Monad/Fresh/Class.hs view
@@ -18,31 +18,47 @@ import Control.Monad.Reader import Control.Monad.Writer -import qualified Control.Monad.Trans.Fresh as Fresh (FreshT, freshIdent)+import qualified Control.Monad.Trans.FastFresh as Fast (FreshT, freshIdents)+import qualified Control.Monad.Trans.PreciseFresh as Precise (FreshT, freshIdent, freshIdents) -- Added 'Applicative' until base states this hierarchy class (Applicative m, Monad m) => MonadFresh m where- freshIdent :: String -- ^ Desired name.- -> m Int -- ^ Fresh identifier.+ -- | Get the integer of the next fresh identifier of this name.+ freshIdent :: String -- ^ Desired name+ -> m Integer + -- | Get a number of fresh identifiers. This reserves the required number+ -- of identifiers on all names.+ freshIdents :: Integer -- ^ Number of desired fresh identifiers.+ -> m Integer -- ^ The first Fresh identifier. -instance (Functor m, Monad m) => MonadFresh (Fresh.FreshT m) where- freshIdent = Fresh.freshIdent +instance (Functor m, Monad m) => MonadFresh (Fast.FreshT m) where+ freshIdent _name = Fast.freshIdents 1+ freshIdents = Fast.freshIdents +instance (Functor m, Monad m) => MonadFresh (Precise.FreshT m) where+ freshIdent = Precise.freshIdent+ freshIdents = Precise.freshIdents++ ---------------------------------------------------------------------------- -- instances for other mtl transformers -- -- TODO: Add remaining ones instance MonadFresh m => MonadFresh (MaybeT m) where- freshIdent = lift . freshIdent+ freshIdent = lift . freshIdent+ freshIdents = lift . freshIdents instance MonadFresh m => MonadFresh (StateT s m) where- freshIdent = lift . freshIdent+ freshIdent = lift . freshIdent+ freshIdents = lift . freshIdents instance MonadFresh m => MonadFresh (ReaderT r m) where- freshIdent = lift . freshIdent+ freshIdent = lift . freshIdent+ freshIdents = lift . freshIdents instance (Monoid w, MonadFresh m) => MonadFresh (WriterT w m) where- freshIdent = lift . freshIdent+ freshIdent = lift . freshIdent+ freshIdents = lift . freshIdents
+ src/Control/Monad/Trans/FastFresh.hs view
@@ -0,0 +1,114 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-} -- require for MonadError+-- |+-- Copyright : (c) 2010 Simon Meier+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Simon Meier <iridcode@gmail.com>+-- Portability : GHC only+--+-- A monad transformer for passing a fast fresh name supply through a+-- computation. It uses an 'Integer' counter to determine the next free name.+--+-- Modeled after the mtl-2.0 library.+--+module Control.Monad.Trans.FastFresh (++ -- * The Fresh monad+ Fresh+ , runFresh+ , evalFresh+ , execFresh++ -- * The FreshT monad transformer+ , FreshT(..)+ , freshT+ , runFreshT+ , evalFreshT+ , execFreshT++ -- * Fresh name generation+ , FreshState+ , nothingUsed+ , freshIdents++ ) where++import Control.Basics+import Control.Monad.Identity+import Control.Monad.State.Strict+import Control.Monad.Error+import Control.Monad.Reader++------------------------------------------------------------------------------+-- FreshT monad transformer+------------------------------------------------------------------------------++-- | The state of the name supply: the first unused sequence number of every name.+type FreshState = Integer++-- | A computation that can generate fresh variables from name hints.+newtype FreshT m a = FreshT { unFreshT :: StateT FreshState m a }+ deriving( Functor, Applicative, Alternative, Monad, MonadPlus, MonadTrans )++-- | Construct a 'FreshT' action from a 'FreshState' modification.+freshT :: (FreshState -> m (a, FreshState)) -> FreshT m a+freshT = FreshT . StateT++-- | The empty fresh state.+nothingUsed :: FreshState+nothingUsed = 0++-- | Run a computation with a fresh name supply.+runFreshT :: FreshT m a -> FreshState -> m (a, FreshState)+runFreshT (FreshT m) used = runStateT m used++-- | Evaluate a computation with a fresh name supply.+evalFreshT :: Monad m => FreshT m a -> FreshState -> m a+evalFreshT (FreshT m) used = evalStateT m used++-- | Execute a computation with a fresh name supply.+execFreshT :: Monad m => FreshT m a -> FreshState -> m FreshState+execFreshT (FreshT m) used = execStateT m used++-- | Get 'k' fresh identifiers.+freshIdents :: Monad m+ => Integer -- ^ number of desired identifiers+ -> FreshT m Integer -- ^ The first fresh identifier.+freshIdents k = do+ i <- FreshT get+ FreshT $ put $ i + k+ return i++-- Instances+------------++instance MonadError e m => MonadError e (FreshT m) where+ throwError = lift . throwError+ catchError m h = FreshT $ catchError (unFreshT m) (unFreshT . h)++instance MonadReader r m => MonadReader r (FreshT m) where+ ask = lift ask+ local f m = FreshT $ local f $ unFreshT m++instance MonadState s m => MonadState s (FreshT m) where+ get = lift get+ put s = lift $ put s++------------------------------------------------------------------------------+-- Fresh monad+------------------------------------------------------------------------------++type Fresh = FreshT Identity++-- | Run a computation with a fresh name supply.+runFresh :: Fresh a -> FreshState -> (a, FreshState)+runFresh (FreshT m) used = runState m used++-- | Evaluate a computation with a fresh name supply.+evalFresh :: Fresh a -> FreshState -> a+evalFresh (FreshT m) used = evalState m used++-- | Execute a computation with a fresh name supply.+execFresh :: Fresh a -> FreshState -> FreshState+execFresh (FreshT m) used = execState m used
− src/Control/Monad/Trans/Fresh.hs
@@ -1,110 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-} -- require for MonadError--- |--- Copyright : (c) 2010 Simon Meier--- License : GPL v3 (see LICENSE)--- --- Maintainer : Simon Meier <iridcode@gmail.com>--- Portability : GHC only------ A monad transformer for passing a fresh name supply through a computation.--- This is just a newtype wrapper around the 'StateT' monad transformer.------ Modeled after the mtl-2.0 library.----module Control.Monad.Trans.Fresh (-- -- * The Fresh monad- Fresh- , runFresh- , evalFresh- , execFresh-- -- * The FreshT monad transformer- , FreshT(..)- , freshT- , runFreshT- , evalFreshT- , execFreshT-- -- * Fresh name generation- , FreshState- , nothingUsed- , freshIdent-- ) where--import Control.Basics-import Control.Monad.Identity-import Control.Monad.State.Strict-import Control.Monad.Error-import Control.Monad.Reader----------------------------------------------------------------------------------- FreshT monad transformer----------------------------------------------------------------------------------- | The state of the name supply: the last used sequence number of every name.-type FreshState = Int---- | A computation that can generate fresh variables from name hints.-newtype FreshT m a = FreshT { unFreshT :: StateT FreshState m a }- deriving( Functor, Applicative, Alternative, Monad, MonadPlus, MonadTrans )---- | Construct a 'FreshT' action from a 'FreshState' modification.-freshT :: (FreshState -> m (a, FreshState)) -> FreshT m a-freshT = FreshT . StateT---- | The empty fresh state.-nothingUsed :: FreshState-nothingUsed = 0---- | Run a computation with a fresh name supply.-runFreshT :: FreshT m a -> FreshState -> m (a, FreshState)-runFreshT (FreshT m) used = runStateT m used---- | Evaluate a computation with a fresh name supply.-evalFreshT :: Monad m => FreshT m a -> FreshState -> m a-evalFreshT (FreshT m) used = evalStateT m used---- | Execute a computation with a fresh name supply.-execFreshT :: Monad m => FreshT m a -> FreshState -> m FreshState-execFreshT (FreshT m) used = execStateT m used---- | Get a fresh identifier.-freshIdent :: Monad m - => String -- ^ Desired name.- -> FreshT m Int -- ^ Fresh identifier for this name.-freshIdent _ = do- i <- FreshT get- FreshT $ put $ succ i- return i---- Instances---------------instance MonadError e m => MonadError e (FreshT m) where- throwError = lift . throwError- catchError m h = FreshT $ catchError (unFreshT m) (unFreshT . h)--instance MonadReader r m => MonadReader r (FreshT m) where- ask = lift ask- local f m = FreshT $ local f $ unFreshT m----------------------------------------------------------------------------------- Fresh monad---------------------------------------------------------------------------------type Fresh = FreshT Identity---- | Run a computation with a fresh name supply.-runFresh :: Fresh a -> FreshState -> (a, FreshState)-runFresh (FreshT m) used = runState m used---- | Evaluate a computation with a fresh name supply.-evalFresh :: Fresh a -> FreshState -> a-evalFresh (FreshT m) used = evalState m used---- | Execute a computation with a fresh name supply.-execFresh :: Fresh a -> FreshState -> FreshState-execFresh (FreshT m) used = execState m used
+ src/Control/Monad/Trans/PreciseFresh.hs view
@@ -0,0 +1,129 @@+{-# LANGUAGE BangPatterns, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-} -- require for MonadError+-- |+-- Copyright : (c) 2010-2012 Simon Meier+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Simon Meier <iridcode@gmail.com>+-- Portability : GHC only+--+-- A monad transformer for passing a fresh name supply through a computation.+-- The name supply is precise in the sense that every 'String' has its own+-- supply of indices for the next fresh name.+--+-- Modeled after the mtl-2.0 library.+--+module Control.Monad.Trans.PreciseFresh (++ -- * The Fresh monad+ Fresh+ , runFresh+ , evalFresh+ , execFresh++ -- * The FreshT monad transformer+ , FreshT(..)+ , freshT+ , runFreshT+ , evalFreshT+ , execFreshT++ -- * Fresh name generation+ , FreshState+ , nothingUsed+ , freshIdent+ , freshIdents++ ) where++import Control.Basics+import Control.Monad.Identity+import Control.Monad.State.Strict+import Control.Monad.Error+import Control.Monad.Reader++import qualified Data.Map as M++------------------------------------------------------------------------------+-- FreshT monad transformer+------------------------------------------------------------------------------++-- | The state of the name supply: the first unused sequence number of every name.+type FreshState = M.Map String Integer++-- | A computation that can generate fresh variables from name hints.+newtype FreshT m a = FreshT { unFreshT :: StateT FreshState m a }+ deriving( Functor, Applicative, Alternative, Monad, MonadPlus, MonadTrans )++-- | Construct a 'FreshT' action from a 'FreshState' modification.+freshT :: (FreshState -> m (a, FreshState)) -> FreshT m a+freshT = FreshT . StateT++-- | The empty fresh state.+nothingUsed :: FreshState+nothingUsed = M.empty++-- | Run a computation with a fresh name supply.+runFreshT :: FreshT m a -> FreshState -> m (a, FreshState)+runFreshT (FreshT m) used = runStateT m used+evalFreshT :: Monad m => FreshT m a -> FreshState -> m a+evalFreshT (FreshT m) used = evalStateT m used++-- | Execute a computation with a fresh name supply.+execFreshT :: Monad m => FreshT m a -> FreshState -> m FreshState+execFreshT (FreshT m) used = execStateT m used++-- | /O(log(n))/. Get a fresh identifier for the given name.+freshIdent :: Monad m => String -> FreshT m Integer+freshIdent name = do+ m <- FreshT get+ let i = M.findWithDefault 0 name m+ !i' = succ i -- avoid building thunks in the Map+ FreshT (modify (M.insert name i'))+ return i++-- | /O(n)/. Get 'k' fresh identifiers.+freshIdents :: Monad m+ => Integer -- ^ number of desired identifiers+ -> FreshT m Integer -- ^ The first fresh identifier.+freshIdents k = do+ m <- FreshT get+ let maxIdx = maximum $ 0 : map snd (M.toList m)+ nextIdx = maxIdx + k+ -- insert 'nextIdx' at "" to remember it for the next call+ FreshT (put (M.insert "" nextIdx $ M.map (const nextIdx) m))+ return maxIdx+++-- Instances+------------++instance MonadError e m => MonadError e (FreshT m) where+ throwError = lift . throwError+ catchError m h = FreshT $ catchError (unFreshT m) (unFreshT . h)++instance MonadReader r m => MonadReader r (FreshT m) where+ ask = lift ask+ local f m = FreshT $ local f $ unFreshT m++instance MonadState s m => MonadState s (FreshT m) where+ get = lift get+ put s = lift $ put s++------------------------------------------------------------------------------+-- Fresh monad+------------------------------------------------------------------------------++type Fresh = FreshT Identity++-- | Run a computation with a fresh name supply.+runFresh :: Fresh a -> FreshState -> (a, FreshState)+runFresh (FreshT m) used = runState m used++-- | Evaluate a computation with a fresh name supply.+evalFresh :: Fresh a -> FreshState -> a+evalFresh (FreshT m) used = evalState m used++-- | Execute a computation with a fresh name supply.+execFresh :: Fresh a -> FreshState -> FreshState+execFresh (FreshT m) used = execState m used
src/Data/DAG/Simple.hs view
@@ -1,23 +1,36 @@ -- |--- Copyright : (c) 2010 Simon Meier+-- Copyright : (c) 2010,2012 Simon Meier -- License : GPL v3 (see LICENSE) -- -- Maintainer : Simon Meier <iridcode@gmail.com> -- -- Simple vertice list based representation of DAGs and some common operations on it. module Data.DAG.Simple (- toposort+ -- * Computing with binary relations+ Relation+ , inverse+ , image , reachableSet+ , restrict++ -- ** Cycles+ , dfsLoopBreakers , cyclic+ , toposort+ ) where -import Data.List-import qualified Data.Set as S+import Control.Basics+import Control.Monad.Writer+import Control.Monad.RWS -import Control.Basics-import Control.Monad.Writer+import Data.List+import qualified Data.DList as D+import qualified Data.Set as S +-- import Test.QuickCheck.Property (label)+-- import Test.QuickCheck (quickCheck) -- | Produce a topological sorting of the given relation. If the relation is -- cyclic, then the result is at least some permutation of all elements of@@ -31,7 +44,7 @@ | otherwise = foldM visit (S.insert x visited) preds <* tell (pure x) where- preds = [ e | (e,e') <- dag, e' == x ]+ preds = x `image` inverse dag -- | Compute the set of nodes reachable from the given set of nodes.@@ -42,9 +55,7 @@ visit visited x | x `S.member` visited = visited | otherwise =- foldl' visit (S.insert x visited) succs- where- succs = [ e' | (e,e') <- dag, e == x ]+ foldl' visit (S.insert x visited) (x `image` dag) -- | Is the relation cyclic. cyclic :: Ord a => [(a,a)] -> Bool@@ -64,3 +75,66 @@ next = [ e' | (e,e') <- rel, e == x ] parents' = S.insert x parents ++-- TODO: Consider implementing something along the lines of Ann Becker, Dan+-- Geiger, Optimization of Pearl's method of conditioning and greedy-like+-- approximation algorithms for the vertex feedback set problem, Artificial+-- Intelligence, Volume 83, Issue 1, May 1996, Pages 167-188, ISSN 0004-3702,+-- 10.1016/0004-3702(95)00004-6.+-- <http://www.sciencedirect.com/science/article/pii/0004370295000046>.++-- | Compute a minimal set of loop-breakers using a greedy DFS strategy. A set+-- of loop-breakers is a set of nodes such that removing them ensures the+-- acyclicity of the relation. It is minimal, if no node can be removed from+-- the set.+dfsLoopBreakers :: Ord a => [(a,a)] -> [a]+dfsLoopBreakers rel = + D.toList $ snd $ execRWS (mapM_ (visit . fst) rel) () S.empty+ where + visit x = do+ visited <- gets (S.member x)+ unless visited $ findLoopBreakers S.empty x++ -- PRE: x0 is not yet visited+ findLoopBreakers parents0 x = do+ modify (S.insert x)+ let parents = S.insert x parents0+ ys = x `image` rel+ if any (`S.member` parents) ys+ then tell (return x) + else forM_ ys $ \y -> do + visited <- gets (S.member y)+ unless visited $ findLoopBreakers parents y++-- | A relation represented as a list of tuples.+type Relation a = [(a,a)]++-- | Restrict a relation to elements satisfying a predicate.+restrict :: Eq a => (a -> Bool) -> Relation a -> Relation a+restrict p = filter (\(x,y) -> p x && p y)++-- | The image of an element under a 'Relation'.+image :: Eq a => a -> Relation a -> [a]+image x rel = [ y' | (x', y') <- rel, x == x' ]++-- | The inverse of a 'Relation'.+inverse :: Relation a -> Relation a+inverse rel = [ (y,x) | (x, y) <- rel ]++{-+prop_dfsLoopBreakers noSelfLoops rel0+ | cyclic rel = label cycleLabel (minimal && not (cyclic (rel' breakers)))+ | otherwise = label "acyclic" (null breakers)+ where+ -- remove (x,x) entries in half of the cases+ removeSelfLoops | noSelfLoops = filter (not . (uncurry (==)))+ | otherwise = id+ -- restrict the relation to get more cyclic cases+ rel = removeSelfLoops $ map ((`mod` (20 :: Int)) *** (`mod` 20)) rel0+ rel' bs = restrict (not . (`elem` bs)) rel+ breakers = dfsLoopBreakers rel+ cycleLabel | any (uncurry (==)) rel = "cyclic (with self-loop)"+ | otherwise = "cyclic (no self-loop)"+ -- true if loop breakers are minimal+ minimal = all (\b -> cyclic (rel' (filter (/= b) breakers))) breakers+-}
src/Extension/Data/Bounded.hs view
@@ -7,6 +7,7 @@ -- Monoids for bounded types. module Extension.Data.Bounded ( BoundedMax(..)+ , BoundedMin(..) ) where import Data.Monoid@@ -14,11 +15,15 @@ -- | A newtype wrapper for a monoid of the maximum of a bounded type. newtype BoundedMax a = BoundedMax {getBoundedMax :: a} deriving( Eq, Ord, Show )- + instance (Ord a, Bounded a) => Monoid (BoundedMax a) where mempty = BoundedMax minBound (BoundedMax x) `mappend` (BoundedMax y) = BoundedMax (max x y) -+-- | A newtype wrapper for a monoid of the minimum of a bounded type.+newtype BoundedMin a = BoundedMin {getBoundedMin :: a}+ deriving( Eq, Ord, Show ) --- TODO: Add BoundedMin+instance (Ord a, Bounded a) => Monoid (BoundedMin a) where+ mempty = BoundedMin maxBound+ (BoundedMin x) `mappend` (BoundedMin y) = BoundedMin (min x y)
+ src/Extension/Data/ByteString.hs view
@@ -0,0 +1,15 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- |+-- Copyright : (c) 2012 Benedikt Schmidt+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>+--+-- Provide NFData instance for ByteString+module Extension.Data.ByteString (+ ) where++import qualified Data.ByteString as B+import Control.DeepSeq++instance NFData B.ByteString
+ src/Extension/Data/Monoid.hs view
@@ -0,0 +1,44 @@+{-# LANGUAGE CPP #-}+-- |+-- Copyright : (c) 2012 Simon Meier+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Simon Meier <iridcode@gmail.com>+--+-- A variant of "Data.Monoid" that also exports '(<>)' for 'mappend'.+module Extension.Data.Monoid (+ (<>)+ , module Data.Monoid++ , MinMax(..)+ , minMaxSingleton+ ) where++import Data.Monoid++#if __GLASGOW_HASKELL__ < 704++infixr 6 <>++-- | An infix synonym for 'mappend'.+(<>) :: Monoid m => m -> m -> m+(<>) = mappend+{-# INLINE (<>) #-}++#endif++-- | A newtype wrapper around 'Maybe' that returns a tuple of the minimum and+-- maximum value encountered, if there was any.+newtype MinMax a = MinMax { getMinMax :: Maybe (a, a) }++-- | Construct a 'MinMax' value from a singleton value.+minMaxSingleton :: a -> MinMax a+minMaxSingleton x = MinMax (Just (x, x))++instance Ord a => Monoid (MinMax a) where+ mempty = MinMax Nothing++ MinMax Nothing `mappend` y = y+ x `mappend` MinMax Nothing = x+ MinMax (Just (xMin, xMax)) `mappend` MinMax (Just (yMin, yMax)) =+ MinMax (Just (min xMin yMin, max xMax yMax))
src/Extension/Prelude.hs view
@@ -21,7 +21,6 @@ import System.IO - -- Bool -- ---------- @@ -37,18 +36,57 @@ singleton x = [x] -- | check whether the given list contains no duplicates+{-# INLINABLE unique #-} unique :: Eq a => [a] -> Bool unique [] = True unique (x:xs) = x `notElem` xs && unique xs -- | Sort list and remove duplicates. O(n*log n)+{-# INLINE sortednub #-} sortednub :: Ord a => [a] -> [a]-sortednub = map head . group . sort+sortednub = sortednubBy compare +-- | Sort a list according to a user-defined comparison function and remove+-- duplicates.+{-# INLINABLE sortednubBy #-}+sortednubBy :: (a -> a -> Ordering) -> [a] -> [a]+sortednubBy cmp = + -- Adapted from GHC's Data.List module+ -- Copyright: (c) The University of Glasgow 2001+ mergeAll . sequences+ where+ sequences (a:xs@(b:xs')) = case a `cmp` b of+ GT -> descending b [a] xs'+ EQ -> sequences xs+ LT -> ascending b (a:) xs+ sequences xs = [xs]++ descending a as (b:bs)+ | a `cmp` b == GT = descending b (a:as) bs+ descending a as bs = (a:as): sequences bs++ ascending a as (b:bs)+ | a `cmp` b == LT = ascending b (\ys -> as (a:ys)) bs+ ascending a as bs = as [a] : sequences bs++ mergeAll [x] = x+ mergeAll xs = mergeAll (mergePairs xs)++ mergePairs (a:b:xs) = merge a b: mergePairs xs+ mergePairs xs = xs++ merge [] bs = bs+ merge as [] = as+ merge as@(a:as') bs@(b:bs') = case a `cmp` b of+ GT -> b : merge as bs'+ EQ -> merge as bs' -- equal elements are dropped+ LT -> a : merge as' bs+ -- | //O(n*log n).// Sort list and remove duplicates with respect to a -- projection. +{-# INLINE sortednubOn #-} sortednubOn :: Ord b => (a -> b) -> [a] -> [a]-sortednubOn proj = map head . groupOn proj . sortOn proj+sortednubOn proj = sortednubBy (comparing proj) -- | Keep only the first element of elements having the same projected value nubOn :: Eq b => (a -> b) -> [a] -> [a]
src/Text/Dot.hs view
@@ -50,8 +50,10 @@ , mrecord_ ) where -import Data.List (intersperse)-import Control.Monad (liftM)+import Data.Char (isSpace)+import Data.List (intersperse)+import Control.Monad (liftM, ap)+import Control.Applicative (Applicative(..)) data NodeId = NodeId String | UserNodeId Int@@ -70,18 +72,35 @@ data Dot a = Dot { unDot :: Int -> ([GraphElement],Int,a) } +instance Functor Dot where+ fmap f m = Dot $ \ uq -> case unDot m uq of (a,b,x) -> (a,b,f x)++instance Applicative Dot where+ pure = return+ (<*>) = ap+ 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) --- | 'node' takes a list of attributes, generates a new node, and gives a 'NodeId'.-node :: [(String,String)] -> Dot NodeId-node attrs = Dot $ \ uq -> let nid = NodeId $ "n" ++ show uq - in ( [ GraphNode nid attrs ],succ uq,nid)+-- | '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 + in ( [ GraphNode nid attrs ],succ uq,nid) +-- | 'node' takes a list of attributes, generates a new node, and gives a+-- 'NodeId'. Multi-line labels are fixed such that they use non-breaking+-- spaces and are terminated with a new-line.+node :: [(String,String)] -> Dot NodeId+node = rawNode . map fixLabel+ where+ fixLabel ("label",lbl) = ("label", fixMultiLineLabel lbl)+ fixLabel attr = attr + -- | 'userNodeId' allows a user to use their own (Int-based) node id's, without needing to remap them. userNodeId :: Int -> NodeId userNodeId i = UserNodeId i@@ -158,11 +177,22 @@ showAttrs' [] = error "showAttrs: the impossible happended" showAttr :: (String, String) -> String-showAttr (name,val) = name ++ "=\"" ++ concatMap escape val ++ "\""- where escape '\n' = "\\l"- escape '"' = "\\\""- escape c = [c]+showAttr (name, val) =+ name ++ "=\"" ++ concatMap escape val ++ "\""+ where + escape '\n' = "\\l"+ escape '"' = "\\\""+ escape c = [c] +-- | Ensure that multi-line labels use non-breaking spaces at the start and+-- are terminated with a newline.+fixMultiLineLabel :: String -> String+fixMultiLineLabel lbl+ | '\n' `elem` lbl = unlines $ map useNonBreakingSpace $ lines lbl+ | otherwise = lbl+ where+ useNonBreakingSpace line = case span isSpace line of+ (spaces, rest) -> concat (replicate (length spaces) " ") ++ rest ------------------------------------------------------------------------------ -- Records@@ -177,16 +207,21 @@ | VCat [Record a] deriving( Eq, Ord, Show ) +-- | Smart constructor for fields that massages the multi-line labels such+-- that dot understands them.+mkField :: Maybe a -> String -> Record a+mkField port = Field port . fixMultiLineLabel+ -- | A simple field of a record. field :: String -> Record a-field = Field Nothing+field = mkField Nothing -- | A field together with a port which can be used to create direct edges to -- this field. Note that you can use any type to identify the ports. When -- creating a record node you will get back an association list between your -- record identifiers and their concrete node ids. portField :: a -> String -> Record a-portField port = Field (Just port)+portField port = mkField (Just port) -- | Concatenate records horizontally. hcat :: [Record a] -> Record a@@ -235,11 +270,12 @@ esc '>' = "\\>" esc c = [c] + -- | A generic version of record creation. genRecord :: String -> Record a -> [(String,String)] -> Dot (NodeId, [(a,NodeId)]) genRecord shape rec attrs = do (lbl, ids) <- renderRecord rec- i <- node ([("shape",shape),("label",lbl)] ++ attrs)+ i <- rawNode ([("shape",shape),("label",lbl)] ++ attrs) return (i, ids i) -- | Create a record node with the given attributes. It returns the node-id of
− src/Text/Isar.hs
@@ -1,319 +0,0 @@--- |--- Copyright : (c) 2011 Simon Meier--- License : GPL v3 (see LICENSE)--- --- Maintainer : Simon Meier <iridcode@gmail.com>--- Portability : portable------ Generating Isabelle/ISAR theory files using 'Text.PrettyPrint'.-module Text.Isar (- -- * ISAR Output- Isar(..)- -- ** Configuration- , IsarStyle(..)- , IsarConf(..)- , defaultIsarConf- , isPlainStyle- , isarPlain- , isarXSymbol-- -- ** Constructions of our security protocol verification theory- , isaExecutionSystemState-- -- ** Special Symbols- , isarightArrow- , isaLongRightArrow- , isaLParr- , isaRParr- , isaLBrack- , isaRBrack- , isaMetaAll- , isaExists- , isaAnd- , isaNotIn- , isaIn- , isaSubsetEq- , isaAlpha- , isaSublocale-- -- * Extensions of 'Text.PrettyPrint'- , module Text.PrettyPrint.Class- , nestBetween- , nestShort- , nestShort'- , nestShortNonEmpty- , nestShortNonEmpty'- , fixedWidthText- , symbol- , numbered- , numbered'--) where--import Data.List--import Extension.Prelude--import Text.PrettyPrint.Class---- | The ISAR style to be used for output.-data IsarStyle = - PlainText - | XSymbol- deriving( Eq, Show )---- | The configuration to be used for output. Apart from the ISAR style, the--- configuration also stores the representation of the reachable state of the--- protocol which we are reasoning about. -data IsarConf = IsarConf {- isarStyle :: IsarStyle- , isarTrace :: Doc -- ^ The ISAR code of the trace- , isarPool :: Doc -- ^ The ISAR code of the thread pool- , isarSubst :: Doc -- ^ The ISAR code of the substitution- }- deriving( Show )---- | Default configuration: plaintext ISAR style and reachable state @(t,r,s)@.-defaultIsarConf :: IsarConf-defaultIsarConf = IsarConf PlainText (char 't') (char 'r') (char 's') ---- | Check if the plaintext style was chosen.-isPlainStyle :: IsarConf -> Bool-isPlainStyle = (PlainText ==) . isarStyle----- | Values that can be output as ISAR code. ------ Minimal definition: 'isar'-class Isar a where- isar :: IsarConf -> a -> Doc---- | Output as ISAR code using 'defaultIsarConf'.-isarPlain :: Isar a => a -> Doc-isarPlain = isar defaultIsarConf---- | Output as ISAR code using 'defaultIsarConf'--- with the XSymbol style.-isarXSymbol :: Isar a => a -> Doc-isarXSymbol = isar (defaultIsarConf { isarStyle = XSymbol })----------------------------------------------------------------------------------- General pretty printing combinators----------------------------------------------------------------------------------- | Nest a document surrounded by a leading and a finishing document breaking--- lead, body, and finish onto separate lines, if they don't fit on a single--- line.-nestBetween :: Document d =>- Int -- ^ Indent of body- -> d -- ^ Leading document- -> d -- ^ Finishing document- -> d -- ^ Body document- -> d-nestBetween n l r x = sep [l, nest n x, r]---- | Nest a document surrounded by a leading and a finishing document with an--- non-compulsory break between lead and body.-nestShort :: Document d =>- Int -- ^ Indent of body- -> d -- ^ Leading document- -> d -- ^ Finishing document- -> d -- ^ Body document- -> d-nestShort n lead finish body = sep [lead $$ nest n body, finish]---- | Nest document between two strings and indent body by @length lead + 1@.-nestShort' :: Document d => String -> String -> d -> d-nestShort' lead finish = - nestShort (length lead + 1) (text lead) (text finish)---- | Like 'nestShort' but doesn't print the lead and finish, if the document is--- empty.-nestShortNonEmpty :: Document d => Int -> d -> d -> d -> d-nestShortNonEmpty n lead finish body =- caseEmptyDoc emptyDoc (nestShort n lead finish body) body---- | Like 'nestShort'' but doesn't print the lead and finish, if the document is--- empty.-nestShortNonEmpty' :: Document d => String -> String -> d -> d-nestShortNonEmpty' lead finish = - nestShortNonEmpty (length lead + 1) (text lead) (text finish)---- | Output text with a fixed width: if it is smaller then nothing happens,--- otherwise care is taken to make the text appear having the given width.-fixedWidthText :: Document d => Int -> String -> d-fixedWidthText n cs- | length cs <= n = text cs- | otherwise = text as <> zeroWidthText bs- where - (as,bs) = splitAt n cs---- | Print string as symbol having width 1.-symbol :: Document d => String -> d-symbol = fixedWidthText 1---- | Number a list of documents that are vertically separated by the given--- separator.-numbered :: Document d => d -> [d] -> d-numbered _ [] = emptyDoc-numbered vsep ds = - foldr1 ($-$) $ intersperse vsep $ map pp $ zip [(1::Int)..] ds- where- n = length ds- nWidth = length (show n)- pp (i, d) = text (flushRight nWidth (show i)) <> d- --- | Number a list of documents with numbers terminated by "." and vertically--- separate using an empty line.-numbered' :: Document d => [d] -> d-numbered' = numbered (text "") . map (text ". " <>)------------------------------------------------------------------------------------ Operational Semantics Constructions----------------------------------------------------------------------------------- | Isabelle representation of the exeuction system state of our operational--- semantics.-isaExecutionSystemState :: IsarConf -> Doc-isaExecutionSystemState conf = - parens . hcat . punctuate comma $ - [isarTrace conf, isarPool conf, isarSubst conf]------------------------------------------------------------------------------------ Isabelle symbols in both styles.----------------------------------------------------------------------------------- | A 'not in' symbol: @~:@-isaNotIn :: Document d => IsarConf -> d-isaNotIn conf- | isPlainStyle conf = text "~:"- | otherwise = symbol "\\<notin>"---- | An 'in' symbol: @:@-isaIn :: Document d => IsarConf -> d-isaIn conf- | isPlainStyle conf = text ":"- | otherwise = symbol "\\<in>"---- | A left parenthesis with an additional vertical line: @(|@-isaLParr :: Document d => IsarConf -> d-isaLParr conf- | isPlainStyle conf = text "(|"- | otherwise = symbol "\\<lparr>"---- | A right parenthesis with an additional vertical line: @|)@-isaRParr :: Document d => IsarConf -> d-isaRParr conf- | isPlainStyle conf = text "|)"- | otherwise = symbol "\\<rparr>"---- | A left bracket with an additional vertical line: @[|@-isaLBrack :: Document d => IsarConf -> d-isaLBrack conf- | isPlainStyle conf = text "[|"- | otherwise = symbol "\\<lbrakk>"---- | A right bracket with an additional vertical line: @|]@-isaRBrack :: Document d => IsarConf -> d-isaRBrack conf- | isPlainStyle conf = text "|]"- | otherwise = symbol "\\<rbrakk>"---- | A short right arrow: @->@-isarightArrow :: Document d => IsarConf -> d-isarightArrow conf- | isPlainStyle conf = text "->"- | otherwise = fixedWidthText 2 "\\<rightarrow>"---- | A long double right arrow: @==>@-isaLongRightArrow :: Document d => IsarConf -> d-isaLongRightArrow conf- | isPlainStyle conf = text "==>"- | otherwise = fixedWidthText 3 "\\<Longrightarrow>"----- | The greek letter alpha: @\\<alpha>@-isaAlpha :: Document d => IsarConf -> d-isaAlpha conf- | isPlainStyle conf = text "\\<alpha>"- | otherwise = symbol "\\<alpha>"---- | The meta all quantifier: @!!@-isaMetaAll :: Document d => IsarConf -> d-isaMetaAll conf- | isPlainStyle conf = text "!! "- | otherwise = symbol "\\<And>"---- | The exists symbol: @?@-isaExists :: Document d => IsarConf -> d-isaExists conf- | isPlainStyle conf = text "? "- | otherwise = symbol "\\<exists>"---- | The logical and symbol: @&@-isaAnd :: Document d => IsarConf -> d-isaAnd conf- | isPlainStyle conf = text "&"- | otherwise = symbol "\\<and>"---- | The non-strict subset symbol.-isaSubsetEq :: Document d => IsarConf -> d-isaSubsetEq conf- | isPlainStyle conf = text "<="- | otherwise = symbol "\\<subseteq>"---- | The sublocale sign.-isaSublocale :: Document d => IsarConf -> d-isaSublocale conf- | isPlainStyle conf = text "<"- | otherwise = symbol "\\<subseteq>"----------------------------------------------------------------------------------- Isabelle theory components---------------------------------------------------------------------------------{- TODO: Finish, if it is used--isaTheory :: Document d =>- String -- ^ Theory name- -> [String] -- ^ Imported theories- -> d -- ^ Theory body- -> d -- ^ The complete theory statement.-isaTheory name imports body =- text "theory" <-> text name $-$- text "imports" $-$- nest 2 (vcat $ map (text . (++"\"") . ('"':)) imports) $-$- text "begin" $-$ text "" $-$- body $-$- text "" $-$ text "end"----- | An logic identifier; properly escaped if needed.--- TODO: Add escaping-logicIdent :: String -> Doc-logicIdent = text----- | A generic text command.-genTextCmd :: String -> String -> Doc-genTextCmd name content = - sep [text name <> text "{*", nest 2 (fsep . map text $ words content), text "*}"]--chapter = genTextCmd "chapter"-section = genTextCmd "section"-subsection = genTextCmd "subsection"-subsubsection = genTextCmd "subsubsection"-paragraph = genTextCmd "text"---- | A comment.-comment :: String -> Doc-comment content = nestShort' "(*" "*)" (fsep $ map text $ words content)---- | Switch into a proof context.-context :: String -> Doc -> Doc-context name body = vcat [text name <-> text "begin", body, text "end"]---}-
src/Text/PrettyPrint/Class.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fno-warn-orphans #-} -- | -- Copyright : (c) 2011 Simon Meier -- License : GPL v3 (see LICENSE)@@ -6,18 +7,19 @@ -- -- 'Document' class allowing to have different interpretations of the -- HughesPJ pretty-printing combinators.-{-# OPTIONS_GHC -fno-warn-orphans #-} module Text.PrettyPrint.Class ( P.Doc , Document(..) , P.isEmpty , P.render , P.renderStyle- , P.style+ , defaultStyle , P.Style(..) , P.Mode(..) , ($--$)+ , emptyDoc+ , (<>) , semi , colon , comma@@ -43,22 +45,38 @@ , hang , punctuate++ -- * Additional combinators+ , nestBetween+ , nestShort+ , nestShort'+ , nestShortNonEmpty+ , nestShortNonEmpty'+ , fixedWidthText+ , symbol+ , numbered+ , numbered' ) where -import Prelude+import Control.DeepSeq (NFData(..))++import Data.List (intersperse)++import Extension.Data.Monoid (Monoid(..), (<>))+import Extension.Prelude (flushRight)+ import qualified Text.PrettyPrint.HughesPJ as P-import Control.DeepSeq -infixl 6 <> -infixl 6 <->+infixr 6 <-> infixl 5 $$, $-$, $--$ -class NFData d => Document d where+-- emptyDoc = P.empty+-- (<>) = (P.<>)++class (Monoid d, NFData d) => Document d where char :: Char -> d text :: String -> d zeroWidthText :: String -> d- emptyDoc :: d- (<>) :: d -> d -> d (<->) :: d -> d -> d hcat :: [d] -> d hsep :: [d] -> d@@ -72,27 +90,13 @@ nest :: Int -> d -> d caseEmptyDoc :: d -> d -> d -> d -instance NFData P.Doc where- rnf = rnf . P.render+-- | The default 'P.Style'.+defaultStyle :: P.Style+defaultStyle = P.style -instance Document P.Doc where- char = P.char- text = P.text- zeroWidthText = P.zeroWidthText- emptyDoc = P.empty- (<>) = (P.<>)- (<->) = (P.<+>)- hcat = P.hcat- hsep = P.hsep- ($$) = (P.$$)- ($-$) = (P.$+$)- vcat = P.vcat- sep = P.sep- cat = P.cat- fsep = P.fsep- fcat = P.fcat- nest = P.nest- caseEmptyDoc yes no d = if P.isEmpty d then yes else no+-- | The empty document.+emptyDoc :: Document d => d+emptyDoc = mempty -- | Vertical concatentation of two documents with an empty line in between. ($--$) :: Document d => d -> d -> d@@ -145,3 +149,99 @@ where go d' [] = [d'] go d' (e:es) = (d' <> p) : go e es+++------------------------------------------------------------------------------+-- The 'Document' instance for 'Text.PrettyPrint.Doc'+------------------------------------------------------------------------------++instance NFData P.Doc where+ rnf = rnf . P.render++instance Document P.Doc where+ char = P.char+ text = P.text+ zeroWidthText = P.zeroWidthText+ (<->) = (P.<+>)+ hcat = P.hcat+ hsep = P.hsep+ ($$) = (P.$$)+ ($-$) = (P.$+$)+ vcat = P.vcat+ sep = P.sep+ cat = P.cat+ fsep = P.fsep+ fcat = P.fcat+ nest = P.nest+ caseEmptyDoc yes no d = if P.isEmpty d then yes else no++------------------------------------------------------------------------------+-- Additional combinators+------------------------------------------------------------------------------++-- | Nest a document surrounded by a leading and a finishing document breaking+-- lead, body, and finish onto separate lines, if they don't fit on a single+-- line.+nestBetween :: Document d =>+ Int -- ^ Indent of body+ -> d -- ^ Leading document+ -> d -- ^ Finishing document+ -> d -- ^ Body document+ -> d+nestBetween n l r x = sep [l, nest n x, r]++-- | Nest a document surrounded by a leading and a finishing document with an+-- non-compulsory break between lead and body.+nestShort :: Document d =>+ Int -- ^ Indent of body+ -> d -- ^ Leading document+ -> d -- ^ Finishing document+ -> d -- ^ Body document+ -> d+nestShort n lead finish body = sep [lead $$ nest n body, finish]++-- | Nest document between two strings and indent body by @length lead + 1@.+nestShort' :: Document d => String -> String -> d -> d+nestShort' lead finish = + nestShort (length lead + 1) (text lead) (text finish)++-- | Like 'nestShort' but doesn't print the lead and finish, if the document is+-- empty.+nestShortNonEmpty :: Document d => Int -> d -> d -> d -> d+nestShortNonEmpty n lead finish body =+ caseEmptyDoc emptyDoc (nestShort n lead finish body) body++-- | Like 'nestShort'' but doesn't print the lead and finish, if the document is+-- empty.+nestShortNonEmpty' :: Document d => String -> String -> d -> d+nestShortNonEmpty' lead finish = + nestShortNonEmpty (length lead + 1) (text lead) (text finish)++-- | Output text with a fixed width: if it is smaller then nothing happens,+-- otherwise care is taken to make the text appear having the given width.+fixedWidthText :: Document d => Int -> String -> d+fixedWidthText n cs+ | length cs <= n = text cs+ | otherwise = text as <> zeroWidthText bs+ where+ (as,bs) = splitAt n cs++-- | Print string as symbol having width 1.+symbol :: Document d => String -> d+symbol = fixedWidthText 1++-- | Number a list of documents that are vertically separated by the given+-- separator.+numbered :: Document d => d -> [d] -> d+numbered _ [] = emptyDoc+numbered vsep ds = + foldr1 ($-$) $ intersperse vsep $ map pp $ zip [(1::Int)..] ds+ where+ n = length ds+ nWidth = length (show n)+ pp (i, d) = text (flushRight nWidth (show i)) <> d++-- | Number a list of documents with numbers terminated by "." and vertically+-- separate using an empty line.+numbered' :: Document d => [d] -> d+numbered' = numbered (text "") . map (text ". " <>)
src/Text/PrettyPrint/Highlight.hs view
@@ -29,13 +29,12 @@ ) where import Text.PrettyPrint.Class-import Control.DeepSeq -- | Currently we support only keywords, operators, and comments. data HighlightStyle = Keyword | Comment | Operator deriving( Eq, Ord, Show ) -class (NFData d, Document d) => HighlightDocument d where+class Document d => HighlightDocument d where -- 'highlight' @style d@ marks that the document @d@ should be highlighted -- using the @style@. highlight :: HighlightStyle -> d -> d
src/Text/PrettyPrint/Html.hs view
@@ -31,6 +31,7 @@ import Data.Char (isSpace) import Data.Traversable (sequenceA)+import Data.Monoid import Control.Arrow (first) import Control.Applicative@@ -89,6 +90,7 @@ -- | A 'Document' transformer that adds proper HTML escaping. newtype HtmlDoc d = HtmlDoc { getHtmlDoc :: d }+ deriving( Monoid ) -- | Wrap a document such that HTML markup can be added without disturbing the -- layout.@@ -102,9 +104,7 @@ char = HtmlDoc . text . escapeHtmlEntities . return text = HtmlDoc . text . escapeHtmlEntities zeroWidthText = HtmlDoc . zeroWidthText . escapeHtmlEntities- emptyDoc = HtmlDoc emptyDoc - HtmlDoc d1 <> HtmlDoc d2 = HtmlDoc $ d1 <> d2 HtmlDoc d1 <-> HtmlDoc d2 = HtmlDoc $ d1 <-> d2 hcat = HtmlDoc . hcat . map getHtmlDoc hsep = HtmlDoc . hsep . map getHtmlDoc@@ -170,6 +170,7 @@ newtype NoHtmlDoc d = NoHtmlDoc { unNoHtmlDoc :: Identity d } deriving( Functor, Applicative ) + -- | Wrap a document such that all 'HtmlDocument' specific methods are ignored. noHtmlDoc :: d -> NoHtmlDoc d noHtmlDoc = NoHtmlDoc . Identity@@ -181,12 +182,14 @@ instance NFData d => NFData (NoHtmlDoc d) where rnf = rnf . getNoHtmlDoc +instance Monoid d => Monoid (NoHtmlDoc d) where+ mempty = pure mempty+ mappend = liftA2 mappend+ instance Document d => Document (NoHtmlDoc d) where char = pure . char text = pure . text zeroWidthText = pure . zeroWidthText- emptyDoc = pure emptyDoc- (<>) = liftA2 (<>) (<->) = liftA2 (<->) hcat = liftA hcat . sequenceA hsep = liftA hsep . sequenceA
src/Utils/Misc.hs view
@@ -1,12 +1,7 @@ {-# LANGUAGE DeriveDataTypeable, RankNTypes, ScopedTypeVariables, BangPatterns #-} module Utils.Misc (- invertMap-- , pNat- , commaWS- -- * Environment- , envIsSet+ envIsSet , getEnvMaybe -- * List operations@@ -19,19 +14,23 @@ -- * Hashing , stringSHA256++ -- * Set operations+ , setAny++ -- * Map operations+ , invertMap ) where import Data.List import System.Environment import System.IO.Unsafe import Data.Maybe+import Data.Set (Set) import qualified Data.Set as S import Data.Map ( Map ) import qualified Data.Map as M-import Control.Applicative -import Text.ParserCombinators.Parsec hiding (many, optional, (<|>))- import Data.Digest.Pure.SHA (bytestringDigest, sha256) import Blaze.ByteString.Builder (toLazyByteString) import qualified Data.ByteString.Char8 as C8@@ -61,14 +60,6 @@ invertMap :: (Ord k, Ord v) => Map k v -> Map v k invertMap = M.fromList . map (uncurry (flip (,))) . M.toList --- | parse natural number-pNat :: GenParser Char st Int-pNat = read <$> many1 digit---- | parse comma-commaWS :: GenParser Char st ()-commaWS = char ',' *> spaces- -- | @whileTrue m@ iterates m until it returns @False@. -- Returns the number of iterations @m@ was run. @0@ -- means @m@ never returned @True@.@@ -93,3 +84,6 @@ replace '/' = '_' replace '+' = '-' replace c = c++setAny :: (a -> Bool) -> Set a -> Bool+setAny f = S.foldr (\x b -> f x || b) False
tamarin-prover-utils.cabal view
@@ -2,7 +2,7 @@ cabal-version: >= 1.8 build-type: Simple-version: 0.1.0.0+version: 0.4.0.0 license: GPL license-file: LICENSE category: Theorem Provers@@ -13,7 +13,7 @@ synopsis: Utility library for the tamarin prover. -description: This is an internal library of the @tamarin@ prover for+description: This is an internal library of the Tamarin prover for security protocol verification (<hackage.haskell.org/package/tamarin-prover>). @@ -25,28 +25,34 @@ ---------------------- library+ ghc-prof-options: -auto-all+ build-depends: base == 4.* , mtl == 2.0.*+ , bytestring == 0.9.* , transformers == 0.2.*- , containers == 0.4.*- , fclabels == 1.0.*+ , containers >= 0.4.2 && < 0.5+ , fclabels == 1.1.* , blaze-builder == 0.3.* , base64-bytestring >= 0.1.0.3 && < 0.2 , bytestring == 0.9.*- , SHA == 1.4.*+ , SHA == 1.5.* , parsec == 3.1.*- , deepseq == 1.1.*+ , deepseq == 1.3.* , syb >= 0.3.3 && < 0.4 , pretty == 1.1.*- , time == 1.2.*+ , time >= 1.2 && < 1.5 , binary == 0.5.*+ , dlist == 0.5.* hs-source-dirs: src exposed-modules: Control.Basics Control.Monad.Fresh+ Control.Monad.Trans.PreciseFresh+ Control.Monad.Trans.FastFresh Control.Monad.Bind Control.Monad.Disj @@ -55,10 +61,11 @@ Extension.Prelude Extension.Data.Label+ Extension.Data.Monoid Extension.Data.Bounded+ Extension.Data.ByteString Text.Dot- Text.Isar Text.PrettyPrint.Class Text.PrettyPrint.Highlight Text.PrettyPrint.Html@@ -72,7 +79,6 @@ Utils.Misc other-modules:- Control.Monad.Trans.Fresh Control.Monad.Fresh.Class Control.Monad.Trans.Disj