packages feed

tamarin-prover-utils 0.6.0.0 → 0.8.0.0

raw patch · 6 files changed

+87/−19 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

- Extension.Data.Monoid: (<>) :: Monoid m => m -> m -> m
+ Control.Monad.Fresh: scopeFreshness :: MonadFresh m => m a -> m a
+ Control.Monad.Trans.FastFresh: scopeFreshness :: Monad m => FreshT m a -> FreshT m a
+ Control.Monad.Trans.PreciseFresh: scopeFreshness :: Monad m => FreshT m a -> FreshT m a
+ Text.Unicode: subscript :: String -> String
+ Text.Unicode: subscriptChar :: Char -> Char

Files

src/Control/Monad/Fresh/Class.hs view
@@ -1,7 +1,7 @@ -- | -- Copyright   : (c) 2010 Simon Meier -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Simon Meier <iridcode@gmail.com> -- Portability : portable --@@ -18,8 +18,8 @@ import Control.Monad.Reader import Control.Monad.Writer -import qualified Control.Monad.Trans.FastFresh    as Fast (FreshT, freshIdents)-import qualified Control.Monad.Trans.PreciseFresh as Precise (FreshT, freshIdent, freshIdents)+import qualified Control.Monad.Trans.FastFresh    as Fast+import qualified Control.Monad.Trans.PreciseFresh as Precise  -- Added 'Applicative' until base states this hierarchy class (Applicative m, Monad m) => MonadFresh m where@@ -32,14 +32,19 @@     freshIdents :: Integer    -- ^ Number of desired fresh identifiers.                 -> m Integer  -- ^ The first Fresh identifier. +    -- | Scope the 'freshIdent' and 'freshIdents' requests such that these+    -- variables are not marked as used once the scope is left.+    scopeFreshness :: m a -> m a  instance (Functor m, Monad m) => MonadFresh (Fast.FreshT m) where     freshIdent _name = Fast.freshIdents 1     freshIdents      = Fast.freshIdents+    scopeFreshness   = Fast.scopeFreshness  instance (Functor m, Monad m) => MonadFresh (Precise.FreshT m) where-    freshIdent  = Precise.freshIdent-    freshIdents = Precise.freshIdents+    freshIdent     = Precise.freshIdent+    freshIdents    = Precise.freshIdents+    scopeFreshness = Precise.scopeFreshness   ----------------------------------------------------------------------------@@ -48,17 +53,21 @@ -- TODO: Add remaining ones  instance MonadFresh m => MonadFresh (MaybeT m) where-    freshIdent  = lift . freshIdent-    freshIdents = lift . freshIdents+    freshIdent       = lift . freshIdent+    freshIdents      = lift . freshIdents+    scopeFreshness m = MaybeT $ scopeFreshness (runMaybeT m)  instance MonadFresh m => MonadFresh (StateT s m) where     freshIdent  = lift . freshIdent     freshIdents = lift . freshIdents+    scopeFreshness m = StateT $ \s -> scopeFreshness (runStateT m s)  instance MonadFresh m => MonadFresh (ReaderT r m) where-    freshIdent  = lift . freshIdent-    freshIdents = lift . freshIdents+    freshIdent       = lift . freshIdent+    freshIdents      = lift . freshIdents+    scopeFreshness m = ReaderT $ \r -> scopeFreshness (runReaderT m r)  instance (Monoid w, MonadFresh m) => MonadFresh (WriterT w m) where-    freshIdent  = lift . freshIdent-    freshIdents = lift . freshIdents+    freshIdent       = lift . freshIdent+    freshIdents      = lift . freshIdents+    scopeFreshness m = WriterT $ scopeFreshness (runWriterT m)
src/Control/Monad/Trans/FastFresh.hs view
@@ -3,7 +3,7 @@ -- | -- Copyright   : (c) 2010 Simon Meier -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Simon Meier <iridcode@gmail.com> -- Portability : GHC only --@@ -31,6 +31,7 @@   , FreshState   , nothingUsed   , freshIdents+  , scopeFreshness    ) where @@ -79,6 +80,15 @@     i <- FreshT get     FreshT $ put $ i + k     return i++-- | 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+    x <- scoped+    FreshT (put state) -- restore freshness state+    return x+  -- Instances ------------
src/Control/Monad/Trans/PreciseFresh.hs view
@@ -3,7 +3,7 @@ -- | -- Copyright   : (c) 2010-2012 Simon Meier -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Simon Meier <iridcode@gmail.com> -- Portability : GHC only --@@ -33,6 +33,7 @@   , nothingUsed   , freshIdent   , freshIdents+  , scopeFreshness    ) where @@ -77,7 +78,7 @@ freshIdent :: Monad m => String -> FreshT m Integer freshIdent name = do     m <- FreshT get-    let i  = M.findWithDefault 0 name m+    let i   = M.findWithDefault 0 name m         !i' = succ i -- avoid building thunks in the Map     FreshT (modify (M.insert name i'))     return i@@ -93,6 +94,14 @@     -- insert 'nextIdx' at "" to remember it for the next call     FreshT (put (M.insert "" nextIdx $ M.map (const nextIdx) m))     return maxIdx++-- | 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+    x <- scoped+    FreshT (put state) -- restore freshness state+    return x   -- Instances
src/Extension/Data/Monoid.hs view
@@ -2,13 +2,16 @@ -- | -- 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+    module Data.Monoid++#if __GLASGOW_HASKELL__ < 704+  , (<>)+#endif    , MinMax(..)   , minMaxSingleton
+ src/Text/Unicode.hs view
@@ -0,0 +1,35 @@+-- |+-- Copyright   : (c) 2010 Simon Meier+-- License     : GPL v3 (see LICENSE)+--+-- Maintainer  : Simon Meier <iridcode@gmail.com>+-- Portability : portable+--+-- Support functions for exploiting Unicode characters.+module Text.Unicode where+++-- | Convert a subscriptable character to its subsript.+subscriptChar :: Char -> Char+subscriptChar c = case c of+    '0' -> '₀'+    '1' -> '₁'+    '2' -> '₂'+    '3' -> '₃'+    '4' -> '₄'+    '5' -> '₅'+    '6' -> '₆'+    '7' -> '₇'+    '8' -> '₈'+    '9' -> '₉'+    '+' -> '₊'+    '-' -> '₋'+    '=' -> '₌'+    '(' -> '₍'+    ')' -> '₎'+    _   -> c  -- FIXME: Add further characters from+              --   http://tlt.its.psu.edu/suggestions/international/bylanguage/mathchart.html#super++-- | Convert all subscriptable characters to subscripts.+subscript :: String -> String+subscript = map subscriptChar
tamarin-prover-utils.cabal view
@@ -2,7 +2,7 @@  cabal-version:      >= 1.8 build-type:         Simple-version:            0.6.0.0+version:            0.8.0.0 license:            GPL license-file:       LICENSE category:           Theorem Provers@@ -17,7 +17,7 @@                     security protocol verification                     (<hackage.haskell.org/package/tamarin-prover>). -homepage:           http://www.infsec.ethz.ch/research/software#TAMARIN+homepage:           http://www.infsec.ethz.ch/research/software/tamarin  source-repository head   type:     git@@ -29,6 +29,7 @@ ----------------------  library+    ghc-options:       -Wall -fwarn-tabs     ghc-prof-options:  -auto-all      build-depends:@@ -70,6 +71,7 @@         Extension.Data.ByteString          Text.Dot+        Text.Unicode         Text.PrettyPrint.Class         Text.PrettyPrint.Highlight         Text.PrettyPrint.Html