diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -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 +-} + +-} diff --git a/src/Term/Builtin/Convenience.hs b/src/Term/Builtin/Convenience.hs --- a/src/Term/Builtin/Convenience.hs +++ b/src/Term/Builtin/Convenience.hs @@ -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 diff --git a/src/Term/Builtin/Rules.hs b/src/Term/Builtin/Rules.hs --- a/src/Term/Builtin/Rules.hs +++ b/src/Term/Builtin/Rules.hs @@ -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) ] diff --git a/src/Term/Builtin/Signature.hs b/src/Term/Builtin/Signature.hs --- a/src/Term/Builtin/Signature.hs +++ b/src/Term/Builtin/Signature.hs @@ -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 ] diff --git a/src/Term/LTerm.hs b/src/Term/LTerm.hs --- a/src/Term/LTerm.hs +++ b/src/Term/LTerm.hs @@ -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 diff --git a/src/Term/Maude/Parser.hs b/src/Term/Maude/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Term/Maude/Parser.hs @@ -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 +-- +-- 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 ++"'" diff --git a/src/Term/Maude/Process.hs b/src/Term/Maude/Process.hs --- a/src/Term/Maude/Process.hs +++ b/src/Term/Maude/Process.hs @@ -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 ------------------------------------------------- diff --git a/src/Term/Maude/Signature.hs b/src/Term/Maude/Signature.hs new file mode 100644 --- /dev/null +++ b/src/Term/Maude/Signature.hs @@ -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 +-- +-- 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) diff --git a/src/Term/Maude/Types.hs b/src/Term/Maude/Types.hs --- a/src/Term/Maude/Types.hs +++ b/src/Term/Maude/Types.hs @@ -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 -- -- 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 diff --git a/src/Term/Narrowing/Narrow.hs b/src/Term/Narrowing/Narrow.hs --- a/src/Term/Narrowing/Narrow.hs +++ b/src/Term/Narrowing/Narrow.hs @@ -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 diff --git a/src/Term/Positions.hs b/src/Term/Positions.hs --- a/src/Term/Positions.hs +++ b/src/Term/Positions.hs @@ -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 @@ -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] diff --git a/src/Term/Rewriting/Definitions.hs b/src/Term/Rewriting/Definitions.hs new file mode 100644 --- /dev/null +++ b/src/Term/Rewriting/Definitions.hs @@ -0,0 +1,102 @@ +{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-} +-- | +-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier +-- License : GPL v3 (see LICENSE) +-- +-- Maintainer : Benedikt Schmidt +-- +-- 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) diff --git a/src/Term/Rewriting/Norm.hs b/src/Term/Rewriting/Norm.hs --- a/src/Term/Rewriting/Norm.hs +++ b/src/Term/Rewriting/Norm.hs @@ -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] diff --git a/src/Term/Rewriting/NormAC.hs b/src/Term/Rewriting/NormAC.hs deleted file mode 100644 --- a/src/Term/Rewriting/NormAC.hs +++ /dev/null @@ -1,47 +0,0 @@ -{-# LANGUAGE PatternGuards, FlexibleContexts #-} --- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt --- License : GPL v3 (see LICENSE) --- --- Maintainer : Benedikt Schmidt --- --- 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 - diff --git a/src/Term/Substitution.hs b/src/Term/Substitution.hs --- a/src/Term/Substitution.hs +++ b/src/Term/Substitution.hs @@ -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 diff --git a/src/Term/Substitution/SubstVFree.hs b/src/Term/Substitution/SubstVFree.hs --- a/src/Term/Substitution/SubstVFree.hs +++ b/src/Term/Substitution/SubstVFree.hs @@ -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) diff --git a/src/Term/Substitution/SubstVFresh.hs b/src/Term/Substitution/SubstVFresh.hs --- a/src/Term/Substitution/SubstVFresh.hs +++ b/src/Term/Substitution/SubstVFresh.hs @@ -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) diff --git a/src/Term/Subsumption.hs b/src/Term/Subsumption.hs --- a/src/Term/Subsumption.hs +++ b/src/Term/Subsumption.hs @@ -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) diff --git a/src/Term/SubtermRule.hs b/src/Term/SubtermRule.hs --- a/src/Term/SubtermRule.hs +++ b/src/Term/SubtermRule.hs @@ -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) {- diff --git a/src/Term/Term.hs b/src/Term/Term.hs --- a/src/Term/Term.hs +++ b/src/Term/Term.hs @@ -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) - - diff --git a/src/Term/Unification.hs b/src/Term/Unification.hs --- a/src/Term/Unification.hs +++ b/src/Term/Unification.hs @@ -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 diff --git a/src/Term/UnitTests.hs b/src/Term/UnitTests.hs new file mode 100644 --- /dev/null +++ b/src/Term/UnitTests.hs @@ -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 +-- +-- 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 diff --git a/src/Term/VTerm.hs b/src/Term/VTerm.hs new file mode 100644 --- /dev/null +++ b/src/Term/VTerm.hs @@ -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 +-- +-- 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) diff --git a/tamarin-prover-term.cabal b/tamarin-prover-term.cabal --- a/tamarin-prover-term.cabal +++ b/tamarin-prover-term.cabal @@ -2,7 +2,7 @@ cabal-version: >= 1.8 build-type: Simple -version: 0.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 (). . This library provides term manipulation infrastructure (matching, unification, narrowing, finite variants) for - the @tamarin@ prover. It uses maude + the Tamarin prover. It uses maude () 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