diff --git a/src/Term/LTerm.hs b/src/Term/LTerm.hs --- a/src/Term/LTerm.hs +++ b/src/Term/LTerm.hs @@ -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 ------------ diff --git a/src/Term/Maude/Signature.hs b/src/Term/Maude/Signature.hs --- a/src/Term/Maude/Signature.hs +++ b/src/Term/Maude/Signature.hs @@ -5,7 +5,7 @@ -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- 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) ] diff --git a/src/Term/Rewriting/Norm.hs b/src/Term/Rewriting/Norm.hs --- a/src/Term/Rewriting/Norm.hs +++ b/src/Term/Rewriting/Norm.hs @@ -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 diff --git a/src/Term/Term.hs b/src/Term/Term.hs --- a/src/Term/Term.hs +++ b/src/Term/Term.hs @@ -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. diff --git a/src/Term/UnitTests.hs b/src/Term/UnitTests.hs --- a/src/Term/UnitTests.hs +++ b/src/Term/UnitTests.hs @@ -7,7 +7,7 @@ -- Maintainer : Benedikt Schmidt -- -- 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 diff --git a/tamarin-prover-term.cabal b/tamarin-prover-term.cabal --- a/tamarin-prover-term.cabal +++ b/tamarin-prover-term.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 @@ -23,7 +23,7 @@ () 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