tamarin-prover-term 0.1.0.0 → 0.4.0.0
raw patch · 24 files changed
+2023/−1039 lines, 24 filesdep +HUnitdep +attoparsecdep +bytestringdep ~containersdep ~deepseqdep ~processsetup-changed
Dependencies added: HUnit, attoparsec, bytestring
Dependency ranges changed: containers, deepseq, process, safe, tamarin-prover-utils
Files
- Setup.hs +91/−0
- src/Term/Builtin/Convenience.hs +48/−75
- src/Term/Builtin/Rules.hs +22/−13
- src/Term/Builtin/Signature.hs +7/−24
- src/Term/LTerm.hs +96/−53
- src/Term/Maude/Parser.hs +262/−0
- src/Term/Maude/Process.hs +81/−144
- src/Term/Maude/Signature.hs +174/−0
- src/Term/Maude/Types.hs +73/−299
- src/Term/Narrowing/Narrow.hs +4/−3
- src/Term/Positions.hs +57/−23
- src/Term/Rewriting/Definitions.hs +102/−0
- src/Term/Rewriting/Norm.hs +107/−14
- src/Term/Rewriting/NormAC.hs +0/−47
- src/Term/Substitution.hs +27/−15
- src/Term/Substitution/SubstVFree.hs +37/−23
- src/Term/Substitution/SubstVFresh.hs +8/−13
- src/Term/Subsumption.hs +9/−11
- src/Term/SubtermRule.hs +8/−4
- src/Term/Term.hs +266/−247
- src/Term/Unification.hs +21/−22
- src/Term/UnitTests.hs +376/−0
- src/Term/VTerm.hs +126/−0
- tamarin-prover-term.cabal +21/−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/Term/Builtin/Convenience.hs view
@@ -15,57 +15,30 @@ -- Shorter syntax for Term constructors ---------------------------------------------------------------------- -(*:) :: Term a -> Term a -> Term a-b *: e = FApp (AC Mult) [b,e]-(#) :: Term a -> Term a -> Term a-b # e = FApp (AC MUn) [b,e]-(+:) :: Term a -> Term a -> Term a-b +: e = FApp (AC Xor) [b,e]---mult :: [Term a] -> Term a-mult ts = FApp (AC Mult) ts--union :: [Term a] -> Term a-union ts = FApp (AC MUn) ts--xor :: [Term a] -> Term a-xor ts = FApp (AC Xor) ts--appFree :: NonACSym -> [Term a] -> Term a-appFree s ts = FApp (NonAC s) ts--one, zero, empty :: Term a-one = appFree oneSym []-zero = appFree zeroSym []-empty = appFree emptySym []--inv :: Term a -> Term a-inv e = appFree invSym [e]--pair :: (Term a,Term a) -> Term a-pair (x,y) = appFree pairSym [x, y]+(*:) :: Ord a => Term a -> Term a -> Term a+b *: e = fAppMult [b,e]+(#) :: Ord a => Term a -> Term a -> Term a+b # e = fAppUnion [b,e]+(+:) :: Ord a => Term a -> Term a -> Term a+b +: e = fAppXor [b,e] -expo, adec, aenc, sdec, senc, sign :: (Term a,Term a) -> Term a-expo (b,e) = appFree expSym [b,e]-adec (a,b) = appFree adecSym [a,b]-aenc (a,b) = appFree aencSym [a,b]-sdec (a,b) = appFree sdecSym [a,b]-senc (a,b) = appFree sencSym [a,b]-sign (a,b) = appFree signSym [a,b]+adec, aenc, sdec, senc, sign :: Ord a => (Term a,Term a) -> Term a+adec (a,b) = fAppNonAC adecSym [a,b]+aenc (a,b) = fAppNonAC aencSym [a,b]+sdec (a,b) = fAppNonAC sdecSym [a,b]+senc (a,b) = fAppNonAC sencSym [a,b]+sign (a,b) = fAppNonAC signSym [a,b] -verify :: (Term a,Term a,Term a) -> Term a-verify (a,b,c) = appFree verifySym [a,b,c]+verify :: Ord a => (Term a,Term a,Term a) -> Term a+verify (a,b,c) = fAppNonAC verifySym [a,b,c] -pk, fstC, sndC :: Term a -> Term a-pk a = appFree pkSym [a]-fstC a = appFree fstSym [a]-sndC a = appFree sndSym [a]+pk :: Ord a => Term a -> Term a+pk a = fAppNonAC pkSym [a] -trueC :: Term a-trueC = appFree trueSym []+trueC :: Ord a => Term a+trueC = fAppNonAC trueSym [] -var :: String -> Int -> LNTerm+var :: String -> Integer -> LNTerm var s i = varTerm $ LVar s LSortMsg i x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 :: LNTerm@@ -93,7 +66,7 @@ y8 = var "y" 8 y9 = var "y" 9 -freshVar :: String -> Int -> LNTerm+freshVar :: String -> Integer -> LNTerm freshVar s i = varTerm $ LVar s LSortFresh i fx0,fx1,fx2,fx3,fx4,fx5,fx6,fx7,fx8,fx9,fx10 :: LNTerm@@ -109,7 +82,7 @@ fx9 = freshVar "fx" 9 fx10 = freshVar "fx" 10 -pubVar :: String -> Int -> LNTerm+pubVar :: String -> Integer -> LNTerm pubVar s i = varTerm $ LVar s LSortPub i px0,px1,px2,px3,px4,px5,px6,px7,px8,px9,px10 :: LNTerm@@ -171,15 +144,15 @@ lv9 = LVar "v9" LSortMsg 0 v1,v2,v3,v4,v5,v6,v7,v8,v9 :: LNTerm-v1 = Lit $ Var $ lv1-v2 = Lit $ Var $ lv2-v3 = Lit $ Var $ lv3-v4 = Lit $ Var $ lv4-v5 = Lit $ Var $ lv5-v6 = Lit $ Var $ lv6-v7 = Lit $ Var $ lv7-v8 = Lit $ Var $ lv8-v9 = Lit $ Var $ lv9+v1 = lit $ Var $ lv1+v2 = lit $ Var $ lv2+v3 = lit $ Var $ lv3+v4 = lit $ Var $ lv4+v5 = lit $ Var $ lv5+v6 = lit $ Var $ lv6+v7 = lit $ Var $ lv7+v8 = lit $ Var $ lv8+v9 = lit $ Var $ lv9 li1,li2,li3,li4,li5,li6,li7,li8,li9 :: LVar li1 = LVar "i1" LSortNode 0@@ -193,15 +166,15 @@ li9 = LVar "i9" LSortNode 0 i1,i2,i3,i4,i5,i6,i7,i8,i9 :: LNTerm-i1 = Lit $ Var $ li1-i2 = Lit $ Var $ li2-i3 = Lit $ Var $ li3-i4 = Lit $ Var $ li4-i5 = Lit $ Var $ li5-i6 = Lit $ Var $ li6-i7 = Lit $ Var $ li7-i8 = Lit $ Var $ li8-i9 = Lit $ Var $ li9+i1 = lit $ Var $ li1+i2 = lit $ Var $ li2+i3 = lit $ Var $ li3+i4 = lit $ Var $ li4+i5 = lit $ Var $ li5+i6 = lit $ Var $ li6+i7 = lit $ Var $ li7+i8 = lit $ Var $ li8+i9 = lit $ Var $ li9 ls1,ls2,ls3,ls4,ls5,ls6,ls7,ls8,ls9 :: LVar ls1 = LVar "s1" LSortMSet 0@@ -215,12 +188,12 @@ ls9 = LVar "s9" LSortMSet 0 s1,s2,s3,s4,s5,s6,s7,s8,s9 :: LNTerm-s1 = Lit $ Var $ ls1-s2 = Lit $ Var $ ls2-s3 = Lit $ Var $ ls3-s4 = Lit $ Var $ ls4-s5 = Lit $ Var $ ls5-s6 = Lit $ Var $ ls6-s7 = Lit $ Var $ ls7-s8 = Lit $ Var $ ls8-s9 = Lit $ Var $ ls9+s1 = lit $ Var $ ls1+s2 = lit $ Var $ ls2+s3 = lit $ Var $ ls3+s4 = lit $ Var $ ls4+s5 = lit $ Var $ ls5+s6 = lit $ Var $ ls6+s7 = lit $ Var $ ls7+s8 = lit $ Var $ ls8+s9 = lit $ Var $ ls9
src/Term/Builtin/Rules.hs view
@@ -25,13 +25,16 @@ import Term.Builtin.Signature import Term.Builtin.Convenience +import qualified Data.Set as S+import Data.Set (Set)+ -- Rules for DH theory ---------------------------------------------------------------------- -- | The rewriting rules for Diffie-Hellman. This is a presentation due to Lankford -- with the finite variant property.-dhRules :: [RRule LNTerm]-dhRules =+dhRules :: Set (RRule LNTerm)+dhRules = S.fromList [ expo(x1,one) `RRule` x1 , expo(expo(x1,x2),x3) `RRule` expo(x1,(x2 *: x3)) @@ -46,24 +49,30 @@ , inv x1 *: (inv x2 *: x3) `RRule` (inv (x1 *: x2) *: x3) , inv (x1 *: x2) *: (x2 *: x3) `RRule` (inv x1 *: x3) ]+ where+ expo = fAppExp+ inv = fAppInv+ one = fAppOne -- | The rewriting rules for Xor.-xorRules :: [RRule LNTerm]-xorRules =+xorRules :: Set (RRule LNTerm)+xorRules = S.fromList [ x1 +: x1 `RRule` zero , x1 +: zero `RRule` x1 , x1 +: (x1 +: x2) `RRule` x2 ]+ where+ zero = fAppZero -- | The rewriting rules for multisets.-msetRules :: [RRule LNTerm]-msetRules = [ s1 # empty `RRule` s1 ]+msetRules :: Set (RRule LNTerm)+msetRules = S.fromList [ s1 # fAppEmpty `RRule` s1 ] -- | The rewriting rules for standard subterm operators that are builtin.-pairRules, symEncRules, asymEncRules, signatureRules :: [StRule]-pairRules =- [ fstC (pair (x1,x2)) `StRule` (RhsPosition [0,0])- , sndC (pair (x1,x2)) `StRule` (RhsPosition [0,1]) ]-symEncRules = [ sdec (senc (x1,x2), x2) `StRule` (RhsPosition [0,0]) ]-asymEncRules = [ adec (aenc (x1, pk x2), x2) `StRule` (RhsPosition [0,0]) ]-signatureRules = [ verify (sign (x1,x2), x1, pk x2) `StRule` (RhsGround trueC) ]+pairRules, symEncRules, asymEncRules, signatureRules :: Set (StRule)+pairRules = S.fromList+ [ fAppFst (fAppPair (x1,x2)) `StRule` (RhsPosition [0,0])+ , fAppSnd (fAppPair (x1,x2)) `StRule` (RhsPosition [0,1]) ]+symEncRules = S.fromList [ sdec (senc (x1,x2), x2) `StRule` (RhsPosition [0,0]) ]+asymEncRules = S.fromList [ adec (aenc (x1, pk x2), x2) `StRule` (RhsPosition [0,0]) ]+signatureRules = S.fromList [ verify (sign (x1,x2), x1, pk x2) `StRule` (RhsGround trueC) ]
src/Term/Builtin/Signature.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE OverloadedStrings #-} -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt -- License : GPL v3 (see LICENSE)@@ -8,7 +9,7 @@ module Term.Builtin.Signature where import Term.LTerm-+import qualified Data.Set as S -- Builtin symbols (pair and inv are defined in Term.Term) ----------------------------------------------------------------------@@ -25,9 +26,7 @@ verifySym = ("verify",3) -- | Unary builtin non-ac function symbols.-fstSym, sndSym, pkSym, hashSym :: NonACSym-fstSym = ("fst",1)-sndSym = ("snd",1)+pkSym, hashSym :: NonACSym pkSym = ("pk",1) hashSym = ("h",1) @@ -38,34 +37,18 @@ -- Builtin signatures ---------------------------------------------------------------------- --- | The signature for the non-AC Diffie-Hellman function symbols.-dhFunSig :: FunSig-dhFunSig = [ expSym, oneSym, invSym ]---- | The signature for the non-AC Xor function symbols.-xorFunSig :: FunSig-xorFunSig = [ zeroSym ]---- | The signature for then non-AC multiset function symbols.-msetFunSig :: FunSig-msetFunSig = [ emptySym ]---- | The signature for pairs.-pairFunSig :: FunSig-pairFunSig = [ pairSym, fstSym, sndSym ]- -- | The signature for symmetric encryption. symEncFunSig :: FunSig-symEncFunSig = [ sdecSym, sencSym ]+symEncFunSig = S.fromList [ sdecSym, sencSym ] -- | The signature for asymmetric encryption. asymEncFunSig :: FunSig-asymEncFunSig = [ adecSym, aencSym, pkSym ]+asymEncFunSig = S.fromList [ adecSym, aencSym, pkSym ] -- | The signature for cryptographic signatures. signatureFunSig :: FunSig-signatureFunSig = [ signSym, verifySym, trueSym, pkSym ]+signatureFunSig = S.fromList [ signSym, verifySym, trueSym, pkSym ] -- | The signature for hashing. hashFunSig :: FunSig-hashFunSig = [ hashSym ]+hashFunSig = S.fromList [ hashSym ]
src/Term/LTerm.hs view
@@ -1,6 +1,10 @@-{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}-{-# LANGUAGE MultiParamTypeClasses, DeriveDataTypeable, StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE + CPP, FlexibleContexts, FlexibleInstances, TypeSynonymInstances,+ MultiParamTypeClasses, DeriveDataTypeable, StandaloneDeriving,+ TemplateHaskell, GeneralizedNewtypeDeriving, ViewPatterns+ #-}+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}+ -- spurious warnings for view patterns -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE)@@ -44,13 +48,14 @@ -- ** Manging Free LVars , HasFrees(..)+ , MonotoneFunction(..) , occurs , freesList , frees , someInst , rename- , eqModuloFreshness- , maximumVarIdx+ , renamePrecise+ , eqModuloFreshnessNoAC , avoid , evalFreshAvoiding , evalFreshTAvoiding@@ -67,17 +72,19 @@ , prettyLNTerm -- * Convenience exports- , module Term.Term+ , module Term.VTerm ) where -import Term.Term+import Term.VTerm+import Term.Rewriting.Definitions -import Text.Isar+import Text.PrettyPrint.Class import Control.Applicative import Control.Monad.Fresh import Control.Monad.Bind import Control.DeepSeq+import Control.Monad.Identity import Data.DeriveTH import qualified Data.Set as S@@ -92,7 +99,7 @@ import Data.Foldable hiding (concatMap, elem) import Extension.Prelude-import Extension.Data.Bounded+import Extension.Data.Monoid import Logic.Connectives @@ -134,11 +141,11 @@ -- | @freshTerm f@ represents the fresh name @f@. freshTerm :: String -> NTerm v-freshTerm = Lit . Con . Name FreshName . NameId+freshTerm = lit . Con . Name FreshName . NameId -- | @pubTerm f@ represents the pub name @f@. pubTerm :: String -> NTerm v-pubTerm = Lit . Con . Name PubName . NameId+pubTerm = lit . Con . Name PubName . NameId -- | Return 'LSort' for given 'Name'. sortOfName :: Name -> LSort@@ -168,7 +175,7 @@ data LVar = LVar { lvarName :: String , lvarSort :: !LSort- , lvarIdx :: {-# UNPACK #-} !Int + , lvarIdx :: !Integer } deriving( Typeable, Data ) @@ -181,15 +188,16 @@ -- | @freshLVar v@ represents a fresh logical variable with name @v@. freshLVar :: MonadFresh m => String -> LSort -> m LVar-freshLVar n s = LVar n s <$> freshIdent n+freshLVar n s = LVar n s <$> freshIdents 1 -- | Returns the most precise sort of an 'LTerm'.-sortOfLTerm :: (c -> LSort) -> LTerm c -> LSort-sortOfLTerm sortOfConst (Lit (Con c)) = sortOfConst c-sortOfLTerm _ (Lit (Var (LVar _ s _))) = s-sortOfLTerm _ (FApp (NonAC ("empty",0)) []) = LSortMSet-sortOfLTerm _ (FApp (AC MUn) _) = LSortMSet-sortOfLTerm _ _ = LSortMsg+sortOfLTerm :: Show c => (c -> LSort) -> LTerm c -> LSort+sortOfLTerm sortOfConst t = case viewTerm2 t of+ Lit2 (Con c) -> sortOfConst c+ Lit2 (Var lv) -> lvarSort lv+ Empty -> LSortMSet+ FUnion _ -> LSortMSet+ _ -> LSortMsg -- | Returns the most precise sort of an 'LNTerm'. sortOfLNTerm :: LNTerm -> LSort@@ -234,46 +242,46 @@ -- | Is a term a message variable? isMsgVar :: LNTerm -> Bool-isMsgVar (Lit (Var v)) = (lvarSort v == LSortMsg)-isMsgVar _ = False+isMsgVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortMsg)+isMsgVar _ = False -- | Is a term a fresh variable? isFreshVar :: LNTerm -> Bool-isFreshVar (Lit (Var v)) = (lvarSort v == LSortFresh)-isFreshVar _ = False+isFreshVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortFresh)+isFreshVar _ = False -- | The required components to construct the message.--- FIXME: Make inv/1 and pair/2 special? input :: LNTerm -> [LNTerm]-input (FApp (AC Mult) ts) = concatMap input ts-input (FApp (NonAC sym) ts) | sym `elem` [ invSym, pairSym ] = concatMap input ts-input t = [t]+input (viewTerm2 -> FMult ts) = concatMap input ts+input (viewTerm2 -> FInv t1) = input t1+input (viewTerm2 -> FPair t1 t2) = input t1 ++ input t2+input t = [t] -- | Is a message trivial; i.e., can for sure be instantiated with something -- known to the intruder? trivial :: LNTerm -> Bool-trivial (FApp _ []) = True-trivial (Lit (Con (Name PubName _))) = True-trivial (Lit (Var v)) = case lvarSort v of- LSortPub -> True- LSortMsg -> True- _ -> False-trivial _ = False+trivial (viewTerm -> FApp _ []) = True+trivial (viewTerm -> Lit (Con (Name PubName _))) = True+trivial (viewTerm -> Lit (Var v)) = case lvarSort v of+ LSortPub -> True+ LSortMsg -> True+ _ -> False+trivial _ = False -- BVar: Bound variables ------------------------ -- | Bound and free variables.-data BVar v = Bound Int -- ^ A bound variable in De-Brujin notation.- | Free v -- ^ A free variable.+data BVar v = Bound Integer -- ^ A bound variable in De-Brujin notation.+ | Free v -- ^ A free variable. deriving( Eq, Ord, Show, Data, Typeable ) -- | Fold a possibly bound variable. {-# INLINE foldBVar #-}-foldBVar :: (Int -> a) -> (v -> a) -> BVar v -> a+foldBVar :: (Integer -> a) -> (v -> a) -> BVar v -> a foldBVar fBound fFree = go where go (Bound i) = fBound i@@ -332,6 +340,14 @@ -- Managing bound and free LVars ------------------------------------------------------------------------------ +-- | For performance reasons, we distinguish between monotone functions on+-- 'LVar's and arbitrary functions. The monotone functions much map 'LVar's to+-- equal or larger 'LVar's. This ensures that the AC-normal form does not have+-- to be recomputed. If you are unsure about what to use, then use the+-- 'Arbitrary' function.+data MonotoneFunction f = Monotone (LVar -> f LVar ) + | Arbitrary (LVar -> f LVar )+ -- | @HasFree t@ denotes that the type @t@ has free @LVar@ variables. They can -- be collected using 'foldFrees' and mapped in the context of an applicative -- functor using 'mapFrees'. @@ -345,8 +361,7 @@ -- class HasFrees t where foldFrees :: Monoid m => (LVar -> m ) -> t -> m- mapFrees :: Applicative f => (LVar -> f LVar ) -> t -> f t-+ mapFrees :: Applicative f => MonotoneFunction f -> t -> f t -- | @v `occurs` t@ iff variable @v@ occurs as a free variable in @t@. occurs :: HasFrees t => LVar -> t -> Bool@@ -369,30 +384,47 @@ -- binding is not yet determined by the caller are replaced with fresh -- variables. someInst :: (MonadFresh m, MonadBind LVar LVar m, HasFrees t) => t -> m t-someInst = mapFrees (\x -> importBinding (`LVar` lvarSort x) x (lvarName x))+someInst = mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x (lvarName x)) --- | @rename t@ replaces all variables in @t@ with fresh variables+-- | @rename t@ replaces all variables in @t@ with fresh variables.+-- Note that the result is not guaranteed to be equal for terms that are+-- equal modulo changing the indices of variables. rename :: (MonadFresh m, HasFrees a) => a -> m a-rename x = evalBindT (someInst x) noBindings+rename x = case boundsVarIdx x of+ Nothing -> return x+ Just (minVarIdx, maxVarIdx) -> do+ freshStart <- freshIdents (succ (maxVarIdx - minVarIdx))+ return . runIdentity . mapFrees (Monotone $ incVar (freshStart - minVarIdx)) $ x+ 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.-eqModuloFreshness :: (HasFrees a, Eq a) => a -> a -> Bool-eqModuloFreshness t1 = +-- renaming of indices of free variables. Note that the normal form is not+-- unique with respect to AC symbols.+eqModuloFreshnessNoAC :: (HasFrees a, Eq a) => a -> a -> Bool+eqModuloFreshnessNoAC t1 = -- this formulation shares normalisation of t1 among further calls to -- different t2. (normIndices t1 ==) . normIndices where- normIndices = (`evalFresh` nothingUsed) . rename+ normIndices = (`evalFresh` nothingUsed) . (`evalBindT` noBindings) .+ mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x "") --- | The maximum index of all free variables.-maximumVarIdx :: HasFrees t => t -> Int-maximumVarIdx = getBoundedMax . foldFrees (BoundedMax . lvarIdx)+-- | The mininum and maximum index of all free variables.+boundsVarIdx :: HasFrees t => t -> Maybe (Integer, Integer)+boundsVarIdx = getMinMax . foldFrees (minMaxSingleton . lvarIdx) -- | @avoid t@ computes a 'FreshState' that avoids generating -- variables occurring in @t@. avoid :: HasFrees t => t -> FreshState -avoid = max 0 . succ . maximumVarIdx+avoid = maybe 0 (succ . snd) . boundsVarIdx -- | @m `evalFreshAvoiding` t@ evaluates the monadic action @m@ with a -- fresh-variable supply that avoids generating variables occurring in @t@.@@ -415,7 +447,8 @@ instance HasFrees LVar where foldFrees = id- mapFrees = id+ mapFrees (Arbitrary f) = f+ mapFrees (Monotone f) = f instance HasFrees v => HasFrees (Lit c v) where foldFrees f (Var x) = foldFrees f x@@ -431,9 +464,11 @@ mapFrees _ b@(Bound _) = pure b mapFrees f (Free v) = Free <$> mapFrees f v -instance HasFrees l => HasFrees (Term l) where+instance (HasFrees l, Ord l) => HasFrees (Term l) where foldFrees f = foldMap (foldFrees f)- mapFrees f = traverse (mapFrees f)+ mapFrees f (viewTerm -> Lit l) = lit <$> mapFrees f l+ mapFrees f@(Arbitrary _) (viewTerm -> FApp o l) = fApp o <$> mapFrees f l+ mapFrees f@(Monotone _) (viewTerm -> FApp o l) = unsafefApp o <$> mapFrees f l instance HasFrees a => HasFrees (Equal a) where foldFrees f = foldMap (foldFrees f)@@ -453,6 +488,14 @@ mapFrees _ = pure instance HasFrees Int where+ foldFrees _ = const mempty+ mapFrees _ = pure++instance HasFrees Integer where+ foldFrees _ = const mempty+ mapFrees _ = pure++instance HasFrees Bool where foldFrees _ = const mempty mapFrees _ = pure
+ src/Term/Maude/Parser.hs view
@@ -0,0 +1,262 @@+{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}+{-# LANGUAGE TemplateHaskell, FlexibleContexts, TupleSections #-}+{-# LANGUAGE ViewPatterns, NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+-- |+-- Copyright : (c) 2010, 2011 Benedikt Schmidt+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>+--+-- Pretty printing and parsing of Maude terms and replies.+module Term.Maude.Parser (+ -- * pretty printing of terms for Maude+ ppMaude+ , ppTheory++ -- * parsing of Maude replies+ , parseUnifyReply+ , parseMatchReply+ , parseReduceReply+ ) where++import Term.LTerm+import Term.Maude.Types+import Term.Maude.Signature+import Term.Rewriting.Definitions++import Control.Monad.Bind++import Control.Basics++import qualified Data.Set as S++import qualified Data.ByteString as B+import Data.ByteString (ByteString)+import qualified Data.ByteString.Char8 as BC++import Data.Attoparsec.ByteString.Char8++import Extension.Data.Monoid++------------------------------------------------------------------------------+-- Pretty printing of Maude terms.+------------------------------------------------------------------------++-- | Pretty print an 'LSort'.+ppLSort :: LSort -> ByteString+ppLSort s = case s of+ LSortPub -> "Pub"+ LSortFresh -> "Fresh"+ LSortMsg -> "Msg"+ LSortNode -> "Node"+ LSortMSet -> "MSet"++ppLSortSym :: LSort -> ByteString+ppLSortSym lsort = case lsort of+ LSortFresh -> "f"+ LSortPub -> "p"+ LSortMsg -> "c"+ LSortNode -> "n"+ LSortMSet -> "m"++parseLSortSym :: ByteString -> Maybe LSort+parseLSortSym s = case s of+ "f" -> Just LSortFresh+ "p" -> Just LSortPub+ "c" -> Just LSortMsg+ "n" -> Just LSortNode+ "m" -> Just LSortMSet+ _ -> Nothing++-- | Used to prevent clashes with predefined Maude function symbols+-- like @true@+funSymPrefix :: ByteString+funSymPrefix = "tamX"++-- | Pretty print an AC symbol for Maude.+ppMaudeACSym :: ACSym -> ByteString+ppMaudeACSym o =+ funSymPrefix <> obs+ where obs = case o of+ Mult -> "mult"+ Union -> "mun"+ Xor -> "xor"++-- | Pretty print an AC symbol for Maude.+ppMaudeNonACSym :: NonACSym -> ByteString+ppMaudeNonACSym (o,_) = funSymPrefix <> o+++-- | @ppMaude t@ pretty prints the term @t@ for Maude.+ppMaude :: Term MaudeLit -> ByteString+ppMaude t = case viewTerm t of+ Lit (MaudeVar i lsort) -> "x" <> ppInt i <> ":" <> ppLSort lsort+ Lit (MaudeConst i lsort) -> ppLSortSym lsort <> "(" <> ppInt i <> ")"+ Lit (FreshVar _ _) -> error "Term.Maude.Types.ppMaude: FreshVar not allowed"+ FApp (NonAC fsym) [] -> ppMaudeNonACSym fsym+ FApp (NonAC fsym) as ->+ ppMaudeNonACSym fsym <> "(" <> (B.intercalate "," (map ppMaude as)) <> ")"+ FApp (AC op) as ->+ ppMaudeACSym op <> "(" <> (B.intercalate "," (map ppMaude as)) <> ")"+ FApp List as ->+ funSymPrefix <> "list(" <> ppList as <> ")"+ where+ ppInt = BC.pack . show+ ppList [] = funSymPrefix <> "nil"+ ppList (x:xs) = funSymPrefix <> "cons(" <> ppMaude x <> "," <> ppList xs <> ")"++------------------------------------------------------------------------------+-- Pretty printing a 'MaudeSig' as a Maude functional module.+------------------------------------------------------------------------------++-- | The term algebra and rewriting rules as a functional module in Maude.+ppTheory :: MaudeSig -> ByteString+ppTheory msig = BC.unlines $+ [ "fmod MSG is"+ , " protecting NAT ." ]+ +++ (if enableMSet msig+ then [ " sort Pub Fresh Msg MSet Node TOP ."+ , " subsort Msg < MSet ."+ , " subsort MSet < TOP ."+ , " op m : Nat -> MSet ."+ , " op " <> funSymPrefix <> "mun : MSet MSet -> MSet [comm assoc] ."+ , " op " <> funSymPrefix <> "empty : -> MSet ."+ ]+ else [ " sort Pub Fresh Msg Node TOP ."])+ +++ [ " subsort Pub < Msg ."+ , " subsort Fresh < Msg ."+ , " subsort Msg < TOP ."+ , " subsort Node < TOP ."+ -- constants+ , " op f : Nat -> Fresh ."+ , " op p : Nat -> Pub ."+ , " op c : Nat -> Msg ."+ , " op n : Nat -> Node ."+ -- used for encoding FApp List [t1,..,tk]+ -- list(cons(t1,cons(t2,..,cons(tk,nil)..)))+ , " op " <> funSymPrefix <> "list : TOP -> TOP ."+ , " op " <> funSymPrefix <> "cons : TOP TOP -> TOP ."+ , " op " <> funSymPrefix <> "nil : -> TOP ." ]+ +++ (if enableDH msig+ then+ [ " op " <> funSymPrefix <> "one : -> Msg ."+ , " op " <> funSymPrefix <> "exp : Msg Msg -> Msg ."+ , " op " <> funSymPrefix <> "mult : Msg Msg -> Msg [comm assoc] ."+ , " op " <> funSymPrefix <> "inv : Msg -> Msg ." ]+ else [])+ +++ (if enableXor msig+ then+ [ " op " <> funSymPrefix <> "zero : -> Msg ."+ , " op " <> funSymPrefix <> "xor : Msg Msg -> Msg [comm assoc] ."]+ else [])+ +++ map theoryFunSym (S.toList $ functionSymbols msig)+ +++ map theoryRule (S.toList $ rrulesForMaudeSig msig)+ +++ [ "endfm" ]+ where+ theoryFunSym (s,ar) =+ " op " <> funSymPrefix <> s <> " : " <> (B.concat $ replicate ar "Msg ") <> " -> Msg ."+ theoryRule (l `RRule` r) =+ " eq " <> ppMaude lm <> " = " <> ppMaude rm <> " ."+ where (lm,rm) = evalBindT ((,) <$> lTermToMTerm' l <*> lTermToMTerm' r) noBindings+ `evalFresh` nothingUsed++-- Parser for Maude output+------------------------------------------------------------------------++-- | @parseUnifyReply reply@ takes a @reply@ to a unification query+-- returned by Maude and extracts the unifiers.+parseUnifyReply :: MaudeSig -> ByteString -> Either String [MSubst]+parseUnifyReply msig reply = flip parseOnly reply $+ choice [ string "No unifier." *> endOfLine *> pure []+ , many1 (parseSubstitution msig) ]+ <* endOfInput++-- | @parseMatchReply reply@ takes a @reply@ to a match query+-- returned by Maude and extracts the unifiers.+parseMatchReply :: MaudeSig -> ByteString -> Either String [MSubst]+parseMatchReply msig reply = flip parseOnly reply $+ choice [ string "No match." *> endOfLine *> pure []+ , many1 (parseSubstitution msig) ]+ <* endOfInput++-- | @parseSubstitution l@ parses a single substitution returned by Maude.+parseSubstitution :: MaudeSig -> Parser MSubst+parseSubstitution msig = do+ endOfLine *> string "Solution " *> takeWhile1 isDigit *> endOfLine+ choice [ string "empty substitution" *> endOfLine *> pure []+ , many1 parseEntry]+ where + parseEntry = (,) <$> (flip (,) <$> (string "x" *> decimal <* string ":") <*> parseSort)+ <*> (string " --> " *> parseTerm msig <* endOfLine)+++-- | @parseReduceReply l@ parses a single solution returned by Maude.+parseReduceReply :: MaudeSig -> ByteString -> Either String MTerm+parseReduceReply msig reply = flip parseOnly reply $ do+ string "result " *> choice [ string "TOP" *> pure LSortMsg, parseSort ] -- we ignore the sort+ *> string ": " *> parseTerm msig <* endOfLine <* endOfInput+++-- | Parse an 'MSort'.+parseSort :: Parser LSort+parseSort = string "Pub" *> return LSortPub+ <|> string "Fresh" *> return LSortFresh+ <|> string "Node" *> return LSortNode+ <|> string "M" *>+ ( string "sg" *> return LSortMsg+ <|> string "Set" *> return LSortMSet)++++-- | @parseTerm@ is a parser for Maude terms.+parseTerm :: MaudeSig -> Parser MTerm+parseTerm msig = choice+ [ string "#" *> (lit <$> (FreshVar <$> (decimal <* string ":") <*> parseSort))+ , do ident <- takeWhile1 (`BC.notElem` (":(,)\n " :: B.ByteString))+ choice [ do string "("+ case parseLSortSym ident of+ Just s -> parseConst s+ Nothing -> parseFApp ident+ , string ":" *> parseMaudeVariable ident+ , parseFAppConst ident+ ]+ ]+ where+ parseConst s = lit <$> (flip MaudeConst s <$> decimal) <* string ")"++ parseFApp ident =+ appIdent <$> sepBy1 (parseTerm msig) (string ", ") <* string ")"+ where+ appIdent args | ident == ppMaudeACSym Mult = fAppAC Mult args+ | ident == ppMaudeACSym Xor = fAppAC Xor args+ | ident == ppMaudeACSym Union = fAppAC Union args+ appIdent [arg] | ident == funSymPrefix <> "list" = fAppList (flattenCons arg)+ appIdent args =+ ensureValidOp op (fAppNonAC op args)+ where op = (BC.drop prefixLen ident, length args)++ flattenCons (viewTerm -> FApp (NonAC ("cons",2)) [x,xs]) = x:flattenCons xs+ flattenCons (viewTerm -> FApp (NonAC ("nil",0)) []) = []+ flattenCons t = [t]++ parseFAppConst ident = return $ ensureValidOp op (fAppNonAC op [])+ where op = (BC.drop prefixLen ident,0)++ parseMaudeVariable ident =+ case BC.uncons ident of+ Just ('x', num) -> lit <$> (MaudeVar (read (BC.unpack num)) <$> parseSort)+ _ -> fail "invalid variable"++ prefixLen = BC.length funSymPrefix+ ensureValidOp op x | op `elem` [("cons",2), ("nil",0)] = x+ | op `S.member` allFunctionSymbols msig = x+ | otherwise = error $ "Maude.Parser.parseTerm: unknown function"+ ++ "symbol `"++ show op ++"'"
src/Term/Maude/Process.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE TemplateHaskell, DeriveDataTypeable, DeriveFunctor #-}-{-# LANGUAGE FlexibleContexts, NamedFieldPuns #-}+{-# LANGUAGE FlexibleContexts, NamedFieldPuns, BangPatterns #-}+{-# LANGUAGE OverloadedStrings #-} -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE)@@ -26,14 +27,15 @@ , WithMaude ) where -import Data.Either-import Data.List import Data.Traversable hiding ( mapM ) import qualified Data.Map as M import Term.Term import Term.LTerm+import Term.Rewriting.Definitions+import Term.Maude.Signature import Term.Maude.Types+import Term.Maude.Parser import Term.Substitution import Control.Applicative@@ -44,82 +46,17 @@ import Control.DeepSeq (rnf) import Control.Monad.Bind +import qualified Data.ByteString as B+import Data.ByteString (ByteString)+import qualified Data.ByteString.Char8 as BC+ import System.Process import System.IO-import System.Directory import Utils.Misc+import Extension.Data.Monoid --- Pretty printing Maude commands--------------------------------------------------------------------------- | The term algebra and rewriting rules as a functional module in Maude.-theory :: MaudeSig -> String-theory msig@(MaudeSig {enableDH, enableXor, enableMSet, funSig}) = unlines $- [ "fmod MSG is"- , " protecting NAT ." ]- ++- (if enableMSet- then [ " sort Pub Fresh Msg MSet Node TOP ."- , " subsort Msg < MSet ."- , " subsort MSet < TOP ."- , " op m : Nat -> MSet ."- , " op "++funsymPrefix++"mun : MSet MSet -> MSet [comm assoc] ."- , " op "++funsymPrefix++"empty : -> MSet ."- ]- else [ " sort Pub Fresh Msg Node TOP ."])- ++- [ " subsort Pub < Msg ."- , " subsort Fresh < Msg ."- , " subsort Msg < TOP ."- , " subsort Node < TOP ."- -- constants- , " op f : Nat -> Fresh ."- , " op p : Nat -> Pub ."- , " op c : Nat -> Msg ."- , " op n : Nat -> Node ."- -- used for encoding App List [t1,..,tk]- -- list(cons(t1,cons(t2,..,cons(tk,nil)..)))- , " op "++funsymPrefix++"list : TOP -> TOP ."- , " op "++funsymPrefix++"cons : TOP TOP -> TOP ."- , " op "++funsymPrefix++"nil : -> TOP ." ]- ++- (if enableDH- then- [ " op "++funsymPrefix++"one : -> Msg ."- , " op "++funsymPrefix++"exp : Msg Msg -> Msg ."- , " op "++funsymPrefix++"mult : Msg Msg -> Msg [comm assoc] ."- , " op "++funsymPrefix++"inv : Msg -> Msg ." ]- else [])- ++- (if enableXor- then- [ " op "++funsymPrefix++"zero : -> Msg ."- , " op "++funsymPrefix++"xor : Msg Msg -> Msg [comm assoc] ."]- else [])- ++- map theoryFunSym funSig- ++- (map theoryRule $ rrulesForMaudeSig msig)- ++- [ "endfm" ]- where- theoryFunSym (s,ar) =- " op " ++ funsymPrefix ++ s ++" : " ++(concat $ replicate ar "Msg ")++" -> Msg ."- theoryRule (l `RRule` r) =- " eq " ++ ppMaude lm ++" = " ++ ppMaude rm ++" ."- where (lm,rm) = evalBindT ((,) <$> lTermToMTerm' l <*> lTermToMTerm' r) noBindings- `evalFresh` nothingUsed------- Unification using Maude--------------------------------------------------------------------------- | Check environment if communication with Maude should be logged-dEBUGMAUDE ::Bool-dEBUGMAUDE = envIsSet "DEBUG_MAUDE"- -- Unification using a persistent Maude process ----------------------------------------------------------------------- @@ -147,68 +84,71 @@ , unifCount :: !Int , matchCount :: !Int , normCount :: !Int- , mFile :: String } -- | @startMaude@ starts a new instance of Maude and returns a Handle to it. startMaude :: FilePath -> MaudeSig -> IO MaudeHandle startMaude maudePath maudeSig = do- -- create theory file for maude- tempDir <- getTemporaryDirectory- (tempFile, tempH) <- openTempFile tempDir "theory.maude"- hPutStr tempH (theory maudeSig)- hClose tempH- -- start maude- mv <- newMVar =<< startMaudeProcess maudePath tempFile- -- Add a finalizer to the MVar that stops maude and removes the theory- -- file.+ mv <- newMVar =<< startMaudeProcess maudePath maudeSig+ -- Add a finalizer to the MVar that stops maude. addMVarFinalizer mv $ withMVar mv $ \mp -> do terminateProcess (mProc mp) <* waitForProcess (mProc mp)- removeFile (mFile mp) -- return the maude handle return (MaudeHandle maudePath maudeSig mv) -- | Start a Maude process. startMaudeProcess :: FilePath -- ^ Path to Maude- -> FilePath -- ^ Path to Maude theory file+ -> MaudeSig -> IO (MaudeProcess)-startMaudeProcess maudePath maudeTheoryFile = do+startMaudeProcess maudePath maudeSig = do (hin,hout,herr,hproc) <- runInteractiveCommand maudeCmd _ <- getToDelim hout- return (MP hin hout herr hproc 0 0 0 maudeTheoryFile)+ -- set maude flags+ mapM_ (executeMaudeCommand hin hout) setupCmds+ -- input the maude theory+ executeMaudeCommand hin hout (ppTheory maudeSig)+ return (MP hin hout herr hproc 0 0 0) where maudeCmd | dEBUGMAUDE = "sh -c \"tee /tmp/maude.input | " ++ maudePath ++ " -no-tecla -no-banner -no-wrap -batch "- ++ maudeTheoryFile ++ "\" | tee /tmp/maude.output"+ ++ "\" | tee /tmp/maude.output" | otherwise = maudePath ++ " -no-tecla -no-banner -no-wrap -batch " - ++ maudeTheoryFile+ executeMaudeCommand hin hout cmd =+ B.hPutStr hin cmd >> hFlush hin >> getToDelim hout >> return ()+ setupCmds = [ "set show command off .\n"+ , "set show timing off .\n"+ , "set show stats off .\n" ]+ dEBUGMAUDE = envIsSet "DEBUG_MAUDE" ++ -- | Restart the Maude process on this handle. restartMaude :: MaudeHandle -> IO ()-restartMaude (MaudeHandle maudePath _ mv) = modifyMVar_ mv $ \mp -> do+restartMaude (MaudeHandle maudePath maudeSig mv) = modifyMVar_ mv $ \mp -> do terminateProcess (mProc mp) <* waitForProcess (mProc mp)- startMaudeProcess maudePath (mFile mp)+ startMaudeProcess maudePath maudeSig --- | @getToDelim ih@ reads input from @ih@ until @mDelim@ is encountered.--- It returns the string read up to (not including) mDelim.-getToDelim :: Handle -> IO String-getToDelim ih = go []+-- | @getToDelim ih@ reads input from @ih@ until the Maude delimitier is encountered.+-- It returns the 'ByteString' up to (not including) the delimiter.+getToDelim :: Handle -> IO ByteString+getToDelim ih =+ go BC.empty where- go acc = do- c <- hGetChar ih- let acc' = c:acc- if mDelim `isPrefixOf` acc'- then return (reverse (drop (length mDelim) acc'))- else go acc'- mDelim = reverse "Maude> "+ go !acc = do+ bs <- BC.append acc <$> B.hGetSome ih 8096+ case BC.breakSubstring mDelim bs of+ (before, after) | after == mDelim -> return before+ (_, after) | after == "" -> go bs+ _ -> error $ "Too much maude output" ++ BC.unpack bs+ mDelim = "Maude> " -- | @callMaude cmd@ sends the command @cmd@ to Maude and returns Maude's -- output up to the next prompt sign. callMaude :: MaudeHandle -> (MaudeProcess -> MaudeProcess) -- ^ Statistics updater.- -> String -> IO String+ -> ByteString -> IO ByteString callMaude hnd updateStatistics cmd = do -- Ensure that the command is fully evaluated and therefore does not depend -- on another call to Maude anymore. Otherwise, we could end up in a@@ -219,7 +159,7 @@ (`onException` restartMaude hnd) $ modifyMVar (mhProc hnd) $ \mp -> do let inp = mIn mp out = mOut mp- hPutStr inp cmd+ B.hPut inp cmd hFlush inp mp' <- evaluate (updateStatistics mp) res <- getToDelim out@@ -229,37 +169,34 @@ computeViaMaude :: (Show a, Show b, Ord c) => MaudeHandle- -> (MaudeProcess -> MaudeProcess) -- ^ Update statistics- -> (a -> BindT (Lit c LVar) MaudeLit Fresh String) -- ^ Conversion to Maude- -> (M.Map MaudeLit (Lit c LVar) -> MSubst -> b) -- ^ Conversion from Maude+ -> (MaudeProcess -> MaudeProcess) -- ^ Update statistics+ -> (a -> BindT (Lit c LVar) MaudeLit Fresh ByteString) -- ^ Conversion to Maude command+ -> (M.Map MaudeLit (Lit c LVar) -> ByteString -> Either String b) -- ^ Conversion from Maude reply -> a- -> IO [b]+ -> IO b computeViaMaude hnd updateStats toMaude fromMaude inp = do let (cmd, bindings) = runConversion $ toMaude inp- s <- callMaude hnd updateStats cmd- let esubstsm = parseMaudeReply s- substs = map (fromMaude bindings) $ rights esubstsm- case lefts esubstsm of- [] -> return $ substs- es -> fail $ "\ncomputeViaMaude:\nParse error: \n" ++ - concatMap show es ++ - "\n For Maude Output:\n" ++ s ++- "\nFor query:\n" ++ cmd+ reply <- callMaude hnd updateStats cmd+ case fromMaude bindings reply of+ Right res -> return res+ Left e -> fail $ "\ncomputeViaMaude:\nParse error: `" ++ e ++"'"+++ "\nFor Maude Output: `" ++ BC.unpack reply ++"'"+++ "\nFor query: `" ++ BC.unpack cmd++"'" --------------------------------------------------------------------------------- Unification+-- Unification modulo AC ------------------------------------------------------------------------------ -- | @unifyCmd eqs@ returns the Maude command to solve the unification problem @eqs@. -- Expects a nonempty list of equations-unifyCmd :: [Equal MTerm] -> [Char]+unifyCmd :: [Equal MTerm] -> ByteString unifyCmd [] = error "unifyCmd: cannot create cmd for empty list of equations." unifyCmd eqs =- "unify in MSG : " ++seqs++" .\n"+ "unify in MSG : " <> seqs <> " .\n" where- ppEq (Equal t1 t2) = ppMaude t1 ++ " =? " ++ ppMaude t2- seqs = intercalate " /\\ " $ map ppEq eqs+ ppEq (Equal t1 t2) = ppMaude t1 <> " =? " <> ppMaude t2+ seqs = B.intercalate " /\\ " $ map ppEq eqs -- | @unifyViaMaude hnd eqs@ computes all AC unifiers of @eqs@ using the@@ -270,25 +207,26 @@ -> (c -> LSort) -> [Equal (VTerm c LVar)] -> IO [SubstVFresh c LVar] unifyViaMaude _ _ [] = return [emptySubstVFresh] unifyViaMaude hnd sortOf eqs =- computeViaMaude hnd incUnifCount toMaude msubstToLSubstVFresh eqs+ computeViaMaude hnd incUnifCount toMaude fromMaude eqs where+ msig = mhMaudeSig hnd toMaude = fmap unifyCmd . mapM (traverse (lTermToMTerm sortOf))+ fromMaude bindings reply =+ map (msubstToLSubstVFresh bindings) <$> parseUnifyReply msig reply incUnifCount mp = mp { unifCount = 1 + unifCount mp } - ------------------------------------------------------------------------------ -- Matching modulo AC ------------------------------------------------------------------------------ -- | @matchCmd p t@ returns the Maude command to match the terms @t@ to the -- pattern @p@.-matchCmd :: [Equal MTerm] -> String+matchCmd :: [Equal MTerm] -> ByteString matchCmd eqs =- "match in MSG : " ++ppTerms t2s++ " <=? " ++ ppTerms t1s++" .\n"+ "match in MSG : " <> ppTerms t2s <> " <=? " <> ppTerms t1s <> " .\n" where- -- FIXME: slow (t1s,t2s) = unzip [ (a,b) | Equal a b <- eqs ]- ppTerms = ppMaude . listToTerm+ ppTerms = ppMaude . fAppList -- | @matchViaMaude (t, p)@ computes a complete set of AC matchers of the term -- @t@ to the pattern @p@ via Maude.@@ -299,9 +237,12 @@ -> IO [Subst c LVar] matchViaMaude _ _ [] = return [emptySubst] matchViaMaude hnd sortOf matcheqs =- computeViaMaude hnd incMatchCount toMaude msubstToLSubstVFree eqs+ computeViaMaude hnd incMatchCount toMaude fromMaude eqs where+ msig = mhMaudeSig hnd toMaude = fmap matchCmd . mapM (traverse (lTermToMTerm sortOf)) + fromMaude bindings reply =+ map (msubstToLSubstVFree bindings) <$> parseMatchReply msig reply incMatchCount mp = mp { matchCount = 1 + matchCount mp } eqs = [Equal t p | MatchWith t p <- matcheqs ] @@ -311,9 +252,8 @@ -- | @normCmd t@ returns the Maude command to normalize the term @t@ -- pattern @p@.-normCmd :: MTerm -> String-normCmd tm = "reduce "++ppMaude tm++" .\n"-+normCmd :: MTerm -> ByteString+normCmd tm = "reduce " <> ppMaude tm <> " .\n" -- | @normViaMaude t@ normalizes the term t via Maude. normViaMaude :: (IsConst c , Show (Lit c LVar), Ord c)@@ -321,19 +261,16 @@ -> (c -> LSort) -> VTerm c LVar -> IO (VTerm c LVar)-normViaMaude hnd sortOf t = do- let (cmd, bindings) = runConversion $ toMaude t- s <- callMaude hnd incNorm cmd- case parseReduceSolution s of- Right mt -> return $ evalBindT (mTermToLNTerm "z" mt) bindings- `evalFresh` nothingUsed- Left e -> fail $ "\ncomputeViaMaude:\nParse error: \n" ++ - show e ++ - "\n For Maude Output:\n" ++ s ++- "\nFor query:\n" ++ cmd+normViaMaude hnd sortOf t =+ computeViaMaude hnd incNormCount toMaude fromMaude t where- toMaude = fmap normCmd . (lTermToMTerm sortOf)- incNorm mp = mp { normCount = 1 + normCount mp }+ msig = mhMaudeSig hnd+ toMaude = fmap normCmd . (lTermToMTerm sortOf)+ fromMaude bindings reply =+ (\mt -> (mTermToLNTerm "z" mt `evalBindT` bindings) `evalFresh` nothingUsed)+ <$> parseReduceReply msig reply+ incNormCount mp = mp { normCount = 1 + normCount mp }+ -- Passing the Handle to Maude via a Reader monad -------------------------------------------------
+ src/Term/Maude/Signature.hs view
@@ -0,0 +1,174 @@+{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}+{-# LANGUAGE TemplateHaskell, FlexibleContexts, TupleSections #-}+{-# LANGUAGE ViewPatterns, NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+-- |+-- Copyright : (c) 2010, 2011 Benedikt Schmidt+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>+--+-- Euqatiuonal signatures for Maude.+module Term.Maude.Signature (+ -- * Maude signatures+ MaudeSig+ , enableDH+ , enableXor+ , enableMSet+ , functionSymbols+ , stRules+ , allFunctionSymbols+ , irreducibleFunctionSymbols+ , rrulesForMaudeSig++ -- * predefined maude signatures+ , dhMaudeSig+ , xorMaudeSig+ , pairMaudeSig+ , asymEncMaudeSig+ , symEncMaudeSig+ , signatureMaudeSig+ , hashMaudeSig+ , msetMaudeSig+ , minimalMaudeSig++ -- * extend maude signatures+ , addFunctionSymbol+ , addStRule++ -- * pretty printing+ , prettyMaudeSig+ ) where++import Term.Term+import Term.LTerm+import Term.Builtin.Rules+import Term.SubtermRule++import Control.Monad.Fresh+import Control.Applicative+import Control.DeepSeq++import Data.DeriveTH+import Data.Binary+import Data.Foldable (asum)+import Data.Monoid+import Data.Set (Set)+import qualified Data.Set as S++import qualified Data.ByteString.Char8 as BC++import qualified Text.PrettyPrint.Highlight as P++------------------------------------------------------------------------------+-- Maude Signatures+----------------------------------------------------------------------++-- | The required information to define a @Maude functional module@.+data MaudeSig = MaudeSig+ { enableDH :: Bool+ , enableXor :: Bool+ , enableMSet :: Bool+ , functionSymbols :: Set NonACSym -- ^ function signature not including the function+ -- symbols for DH, Xor, and MSet+ , stRules :: Set StRule+ , allFunctionSymbols :: Set NonACSym -- ^ function signature including the+ -- nonAC function symbols for DH, Xor, and MSet+ -- can be computed from enableX and functionSymbols+ , irreducibleFunctionSymbols :: Set NonACSym+ }+ deriving (Ord, Show, Eq)++-- | Smart constructor for MaudeSig. Computes allFunctionSymbols and irreducibleFunctionSymbols.+maudeSig :: Bool -> Bool -> Bool -> Set NonACSym -> Set StRule -> MaudeSig+maudeSig dh xor mset funs strs =+ MaudeSig dh xor mset funs strs allfuns irreduciblefuns+ where+ allfuns = funs `S.union` (if dh then dhFunSig else S.empty)+ `S.union` (if xor then xorFunSig else S.empty)+ `S.union` (if mset then msetFunSig else S.empty)+ irreduciblefuns = allfuns `S.difference` reducible+ reducible =+ S.fromList [ o | StRule (viewTerm -> FApp (NonAC o) _) _ <- S.toList strs ]+ `S.union` dhReducibleFunSig++-- | A monoid instance to combine maude signatures.+instance Monoid MaudeSig where+ (MaudeSig dh1 xor1 mset1 funsymbols1 stRules1 _ _) `mappend` (MaudeSig dh2 xor2 mset2 funsymbols2 stRules2 _ _) =+ maudeSig (dh1 || dh2) (xor1 || xor2) (mset1 || mset2)+ (S.union funsymbols1 funsymbols2)+ (S.union stRules1 stRules2)+ mempty = maudeSig False False False S.empty S.empty++-- | Add function symbol to given maude signature.+addFunctionSymbol :: NonACSym -> MaudeSig -> MaudeSig+addFunctionSymbol funsym msig =+ msig `mappend` maudeSig False False False (S.fromList [funsym]) S.empty++-- | Add subterm rule to given maude signature.+addStRule :: StRule -> MaudeSig -> MaudeSig+addStRule str msig =+ msig `mappend` maudeSig False False False S.empty (S.fromList [str])++-- | @rrulesForMaudeSig msig@ returns all rewriting rules including the rules+-- for xor, dh, and multiset.+rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)+rrulesForMaudeSig (MaudeSig {enableXor, enableDH, enableMSet, stRules}) =+ (S.map stRuleToRRule stRules)+ `S.union` (if enableDH then dhRules else S.empty)+ `S.union` (if enableXor then xorRules else S.empty)+ `S.union` (if enableMSet then msetRules else S.empty)++------------------------------------------------------------------------------+-- Builtin maude signatures+------------------------------------------------------------------------------++-- | Maude signatures for the AC symbols.+dhMaudeSig, xorMaudeSig, msetMaudeSig :: MaudeSig+dhMaudeSig = maudeSig True False False S.empty S.empty+xorMaudeSig = maudeSig False True False S.empty S.empty+msetMaudeSig = maudeSig False False True S.empty S.empty++-- | Maude signatures for the default subterm symbols.+pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig :: MaudeSig+pairMaudeSig = maudeSig False False False pairFunSig pairRules+symEncMaudeSig = maudeSig False False False symEncFunSig symEncRules+asymEncMaudeSig = maudeSig False False False asymEncFunSig asymEncRules+signatureMaudeSig = maudeSig False False False signatureFunSig signatureRules+hashMaudeSig = maudeSig False False False hashFunSig S.empty++-- | The minimal maude signature.+minimalMaudeSig :: MaudeSig+minimalMaudeSig = pairMaudeSig++------------------------------------------------------------------------------+-- Pretty Printing+------------------------------------------------------------------------------++prettyMaudeSig :: P.HighlightDocument d => MaudeSig -> d+prettyMaudeSig sig = P.vcat+ [ ppNonEmptyList' "builtin:" P.text builtIns+ , ppNonEmptyList' "functions:" ppFunSymb $ S.toList (functionSymbols sig)+ , ppNonEmptyList + (\ds -> P.sep (P.keyword_ "equations:" : map (P.nest 2) ds))+ prettyStRule $ S.toList (stRules sig)+ ]+ where+ ppNonEmptyList' name = ppNonEmptyList ((P.keyword_ name P.<->) . P.fsep)+ ppNonEmptyList _ _ [] = P.emptyDoc+ ppNonEmptyList hdr pp xs = hdr $ P.punctuate P.comma $ map pp xs++ builtIns = asum $ map (\(f, x) -> guard (f sig) *> pure x)+ [ (enableDH, "diffie-hellman")+ , (enableXor, "xor")+ , (enableMSet, "multiset")+ ]++ ppFunSymb (f,k) = P.text $ BC.unpack f ++ "/" ++ show k+++-- derived instances+--------------------++$(derive makeBinary ''MaudeSig)+$(derive makeNFData ''MaudeSig)
src/Term/Maude/Types.hs view
@@ -1,5 +1,7 @@ {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}-{-# LANGUAGE TemplateHaskell, FlexibleContexts, TupleSections, NamedFieldPuns #-}+{-# LANGUAGE TemplateHaskell, FlexibleContexts, TupleSections #-}+{-# LANGUAGE ViewPatterns, NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-} -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt -- License : GPL v3 (see LICENSE)@@ -7,115 +9,51 @@ -- Maintainer : Benedikt Schmidt <beschmi@gmail.com> -- -- Types for communicating with Maude.-module Term.Maude.Types where+module Term.Maude.Types (+ -- * Maude terms+ MaudeLit(..)+ , MSubst+ , MTerm + -- * conversion from/to maude terms+ , lTermToMTerm+ , lTermToMTerm'+ , mTermToLNTerm+ , runConversion+ , msubstToLSubstVFresh+ , msubstToLSubstVFree++ ) where+ import Term.Term import Term.LTerm-import Term.Builtin.Rules import Term.Substitution-import Term.SubtermRule import Utils.Misc-import Extension.Prelude import Control.Monad.Fresh import Control.Monad.Bind import Control.Applicative-import Control.DeepSeq -import Data.DeriveTH-import Data.Binary-import Data.Foldable (asum)-import Data.Traversable-import Data.List-import Data.Monoid-import Data.List.Split hiding (sepBy, oneOf)+import Data.Traversable hiding (mapM) import Data.Maybe import qualified Data.Map as M import Data.Map ( Map ) -import Text.ParserCombinators.Parsec hiding (many, optional, (<|>))-import qualified Text.PrettyPrint.Highlight as P- -- Maude Terms ---------------------------------------------------------------------- -data MaudeLit = MaudeVar Int LSort- | FreshVar Int LSort- | MaudeConst Int LSort+data MaudeLit = MaudeVar Integer LSort+ | FreshVar Integer LSort+ | MaudeConst Integer LSort deriving (Eq, Ord, Show) type MTerm = Term MaudeLit -type MSubst = [((LSort, Int), MTerm)]+type MSubst = [((LSort, Integer), MTerm)] --- Maude Signatures--------------------------------------------------------------------------- | The required information to define a @Maude functional module@.-data MaudeSig = MaudeSig- { enableDH :: Bool- , enableXor :: Bool- , enableMSet :: Bool- , funSig :: FunSig -- ^ function signature not including the function symbols for DH, Xor, MSet- , stRules :: [StRule]- }- deriving (Ord, Show, Eq)---- | The empty maude signature.-emptyMaudeSig :: MaudeSig-emptyMaudeSig = MaudeSig False False False [] []---- | A monoid instance to combine maude signatures.-instance Monoid MaudeSig where- (MaudeSig dh xor mset funsig stRules) `mappend` (MaudeSig dh' xor' mset' funsig' stRules') =- MaudeSig (dh || dh') (xor || xor') (mset || mset')- (sortednub $ funsig ++ funsig') (sortednub $ stRules ++ stRules')- mempty = emptyMaudeSig---- | Maude signatures for the AC symbols.-dhMaudeSig, xorMaudeSig, msetMaudeSig :: MaudeSig-dhMaudeSig = emptyMaudeSig { enableDH = True }-xorMaudeSig = emptyMaudeSig { enableXor = True }-msetMaudeSig = emptyMaudeSig { enableMSet = True }---- | Maude signatures for the default subterm symbols.-pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig :: MaudeSig-pairMaudeSig = emptyMaudeSig { funSig = pairFunSig, stRules = pairRules }-symEncMaudeSig = emptyMaudeSig { funSig = symEncFunSig, stRules = symEncRules }-asymEncMaudeSig = emptyMaudeSig { funSig = asymEncFunSig, stRules = asymEncRules }-signatureMaudeSig = emptyMaudeSig { funSig = signatureFunSig, stRules = signatureRules }-hashMaudeSig = emptyMaudeSig { funSig = hashFunSig, stRules = [] }---- | The minimal maude signature.-minimalMaudeSig :: MaudeSig-minimalMaudeSig = pairMaudeSig---- | Maude signatures with all builtin symbols.-allMaudeSig :: MaudeSig-allMaudeSig = mconcat- [ dhMaudeSig, xorMaudeSig, msetMaudeSig- , pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig ]---- | @rrulesForMaudeSig msig@ returns all rewriting rules including the rules--- for xor, dh, and multiset.-rrulesForMaudeSig :: MaudeSig -> [RRule LNTerm]-rrulesForMaudeSig (MaudeSig {enableXor, enableDH, enableMSet, stRules}) =- map stRuleToRRule stRules- ++ (if enableDH then dhRules else [])- ++ (if enableXor then xorRules else [])- ++ (if enableMSet then msetRules else [])---- | @funSigForMaudeSig msig@ returns all non-AC function symbols including the--- function symbols for xor, dh, and multiset.-funSigForMaudeSig :: MaudeSig -> FunSig-funSigForMaudeSig (MaudeSig {enableXor, enableDH, enableMSet, funSig}) =- funSig- ++ (if enableDH then dhFunSig else [])- ++ (if enableXor then xorFunSig else [])- ++ (if enableMSet then msetFunSig else [])-+------------------------------------------------------------------------ -- Convert between MTerms and LNTerms ------------------------------------------------------------------------ @@ -125,34 +63,37 @@ -> m MTerm lTermToMTerm' = lTermToMTerm sortOfName + -- | Convert an @LNTerm@ with arbitrary names to an @MTerm@. lTermToMTerm :: (MonadBind (Lit c LVar) MaudeLit m, MonadFresh m, Show (Lit c LVar), Ord c) => (c -> LSort) -- ^ A function that returns the sort of a constant. -> VTerm c LVar -- ^ The term to translate. -> m MTerm lTermToMTerm sortOf =- traverse exportLit- where- exportLit a@(Var lv) =- importBinding (\_ i -> MaudeVar i (lvarSort lv)) a "x"- exportLit a@(Con n) = importBinding (\_ i -> MaudeConst i (sortOf n)) a "a"+ go . viewTerm+ where+ go (Lit l) = lit <$> exportLit l+ go (FApp o as) = fApp o <$> mapM (go . viewTerm) as+ exportLit a@(Var lv) =+ importBinding (\_ i -> MaudeVar i (lvarSort lv)) a "x"+ exportLit a@(Con n) = importBinding (\_ i -> MaudeConst i (sortOf n)) a "a" --- | Convert a 'MaudeTerm' to an 'LNTerm' under the assumption that the bindings++-- | Convert an 'MTerm' to an 'LNTerm' under the assumption that the bindings -- for the constants are already available.------ Use @runBindCtxt@ with the inverted map from the @lTermtoMaudeTerm@ conversion to--- ensure this. mTermToLNTerm :: (MonadBind MaudeLit (Lit c LVar) m, MonadFresh m, Show (Lit c LVar), Ord c, Show c) => String -- ^ Name hint for freshly generated variables. -> MTerm -- ^ The maude term to convert. -> m (VTerm c LVar) mTermToLNTerm nameHint =- traverse importLit+ go . viewTerm where- importLit a@(MaudeVar _ lsort) = importBinding (\n i -> Var (LVar n lsort i)) a nameHint- importLit a@(FreshVar _ lsort) = importBinding (\n i -> Var (LVar n lsort i)) a nameHint- importLit a = fromMaybe (error $ "fromMTerm: unknown constant `" ++ show a ++ "'") <$>- lookupBinding a+ go (Lit l) = lit <$> importLit l+ go (FApp o as) = fApp o <$> mapM (go . viewTerm) as+ importLit a@(MaudeVar _ lsort) = importBinding (\n i -> Var (LVar n lsort i)) a nameHint+ importLit a@(FreshVar _ lsort) = importBinding (\n i -> Var (LVar n lsort i)) a nameHint+ importLit a = fromMaybe (error $ "fromMTerm: unknown constant `" ++ show a ++ "'") <$>+ lookupBinding a -- Back and forth conversions@@ -164,8 +105,9 @@ runConversion :: Ord c => BindT (Lit c LVar) MaudeLit Fresh a -- ^ Computation to execute. -> (a, Map MaudeLit (Lit c LVar))-runConversion to = (x, invertMap bindings)- where (x, bindings) = runBindT to noBindings `evalFresh` nothingUsed+runConversion to =+ (x, invertMap bindings)+ where (x, bindings) = runBindT to noBindings `evalFresh` nothingUsed -- | Run a @BindT MaudeLit (Lit c LVar) Fresh@ computation using the -- supplied binding map and the corresponding fresh supply.@@ -173,10 +115,11 @@ -> Map MaudeLit (Lit c LVar) -- ^ Binding map that should be used. -> a runBackConversion back bindings =- evalBindT back bindings `evalFreshAvoiding` M.elems bindings+ evalBindT back bindings `evalFreshAvoiding` M.elems bindings --- Conversion between Maude and standard substitutions ------------------------------------------------------------------------+-- Conversion between Maude and Standard substitutions+------------------------------------------------------------------------ -- | @msubstToLSubstVFresh bindings substMaude@ converts a substitution -- returned by Maude to a 'VFresh' substitution. It expects that the@@ -187,22 +130,22 @@ -> MSubst -- ^ The maude substitution. -> SubstVFresh c LVar msubstToLSubstVFresh bindings substMaude- | not $ null [i | (_,t) <- substMaude, MaudeVar _ i <- lits t] =- error $ "msubstToLSubstVFresh: nonfresh variables in `"++show substMaude++"'"- | otherwise = removeRenamings $ substFromListVFresh slist+ | not $ null [i | (_,t) <- substMaude, MaudeVar _ i <- lits t] =+ error $ "msubstToLSubstVFresh: nonfresh variables in `"++show substMaude++"'"+ | otherwise = removeRenamings $ substFromListVFresh slist where- slist = runBackConversion (traverse translate substMaude) bindings- -- try to keep variable name for xi -> xj mappings- -- commented out, seems wrong- -- translate ((s,i), mt@(Lit (FreshVar _ _))) = do- -- lv <- lookupVar s i- -- (lv,) <$> mTermToLNTerm (lvarName lv) mt- translate ((s,i),mt) = (,) <$> lookupVar s i <*> mTermToLNTerm "x" mt- lookupVar s i = do b <- lookupBinding (MaudeVar i s)- case b of- Just (Var lv) -> return lv- _ -> error $ "msubstToLSubstVFrsh: binding for maude variable `"- ++show (s,i) ++"' not found in "++show bindings+ slist = runBackConversion (traverse translate substMaude) bindings+ -- try to keep variable name for xi -> xj mappings+ -- commented out, seems wrong+ -- translate ((s,i), mt@(Lit (FreshVar _ _))) = do+ -- lv <- lookupVar s i+ -- (lv,) <$> mTermToLNTerm (lvarName lv) mt+ translate ((s,i),mt) = (,) <$> lookupVar s i <*> mTermToLNTerm "x" mt+ lookupVar s i = do b <- lookupBinding (MaudeVar i s)+ case b of+ Just (Var lv) -> return lv+ _ -> error $ "msubstToLSubstVFrsh: binding for maude variable `"+ ++show (s,i) ++"' not found in "++show bindings -- | @msubstToLSubstVFree bindings substMaude@ converts a substitution -- returned by Maude to a 'VFree' substitution. It expects that the@@ -211,184 +154,15 @@ msubstToLSubstVFree :: (Ord c, Show (Lit c LVar), Show c) => Map MaudeLit (Lit c LVar) -> MSubst -> Subst c LVar msubstToLSubstVFree bindings substMaude- | not $ null [i | (_,t) <- substMaude, FreshVar _ i <- lits t] =- error $ "msubstToLSubstVFree: fresh variables in `"++show substMaude- | otherwise = substFromList slist- where- slist = evalBindT (traverse translate substMaude) bindings- `evalFreshAvoiding` M.elems bindings- translate ((s,i),mt) = (,) <$> lookupVar s i <*> mTermToLNTerm "x" mt- lookupVar s i = do b <- lookupBinding (MaudeVar i s)- case b of- Just (Var lv) -> return lv- _ -> error $ "msubstToLSubstVFree: binding for maude variable `"- ++show (s,i)++"' not found in "++show bindings----- Pretty printing of Maude terms.----------------------------------------------------------------------------- | Pretty print an 'LSort'.-ppMSort :: LSort -> String-ppMSort LSortPub = "Pub"-ppMSort LSortFresh = "Fresh"-ppMSort LSortMsg = "Msg"-ppMSort LSortNode = "Node"-ppMSort LSortMSet = "MSet"---- | Used to prevent clashes with predefined Maude function symbols--- like @true@-funsymPrefix :: String-funsymPrefix = "tamX"---- | Pretty print an AC symbol for Maude.-ppMaudeACSym :: ACSym -> String-ppMaudeACSym o =- funsymPrefix- ++ case o of- Mult -> "mult"- MUn -> "mun"- Xor -> "xor"---- | @ppMaude t@ pretty prints the term @t@ for Maude.-ppMaude :: Term MaudeLit -> String-ppMaude (Lit (MaudeVar i lsort)) = "x"++ show i ++":"++ppMSort lsort-ppMaude (Lit (MaudeConst i LSortFresh)) = "f("++ show i ++")"-ppMaude (Lit (MaudeConst i LSortPub)) = "p("++ show i ++")"-ppMaude (Lit (MaudeConst i LSortMsg)) = "c("++ show i ++")"-ppMaude (Lit (MaudeConst i LSortNode)) = "n("++ show i ++")"-ppMaude (Lit (MaudeConst i LSortMSet)) = "m("++ show i ++")"-ppMaude (Lit (FreshVar _ _)) = error "ppMaude: FreshVar not allowed"-ppMaude (FApp (NonAC (fsym,_)) []) = funsymPrefix++fsym-ppMaude (FApp (NonAC (fsym,_)) as) =- funsymPrefix++fsym++"("++(intercalate "," (map ppMaude as))++")"-ppMaude (FApp (AC op) as) =- ppMaudeACSym op ++ "("++(intercalate "," (map ppMaude as))++")"-ppMaude (FApp List as) =- funsymPrefix++"list(" ++ ppList as ++ ")"- where- ppList [] = funsymPrefix++"nil"- ppList (x:xs) = funsymPrefix++"cons(" ++ ppMaude x ++ "," ++ ppList xs ++ ")"---- Parser for Maude output----------------------------------------------------------------------------- | @parseSolutions reply@ takes a @reply@ to a unification query--- returned by Maude and extracts the unifiers.-parseMaudeReply :: String -> [Either ParseError MSubst]-parseMaudeReply reply =- case find (\s -> s `elem` ["No unifier.", "No match."]) linesReply of- Just _ -> []- Nothing -> map parseSolution $ splitOn [""] $- dropWhile (\s -> not ("Solution" `isPrefixOf` s)) linesReply- where- linesReply = lines reply---- | @parseSolution l@ parses a single solution returned by Maude.-parseSolution :: [String] -> Either ParseError MSubst-parseSolution l = parse pSolution "" (unlines l)- where- pSolution = do- string "Solution" <* space- many1 digit <* newline- (many1 pmap <|> (string "empty substitution" *> newline *> return []))- pmap = (,) <$> (flip (,) <$> (char 'x' *> pNat <* string ":") <*> psort)- <*> (space *> string "-->" *> space *> expr <* newline)---- | Parse an 'MSort'.-psort :: GenParser Char st LSort-psort = string "Pub" *> return LSortPub- <|> string "Fresh" *> return LSortFresh- <|> try (string "Msg" *> return LSortMsg)- <|> string "MSet" *> return LSortMSet- <|> string "Node" *> return LSortNode----- | @expr@ is a parser for Maude Msg expressions.--- We parse list, cons and nil as FreeSym. We therefore--- have to fixup the term later on.-expr :: GenParser Char st MTerm-expr = fixup <$> p- where- p = Lit <$> ( flip MaudeConst <$> try parseConstSym <*> pNat <* string ")")- <|> Lit <$> (MaudeVar <$> (try (string "x" *> pNat <* string ":")) <*> psort)- <|> Lit <$> (FreshVar <$> (string "#" *> pNat <* string ":") <*> psort)- <|> do op <- try parseACSym- args <- sepBy expr commaWS- char ')'- return $ FApp (AC op) args- <|> do fsym <- try (parseFreeSym <* string "(")- args <- sepBy expr commaWS- string ")"- return $ FApp (NonAC (fsym, length args)) args- <|> do fsym <- parseFreeSym- return $ FApp (NonAC (fsym, 0)) []-- parseConstSym = (string "f(" *> pure LSortFresh)- <|> (string "p(" *> pure LSortPub)- <|> (string "c(" *> pure LSortMsg)- <|> (string "n(" *> pure LSortNode)- <|> (string "m(" *> pure LSortMSet)-- parseACSym = try (string (ppMaudeACSym Mult++"(")) *> return Mult- <|> try (string (ppMaudeACSym MUn++"(")) *> return MUn- <|> (string (ppMaudeACSym Xor++"(")) *> return Xor-- parseFreeSym = string funsymPrefix *> many1 (oneOf (['a' .. 'z']++['A'..'Z']))- - fixup t@(Lit _) = t- fixup (FApp (NonAC ("list",1)) [a]) = FApp List (collect a)- where- collect (FApp (NonAC ("cons",2)) [x,xs]) = fixup x:collect xs- collect (FApp (NonAC ("nil",0)) []) = []- collect t =- error $"MTerm.expr: fixup failed, Maude returned invalid term, "++show t- fixup (FApp (NonAC ("list",_)) _) =- error "MTerm.expr: fixup failed, Maude returned invalid term, list not unary"- fixup (FApp x ts) = FApp x $ map fixup ts---- | @parseSolution l@ parses a single solution returned by Maude.-parseReduceSolution :: String -> Either ParseError MTerm-parseReduceSolution s = case lines s of- [_,_,_,res] -> parse pReduceSolution "" res- _ -> fail ("parseReduceSolution: invalid Maude output: `" ++ s ++ "'")- where- pReduceSolution = do- string "result" <* space- (psort <|> (string "TOP" *> pure LSortPub))- -- FIXME: clean up, we use TOP for lists- string ":" *> space *> expr----------------------------------------------------------------------------------- Pretty Printing---------------------------------------------------------------------------------prettyMaudeSig :: P.HighlightDocument d => MaudeSig -> d-prettyMaudeSig sig = P.vcat- [ ppNonEmptyList' "builtin:" P.text builtIns- , ppNonEmptyList' "functions:" ppFunSymb $ funSig sig- , ppNonEmptyList - (\ds -> P.sep (P.keyword_ "equations:" : map (P.nest 2) ds))- prettyStRule $ stRules sig- ]+ | not $ null [i | (_,t) <- substMaude, FreshVar _ i <- lits t] =+ error $ "msubstToLSubstVFree: fresh variables in `"++show substMaude+ | otherwise = substFromList slist where- ppNonEmptyList' name = ppNonEmptyList ((P.keyword_ name P.<->) . P.fsep)- ppNonEmptyList _ _ [] = P.emptyDoc- ppNonEmptyList hdr pp xs = hdr $ P.punctuate P.comma $ map pp xs-- builtIns = asum $ map (\(f, x) -> guard (f sig) *> pure x)- [ (enableDH, "diffie-hellman")- , (enableXor, "xor")- , (enableMSet, "multiset")- ]-- ppFunSymb (f,k) = P.text $ f ++ "/" ++ show k----- derived instances-----------------------$(derive makeBinary ''MaudeSig)-$(derive makeNFData ''MaudeSig)--+ slist = evalBindT (traverse translate substMaude) bindings+ `evalFreshAvoiding` M.elems bindings+ translate ((s,i),mt) = (,) <$> lookupVar s i <*> mTermToLNTerm "x" mt+ lookupVar s i = do b <- lookupBinding (MaudeVar i s)+ case b of+ Just (Var lv) -> return lv+ _ -> error $ "msubstToLSubstVFree: binding for maude variable `"+ ++show (s,i)++"' not found in "++show bindings
src/Term/Narrowing/Narrow.hs view
@@ -16,6 +16,7 @@ import Control.Monad.Reader import Extension.Prelude+import qualified Data.Set as S import Debug.Trace.Ignore @@ -30,9 +31,9 @@ -- then @s@ is included in the list of returned substitutions. narrowSubsts :: LNTerm -> WithMaude [LNSubstVFresh] narrowSubsts t = reader $ \hnd -> sortednub $ do- let rules0 = rrulesForMaudeSig $ mhMaudeSig hnd+ let rules0 = S.toList . rrulesForMaudeSig $ mhMaudeSig hnd (l `RRule` _r) <- renameAvoiding rules0 t p <- positionsNonVar t- subst <- unifyLNTerm [Equal (t >* p) l] `runReader` hnd- guard (trace ("narrowSubsts"++ (show ((t >* p), l, restrictVFresh (frees t) subst))) True)+ subst <- unifyLNTerm [Equal (t `atPos` p) l] `runReader` hnd+ guard (trace ("narrowSubsts"++ (show ((t `atPos` p), l, restrictVFresh (frees t) subst))) True) return $ restrictVFresh (frees t) subst
src/Term/Positions.hs view
@@ -1,5 +1,8 @@+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}+ -- spurious warnings for view patterns -- |--- Copyright : (c) 2010, 2011 Benedikt Schmidt+-- Copyright : (c) 2010-12 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt <beschmi@gmail.com>@@ -7,7 +10,7 @@ -- Positions and replacement in terms. module Term.Positions where -import Term.Term+import Term.VTerm import Safe -- Positions, subterm access, subterm replacement@@ -16,28 +19,59 @@ -- | A position in a term is a list of integers. type Position = [Int] --- | @t >* p@ returns the subterm of term @t@ at position @p@.--- The standard standard notation for @t >* p@ is @t|_p@.-(>*) :: Term a -> Position -> Term a-t >* [] = t-(FApp _ as) >* (i:ps) = case atMay as i of- Nothing -> error "Term.Positions.(>*): invalid position given"- Just a -> a >* ps-(Lit _) >* (_:_) = error "Term.Positions.(>*): invalid position given"+-- | @t `atPos` p@ returns the subterm of term @t@ at position @p@.+-- The standard notation for @t `atPos` p@ is @t|_p@.+-- 'atPos' accounts for AC symbols by interpreting n-ary operator+-- applications @*[t1,t2,..tk-1,tk]@ as binary applications+-- @t1*(t2*..(tk-1*tk)..)@.+atPos :: Ord a => Term a -> Position -> Term a+atPos t [] = t+atPos (viewTerm -> FApp (AC _) (a:_)) (0:ps) =+ a `atPos` ps+atPos (viewTerm -> FApp (AC _) [_]) _ =+ error "Term.Positions.atPos: invalid position given"+atPos (viewTerm -> FApp fsym@(AC _) (_:as)) (1:ps) =+ (fApp fsym as) `atPos` ps+atPos (viewTerm -> FApp (AC _) []) _ =+ error $ "Term.Positions.positionsNonVar: impossible, "+ ++"nullary AC symbol appliction"+atPos (viewTerm -> FApp _ as) (i:ps) = case atMay as i of+ Nothing -> error "Term.Positions.atPos: invalid position given"+ Just a -> a `atPos` ps+atPos (viewTerm -> Lit _) (_:_) =+ error "Term.Positions.atPos: invalid position given" --- | @t >=*(s,p)@ returns the term @t'@ where the subterm a position @p@--- is replaced by @s@. The standard notation for @t >=*(s,p)@ is @t[s]_p@.-(>=*) :: Term a -> (Term a, Position) -> Term a-_ >=* (s,[]) = s-(FApp fsym as) >=* (s,i:ps) = if 0 <= i && i < length as- then FApp fsym ((take i as)++[as!!i >=* (s,ps)]++(drop (i+1) as))- else error "Term.Positions.(>=*): invalid position given"-(Lit _) >=* (_,_:_) = error "Term.Positions.(>=*): invalid position given"+-- | @t `replacePos` (s,p)@ returns the term @t'@ where the subterm at position @p@+-- is replaced by @s@. The standard notation for @t `replacePos` (s,p)@ is @t[s]_p@.+-- 'replacePos' accounts for AC symbols in the same ways as 'atPos'.+-- FIXME: The AC can be optimized.+replacePos :: Ord a => Term a -> (Term a, Position) -> Term a+replacePos _ (s,[]) = s+replacePos (viewTerm -> FApp fsym@(AC _) (a:as)) (s,0:ps) =+ fApp fsym ((a `replacePos` (s,ps)):as)+replacePos (viewTerm -> FApp fsym@(AC _) (a:as)) (s,1:ps) =+ fApp fsym [a, (fApp fsym as) `replacePos` (s,ps)]+replacePos (viewTerm -> FApp (AC _) _) _ =+ error "Term.Positions.replacePos: invalid position given"+replacePos (viewTerm -> FApp fsym as) (s,i:ps) =+ if 0 <= i && i < length as+ then fApp fsym ((take i as)++[as!!i `replacePos` (s,ps)]++(drop (i+1) as))+ else error "Term.Positions.replacePos: invalid position given"+replacePos (viewTerm -> Lit _) (_,_:_) = error "Term.Positions.replacePos: invalid position given" -- | @positionsNonVar t@ returns all the non-variable positions in the term @t@.-positionsNonVar :: VTerm a b -> [Position]-positionsNonVar t = go t- where go (Lit (Con _)) = [[]]- go (Lit (Var _)) = []- go (FApp _ as) = []:concat (zipWith (\i a -> map (i:) (go a)) [0..] as)+-- 'positionsNonVar' accounts for AC symbols in the same ways as 'atPos'.+positionsNonVar :: (Show a, Show b) => VTerm a b -> [Position]+positionsNonVar t =+ go t+ where+ go (viewTerm -> Lit (Con _)) = [[]]+ go (viewTerm -> Lit (Var _)) = []+ go (viewTerm -> FApp (AC _) as) = []:concat (zipWith (\i a -> map ((position i len)++) (go a))+ [0..] as)+ where len = length as+ go (viewTerm -> FApp _ as) = []:concat (zipWith (\i a -> map (i:) (go a)) [0..] as)++ position i len | i == len - 1 = replicate i 1+ | otherwise = replicate i 1 ++ [0]
+ src/Term/Rewriting/Definitions.hs view
@@ -0,0 +1,102 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-}+-- |+-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>+--+-- Term Equalities, Matching Problems, and Subterm Rules.+module Term.Rewriting.Definitions (+ -- * Equalities+ Equal (..)+ , evalEqual++ -- * Matching Problems+ , Match(..)++ -- * Rewriting Rules+ , RRule(..)++ ) where++import Control.Applicative+import Data.Monoid+import Data.Foldable+import Data.Traversable++----------------------------------------------------------------------+-- Equalities, matching problems, and rewriting rules+----------------------------------------------------------------------++-- | An equality.+data Equal a = Equal { eqLHS :: a, eqRHS :: a }+ deriving (Eq, Show)++-- | True iff the two sides of the equality are equal with respect to their+-- 'Eq' instance.+evalEqual :: Eq a => Equal a -> Bool+evalEqual (Equal l r) = l == r++instance Functor Equal where+ fmap f (Equal lhs rhs) = Equal (f lhs) (f rhs) ++instance Monoid a => Monoid (Equal a) where+ mempty = Equal mempty mempty+ (Equal l1 r1) `mappend` (Equal l2 r2) = + Equal (l1 `mappend` l2) (r1 `mappend` r2)++instance Foldable Equal where+ foldMap f (Equal l r) = f l `mappend` f r++instance Traversable Equal where+ traverse f (Equal l r) = Equal <$> f l <*> f r++instance Applicative Equal where+ pure x = Equal x x+ (Equal fl fr) <*> (Equal l r) = Equal (fl l) (fr r)++-- | A matching problem.+data Match a = MatchWith { matchTerm :: a, matchPattern :: a }+ deriving (Eq, Show)++instance Functor Match where+ fmap f (MatchWith t p) = MatchWith (f t) (f p) ++instance Monoid a => Monoid (Match a) where+ mempty =+ MatchWith mempty mempty+ (MatchWith t1 p1) `mappend` (MatchWith t2 p2) = + MatchWith (t1 `mappend` t2) (p1 `mappend` p2)++instance Foldable Match where+ foldMap f (MatchWith t p) = f t `mappend` f p++instance Traversable Match where+ traverse f (MatchWith t p) = MatchWith <$> f t <*> f p++instance Applicative Match where+ pure x = MatchWith x x+ (MatchWith ft fp) <*> (MatchWith t p) = MatchWith (ft t) (fp p)+++-- | A rewrite rule.+data RRule a = RRule a a+ deriving (Show, Ord, Eq)++instance Functor RRule where+ fmap f (RRule lhs rhs) = RRule (f lhs) (f rhs) ++instance Monoid a => Monoid (RRule a) where+ mempty = RRule mempty mempty+ (RRule l1 r1) `mappend` (RRule l2 r2) = + RRule (l1 `mappend` l2) (r1 `mappend` r2)++instance Foldable RRule where+ foldMap f (RRule l r) = f l `mappend` f r++instance Traversable RRule where+ traverse f (RRule l r) = RRule <$> f l <*> f r++instance Applicative RRule where+ pure x = RRule x x+ (RRule fl fr) <*> (RRule l r) = RRule (fl l) (fr r)
src/Term/Rewriting/Norm.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE PatternGuards, FlexibleContexts #-}+{-# LANGUAGE PatternGuards, FlexibleContexts, ExplicitForAll #-}+{-# LANGUAGE ScopedTypeVariables, ViewPatterns #-}+ -- spurious warnings for view patterns -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt -- License : GPL v3 (see LICENSE)@@ -9,45 +11,128 @@ -- rewriting and an ad-hoc function that uses the @TermAC@ representation of -- terms modulo AC. module Term.Rewriting.Norm (- norm- , norm'- , nf+-- norm+ norm' , nf' , nfSubstVFresh' , normSubstVFresh'+ , maybeNotNfSubterms ) where import Term.Term import Term.LTerm-import Term.Rewriting.NormAC import Term.Substitution+import Term.Maude.Signature import Term.Maude.Process+import Term.SubtermRule+import Term.Unification +import Utils.Misc+ import Control.Basics import Control.Monad.Reader +import Data.List+import qualified Data.Set as S+ import System.IO.Unsafe (unsafePerformIO) -- Normalization using Maude ---------------------------------------------------------------------- --- | @norm t@ normalized the term @t@ using Maude.+-- | @norm t@ normalizes the term @t@ using Maude. norm :: (Show (Lit c LVar), Ord c, IsConst c)- => (c -> LSort) -> VTerm c LVar -> WithMaude (VTerm c LVar)-norm _ t@(Lit _) = return t-norm sortOf t = reader $ \hnd -> normAC $ unsafePerformIO $ normViaMaude hnd sortOf t+ => (c -> LSort) -> LTerm c -> WithMaude (LTerm c)+norm _ t@(viewTerm -> Lit _) = return t+norm sortOf t = reader $ \hnd -> unsafePerformIO $ normViaMaude hnd sortOf t +-- | @norm' t@ normalizes the term @t@ using Maude. norm' :: LNTerm -> WithMaude LNTerm norm' = norm sortOfName --- | @nf t@ returns @True@ if the term @t@ is in normal form.-nf :: (Show (Lit c LVar), Ord c, IsConst c)- => (c -> LSort) -> VTerm c LVar -> WithMaude Bool-nf sortOf t = (t ==#) <$> norm sortOf t +-- | @nfViaHaskell t@ returns @True@ if the term @t@ is in normal form.+nfViaHaskell :: LNTerm -> WithMaude Bool+nfViaHaskell t0 = reader $ \hnd -> check hnd+ where+ check hnd = go t0+ where+ go t = case viewTerm2 t of+ -- irreducible function symbols+ FAppNonAC o ts | o `S.member` irreducible -> all go ts+ FList ts -> all go ts+ FPair t1 t2 -> go t1 && go t2+ One -> True+ Empty -> True+ Zero -> True+ Lit2 _ -> True+ -- subterm rules+ FAppNonAC _ _ | setAny (struleApplicable t) strules -> False+ -- exponentiation+ FExp (viewTerm2 -> FExp _ _) _ | dh -> False+ FExp _ (viewTerm2 -> One) | dh -> False+ -- inverses+ FInv (viewTerm2 -> FInv _) | dh -> False+ FInv (viewTerm2 -> FMult ts) | dh && any isInverse ts -> False+ FInv (viewTerm2 -> One) | dh -> False+ -- multiplication+ FMult ts | fAppOne `elem` ts || any isProduct ts || invalidMult ts -> False+ -- xor+ FXor ts | fAppZero `elem` ts || any isXor ts || not (noDuplicates ts) -> False+ -- multiset union+ FUnion ts | fAppEmpty `elem` ts || any isUnion ts -> False++ -- topmost position not reducible, check subterms+ FExp t1 t2 -> go t1 && go t2+ FInv t1 -> go t1+ FMult ts -> all go ts+ FXor ts -> all go ts+ FUnion ts -> all go ts+ FAppNonAC _ ts -> all go ts++ struleApplicable t (StRule lhs rhs) =+ case matchLNTerm [t `MatchWith` lhs] `runReader` hnd of+ [] -> False+ _:_ -> case rhs of+ RhsPosition _ -> True+ RhsGround s -> not (t == s)+ -- reducible, but RHS might be already equal to t++ invalidMult ts = case partition isInverse ts of+ ([],_) -> False+ ([ viewTerm2 -> FInv (viewTerm2 -> FMult ifactors) ], factors) ->+ (ifactors \\ factors /= ifactors) || (factors \\ ifactors /= factors)+ ([ viewTerm2 -> FInv t ], factors) -> t `elem` factors+ (_:_:_, _) -> True+ _ -> False++ msig = mhMaudeSig hnd+ strules = stRules msig+ irreducible = irreducibleFunctionSymbols msig+ dh = enableDH msig+++-- | @nf' t@ returns @True@ if the term @t@ is in normal form. nf' :: LNTerm -> WithMaude Bool-nf' = nf sortOfName+nf' = nfViaHaskell +-- | @nfViaMaude t@ returns @True@ if the term @t@ is in normal form.+nfViaMaude :: (Show (Lit c LVar), Ord c, IsConst c)+ => (c -> LSort) -> LTerm c -> WithMaude Bool+nfViaMaude sortOf t = (t ==) <$> norm sortOf t+++-- | @nfCompare t@ performs normal-form checks using maude and the haskell function+-- and fails if the results differ.+_nfCompare' :: LNTerm -> WithMaude Bool+_nfCompare' t0 = reader $ \hnd ->+ case ((nfViaMaude sortOfName t0) `runReader` hnd, (nfViaHaskell t0) `runReader` hnd) of+ (x, y) | x == y -> x+ (x, y) ->+ error $ "nfCompare: Maude disagrees with haskell nf: "++ show t0+ ++" maude: " ++ show x ++ " haskell: "++show y++ -- Normalization ---------------------------------------------------- @@ -65,3 +150,11 @@ -- | @normSubst s@ normalizes the substitution @s@. normSubstVFresh' :: LNSubstVFresh -> WithMaude LNSubstVFresh normSubstVFresh' s = reader $ \hnd -> mapRangeVFresh (\t -> norm' t `runReader` hnd) s++-- | Returns all subterms that may be not in normal form.+maybeNotNfSubterms :: MaudeSig -> LNTerm -> [LNTerm]+maybeNotNfSubterms msig t0 = go t0+ where irreducible = irreducibleFunctionSymbols msig+ go (viewTerm -> Lit _) = []+ go (viewTerm -> FApp (NonAC o) as) | o `S.member` irreducible = concatMap go as+ go t = [t]
− src/Term/Rewriting/NormAC.hs
@@ -1,47 +0,0 @@-{-# LANGUAGE PatternGuards, FlexibleContexts #-}--- |--- Copyright : (c) 2010, 2011 Benedikt Schmidt--- License : GPL v3 (see LICENSE)--- --- Maintainer : Benedikt Schmidt <beschmi@gmail.com>------ This module implements normalization with respect to AC.-module Term.Rewriting.NormAC (- (==#)- , termFlatten- , normAC-) where--import Term.Term--import Data.List ( sort )---- Normalization modulo AC = flatten + sort--------------------------------------------------------------------------- | @termFlatten t@ converts a term @t@ to its flat representation, i.e.,--- AC-operator applications are replaced by n-ary, non-nested--- AC-operator applications.-termFlatten :: (Ord a) => Term a -> Term a-termFlatten t =- go t- where- go (Lit l) = Lit l- go (FApp (AC o) as) = FApp (AC o) (concatMap collectOTerms (map go as))- where- collectOTerms (FApp (AC o') ts) | o == o' = ts- collectOTerms a = [a]- go (FApp o as) = FApp o (map go as)---- | @normAC t@ normalizes the term @t@ wrt. to the equations AC,--- i.e., by flattening and sorting wrt. Ord.-normAC :: (Ord t) => Term t -> Term t-normAC = foldTerm Lit (\o -> FApp o . sortAC o) . termFlatten- where- sortAC (AC _) as = sort as- sortAC _ as = as---- | @a ==# b@ returns @True@ if @a@ is equal @b@ modulo AC.-(==#) :: (Ord a) => Term a -> Term a -> Bool-a ==# b = normAC a == normAC b-
src/Term/Substitution.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE TupleSections, TypeSynonymInstances, GADTs,FlexibleContexts,EmptyDataDecls,StandaloneDeriving, DeriveDataTypeable, FlexibleInstances, MultiParamTypeClasses, DeriveFunctor, ScopedTypeVariables #-}+{-# LANGUAGE TupleSections, TypeSynonymInstances, GADTs,FlexibleContexts,EmptyDataDecls #-}+{-# LANGUAGE StandaloneDeriving, DeriveDataTypeable, FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses, DeriveFunctor, ScopedTypeVariables #-} -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt -- License : GPL v3 (see LICENSE)@@ -14,6 +16,7 @@ -- ** Conversion between fresh and free , freshToFree , freshToFreeAvoiding+ , freshToFreeAvoidingFast , freeToFreshRaw @@ -30,10 +33,7 @@ import Extension.Prelude import Control.Monad.Bind--import Data.Traversable hiding (mapM)-import Control.Applicative-+import Control.Basics -- Composition of VFresh and VFresh substitutions ----------------------------------------------------------------------@@ -41,16 +41,17 @@ -- | @composeVFresh s1 s2@ composes the fresh substitution s1 and the free substitution s2. -- The result is the fresh substitution s = s1.s2. composeVFresh :: (IsConst c, Show (Lit c LVar))- => SubstVFresh c LVar -> Subst c LVar -> SubstVFresh c LVar+ => LSubstVFresh c -> LSubst c -> LSubstVFresh c composeVFresh s1_0 s2 =+ -- all variables in vrange(s1.s2) originate from s1 and can be considered fresh. freeToFreshRaw (s1 `compose` s2) where- s1 = freshToFreeAvoiding (extendWithRenaming (varsRange s2) s1_0) (s2,s1_0)+ s1 = freshToFreeAvoidingFast (extendWithRenaming (varsRange s2) s1_0) (s2,s1_0) -- Conversion between substitutions ---------------------------------------------------------------------- --- | @freshToFreeSimp s@ converts the bound variables in @s@ to free variables+-- | @freshToFree s@ converts the bound variables in @s@ to free variables -- using fresh variable names. We try to preserve variables names if possible. freshToFree :: (MonadFresh m, IsConst c) => SubstVFresh c LVar -> m (Subst c LVar)@@ -59,19 +60,30 @@ -- import oldvar ~> newvar mappings first, keep namehint from oldvar substFromList <$> mapM convertMapping slist where- convertMapping (lv,t) = (lv,) <$> traverse importLit t+ convertMapping (lv,t) = (lv,) <$> mapFrees (Arbitrary importVar) t where- importLit (Con c) = return (Con c)- importLit (Var v) =- Var <$> importBinding (\s i -> LVar s (lvarSort v) i) v (namehint v)- namehint v = case t of+ importVar v = importBinding (\s i -> LVar s (lvarSort v) i) v (namehint v)+ namehint v = case viewTerm t of Lit (Var _) -> lvarName lv -- keep name of oldvar _ -> lvarName v --- | @freshToFreeSimpAvoiding s t@ converts all fresh variables in the range of--- @s@ to free variables avoiding free variables in @t@.++-- | @freshToFreeAvoiding s t@ converts all fresh variables in the range of+-- @s@ to free variables avoiding free variables in @t@. This function tries+-- to reuse variable names from the domain of the substitution if possible. freshToFreeAvoiding :: (HasFrees t, IsConst c) => SubstVFresh c LVar -> t -> Subst c LVar freshToFreeAvoiding s t = freshToFree s `evalFreshAvoiding` t+++-- | @freshToFreeAvoidingFast s t@ converts all fresh variables in the range of+-- @s@ to free variables avoiding free variables in @t@. This function does+-- not try to reuse variable names from the domain of the substitution.+freshToFreeAvoidingFast :: (HasFrees t, Ord c) => LSubstVFresh c -> t -> LSubst c+freshToFreeAvoidingFast s t =+ substFromList . renameMappings . substToListVFresh $ s+ where+ renameMappings l = zip (map fst l) (rename (map snd l) `evalFreshAvoiding` t)+ -- | @freeToFreshRaw s@ considers all variables in the range of @s@ as fresh. freeToFreshRaw :: Subst c LVar -> SubstVFresh c LVar
src/Term/Substitution/SubstVFree.hs view
@@ -1,4 +1,8 @@-{-# LANGUAGE TupleSections, GeneralizedNewtypeDeriving, TypeSynonymInstances, GADTs,FlexibleContexts,EmptyDataDecls,StandaloneDeriving, DeriveDataTypeable, FlexibleInstances, MultiParamTypeClasses, DeriveFunctor, ScopedTypeVariables #-}+{-# LANGUAGE TupleSections, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ViewPatterns, TypeSynonymInstances, FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}+ -- spurious warnings for view patterns -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE)@@ -51,11 +55,11 @@ import Term.LTerm-import Term.Rewriting.NormAC+import Term.Rewriting.Definitions+-- import Term.Rewriting.NormAC import Text.PrettyPrint.Highlight import Logic.Connectives -import Extension.Prelude import Utils.Misc import Data.Maybe@@ -89,14 +93,18 @@ -- | @applyLit subst l@ applies the substitution @subst@ to the literal @l@. applyLit :: IsVar v => Subst c v -> Lit c v -> VTerm c v-applyLit subst v@(Var i) = fromMaybe (Lit v) $ M.lookup i (sMap subst)-applyLit _ c@(Con _) = Lit c+applyLit subst v@(Var i) = fromMaybe (lit v) $ M.lookup i (sMap subst)+applyLit _ c@(Con _) = lit c --- | @applyTermVFree subst t@ applies the substitution @subst@ to the term @t@.-applyVTerm :: (IsConst c, IsVar v) => Subst c v -> VTerm c v -> VTerm c v-applyVTerm subst = (>>= applyLit subst)+-- | @applyVTerm subst t@ applies the substitution @subst@ to the term @t@.+applyVTerm :: (IsConst c, IsVar v, Ord c) => Subst c v -> VTerm c v -> VTerm c v+applyVTerm subst t = case viewTerm t of+ Lit l -> applyLit subst l+ FApp (AC o) ts -> fAppAC o (map (applyVTerm subst) ts)+ FApp (NonAC o) ts -> fAppNonAC o (map (applyVTerm subst) ts)+ FApp List ts -> fAppList (map (applyVTerm subst) ts) -- Construction@@ -105,15 +113,17 @@ -- | Convert a list to a substitution. The @x/x@ mappings are removed. substFromList :: IsVar v => [(v, VTerm c v)] -> Subst c v substFromList xs =- Subst (M.fromList [ (v,t) | (v,t) <- xs, not (t `equalToVar` v) ])- where- equalToVar (Lit (Var v')) v = v == v'- equalToVar _ _ = False+ Subst (M.fromList [ (v,t) | (v,t) <- xs, not (equalToVar t v) ]) +-- | Returns @True@ if given term is equal to given variable.+equalToVar :: IsVar v => VTerm c v -> v -> Bool+equalToVar (viewTerm -> Lit (Var v')) v = v == v'+equalToVar _ _ = False+ -- | Convert a map to a substitution. The @x/x@ mappings are removed. -- FIXME: implement directly, use substFromMap for substFromList. substFromMap :: IsVar v => Map v (VTerm c v) -> Subst c v-substFromMap = substFromList . M.toList+substFromMap = Subst . M.filterWithKey (\v t -> not $ equalToVar t v) -- | @emptySubVFree@ is the substitution with empty domain. emptySubst :: Subst c v@@ -134,8 +144,7 @@ compose :: (IsConst c, IsVar v) => Subst c v -> Subst c v -> Subst c v compose s1 s2 =- Subst $- sMap (applySubst s1 s2) `M.union` sMap (restrict (dom s1 \\ dom s2) s1)+ Subst $ sMap (applySubst s1 s2) `M.union` sMap (restrict (dom s1 \\ dom s2) s1) -- Operations ----------------------------------------------------------------------@@ -151,8 +160,8 @@ mapRange f subst@(Subst _) = Subst $ M.mapMaybeWithKey (\i t -> filterRefl i (f t)) (sMap subst) where- filterRefl i (Lit (Var j)) | i == j = Nothing- filterRefl _ t = Just t+ filterRefl i (viewTerm -> Lit (Var j)) | i == j = Nothing+ filterRefl _ t = Just t -- Queries@@ -166,10 +175,9 @@ range :: Subst c v -> [VTerm c v] range = M.elems . sMap --- | @varsRange subst@ returns all variables in the range of the substitution--- FIXME: use Monoid, dlist, write occurs function.+-- | @varsRange subst@ returns all variables in the range of the substitution. varsRange :: IsVar v => Subst c v -> [v]-varsRange = sortednub . concatMap varsVTerm . range+varsRange = varsVTerm . fAppList . range -- Views ----------------------------------------------------------------------@@ -203,7 +211,7 @@ -- Instances ------------ -instance HasFrees (LSubst c) where+instance Ord c => HasFrees (LSubst c) where foldFrees f = foldFrees f . sMap mapFrees f = (substFromList <$>) . mapFrees f . substToList @@ -214,13 +222,13 @@ instance Apply LVar where apply subst x = maybe x extractVar $ imageOf subst x where- extractVar (Lit (Var x')) = x'+ extractVar (viewTerm -> Lit (Var x')) = x' extractVar t = error $ "apply (LVar): variable '" ++ show x ++ "' substituted with term '" ++ show t ++ "'" instance Apply LNTerm where- apply subst = normAC . applyVTerm subst+ apply subst = applyVTerm subst instance Apply () where apply _ = id@@ -230,6 +238,12 @@ instance Apply Int where apply _ = id++instance Apply Bool where+ apply _ = id++instance (Apply a, Apply b) => Apply (a, b) where+ apply subst (x,y) = (apply subst x, apply subst y) instance Apply a => Apply [a] where apply subst = fmap (apply subst)
src/Term/Substitution/SubstVFresh.hs view
@@ -58,20 +58,16 @@ import Term.LTerm-import Text.Isar (numbered') import Text.PrettyPrint.Highlight import Control.Applicative import Control.Monad.Fresh import Control.DeepSeq -import Extension.Prelude- import Logic.Connectives import Utils.Misc -import Data.Maybe import Data.Map ( Map ) import qualified Data.Map as M import qualified Data.Set as S@@ -128,12 +124,12 @@ -- | @extendWithRenaming vs s@ extends the substitution @s@ with renamings (with -- fresh variables) for the variables in @vs@ that are not already in @dom s@.-extendWithRenaming :: Show (Lit c LVar)+extendWithRenaming :: (Ord c, Show (Lit c LVar)) => [LVar] -> SubstVFresh c LVar -> SubstVFresh c LVar extendWithRenaming vs0 s = substFromListVFresh $ substToListVFresh s ++ substToListVFresh (renameFreshAvoiding s2 (varsRangeVFresh s))- where s2 = substFromListVFresh [(v, Lit (Var v)) | v <- vs ]+ where s2 = substFromListVFresh [(v, lit (Var v)) | v <- vs ] vs = vs0 \\ domVFresh s @@ -149,17 +145,16 @@ rangeVFresh = M.elems . svMap -- | @varsRangeVFresh subst@ returns all variables in the range of the substitution--- FIXME: use Monoid, dlist, write occurs function. varsRangeVFresh :: IsVar v => SubstVFresh c v -> [v]-varsRangeVFresh = sortednub . concatMap varsVTerm . rangeVFresh+varsRangeVFresh = varsVTerm . fAppList . rangeVFresh -- | Returns @True@ if the given variable in the domain of the -- substitution is just renamed by the substitution. isRenamedVar :: LVar -> LSubstVFresh c -> Bool isRenamedVar lv subst =- case imageOfVFresh subst lv of+ case viewTerm <$> imageOfVFresh subst lv of Just (Lit (Var lv')) | lvarSort lv == lvarSort lv' ->- lv' `notElem` (concatMap varsVTerm $ [ t | (v,t) <- substToListVFresh subst, v /= lv ])+ lv' `notElem` (varsVTerm . fAppList $ [ t | (v,t) <- substToListVFresh subst, v /= lv ]) _ -> False -- | Returns @True@ if the substitution is a renaming.@@ -183,13 +178,13 @@ -- | @renameFresh s@ renames the fresh variables in @s@ using fresh variables. -- This function can be used to prevent overshadowing which might -- make output hard to read.-renameFresh :: MonadFresh m => SubstVFresh c LVar -> m (SubstVFresh c LVar)+renameFresh :: (Ord c, MonadFresh m) => SubstVFresh c LVar -> m (SubstVFresh c LVar) renameFresh subst = substFromListVFresh . zip (map fst slist) <$> rename (map snd slist) where slist = substToListVFresh subst -- | @renameFreshAvoiding s t@ renames the fresh variables in the range of @s@ away from -- variables that are free in @t@. This is an internal function.-renameFreshAvoiding :: HasFrees t => LSubstVFresh c -> t -> SubstVFresh c LVar+renameFreshAvoiding :: (Ord c, HasFrees t) => LSubstVFresh c -> t -> SubstVFresh c LVar renameFreshAvoiding s t = renameFresh s `evalFreshAvoiding` t -- | @removeRenamings s@ removes all renamings (see 'isRenamedVar') from @s@.@@ -242,4 +237,4 @@ where ppConj = vcat . map prettyEq . substToListVFresh prettyEq (a,b) = - prettyNTerm (Lit (Var a)) $$ nest (6::Int) (text "=" <-> prettyNTerm b)+ prettyNTerm (lit (Var a)) $$ nest (6::Int) (text "=" <-> prettyNTerm b)
src/Term/Subsumption.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE GADTs, FlexibleContexts #-}+{-# LANGUAGE GADTs, FlexibleContexts, ViewPatterns #-}+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}+ -- spurious warnings for view patterns -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt -- License : GPL v3 (see LICENSE)@@ -24,15 +26,11 @@ import Term.Term import Term.LTerm import Term.Unification-import Term.Rewriting.NormAC import Term.Positions import Extension.Prelude -- import Utils.Misc -import Data.List-import Data.Ord-import Data.Maybe import Control.Basics ----------------------------------------------------------------------@@ -90,7 +88,7 @@ -- | Returns a substitution that is equivalent modulo renaming to the given substitution. canonizeSubst :: LNSubstVFresh -> LNSubstVFresh canonizeSubst subst =- mapRangeVFresh (normAC . applyVTerm renaming) subst+ mapRangeVFresh (applyVTerm renaming) subst where vrangeSorted = sortOn (varOccurences subst) (varsRangeVFresh subst) renaming = substFromList $@@ -102,11 +100,11 @@ -- terms that are equal modulo AC since the flattened term representation -- is used. varOccurences :: LNSubstVFresh -> LVar -> [[Position]]-varOccurences subst v = map (sort . go [] . normAC) $ rangeVFresh subst+varOccurences subst v = map (go []) $ rangeVFresh subst where- go pos (Lit (Var v')) | v == v' = [pos]+ go pos (viewTerm -> Lit (Var v')) | v == v' = [pos] | otherwise = []- go _ (Lit (Con _)) = []- go pos (FApp (AC _) as) = concatMap (go (0:pos)) as- go pos (FApp _ as) =+ go _ (viewTerm -> Lit (Con _)) = []+ go pos (viewTerm -> FApp (AC _) as) = concatMap (go (0:pos)) as+ go pos (viewTerm -> FApp _ as) = concat (zipWith (\i -> go (i:pos)) [0 .. ] as)
src/Term/SubtermRule.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-}+{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable, ViewPatterns #-}+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}+ -- spurious warnings for view patterns -- | -- Copyright : (c) 2011, 2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE)@@ -14,6 +16,7 @@ -- * Pretty Printing , prettyStRule+ , module Term.Rewriting.Definitions ) where import Control.DeepSeq@@ -23,6 +26,7 @@ import Term.LTerm import Term.Positions+import Term.Rewriting.Definitions import Text.PrettyPrint.Highlight -- | The righthand-side of a subterm rewrite rule.@@ -44,15 +48,15 @@ [] -> Nothing where findSubterm t rpos | t == rhs = [rpos]- findSubterm (FApp _ args) rpos =+ findSubterm (viewTerm -> FApp _ args) rpos = concat $ zipWith (\t i -> findSubterm t (i:rpos)) args [0..]- findSubterm (Lit _) _ = []+ findSubterm (viewTerm -> Lit _) _ = [] -- | Convert a subterm rewrite rule to a rewrite rule. stRuleToRRule :: StRule -> RRule LNTerm stRuleToRRule (StRule lhs rhs) = case rhs of RhsGround t -> lhs `RRule` t- RhsPosition p -> lhs `RRule` (lhs >* p)+ RhsPosition p -> lhs `RRule` (lhs `atPos` p) {-
src/Term/Term.hs view
@@ -1,4 +1,8 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE TemplateHaskell, FlexibleInstances #-}+{-# LANGUAGE DeriveDataTypeable, ViewPatterns #-}+{-# LANGUAGE OverloadedStrings #-}+ -- for ByteString -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE)@@ -11,73 +15,86 @@ FunSym(..) , ACSym(..) , NonACSym- , expSym- , pairSym- , invSym- , oneSym- , emptySym- , zeroSym , FunSig-+ , dhFunSig+ , xorFunSig+ , msetFunSig+ , pairFunSig+ , dhReducibleFunSig+ , implicitFunSig -- * Terms- , Term (..)+ , Term+ , TermView (..)+ , viewTerm+ , TermView2 (..)+ , viewTerm2 - , foldTerm+ , traverseTerm+ , fmapTerm+ , bindTerm , lits , prettyTerm -- ** Smart constructors- , listToTerm+ , lit+ , fApp+ , fAppAC+ , fAppNonAC+ , fAppList+ , unsafefApp - -- ** Destrutors- , destPair- , destInv- - -- * Terms with constants and variables- , Lit(..)- , VTerm+ , fAppMult+ , fAppOne+ , fAppExp+ , fAppInv+ , fAppXor+ , fAppZero+ , fAppUnion+ , fAppEmpty+ , fAppPair+ , fAppFst+ , fAppSnd - , varTerm- , constTerm- , varsVTerm- , occursVTerm- , constsVTerm- , isVar - , IsVar- , IsConst-- -- * Equalities- , Equal (..)- , evalEqual-- -- * Matching Problems- , Match(..)+ -- ** Destructors and classifiers+ , destPair+ , destInverse+ , destProduct+ , destXor+ , destUnion - -- * Rewriting Rules- , RRule(..)+ , isPair+ , isInverse+ , isProduct+ , isXor+ , isUnion , module Term.Classes ) where import Data.List-import qualified Data.DList as D import Data.Monoid import Data.Foldable (Foldable, foldMap)-import Data.Traversable +import Data.Traversable import Data.Typeable import Data.Generics import Data.DeriveTH import Data.Binary+import Data.Maybe (isJust) import Control.DeepSeq import Control.Basics -import Extension.Prelude+import Data.ByteString (ByteString)+import qualified Data.ByteString.Char8 as BC+import Extension.Data.ByteString () -import Text.Isar+import Data.Set (Set)+import qualified Data.Set as S +import Text.PrettyPrint.Class+ import Term.Classes ----------------------------------------------------------------------@@ -85,11 +102,11 @@ ---------------------------------------------------------------------- -- | AC function symbols.-data ACSym = MUn | Xor | Mult+data ACSym = Union | Xor | Mult deriving (Eq, Ord, Typeable, Data, Show) -- | non-AC function symbols-type NonACSym = (String, Int)+type NonACSym = (ByteString, Int) -- | Function symbols data FunSym = NonAC NonACSym -- ^ a non-AC function function symbol of a given arity@@ -98,11 +115,11 @@ deriving (Eq, Ord, Typeable, Data, Show) -- | Function signatures.-type FunSig = [NonACSym]+type FunSig = Set NonACSym -pairSym, expSym, invSym, oneSym, zeroSym, emptySym :: NonACSym+pairSym, expSym, invSym, oneSym, zeroSym, emptySym, fstSym, sndSym :: NonACSym -- | Pairing. pairSym = ("pair",2) -- | Exponentiation.@@ -115,245 +132,251 @@ zeroSym = ("zero",0) -- | The empty multiset. emptySym = ("empty",0)---- | Destruct a top-level function application.-{-# INLINE destFunApp #-}-destFunApp :: FunSym -> Term a -> Maybe [Term a]-destFunApp fsym (FApp fsym' args) | fsym == fsym' = Just args-destFunApp _ _ = Nothing---- | Destruct a top-level pair.-destPair :: Term a -> Maybe (Term a, Term a)-destPair t = do [t1, t2] <- destFunApp (NonAC pairSym) t; return (t1, t2)---- | Destruct a top-level inverse in the group of exponents.-destInv :: Term a -> Maybe (Term a)-destInv t = do [t1] <- destFunApp (NonAC invSym) t; return t1--------------------------------------------------------------------------- Terms--------------------------------------------------------------------------- | A term in T(Sigma,a).-data Term a = Lit a -- ^ atomic terms (constants, variables, ..)- | FApp FunSym [Term a] -- ^ function applications- deriving (Eq, Ord, Typeable, Data )----- Instances---------------instance Functor Term where- {-# INLINE fmap #-}- fmap f = foldTerm (Lit . f) FApp--instance Foldable Term where- {-# INLINE foldMap #-}- foldMap f = foldTerm f (const mconcat)--instance Traversable Term where- {-# INLINE traverse #-}- traverse f (Lit x) = Lit <$> f x- traverse f (FApp fsym as) = FApp fsym <$> traverse (traverse f) as--instance Applicative Term where- {-# INLINE pure #-}- pure = Lit- {-# INLINE (<*>) #-}- f <*> a = a >>= (\x -> fmap ($ x) f)--instance Monad Term where- {-# INLINE return #-}- return = Lit- {-# INLINE (>>=) #-}- m >>= f = foldTerm f FApp m--instance Show a => Show (Term a) where- show (Lit l) = show l- show (FApp (NonAC (s,_)) []) = s- show (FApp (NonAC (s,_)) as) = s++"("++(intercalate "," (map show as))++")"- show (FApp List as) = "LIST"++"("++(intercalate "," (map show as))++")"- show (FApp (AC o) as) = show o++"("++(intercalate "," (map show as))++")"+-- | Projection of first component of pair. Only required for pairFunSig.+fstSym = ("fst",1)+-- | Projection of second component of pair. Only required for pairFunSig.+sndSym = ("snd",1) +-- | The signature for the non-AC Diffie-Hellman function symbols.+dhFunSig :: FunSig+dhFunSig = S.fromList [ expSym, oneSym, invSym ] --- | The fold function for @Term a@.-{-# INLINE foldTerm #-}-foldTerm :: (t -> b) -> (FunSym -> [b] -> b)- -> Term t -> b-foldTerm fLit fApp t = go t- where go (Lit a) = fLit a- go (FApp fsym a) = fApp fsym $ map go a+-- | The signature for the non-AC Xor function symbols.+xorFunSig :: FunSig+xorFunSig = S.fromList [ zeroSym ] +-- | The signature for then non-AC multiset function symbols.+msetFunSig :: FunSig+msetFunSig = S.fromList [ emptySym ] -instance Sized a => Sized (Term a) where- size = foldTerm size (const $ \xs -> sum xs + 1)+-- | The signature for pairing.+pairFunSig :: FunSig+pairFunSig = S.fromList [ pairSym, fstSym, sndSym ] --- | @lits t@ returns all literals that occur in term @t@. List can contain duplicates.-lits :: Ord a => Term a -> [a]-lits = foldMap return+-- | Reducible non-AC symbols for DH.+dhReducibleFunSig :: FunSig+dhReducibleFunSig = S.fromList [ expSym, invSym ] --- | @listToTerm ts@ returns a term that represents @ts@.-listToTerm :: [Term a] -> Term a-listToTerm ts = FApp List ts+-- | Implicit non-AC symbols.+implicitFunSig :: FunSig+implicitFunSig = S.fromList [ invSym, pairSym ] ------------------------------------------------------------------------- Terms with constants and variables+-- Terms ---------------------------------------------------------------------- +-- | A term in T(Sigma,a). Its constructors are kept abstract. Use 'viewTerm'+-- or 'viewTerm2' to inspect it.+data Term a = LIT a -- ^ atomic terms (constants, variables, ..)+ | FAPP FunSym [Term a] -- ^ function applications+ deriving (Eq, Ord, Typeable, Data ) --- | A Lit is either a constant or a variable. (@Const@ is taken by Control.Applicative)-data Lit c v = Con c | Var v- deriving (Eq, Ord, Data, Typeable)+-- | Destruct a top-level function application.+{-# INLINE destFunApp #-}+destFunApp :: FunSym -> Term a -> Maybe [Term a]+destFunApp fsym (FAPP fsym' args) | fsym == fsym' = Just args+destFunApp _ _ = Nothing --- | A VTerm is a term with constants and variables-type VTerm c v = Term (Lit c v)+-- | Destruct a top-level pair.+destPair :: Term a -> Maybe (Term a, Term a)+destPair t = do [t1, t2] <- destFunApp (NonAC pairSym) t; return (t1, t2) --- | collect class constraints for variables-class (Ord v, Eq v, Show v) => IsVar v where+-- | Destruct a top-level inverse in the group of exponents.+destInverse :: Term a -> Maybe (Term a)+destInverse t = do [t1] <- destFunApp (NonAC invSym) t; return t1 --- | collect class constraints for constants-class (Ord c, Eq c, Show c, Data c) => IsConst c where+-- | Destruct a top-level product.+destProduct :: Term a -> Maybe [Term a]+destProduct (FAPP (AC Mult) ts) = return ts+destProduct _ = Nothing --- | Functor instance in the variable.-instance Functor (Lit c) where- fmap f (Var v) = Var (f v)- fmap _ (Con c) = Con c+-- | Destruct a top-level product.+destXor :: Term a -> Maybe [Term a]+destXor (FAPP (AC Xor) ts) = return ts+destXor _ = Nothing --- | Foldable instance in the variable.-instance Foldable (Lit c) where- foldMap f (Var v) = f v- foldMap _ (Con _) = mempty+-- | Destruct a top-level multiset union.+destUnion :: Term a -> Maybe [Term a]+destUnion (FAPP (AC Union) ts) = return ts+destUnion _ = Nothing --- | Traversable instance in the variable.-instance Traversable (Lit c) where- sequenceA (Var v) = Var <$> v- sequenceA (Con n) = pure $ Con n+-- | 'True' iff the term is a well-formed pair.+isPair :: Term a -> Bool+isPair = isJust . destPair --- | Applicative instance in the variable.-instance Applicative (Lit c) where- pure = Var- (Var f) <*> (Var x) = Var (f x)- (Var _) <*> (Con n) = Con n- (Con n) <*> _ = Con n+-- | 'True' iff the term is a well-formed inverse.+isInverse :: Term a -> Bool+isInverse = isJust . destInverse --- | Monad instance in the variable-instance Monad (Lit c) where- return = Var- (Var x) >>= f = f x- (Con n) >>= _ = Con n+-- | 'True' iff the term is a well-formed product.+isProduct :: Term a -> Bool+isProduct = isJust . destProduct -instance Sized (Lit c v) where- size _ = 1+-- | 'True' iff the term is a well-formed xor'ing.+isXor :: Term a -> Bool+isXor = isJust . destXor -instance (Show v, Show c) => Show (Lit c v) where- show (Var x) = show x- show (Con n) = show n+-- | 'True' iff the term is a well-formed xor'ing.+isUnion :: Term a -> Bool+isUnion = isJust . destXor --- | @varTerm v@ is the 'VTerm' with the variable @v@.-varTerm :: v -> VTerm c v-varTerm = Lit . Var +-- | View on terms that corresponds to representation.+data TermView a = Lit a+ | FApp FunSym [Term a]+ deriving (Show, Eq, Ord) --- | @constTerm c@ is the 'VTerm' with the const @c@.-constTerm :: c -> VTerm c v-constTerm = Lit . Con+{-# INLINE viewTerm #-}+-- | Return the 'TermView' of the given term.+viewTerm :: Term a -> TermView a+viewTerm (LIT l) = Lit l+viewTerm (FAPP sym ts) = FApp sym ts --- | @isVar t returns @True@ if @t@ is a variable.-isVar :: VTerm c v -> Bool-isVar (Lit (Var _)) = True-isVar _ = False+-- | @fApp fsym as@ creates an application of @fsym@ to @as@. The function+-- ensures that the resulting term is in AC-normal-form.+{-# INLINE fApp #-}+fApp :: Ord a => FunSym -> [Term a] -> Term a+fApp (AC acSym) ts = fAppAC acSym ts+fApp o ts = FAPP o ts --- | @vars t@ returns a duplicate-free list of variables that occur in @t@.-varsVTerm :: (Eq v, Ord v) => VTerm c v -> [v]-varsVTerm = sortednub . D.toList . foldMap (foldMap return)+-- | Smart constructor for AC terms.+fAppAC :: Ord a => ACSym -> [Term a] -> Term a+fAppAC _ [] = error "Term.fAppAC: empty argument list"+fAppAC _ [a] = a+fAppAC acsym as =+ FAPP (AC acsym) (sort (o_as ++ non_o_as))+ where+ o = AC acsym+ isOTerm (FAPP o' _) | o' == o = True+ isOTerm _ = False+ (o_as0, non_o_as) = partition isOTerm as+ o_as = [ a | FAPP _ ts <- o_as0, a <- ts ] --- | @occurs v t@ returns @True@ if @v@ occurs in @t@-occursVTerm :: Eq v => v -> VTerm c v -> Bool-occursVTerm v = getAny . foldMap (foldMap (Any . (v==)))+-- | Smart constructor for non-AC terms.+{-# INLINE fAppNonAC #-}+fAppNonAC :: NonACSym -> [Term a] -> Term a+fAppNonAC nacsym = FAPP (NonAC nacsym) --- | @constsVTerm t@ returns a duplicate-free list of constants that occur in @t@.-constsVTerm :: IsConst c => VTerm c v -> [c]-constsVTerm = sortednub . D.toList . foldMap fLit- where fLit (Var _) = mempty- fLit (Con n) = return n+-- | Smart constructor for list terms.+{-# INLINE fAppList #-}+fAppList :: [Term a] -> Term a+fAppList = FAPP List -------------------------------------------------------------------------- Equalities, matching problems, and rewriting rules-----------------------------------------------------------------------+-- | @lit l@ creates a term from the literal @l@.+{-# INLINE lit #-}+lit :: a -> Term a+lit l = LIT l --- | An equality.-data Equal a = Equal { eqLHS :: a, eqRHS :: a }- deriving (Eq, Show)+-- | @unsafefApp fsym as@ creates an application of @fsym@ to as. The+-- caller has to ensure that the resulting term is in AC-normal-form.+unsafefApp :: FunSym -> [Term a] -> Term a+unsafefApp fsym as = FAPP fsym as --- | True iff the two sides of the equality are equal with respect to their--- 'Eq' instance.-evalEqual :: Eq a => Equal a -> Bool-evalEqual (Equal l r) = l == r -instance Functor Equal where- fmap f (Equal lhs rhs) = Equal (f lhs) (f rhs) +-- | View on terms that distinguishes function application of builtin symbols like exp.+data TermView2 a = FExp (Term a) (Term a) | FInv (Term a) | FMult [Term a] | One+ | FXor [Term a] | Zero+ | FUnion [Term a] | Empty+ | FPair (Term a) (Term a)+ | FAppNonAC NonACSym [Term a]+ | FList [Term a]+ | Lit2 a+ deriving (Show, Eq, Ord) -instance Monoid a => Monoid (Equal a) where- mempty = Equal mempty mempty- (Equal l1 r1) `mappend` (Equal l2 r2) = - Equal (l1 `mappend` l2) (r1 `mappend` r2)+-- | Returns the 'TermView2' of the given term.+viewTerm2 :: Show a => Term a -> TermView2 a+viewTerm2 (LIT l) = Lit2 l+viewTerm2 (FAPP List ts) = FList ts+viewTerm2 t@(FAPP (AC o) ts)+ | length ts < 2 = error $ "viewTerm2: malformed term `"++show t++"'"+ | otherwise = (acSymToConstr o) ts+ where+ acSymToConstr Mult = FMult+ acSymToConstr Xor = FXor+ acSymToConstr Union = FUnion+viewTerm2 t@(FAPP (NonAC o) ts) = case ts of+ [ t1, t2 ] | o == expSym -> FExp t1 t2+ [ t1, t2 ] | o == pairSym -> FPair t1 t2+ [ t1 ] | o == invSym -> FInv t1+ [] | o == oneSym -> One+ [] | o == zeroSym -> Zero+ [] | o == emptySym -> Empty+ _ | o `elem` ssyms -> error $ "viewTerm2: malformed term `"++show t++"'"+ _ -> FAppNonAC o ts+ where+ -- special symbols+ ssyms = [ expSym, pairSym, invSym, oneSym, zeroSym, emptySym ] -instance Foldable Equal where- foldMap f (Equal l r) = f l `mappend` f r -instance Traversable Equal where- traverse f (Equal l r) = Equal <$> f l <*> f r+-- | Smart constructors for mult, union, and xor.+fAppMult, fAppUnion, fAppXor :: Ord a => [Term a] -> Term a+fAppMult ts = fApp (AC Mult) ts+fAppUnion ts = fApp (AC Union) ts+fAppXor ts = fApp (AC Xor) ts -instance Applicative Equal where- pure x = Equal x x- (Equal fl fr) <*> (Equal l r) = Equal (fl l) (fr r)+-- | Smart constructors for one, zero, and empty.+fAppOne, fAppZero, fAppEmpty :: Term a+fAppOne = fAppNonAC oneSym []+fAppZero = fAppNonAC zeroSym []+fAppEmpty = fAppNonAC emptySym [] --- | A matching problem.-data Match a = MatchWith { matchTerm :: a, matchPattern :: a }- deriving (Eq, Show)+-- | Smart constructors for pair and exp.+fAppPair, fAppExp :: (Term a, Term a) -> Term a+fAppPair (x,y) = fAppNonAC pairSym [x, y]+fAppExp (b,e) = fAppNonAC expSym [b, e] -instance Functor Match where- fmap f (MatchWith t p) = MatchWith (f t) (f p) +-- | Smart constructors for inv, fst, and snd.+fAppInv, fAppFst, fAppSnd :: Term a -> Term a+fAppInv e = fAppNonAC invSym [e]+fAppFst a = fAppNonAC fstSym [a]+fAppSnd a = fAppNonAC sndSym [a] -instance Monoid a => Monoid (Match a) where- mempty =- MatchWith mempty mempty- (MatchWith t1 p1) `mappend` (MatchWith t2 p2) = - MatchWith (t1 `mappend` t2) (p1 `mappend` p2) -instance Foldable Match where- foldMap f (MatchWith t p) = f t `mappend` f p+-- Instances+------------ -instance Traversable Match where- traverse f (MatchWith t p) = MatchWith <$> f t <*> f p+{-# INLINE traverseTerm #-}+traverseTerm :: (Applicative f, Ord a, Ord b) => (a -> f b) -> Term a -> f (Term b)+traverseTerm f (LIT x) = LIT <$> f x+traverseTerm f (FAPP fsym as) = fApp fsym <$> traverse (traverseTerm f) as -instance Applicative Match where- pure x = MatchWith x x- (MatchWith ft fp) <*> (MatchWith t p) = MatchWith (ft t) (fp p)+{-# INLINE fmapTerm #-}+fmapTerm :: (Ord a, Ord b) => (a -> b) -> Term a -> Term b+fmapTerm f = foldTerm (lit . f) fApp +{-# INLINE bindTerm #-}+bindTerm :: (Ord a, Ord b) => Term a -> (a -> Term b) -> Term b+bindTerm m f = foldTerm f fApp m --- | A rewrite rule.-data RRule a = RRule a a- deriving (Show, Ord, Eq)+instance Foldable Term where+ {-# INLINE foldMap #-}+ foldMap f = foldTerm f (const mconcat) -instance Functor RRule where- fmap f (RRule lhs rhs) = RRule (f lhs) (f rhs) +instance Show a => Show (Term a) where+ show (LIT l) = show l+ show (FAPP (NonAC (s,_)) []) = BC.unpack s+ show (FAPP (NonAC (s,_)) as) = BC.unpack s++"("++(intercalate "," (map show as))++")"+ show (FAPP List as) = "LIST"++"("++(intercalate "," (map show as))++")"+ show (FAPP (AC o) as) = show o++"("++(intercalate "," (map show as))++")" -instance Monoid a => Monoid (RRule a) where- mempty = RRule mempty mempty- (RRule l1 r1) `mappend` (RRule l2 r2) = - RRule (l1 `mappend` l2) (r1 `mappend` r2) -instance Foldable RRule where- foldMap f (RRule l r) = f l `mappend` f r -instance Traversable RRule where- traverse f (RRule l r) = RRule <$> f l <*> f r+-- | The fold function for @Term a@.+{-# INLINE foldTerm #-}+foldTerm :: (t -> b) -> (FunSym -> [b] -> b)+ -> Term t -> b+foldTerm fLIT fFAPP t = go t+ where go (LIT a) = fLIT a+ go (FAPP fsym a) = fFAPP fsym $ map go a -instance Applicative RRule where- pure x = RRule x x- (RRule fl fr) <*> (RRule l r) = RRule (fl l) (fr r) +instance Sized a => Sized (Term a) where+ size = foldTerm size (const $ \xs -> sum xs + 1)++-- | @lits t@ returns all literals that occur in term @t@. List can contain duplicates.+lits :: Ord a => Term a -> [a]+lits = foldMap return+ ---------------------------------------------------------------------- -- Pretty printing ----------------------------------------------------------------------@@ -363,26 +386,26 @@ prettyTerm ppLit = ppTerm where ppTerm t = case t of- Lit l -> ppLit l- FApp (AC o) ts -> ppTerms (ppACOp o) 1 "(" ")" ts- FApp (NonAC ("exp",2)) [t1,t2] -> ppTerm t1 <> text "^" <> ppTerm t2- FApp (NonAC ("pair",2)) _ -> ppTerms ", " 1 "<" ">" (split t)- FApp (NonAC (f,_)) ts -> ppFun f ts- FApp List ts -> ppFun "LIST" ts+ LIT l -> ppLit l+ FAPP (AC o) ts -> ppTerms (ppACOp o) 1 "(" ")" ts+ FAPP (NonAC ("exp",2)) [t1,t2] -> ppTerm t1 <> text "^" <> ppTerm t2+ FAPP (NonAC ("pair",2)) _ -> ppTerms ", " 1 "<" ">" (split t)+ FAPP (NonAC (f,_)) ts -> ppFun f ts+ FAPP List ts -> ppFun "LIST" ts - ppACOp Mult = "*"- ppACOp MUn = "#"- ppACOp Xor = "+"+ ppACOp Mult = "*"+ ppACOp Union = "#"+ ppACOp Xor = "+" ppTerms sepa n lead finish ts = fcat . (text lead :) . (++[text finish]) . map (nest n) . punctuate (text sepa) . map ppTerm $ ts - split (FApp (NonAC ("pair",2)) [t1,t2]) = t1 : split t2+ split (FAPP (NonAC ("pair",2)) [t1,t2]) = t1 : split t2 split t = [t] ppFun f ts =- text (f ++"(") <> fsep (punctuate comma (map ppTerm ts)) <> text ")"+ text (BC.unpack f ++"(") <> fsep (punctuate comma (map ppTerm ts)) <> text ")" -- Derived instances --------------------@@ -390,11 +413,7 @@ $( derive makeNFData ''FunSym) $( derive makeNFData ''ACSym) $( derive makeNFData ''Term )-$( derive makeNFData ''Lit) $( derive makeBinary ''FunSym) $( derive makeBinary ''ACSym) $( derive makeBinary ''Term )-$( derive makeBinary ''Lit)--
src/Term/Unification.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE FlexibleContexts, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FlexibleContexts, GeneralizedNewtypeDeriving, ViewPatterns #-} -- | -- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE)@@ -27,8 +27,10 @@ , mhFilePath -- * Maude signatures- , MaudeSig(..)- , emptyMaudeSig+ , MaudeSig+ , enableDH+ , enableXor+ , enableMSet , minimalMaudeSig , dhMaudeSig , xorMaudeSig@@ -38,13 +40,16 @@ , asymEncMaudeSig , signatureMaudeSig , hashMaudeSig- , allMaudeSig , rrulesForMaudeSig- , funSigForMaudeSig-+ , allFunctionSymbols+ , stRules+ , irreducibleFunctionSymbols+ , addFunctionSymbol+ , addStRule -- * Convenience exports , module Term.Substitution+ , module Term.Rewriting.Definitions ) where import Control.Applicative@@ -52,23 +57,17 @@ import Control.Monad.Reader import Control.Monad.Error import Control.Monad.State-import Data.List import qualified Data.Map as M import Data.Map (Map) import System.IO.Unsafe (unsafePerformIO) -import Term.Rewriting.NormAC ( (==#) )+import Term.Rewriting.Definitions import Term.Substitution import qualified Term.Maude.Process as UM import Term.Maude.Process (MaudeHandle, WithMaude, startMaude, getMaudeStats, mhMaudeSig, mhFilePath)-import Term.Maude.Types- (MaudeSig(..), emptyMaudeSig, allMaudeSig, rrulesForMaudeSig,- funSigForMaudeSig, dhMaudeSig, xorMaudeSig, msetMaudeSig,- pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig,- hashMaudeSig, minimalMaudeSig)-+import Term.Maude.Signature import Debug.Trace.Ignore -- import qualified Debug.Trace as DT @@ -151,7 +150,7 @@ l <- gets ((`applyVTerm` l0) . substFromMap) r <- gets ((`applyVTerm` r0) . substFromMap) guard (trace (show ("unifyRaw", mappings, l ,r)) True)- case (l, r) of+ case (viewTerm l, viewTerm r) of (Lit (Var vl), Lit (Var vr)) | vl == vr -> return () | otherwise -> case (lvarSort vl, lvarSort vr) of@@ -160,7 +159,7 @@ _ | sortGeqLTerm sortOf vl r -> elim vl r -- If unification can succeed here, then it must work by -- elimating the right-hand variable with the left-hand side.- _ -> elim vr l+ _ -> elim vr l (Lit (Var vl), _ ) -> elim vl r (_, Lit (Var vr) ) -> elim vr l@@ -202,23 +201,23 @@ mappings <- get guard (trace (show (mappings,t,p)) True) case (t, p) of- (_, Lit (Var vp)) ->+ (_, viewTerm -> Lit (Var vp)) -> case M.lookup vp mappings of Nothing -> do unless (sortGeqLTerm sortOf vp t) $ throwError NoMatch modify (M.insert vp t)- Just tp | t ==# tp -> return ()+ Just tp | t == tp -> return () | otherwise -> throwError NoMatch - (Lit (Con ct), Lit (Con cp)) -> guard (ct == cp)- (FApp (NonAC tfsym) targs, FApp (NonAC pfsym) pargs) ->+ (viewTerm -> Lit (Con ct), viewTerm -> Lit (Con cp)) -> guard (ct == cp)+ (viewTerm -> FApp (NonAC tfsym) targs, viewTerm -> FApp (NonAC pfsym) pargs) -> guard (tfsym == pfsym && length targs == length pargs) >> sequence_ (zipWith (matchRaw sortOf) targs pargs)- (FApp List targs, FApp List pargs) ->+ (viewTerm -> FApp List targs, viewTerm -> FApp List pargs) -> guard (length targs == length pargs) >> sequence_ (zipWith (matchRaw sortOf) targs pargs)- (FApp (AC _) _, FApp (AC _) _) -> throwError ACProblem+ (viewTerm -> FApp (AC _) _, viewTerm -> FApp (AC _) _) -> throwError ACProblem -- all matchable pairs of term constructors have been enumerated _ -> throwError NoMatch
+ src/Term/UnitTests.hs view
@@ -0,0 +1,376 @@+{-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-}+{-# OPTIONS_GHC -fno-warn-unused-binds #-}+-- |+-- Copyright : (c) 2012 Benedikt Schmidt+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>+--+-- Unit tests for the functions dealing with term algebra and related notions.+module Term.UnitTests (main) where++import Term.Substitution+import Term.Subsumption+import Term.Builtin.Convenience+import Term.Unification+import Term.Rewriting.Norm+import Term.Narrowing.Variants+import Term.Positions++import Text.PrettyPrint.Class++import Data.List+import Data.Maybe+import Prelude hiding ( catch )+import Test.HUnit+import Control.Monad.Reader+import Data.Monoid+++testEqual :: (Eq a, Show a) => String -> a -> a -> Test+testEqual t a b = TestLabel t $ TestCase $ assertEqual t b a++testTrue :: String -> Bool -> Test+testTrue t a = TestLabel t $ TestCase $ assertBool t a++-- *****************************************************************************+-- Tests for Matching+-- *****************************************************************************++testsMatching :: MaudeHandle -> Test+testsMatching hnd = TestLabel "Tests for Matching" $+ TestList+ [ testTrue "a" (propMatchSound hnd f1 f2)+ , testTrue "b" (propMatchSound hnd (pair(f1,inv(f2))) (pair(f1,inv(f2))))+ , testTrue "c" (propMatchSound hnd t1 t2)+ , testTrue "d" (propMatchSound hnd (x1 # f1) f1)+ , testTrue "e" $ null (matchLNTerm [pair(x1,x2) `MatchWith` pair(x1,x1)] `runReader` hnd)+ ]+ where+ t1 = expo (inv(pair(f1,f2)), f2 # (inv f2) # f3 # f4 # f2)+ t2 = expo (inv(pair(f1,f2)), f3 # (inv f2) # f2 # x1 # f5 # f2)++propMatchSound :: MaudeHandle -> LNTerm -> LNTerm -> Bool+propMatchSound mhnd t1 p = all (\s -> applyVTerm s t1 == applyVTerm s p) substs+ where substs = matchLNTerm [t1 `MatchWith` p] `runReader` mhnd++++-- *****************************************************************************+-- Tests for Unification+-- *****************************************************************************++testsUnify :: MaudeHandle -> Test+testsUnify mhnd = TestLabel "Tests for Unify" $+ TestList+ [ testTrue "a" (propUnifySound mhnd f1 f2)+ , testTrue "b" (propUnifySound mhnd (pair(f1,inv(f2))) (pair(f1,inv(f2))))+ , testTrue "c" (propUnifySound mhnd t1 t2)+ , testTrue "d" (propUnifySound mhnd u1 u2)+ , testTrue "f" (propUnifySound mhnd (sdec(x1,y1)) (sdec(senc(x2,x3), x4)))+ ]+ where+ t1 = expo (inv(pair(f1,f2)), f2 *: (inv f2) *: f3 *: f4 *: x2)+ t2 = expo (inv(pair(f1,f2)), f3 *: (inv f2) *: f2 *: f4 *: f5 *: f2)+ u1 = (f2 *: (inv f2) *: f3 *: f4 *: x2)+ u2 = (f3 *: (inv f2) *: f2 *: f4 *: f5 *: f2)++propUnifySound :: MaudeHandle -> LNTerm -> LNTerm -> Bool+propUnifySound hnd t1 t2 = all (\s -> let s' = freshToFreeAvoiding s [t1,t2]in+ applyVTerm s' t1 == applyVTerm s' t2) substs+ where+ substs = unifyLNTerm [Equal t1 t2] `runReader` hnd+++-- *****************************************************************************+-- Tests for Substitutions+-- *****************************************************************************++testsSubst :: Test+testsSubst = TestLabel "Tests for Substitution" $+ TestList+ [ -- introduce renaming for x3+ testEqual "a" (substFromListVFresh [(lx1, p1), (lx2, x9), (lx3,x9), (lx5, p1)])+ (composeVFresh (substFromListVFresh [(lx5, p1)])+ (substFromList [(lx1, x5), (lx2, x3)]))+ -- rename (fresh) x6 in s1b and do not mix up with x6 in s3f+ , testEqual "b" s1b_o_s3f (composeVFresh s1b s3f)+ -- drop x1 |-> p1 mapping from s1b, but apply to x2 |-> pair(x3,x1) in s3f+ , testEqual "c" s1b_o_s4f (composeVFresh s1b s4f)+ , testEqual "d" s4f_o_s3f (compose s4f s3f)+ , testEqual "e" (substFromList [(lx1,f1), (lx2,f1)])+ (mapRange (const f1) s4f)+ , testTrue "f" (isRenaming (substFromListVFresh [(lx1,x3), (lx2,x2), (lx3,x1)]))++ , testEqual "g" (substFromListVFresh [(lx1, f1)])+ (extendWithRenaming [lx1] (substFromListVFresh [(lx1, f1)]))++ , testEqual "h" (substFromListVFresh [(lx2, x1), (lx1, x3)])+ (extendWithRenaming [lx1] (substFromListVFresh [(lx2, x1)]))+ -- trivial, increase coverage+ , testTrue "i" ((>0) . length $ show s1b)+ , testTrue "j" ((>0) . length $ (render $ prettyLSubstVFresh s1b))+ , testTrue "k" (not . null $ domVFresh s1b)+ , testTrue "l" (not . null $ varsRangeVFresh s1b)+ , testTrue "m" ((>0) . length $ show $ substToListOn [lx1] s4f)+ , testTrue "n" ((<100) . size $ emptySubst)+ , testTrue "o" ((<10000) . size $ s1b)+ , testTrue "p" ((<100) . size $ emptySubstVFresh)+ ]+ where+ s1b = substFromListVFresh [(lx1, p1), (lx2, x6), (lx3, x6), (lx4, f1)]+ s3f = substFromList [(lx8, x6), (lx2, pair(x2,x1))]+ s1b_o_s3f = substFromListVFresh -- x2 not identified with x8+ [(lx1, p1), (lx2, pair(x15, p1)), (lx3, x15), (lx4, f1), (lx6, x22), (lx8, x22)]+ s4f = substFromList [(lx1, x6), (lx2, pair(x3,x1))]+ s1b_o_s4f = substFromListVFresh+ [(lx1, x20), (lx2, pair(x13, p1)), (lx3, x13), (lx4, f1), (lx6, x20)]++ s4f_o_s3f = substFromList [(lx1, x6), (lx2, pair(pair(x3,x1),x6)), (lx8, x6)]+ x15 = varTerm $ LVar "x" LSortMsg 15+ x13 = varTerm $ LVar "x" LSortMsg 13+ x20 = varTerm $ LVar "x" LSortMsg 20+ x22 = varTerm $ LVar "x" LSortMsg 22++-- *****************************************************************************+-- Tests for Subsumption+-- *****************************************************************************++testsSubs :: MaudeHandle -> Test+testsSubs mhnd = TestLabel "Tests for Subsumption" $ TestList+ [ tct Nothing f1 f2+ , tct (Just EQ) x1 x2+ , tct (Just LT) x1 (x1 *: x1)+ , tct (Just GT) (x1 *: x1) x1+ , tct (Just GT) (pair(f1 *: f2,f1)) (pair(f2 *: f1,x2))+ , testEqual "a" [substFromList [(lx2, pair(x6,x7)), (lx3, p1)]]+ (factorSubstVia [lx1]+ (substFromList [(lx1,pair(pair(x6,x7),p1))])+ (substFromList [(lx1,pair(x2,x3))]) `runReader` mhnd)++ , testEqual "b" [substFromList [(lx2, pair(x6,x7)), (lx3, p1), (lx5, f1), (lx6,f2)]]+ (factorSubstVia [lx1, lx5, lx6]+ (substFromList [(lx1,pair(pair(x6,x7),p1)), (lx5,f1), (lx6,f2)])+ (substFromList [(lx1,pair(x2,x3))]) `runReader` mhnd)++ , testTrue "c" (eqTermSubs p1 p1 `runReader` mhnd)+ ]+ where+ tct res e1 e2 =+ testEqual ("termCompareSubs "++ppLTerm e1++" "++ppLTerm e2) res (compareTermSubs e1 e2 `runReader` mhnd)++ppLTerm :: LNTerm -> String+ppLTerm = render . prettyNTerm++ppLSubst :: LNSubst -> String+ppLSubst = render . prettyLNSubst++-- *****************************************************************************+-- Tests for Norm+-- *****************************************************************************++testsNorm :: MaudeHandle -> Test+testsNorm hnd = TestLabel "Tests for normalization" $ TestList+ [ tcn normBigTerm bigTerm+ , tcn (expo(f3,f1 *: f4))+ (expo(expo(f3,f4),f1 *: f1 *: f2 *: inv (inv (inv f1)) *: one *: expo(inv f2,one)))+ , tcn (mult [f1, f1, f2]) (f1 *: (f1 *: f2))+ , tcn (inv (f1 *: f2)) (inv f2 *: inv f1)+ , tcn (f1 *: inv f2) (f1 *: inv f2)+ , tcn (one::LNTerm) one+ , tcn x6 (expo(expo(x6,inv x3),x3))+ +-- , testEqual "a" (normAC (p3 *: (p1 *: p2))) (mult [p1, p2, p3])+-- , testEqual "b" (normAC (p3 *: (p1 *: inv p3))) (mult [p1, p3, inv p3])+-- , testEqual "c" (normAC ((p1 *: p2) *: p3)) (mult [p1, p2, p3])+-- , testEqual "d" (normAC t1) (mult [p1, p2, p3, p4])+-- , testEqual "e" (normAC ((p1 # p2) *: p3)) (p3 *: (p1 # p2))+-- , testEqual "f" (normAC (p3 *: (p1 # p2))) (p3 *: (p1 # p2))+-- , testEqual "g" (normAC ((p3 *: p4) *: (p1 # p2))) (mult [p3, p4, p1 # p2])+ ]+ where+ tcn e1 e2 = testEqual ("norm "++ppLTerm e2) e1 (norm' e2 `runReader` hnd)+ t1 = (p1 *: p2) *: (p3 *: p4)++-- *****************************************************************************+-- Tests for Term+-- *****************************************************************************++testsTerm :: Test+testsTerm = TestLabel "Tests for Terms" $ TestList+ [ uncurry (testEqual "Terms: propSubtermReplace") (propSubtermReplace bigTerm [1,0]) ]++propSubtermReplace :: Ord a => Term a -> Position -> (Term a, Term a)+propSubtermReplace t p = (t,(t `replacePos` (t `atPos` p,p)))++bigTerm :: LNTerm+bigTerm = pair(pk(x1),+ expo(expo (inv x3,+ x2 *: x4 *: f1 *: one *: inv (f3 *: f4) *: f3 *: f4 *: inv one),+ inv(expo(x2,one)) *: f2))++normBigTerm :: LNTerm+normBigTerm = pair(pk(x1),expo(inv x3,mult [f1, f2, x4]))++tcompare :: MaudeHandle -> Test+tcompare hnd =+ TestLabel "Tests for variant order" $ TestList+ [ testTrue "a" (run $ isNormalInstance t su1 su2)+ , testTrue "b" $ not (run $ isNormalInstance t su1 su3)++ , testTrue "c" $ (run $ leqSubstVariant t su5 su4)+ , testTrue "d" $ not (run $ leqSubstVariant t su6 su4)++ , testEqual "e" (run $ compareSubstVariant t su4 su4) (Just EQ)+ , testEqual "f" (run $ compareSubstVariant t su5 su4) (Just LT)+ , testEqual "g" (run $ compareSubstVariant t su4 su5) (Just GT)+ , testEqual "h" (run $ compareSubstVariant t su6 su4) Nothing+ ]+ where+ run :: WithMaude a -> a+ run m = runReader m hnd+ t = pair(inv(x1) *: x2, inv(x3) *: x2)+ su1 = substFromList [(lx1, x2)]+ su2 = substFromList [(lx2, p1)]+ su3 = substFromList [(lx3, x2)]+ su4 = substFromListVFresh [(lx1, x4), (lx2, x4)]+ su5 = substFromListVFresh [(lx1, p1), (lx2, p1)]+ su6 = substFromListVFresh [(lx1, x4), (lx2, x4), (lx3, x4)]++testsVariant :: MaudeHandle -> Test+testsVariant hnd =+ TestLabel "Tests for variant computation" $ TestList+ [ testEqual "a" (computeVariantsCheck (sdec(x1, p1)) `runReader` hnd)+ (toSubsts [ []+ , [(lx1, senc(x1, p1))] ])++ , testEqual "b" (computeVariantsCheck (x1 *: p1) `runReader` hnd)+ (toSubsts [ []+ , [(lx1, one)]+ , [(lx1, inv(p1))]+ , [(lx1, inv(p1 *: x1))]+ , [(lx1, x1 *: inv(p1))]+ , [(lx1, x1 *: inv(p1 *: x2))]+ ])++ , testEqual "c" (sort $ computeVariantsCheck (fAppList [x1, x2, x1 +: x2]) `runReader` hnd)+ (sort $ toSubsts+ [ []+ , [(lx1, x1), (lx2,x1) ]+ , [(lx2,zero)]+ , [(lx1,zero)]+ , [(lx2, x1 +: x2), (lx1, x2)]+ , [(lx1, x1 +: x2), (lx2, x2)]+ , [(lx1, x2 +: x3), (lx2, x1 +: x3)]+ ])++ , testEqual "d" (computeVariantsCheck (fAppList [s1, s2, s1 # s2]) `runReader` hnd)+ (toSubsts [ []+ , [(ls1, emptyMSet)]+ , [(ls2, emptyMSet) ] ])++ , testTrue "e" $ not (checkComplete (sdec(x1, p1)) (toSubsts [[]]) `runReader` hnd)+ , testTrue "f" $ (checkComplete (sdec(x1, p1)) (toSubsts [[], [(lx1, senc(x1,p1))]])+ `runReader` hnd)+ ]+ where+ toSubsts = map substFromListVFresh++testsSimple :: MaudeHandle -> Test+testsSimple _hnd =+ 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+ mhnd <- startMaude maudePath allMaudeSig+ runTestTT $ 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+allMaudeSig = mconcat+ [ dhMaudeSig, xorMaudeSig, msetMaudeSig+ , pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig ]+++-- testing in ghci+----------------------------------------------------------------------------------++te :: LNTerm+te = pair(inv(x1) *: x2, inv(x3) *: x2)++sub4, sub6 :: LNSubstVFresh+sub4 = substFromListVFresh [(lx1, x4), (lx2, x4)]+sub6 = substFromListVFresh [(lx1, x4), (lx2, x4), (lx3, x4)]++sub4', sub6' :: LNSubst+sub4' = freshToFreeAvoiding sub4 te+sub6' = freshToFreeAvoiding sub6 te++tevs :: [LVar]+tevs = frees te++runTest :: WithMaude a -> IO a+runTest m = do+ hnd <- startMaude "maude" allMaudeSig+ return $ m `runReader` hnd+++ts1 :: LNSubstVFresh+ts1 = substFromListVFresh [(lx1, xor [x2,x3]), (lx2, xor [x1,x2,x3]) ]++ts2 :: LNSubstVFresh+ts2 = substFromListVFresh [(lx1, x2), (lx2, xor [x1,x2]) ]++ts1' :: LNSubst+ts1' = substFromList [(lx1, xor [x5,x6]), (lx2, xor [x4,x5,x6]) ]++ts2' :: LNSubst+ts2' = substFromList [(lx1, y2), (lx2, xor [y1, y2]) ]++ts2'' :: LNSubst+ts2'' = substFromList [(lx1, x5), (lx2, xor [x5, x6]) ]++tterm :: LNTerm+tterm = fAppList [x1, x2, (x1 +: x2)]++{-++runTest $ matchLNTerm [ pair(xor [x5,x6],xor [x4,x5,x6]) `MatchWith` pair(x5,xor [x5,x4]) ]++should be matchable if next matchable also++runTest $ matchLNTerm [ pair(xor [x5,x6],xor [x4,x5,x6]) `MatchWith` pair(x5,xor [x5,x6]) ]++-}++-- convenience abbreviations+----------------------------------------------------------------------------------++pair, expo :: (Term a, Term a) -> Term a+expo = fAppExp+pair = fAppPair++inv :: Term a -> Term a+inv = fAppInv++xor, union, mult :: Ord a => [Term a] -> Term a+xor = fAppXor+union = fAppUnion+mult = fAppMult++one, zero, emptyMSet :: Term a+one = fAppOne+zero = fAppZero+emptyMSet = fAppEmpty
+ src/Term/VTerm.hs view
@@ -0,0 +1,126 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable, ViewPatterns #-}+-- |+-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>+--+-- Terms with variables and constants.++module Term.VTerm (+ -- * Terms with constants and variables+ Lit(..)+ , VTerm++ , varTerm+ , constTerm+ , varsVTerm+ , occursVTerm+ , constsVTerm+ , isVar++ , IsVar+ , IsConst+ , module Term.Term+ ) where++import Data.Foldable+import Data.Traversable+import qualified Data.DList as D+import Data.Typeable+import Data.Generics+import Data.DeriveTH+import Data.Binary+import Data.Monoid+import Control.DeepSeq+import Control.Basics++import Extension.Prelude++import Term.Term++----------------------------------------------------------------------+-- Terms with constants and variables+----------------------------------------------------------------------+++-- | A Lit is either a constant or a variable. (@Const@ is taken by Control.Applicative)+data Lit c v = Con c | Var v+ deriving (Eq, Ord, Data, Typeable)++-- | A VTerm is a term with constants and variables+type VTerm c v = Term (Lit c v)++-- | collect class constraints for variables+class (Ord v, Eq v, Show v) => IsVar v where++-- | collect class constraints for constants+class (Ord c, Eq c, Show c, Data c) => IsConst c where++-- | Functor instance in the variable.+instance Functor (Lit c) where+ fmap f (Var v) = Var (f v)+ fmap _ (Con c) = Con c++-- | Foldable instance in the variable.+instance Foldable (Lit c) where+ foldMap f (Var v) = f v+ foldMap _ (Con _) = mempty++-- | Traversable instance in the variable.+instance Traversable (Lit c) where+ sequenceA (Var v) = Var <$> v+ sequenceA (Con n) = pure $ Con n++-- | Applicative instance in the variable.+instance Applicative (Lit c) where+ pure = Var+ (Var f) <*> (Var x) = Var (f x)+ (Var _) <*> (Con n) = Con n+ (Con n) <*> _ = Con n++-- | Monad instance in the variable+instance Monad (Lit c) where+ return = Var+ (Var x) >>= f = f x+ (Con n) >>= _ = Con n++instance Sized (Lit c v) where+ size _ = 1++instance (Show v, Show c) => Show (Lit c v) where+ show (Var x) = show x+ show (Con n) = show n++-- | @varTerm v@ is the 'VTerm' with the variable @v@.+varTerm :: v -> VTerm c v+varTerm = lit . Var ++-- | @constTerm c@ is the 'VTerm' with the const @c@.+constTerm :: c -> VTerm c v+constTerm = lit . Con++-- | @isVar t returns @True@ if @t@ is a variable.+isVar :: VTerm c v -> Bool+isVar (viewTerm -> Lit (Var _)) = True+isVar _ = False++-- | @vars t@ returns a duplicate-free list of variables that occur in @t@.+varsVTerm :: (Eq v, Ord v) => VTerm c v -> [v]+varsVTerm = sortednub . D.toList . foldMap (foldMap return)++-- | @occurs v t@ returns @True@ if @v@ occurs in @t@+occursVTerm :: Eq v => v -> VTerm c v -> Bool+occursVTerm v = getAny . foldMap (foldMap (Any . (v==)))++-- | @constsVTerm t@ returns a duplicate-free list of constants that occur in @t@.+constsVTerm :: IsConst c => VTerm c v -> [c]+constsVTerm = sortednub . D.toList . foldMap fLit+ where fLit (Var _) = mempty+ fLit (Con n) = return n++-- Derived instances+--------------------++$( derive makeNFData ''Lit)+$( derive makeBinary ''Lit)
tamarin-prover-term.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,13 +13,13 @@ synopsis: Term manipulation 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>). . This library provides term manipulation infrastructure (matching, unification, narrowing, finite variants) for- the @tamarin@ prover. It uses maude+ the Tamarin prover. It uses maude (<http://maude.cs.uiuc.edu/>) as a backend for normalization, equational matching, and unification. @@ -31,35 +31,43 @@ ---------------------- library+ ghc-prof-options: -auto-all+ build-depends: base == 4.* , mtl == 2.0.*- , containers == 0.4.*+ , bytestring == 0.9.*+ , attoparsec == 0.10.*+ , containers >= 0.4.2 && < 0.5 , dlist == 0.5.*- , safe == 0.2.*+ , safe >= 0.2 && < 0.4 , split == 0.1.* , parsec == 3.1.* , syb >= 0.3.3 && < 0.4 , directory == 1.1.*- , process == 1.0.*- , deepseq == 1.1.*+ , process == 1.1.*+ , deepseq == 1.3.* , binary == 0.5.* , derive == 2.5.*++ , HUnit == 1.2.* - , tamarin-prover-utils == 0.1.*+ , tamarin-prover-utils == 0.4.* + hs-source-dirs: src exposed-modules: Term.Unification+ Term.VTerm Term.LTerm Term.Positions Term.SubtermRule Term.Subsumption Term.Substitution + Term.Rewriting.Definitions Term.Rewriting.Norm- Term.Rewriting.NormAC Term.Narrowing.Variants Term.Narrowing.Variants.Check@@ -70,7 +78,11 @@ Term.Builtin.Signature Term.Maude.Process+ Term.Maude.Signature Term.Maude.Types+ Term.Maude.Parser++ Term.UnitTests other-modules: Term.Term