tamarin-prover-term 0.6.0.0 → 0.8.0.0

raw patch · 6 files changed

+81/−62 lines, 6 filesdep ~tamarin-prover-utilsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: tamarin-prover-utils

API changes (from Hackage documentation)

Files

• src/Term/LTerm.hs +49/−37
• src/Term/Maude/Signature.hs +3/−3
• src/Term/Rewriting/Norm.hs +1/−2
• src/Term/Term.hs +9/−2
• src/Term/UnitTests.hs +14/−15
• tamarin-prover-term.cabal +5/−3

@@ -1,8 +1,13 @@-{-# LANGUAGE-      CPP, FlexibleContexts, FlexibleInstances, TypeSynonymInstances,-      MultiParamTypeClasses, DeriveDataTypeable, StandaloneDeriving,-      TemplateHaskell, GeneralizedNewtypeDeriving, ViewPatterns-  #-}+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE DeriveDataTypeable         #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE StandaloneDeriving         #-}+{-# LANGUAGE TemplateHaskell            #-}+{-# LANGUAGE TypeSynonymInstances       #-}+{-# LANGUAGE ViewPatterns               #-} {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}   -- spurious warnings for view patterns -- |@@ -64,12 +69,13 @@   , frees   , someInst   , rename-  , renamePrecise   , eqModuloFreshnessNoAC   , avoid   , evalFreshAvoiding   , evalFreshTAvoiding   , renameAvoiding+  , avoidPrecise+  , renamePrecise    -- * BVar   , BVar(..)@@ -88,35 +94,33 @@   , module Term.VTerm ) where -import Term.VTerm-import Term.Rewriting.Definitions--import Text.PrettyPrint.Class--import Control.Applicative-import Control.Monad.Fresh-import Control.Monad.Bind-import Control.DeepSeq-import Control.Monad.Identity+import           Term.Rewriting.Definitions+import           Term.VTerm -import Data.DeriveTH-import qualified Data.Set   as S-import qualified Data.Map as M+import           Text.PrettyPrint.Class -import Data.Generics hiding (GT)+import           Control.Applicative+import           Control.DeepSeq+import           Control.Monad.Bind+import           Control.Monad.Identity+import qualified Control.Monad.Trans.PreciseFresh as Precise -import qualified Data.DList as D-import Data.Traversable-import Data.Monoid-import Data.Binary-import Data.Foldable hiding (concatMap, elem)+import           Data.Binary+import qualified Data.DList                       as D+import           Data.DeriveTH+import           Data.Foldable                    hiding (concatMap, elem)+import           Data.Generics                    hiding (GT)+import qualified Data.Map                         as M+import           Data.Monoid+import qualified Data.Set                         as S+import           Data.Traversable -import Safe (fromJustNote)+import           Safe                             (fromJustNote) -import Extension.Prelude-import Extension.Data.Monoid+import           Extension.Data.Monoid+import           Extension.Prelude -import Logic.Connectives+import           Logic.Connectives  ------------------------------------------------------------------------------ -- Sorts.@@ -249,7 +253,7 @@  -- | @freshLVar v@ represents a fresh logical variable with name @v@. freshLVar :: MonadFresh m => String -> LSort -> m LVar-freshLVar n s = LVar n s <$> freshIdents 1+freshLVar n s = LVar n s <$> freshIdent n  -- | Returns the most precise sort of an 'LTerm'. sortOfLTerm :: Show c => (c -> LSort) -> LTerm c -> LSort@@ -477,13 +481,6 @@   where     incVar shift (LVar n so i) = pure $ LVar n so (i+shift) --- | @renamePrecise t@ replaces all variables in @t@ with fresh variables.---   If 'Control.Monad.PreciseFresh' is used with non-AC terms and identical---   fresh state, the same result is returned for two terms that only differ---   in the indices of variables.-renamePrecise :: (MonadFresh m, HasFrees a) => a -> m a-renamePrecise x = evalBindT (someInst x) noBindings- -- | @eqModuloFreshness t1 t2@ checks whether @t1@ is equal to @t2@ modulo -- renaming of indices of free variables. Note that the normal form is not -- unique with respect to AC symbols.@@ -520,6 +517,21 @@ --   fresh variables avoiding variables in @t@. renameAvoiding :: (HasFrees s, HasFrees t) => s -> t -> s s `renameAvoiding` t = rename s `evalFreshAvoiding` t++-- | @avoidPrecise t@ computes a 'Precise.FreshState' that avoids generating+-- variables occurring in @t@.+avoidPrecise :: HasFrees t => t -> Precise.FreshState+avoidPrecise =+    foldl' ins M.empty . frees+  where+    ins m v = M.insertWith' max (lvarName v) (lvarIdx v + 1) m++-- | @renamePrecise t@ replaces all variables in @t@ with fresh variables.+--   If 'Control.Monad.PreciseFresh' is used with non-AC terms and identical+--   fresh state, the same result is returned for two terms that only differ+--   in the indices of variables.+renamePrecise :: (MonadFresh m, HasFrees a) => a -> m a+renamePrecise x = evalBindT (someInst x) noBindings  -- Instances ------------

@@ -5,7 +5,7 @@ -- | -- Copyright   : (c) 2010, 2011 Benedikt Schmidt -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- Euqatiuonal signatures for Maude.@@ -147,9 +147,9 @@  prettyMaudeSig :: P.HighlightDocument d => MaudeSig -> d prettyMaudeSig sig = P.vcat-    [ ppNonEmptyList' "builtin:"   P.text      builtIns+    [ ppNonEmptyList' "builtins:"  P.text      builtIns     , ppNonEmptyList' "functions:" ppFunSymb $ S.toList (functionSymbols sig)-    , ppNonEmptyList  +    , ppNonEmptyList         (\ds -> P.sep (P.keyword_ "equations:" : map (P.nest 2) ds))         prettyStRule $ S.toList (stRules sig)     ]

@@ -15,7 +15,7 @@ -- terms modulo AC. module Term.Rewriting.Norm ( --    norm-   norm'+    norm'   , nf'   , nfSubstVFresh'   , normSubstVFresh'@@ -27,7 +27,6 @@ import           Term.Maude.Signature import           Term.Substitution import           Term.SubtermRule-import           Term.Term import           Term.Unification  import           Utils.Misc

@@ -56,6 +56,9 @@     , fAppFst     , fAppSnd +    -- ** exp symbol+    , expSymString+    , invSymString      -- ** Destructors and classifiers     , destPair@@ -117,15 +120,19 @@ -- | Function signatures. type FunSig = Set NonACSym +expSymString :: ByteString+expSymString = "exp" +invSymString :: ByteString+invSymString = "inv"  pairSym, expSym, invSym, oneSym, zeroSym, emptySym, fstSym, sndSym :: NonACSym -- | Pairing. pairSym  = ("pair",2) -- | Exponentiation.-expSym   = ("exp",2)+expSym   = (expSymString,2) -- | The inverse in the groups of exponents.-invSym   = ("inv",1) +invSym   = (invSymString,1) -- | The one in the group of exponents. oneSym   = ("one", 0) -- | The zero for Xor.

@@ -7,7 +7,7 @@ -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- Unit tests for the functions dealing with term algebra and related notions.-module Term.UnitTests (main) where+module Term.UnitTests (tests) where  import Term.Substitution import Term.Subsumption@@ -281,21 +281,20 @@     TestLabel "Tests for simple functions" $ TestList       [ testTrue "" (size [bigTerm] > 0) ] --- | Execute all unification infrastructure unit tests.-main :: FilePath -- ^ Path to maude executable.-     -> IO Counts-main maudePath = do+-- | All unification infrastructure unit tests.+tests :: FilePath -> IO Test+tests maudePath = do     mhnd <- startMaude maudePath allMaudeSig-    runTestTT $ TestList [ testsVariant mhnd-                         , tcompare mhnd-                         , testsSubs mhnd-                         , testsTerm-                         , testsSubst-                         , testsNorm mhnd-                         , testsUnify mhnd-                         , testsSimple mhnd-                         , testsMatching mhnd-                         ]+    return $ TestList [ testsVariant mhnd+                      , tcompare mhnd+                      , testsSubs mhnd+                      , testsTerm+                      , testsSubst+                      , testsNorm mhnd+                      , testsUnify mhnd+                      , testsSimple mhnd+                      , testsMatching mhnd+                      ]  -- | Maude signatures with all builtin symbols. allMaudeSig :: MaudeSig

@@ -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@@ -23,7 +23,7 @@                     (<http://maude.cs.uiuc.edu/>) as a backend for                     normalization, equational matching, and unification. -homepage:           http://www.infsec.ethz.ch/research/software#TAMARIN+homepage:           http://www.infsec.ethz.ch/research/software/tamarin   source-repository head@@ -35,6 +35,8 @@ ----------------------  library+    ghc-options:       -Wall -fwarn-tabs+     ghc-prof-options:  -auto-all      build-depends:@@ -56,7 +58,7 @@        , HUnit                == 1.2.* -      , tamarin-prover-utils == 0.6.*+      , tamarin-prover-utils == 0.8.*       hs-source-dirs: src