diff --git a/src/Control/Monad/Fresh/Class.hs b/src/Control/Monad/Fresh/Class.hs --- a/src/Control/Monad/Fresh/Class.hs +++ b/src/Control/Monad/Fresh/Class.hs @@ -1,7 +1,7 @@ -- | -- Copyright : (c) 2010 Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Simon Meier -- 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) diff --git a/src/Control/Monad/Trans/FastFresh.hs b/src/Control/Monad/Trans/FastFresh.hs --- a/src/Control/Monad/Trans/FastFresh.hs +++ b/src/Control/Monad/Trans/FastFresh.hs @@ -3,7 +3,7 @@ -- | -- Copyright : (c) 2010 Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Simon Meier -- 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 ------------ diff --git a/src/Control/Monad/Trans/PreciseFresh.hs b/src/Control/Monad/Trans/PreciseFresh.hs --- a/src/Control/Monad/Trans/PreciseFresh.hs +++ b/src/Control/Monad/Trans/PreciseFresh.hs @@ -3,7 +3,7 @@ -- | -- Copyright : (c) 2010-2012 Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Simon Meier -- 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 diff --git a/src/Extension/Data/Monoid.hs b/src/Extension/Data/Monoid.hs --- a/src/Extension/Data/Monoid.hs +++ b/src/Extension/Data/Monoid.hs @@ -2,13 +2,16 @@ -- | -- Copyright : (c) 2012 Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Simon Meier -- -- 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 diff --git a/src/Text/Unicode.hs b/src/Text/Unicode.hs new file mode 100644 --- /dev/null +++ b/src/Text/Unicode.hs @@ -0,0 +1,35 @@ +-- | +-- Copyright : (c) 2010 Simon Meier +-- License : GPL v3 (see LICENSE) +-- +-- Maintainer : Simon Meier +-- 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 diff --git a/tamarin-prover-utils.cabal b/tamarin-prover-utils.cabal --- a/tamarin-prover-utils.cabal +++ b/tamarin-prover-utils.cabal @@ -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 (). -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