diff --git a/src/Term/LTerm.hs b/src/Term/LTerm.hs --- a/src/Term/LTerm.hs +++ b/src/Term/LTerm.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE +{-# LANGUAGE CPP, FlexibleContexts, FlexibleInstances, TypeSynonymInstances, MultiParamTypeClasses, DeriveDataTypeable, StandaloneDeriving, TemplateHaskell, GeneralizedNewtypeDeriving, ViewPatterns @@ -8,7 +8,7 @@ -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- Terms with logical variables and names. @@ -31,6 +31,7 @@ -- * LVar , LSort(..) , LVar(..) + , NodeId , LTerm , LNTerm @@ -42,11 +43,20 @@ , sortOfLNTerm , isMsgVar , isFreshVar - , trivial - , input - + , isSimpleTerm + , inputTerms + + -- ** Destructors + , ltermVar + , ltermVar' + , ltermNodeId + , ltermNodeId' + , bltermNodeId + , bltermNodeId' + + -- ** Manging Free LVars - + , HasFrees(..) , MonotoneFunction(..) , occurs @@ -63,11 +73,14 @@ -- * BVar , BVar(..) + , BLVar + , BLTerm , foldBVar , fromFree -- * Pretty-Printing , prettyLVar + , prettyNodeId , prettyNTerm , prettyLNTerm @@ -98,12 +111,68 @@ import Data.Binary import Data.Foldable hiding (concatMap, elem) +import Safe (fromJustNote) + import Extension.Prelude import Extension.Data.Monoid import Logic.Connectives +------------------------------------------------------------------------------ +-- Sorts. +------------------------------------------------------------------------------ +-- | Sorts for logical variables. They satisfy the following sub-sort relation: +-- +-- > LSortMsg < LSortMSet +-- > LSortFresh < LSortMsg +-- > LSortPub < LSortMsg +-- +data LSort = LSortPub -- ^ Arbitrary public names. + | LSortFresh -- ^ Arbitrary fresh names. + | LSortMsg -- ^ Arbitrary messages. + | LSortMSet -- ^ Sort for multisets. + | LSortNode -- ^ Sort for variables denoting nodes of derivation graphs. + deriving( Eq, Ord, Show, Enum, Bounded, Typeable, Data ) + +-- | @sortCompare s1 s2@ compares @s1@ and @s2@ with respect to the partial order on sorts. +-- Partial order: Node MSet +-- | +-- Msg +-- / \ +-- Pub Fresh +sortCompare :: LSort -> LSort -> Maybe Ordering +sortCompare s1 s2 = case (s1, s2) of + (a, b) | a == b -> Just EQ + -- Node is incomparable to all other sorts, invalid input + (LSortNode, _ ) -> Nothing + (_, LSortNode) -> Nothing + -- MSet is greater than all except Node + (LSortMSet, _ ) -> Just GT + (_, LSortMSet) -> Just LT + -- Msg is greater than all sorts except Node and MSet + (LSortMsg, _ ) -> Just GT + (_, LSortMsg ) -> Just LT + -- The remaining combinations (Pub/Fresh) are incomparable + _ -> Nothing + +-- | @sortPrefix s@ is the prefix we use for annotating variables of sort @s@. +sortPrefix :: LSort -> String +sortPrefix LSortMsg = "" +sortPrefix LSortFresh = "~" +sortPrefix LSortPub = "$" +sortPrefix LSortNode = "#" +sortPrefix LSortMSet = "%" + +-- | @sortSuffix s@ is the suffix we use for annotating variables of sort @s@. +sortSuffix :: LSort -> String +sortSuffix LSortMsg = "msg" +sortSuffix LSortFresh = "fresh" +sortSuffix LSortPub = "pub" +sortSuffix LSortNode = "node" +sortSuffix LSortMSet = "mset" + + ------------------------------------------------------------------------------ -- Names ------------------------------------------------------------------------------ @@ -152,33 +221,25 @@ sortOfName (Name FreshName _) = LSortFresh sortOfName (Name PubName _) = LSortPub - ------------------------------------------------------------------------------ -- LVar: logical variables ------------------------------------------------------------------------------ --- | Sorts for logical variables. They satisfy the following sub-sort relation: --- --- > LSortMsg < LSortMSet --- > LSortFresh < LSortMsg --- > LSortPub < LSortMsg --- -data LSort = LSortPub -- ^ Arbitrary public names. - | LSortFresh -- ^ Arbitrary fresh names. - | LSortMsg -- ^ Arbitrary messages. - | LSortMSet -- ^ Sort for multisets. - | LSortNode -- ^ Sort for variables denoting nodes of derivation graphs. - deriving( Eq, Ord, Show, Enum, Bounded, Typeable, Data ) -- | Logical variables. Variables with the same name and index but different -- sorts are regarded as different variables. -data LVar = LVar +data LVar = LVar { lvarName :: String - , lvarSort :: !LSort + , lvarSort :: !LSort -- FIXME: Rename to 'sortOfLVar' for consistency + -- with the other 'sortOf' functions. , lvarIdx :: !Integer } deriving( Typeable, Data ) +-- | An alternative name for logical variables, which are intented to be +-- variables of sort 'LSortNode'. +type NodeId = LVar + -- | Terms used for proving; i.e., variables fixed to logical variables. type LTerm c = VTerm c LVar @@ -203,43 +264,6 @@ sortOfLNTerm :: LNTerm -> LSort sortOfLNTerm = sortOfLTerm sortOfName --- | @sortCompare s1 s2@ compares @s1@ and @s2@ with respect to the partial order on sorts. --- Partial order: Node MSet --- | --- Msg --- / \ --- Pub Fresh -sortCompare :: LSort -> LSort -> Maybe Ordering -sortCompare s1 s2 = case (s1, s2) of - (a, b) | a == b -> Just EQ - -- Node is incomparable to all other sorts, invalid input - (LSortNode, _ ) -> Nothing - (_, LSortNode) -> Nothing - -- MSet is greater than all except Node - (LSortMSet, _ ) -> Just GT - (_, LSortMSet) -> Just LT - -- Msg is greater than all sorts except Node and MSet - (LSortMsg, _ ) -> Just GT - (_, LSortMsg ) -> Just LT - -- The remaining combinations (Pub/Fresh) are incomparable - _ -> Nothing - --- | @sortPrefix s@ is the prefix we use for annotating variables of sort @s@. -sortPrefix :: LSort -> String -sortPrefix LSortMsg = "" -sortPrefix LSortFresh = "~" -sortPrefix LSortPub = "$" -sortPrefix LSortNode = "#" -sortPrefix LSortMSet = "%" - --- | @sortSuffix s@ is the suffix we use for annotating variables of sort @s@. -sortSuffix :: LSort -> String -sortSuffix LSortMsg = "msg" -sortSuffix LSortFresh = "fresh" -sortSuffix LSortPub = "pub" -sortSuffix LSortNode = "node" -sortSuffix LSortMSet = "mset" - -- | Is a term a message variable? isMsgVar :: LNTerm -> Bool isMsgVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortMsg) @@ -251,12 +275,13 @@ isFreshVar _ = False -- | The required components to construct the message. -input :: LNTerm -> [LNTerm] -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] +inputTerms :: LNTerm -> [LNTerm] +inputTerms (viewTerm2 -> FMult ts) = concatMap inputTerms ts +inputTerms (viewTerm2 -> FInv t1) = inputTerms t1 +inputTerms (viewTerm2 -> FPair t1 t2) = inputTerms t1 ++ inputTerms t2 +inputTerms t = [t] +{- -- | Is a message trivial; i.e., can for sure be instantiated with something -- known to the intruder? trivial :: LNTerm -> Bool @@ -267,8 +292,45 @@ LSortMsg -> True _ -> False trivial _ = False +-} +-- | A term is *simple* iff there is an instance of this term that can be +-- constructed from public names only. i.e., the term does not contain any +-- fresh names or fresh variables. +isSimpleTerm :: LNTerm -> Bool +isSimpleTerm = + getAll . foldMap (All . (LSortFresh /=) . sortOfLit) + where + sortOfLit (Con n) = sortOfName n + sortOfLit (Var v) = lvarSort v + +-- Destructors +-------------- + +-- | Extract a variable of the given sort from a term that may be such a +-- variable. Use 'termVar', if you do not want to restrict the sort. +ltermVar :: LSort -> LTerm c -> Maybe LVar +ltermVar s t = do v <- termVar t; guard (s == lvarSort v); return v + +-- | Extract a variable of the given sort from a term that must be such a +-- variable. Fails with an error, if that is not possible. +ltermVar' :: Show c => LSort -> LTerm c -> LVar +ltermVar' s t = + fromJustNote err (ltermVar s t) + where + err = "ltermVar': expected variable term of sort " ++ show s ++ ", but got " ++ show t + +-- | Extract a node-id variable from a term that may be a node-id variable. +ltermNodeId :: LTerm c -> Maybe LVar +ltermNodeId = ltermVar LSortNode + +-- | Extract a node-id variable from a term that must be a node-id variable. +ltermNodeId' :: Show c => LTerm c -> LVar +ltermNodeId' = ltermVar' LSortNode + + + -- BVar: Bound variables ------------------------ @@ -277,8 +339,13 @@ | Free v -- ^ A free variable. deriving( Eq, Ord, Show, Data, Typeable ) +-- | 'LVar's combined with quantified variables. They occur only in 'LFormula's. +type BLVar = BVar LVar +-- | Terms built over names and 'LVar's combined with quantified variables. +type BLTerm = NTerm BLVar + -- | Fold a possibly bound variable. {-# INLINE foldBVar #-} foldBVar :: (Integer -> a) -> (v -> a) -> BVar v -> a @@ -310,7 +377,19 @@ fromFree (Free v) = v fromFree (Bound i) = error $ "fromFree: bound variable '" ++ show i ++ "'" +-- | Extract a node-id variable from a term that may be a node-id variable. +bltermNodeId :: BLTerm -> Maybe LVar +bltermNodeId t = do + Free v <- termVar t; guard (LSortNode == lvarSort v); return v +-- | Extract a node-id variable from a term that must be a node-id variable. +bltermNodeId' :: BLTerm -> LVar +bltermNodeId' t = + fromJustNote err (bltermNodeId t) + where + err = "bltermNodeId': expected free node-id variable term, but got " ++ + show t + -- Instances ------------ @@ -319,7 +398,7 @@ -- An ord instane that prefers the 'lvarIdx' over the 'lvarName'. instance Ord LVar where - compare (LVar x1 x2 x3) (LVar y1 y2 y3) = + compare (LVar x1 x2 x3) (LVar y1 y2 y3) = compare x3 y3 & compare x2 y2 & compare x1 y1 & EQ where EQ & x = x @@ -345,12 +424,12 @@ -- 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 ) +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'. +-- functor using 'mapFrees'. -- -- When defining instances of this class, you have to ensure that only the free -- LVars are collected and mapped and no others. The instances for standard @@ -409,10 +488,10 @@ -- 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 = +eqModuloFreshnessNoAC t1 = -- this formulation shares normalisation of t1 among further calls to -- different t2. - (normIndices t1 ==) . normIndices + (normIndices t1 ==) . normIndices where normIndices = (`evalFresh` nothingUsed) . (`evalBindT` noBindings) . mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x "") @@ -423,7 +502,7 @@ -- | @avoid t@ computes a 'FreshState' that avoids generating -- variables occurring in @t@. -avoid :: HasFrees t => t -> FreshState +avoid :: HasFrees t => t -> FreshState avoid = maybe 0 (succ . snd) . boundsVarIdx -- | @m `evalFreshAvoiding` t@ evaluates the monadic action @m@ with a @@ -449,7 +528,7 @@ foldFrees = id mapFrees (Arbitrary f) = f mapFrees (Monotone f) = f - + instance HasFrees v => HasFrees (Lit c v) where foldFrees f (Var x) = foldFrees f x foldFrees _ _ = mempty @@ -517,7 +596,7 @@ instance (HasFrees a, HasFrees b, HasFrees c) => HasFrees (a, b, c) where foldFrees f (x, y, z) = foldFrees f (x, (y, z)) - mapFrees f (x0, y0, z0) = + mapFrees f (x0, y0, z0) = (\(x, (y, z)) -> (x, y, z)) <$> mapFrees f (x0, (y0, z0)) instance HasFrees a => HasFrees [a] where @@ -550,6 +629,10 @@ -- | Pretty print a 'LVar'. prettyLVar :: Document d => LVar -> d prettyLVar = text . show + +-- | Pretty print a 'NodeId'. +prettyNodeId :: Document d => NodeId -> d +prettyNodeId = text . show -- | Pretty print an @NTerm@. prettyNTerm :: (Show v, Document d) => NTerm v -> d 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 @@ -4,7 +4,7 @@ -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- AC-unification of DH terms using Maude as a backend. @@ -16,13 +16,13 @@ -- * Unification using Maude , unifyViaMaude - + -- * Matching using Maude , matchViaMaude -- * Normalization using Maude , normViaMaude - + -- * Managing the persistent Maude process , WithMaude ) where @@ -87,7 +87,7 @@ } -- | @startMaude@ starts a new instance of Maude and returns a Handle to it. -startMaude :: FilePath -> MaudeSig -> IO MaudeHandle +startMaude :: FilePath -> MaudeSig -> IO MaudeHandle startMaude maudePath maudeSig = do mv <- newMVar =<< startMaudeProcess maudePath maudeSig -- Add a finalizer to the MVar that stops maude. @@ -108,13 +108,13 @@ -- input the maude theory executeMaudeCommand hin hout (ppTheory maudeSig) return (MP hin hout herr hproc 0 0 0) - where + where maudeCmd - | dEBUGMAUDE = "sh -c \"tee /tmp/maude.input | " + | dEBUGMAUDE = "sh -c \"tee /tmp/maude.input | " ++ maudePath ++ " -no-tecla -no-banner -no-wrap -batch " ++ "\" | tee /tmp/maude.output" - | otherwise = - maudePath ++ " -no-tecla -no-banner -no-wrap -batch " + | otherwise = + maudePath ++ " -no-tecla -no-banner -no-wrap -batch " executeMaudeCommand hin hout cmd = B.hPutStr hin cmd >> hFlush hin >> getToDelim hout >> return () setupCmds = [ "set show command off .\n" @@ -166,7 +166,7 @@ return (mp', res) -- | Compute a result via Maude. -computeViaMaude :: +computeViaMaude :: (Show a, Show b, Ord c) => MaudeHandle -> (MaudeProcess -> MaudeProcess) -- ^ Update statistics @@ -201,7 +201,7 @@ -- | @unifyViaMaude hnd eqs@ computes all AC unifiers of @eqs@ using the -- Maude process @hnd@. -unifyViaMaude +unifyViaMaude :: (IsConst c , Show (Lit c LVar), Ord c) => MaudeHandle -> (c -> LSort) -> [Equal (VTerm c LVar)] -> IO [SubstVFresh c LVar] @@ -233,18 +233,21 @@ matchViaMaude :: (IsConst c , Show (Lit c LVar), Ord c) => MaudeHandle -> (c -> LSort) - -> [Match (VTerm c LVar)] + -> Match (VTerm c LVar) -> IO [Subst c LVar] -matchViaMaude _ _ [] = return [emptySubst] -matchViaMaude hnd sortOf matcheqs = - computeViaMaude hnd incMatchCount toMaude fromMaude eqs +matchViaMaude hnd sortOf matchProblem = + case flattenMatch matchProblem of + Nothing -> return [] + Just [] -> return [emptySubst] + Just ms -> computeViaMaude hnd incMatchCount toMaude fromMaude + (uncurry Equal <$> ms) where msig = mhMaudeSig hnd - toMaude = fmap matchCmd . mapM (traverse (lTermToMTerm sortOf)) + 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 ] + ------------------------------------------------------------------------------ -- Normalization of terms diff --git a/src/Term/Rewriting/Definitions.hs b/src/Term/Rewriting/Definitions.hs --- a/src/Term/Rewriting/Definitions.hs +++ b/src/Term/Rewriting/Definitions.hs @@ -1,8 +1,8 @@ {-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier +-- Copyright : (c) 2010 - 2012 Benedikt Schmidt, Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- Term Equalities, Matching Problems, and Subterm Rules. @@ -13,14 +13,19 @@ -- * Matching Problems , Match(..) + , flattenMatch + , matchWith + , matchOnlyIf -- * Rewriting Rules , RRule(..) ) where +import Control.Arrow ( (***) ) import Control.Applicative -import Data.Monoid + +import Extension.Data.Monoid import Data.Foldable import Data.Traversable @@ -38,11 +43,11 @@ evalEqual (Equal l r) = l == r instance Functor Equal where - fmap f (Equal lhs rhs) = Equal (f lhs) (f rhs) + 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 r1) `mappend` (Equal l2 r2) = Equal (l1 `mappend` l2) (r1 `mappend` r2) instance Foldable Equal where @@ -55,28 +60,74 @@ 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) +-- | Matching problems. Use the 'Monoid' instance to compose matching +-- problems. +data Match a = + NoMatch + -- ^ No matcher exists. + | DelayedMatches [(a,a)] + -- ^ A bunch of delayed (term,pattern) pairs. +instance Eq a => Eq (Match a) where + x == y = flattenMatch x == flattenMatch y + +instance Show a => Show (Match a) where + show = show . flattenMatch + + +-- Smart constructors +--------------------- + +-- | Ensure that matching only succeeds if the condition holds. +matchOnlyIf :: Bool -> Match a +matchOnlyIf False = NoMatch +matchOnlyIf True = mempty + +-- | Match a term with a pattern. +matchWith :: a -- ^ Term + -> a -- ^ Pattern + -> Match a -- ^ Matching problem. +matchWith t p = DelayedMatches [(t, p)] + +-- Destructors +-------------- + +-- | Flatten a matching problem to a list of (term,pattern) pairs. If no +-- matcher exists, then 'Nothing' is returned. +flattenMatch :: Match a -> Maybe [(a, a)] +flattenMatch NoMatch = Nothing +flattenMatch (DelayedMatches ms) = Just ms + +-- Instances +------------ + instance Functor Match where - fmap f (MatchWith t p) = MatchWith (f t) (f p) + fmap _ NoMatch = NoMatch + fmap f (DelayedMatches ms) = DelayedMatches (fmap (f *** f) ms) -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 Monoid (Match a) where + mempty = DelayedMatches [] + NoMatch `mappend` _ = NoMatch + _ `mappend` NoMatch = NoMatch + DelayedMatches ms1 `mappend` DelayedMatches ms2 = + DelayedMatches (ms1 `mappend` ms2) + + instance Foldable Match where - foldMap f (MatchWith t p) = f t `mappend` f p + foldMap _ NoMatch = mempty + foldMap f (DelayedMatches ms) = foldMap (\(t, p) -> f t <> f p) ms instance Traversable Match where - traverse f (MatchWith t p) = MatchWith <$> f t <*> f p + traverse _ NoMatch = pure NoMatch + traverse f (DelayedMatches ms) = + DelayedMatches <$> traverse (\(t, p) -> (,) <$> f t <*> f p) ms +{- instance Applicative Match where pure x = MatchWith x x (MatchWith ft fp) <*> (MatchWith t p) = MatchWith (ft t) (fp p) +-} -- | A rewrite rule. @@ -84,11 +135,11 @@ deriving (Show, Ord, Eq) instance Functor RRule where - fmap f (RRule lhs rhs) = RRule (f lhs) (f rhs) + 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 r1) `mappend` (RRule l2 r2) = RRule (l1 `mappend` l2) (r1 `mappend` r2) instance Foldable RRule where 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,15 +1,18 @@ -{-# LANGUAGE PatternGuards, FlexibleContexts, ExplicitForAll #-} -{-# LANGUAGE ScopedTypeVariables, ViewPatterns #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} -- spurious warnings for view patterns -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- This module implements normalization with respect to DH u AC using class -- rewriting and an ad-hoc function that uses the @TermAC@ representation of --- terms modulo AC. +-- terms modulo AC. module Term.Rewriting.Norm ( -- norm norm' @@ -19,23 +22,23 @@ , maybeNotNfSubterms ) where -import Term.Term -import Term.LTerm -import Term.Substitution -import Term.Maude.Signature -import Term.Maude.Process -import Term.SubtermRule -import Term.Unification +import Term.LTerm +import Term.Maude.Process +import Term.Maude.Signature +import Term.Substitution +import Term.SubtermRule +import Term.Term +import Term.Unification -import Utils.Misc +import Utils.Misc -import Control.Basics -import Control.Monad.Reader +import Control.Basics +import Control.Monad.Reader -import Data.List -import qualified Data.Set as S +import Data.List +import qualified Data.Set as S -import System.IO.Unsafe (unsafePerformIO) +import System.IO.Unsafe (unsafePerformIO) -- Normalization using Maude ---------------------------------------------------------------------- @@ -91,7 +94,7 @@ FAppNonAC _ ts -> all go ts struleApplicable t (StRule lhs rhs) = - case matchLNTerm [t `MatchWith` lhs] `runReader` hnd of + case solveMatchLNTerm (t `matchWith` lhs) `runReader` hnd of [] -> False _:_ -> case rhs of RhsPosition _ -> True @@ -133,7 +136,7 @@ ++" maude: " ++ show x ++ " haskell: "++show y --- Normalization +-- Normalization ---------------------------------------------------- -- | @nfSubst s@ returns @True@ if the substitution @s@ is in normal form. 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 @@ -6,7 +6,7 @@ -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- Standard substitutions (with free variables). @@ -137,7 +137,7 @@ applySubst :: (IsConst c, IsVar v) => Subst c v -> Subst c v -> Subst c v applySubst subst subst' = mapRange (applyVTerm subst) subst' - + -- | @compose s1 s2@ composes the substitutions s1 and s2. The result is -- @s1.s2@, i.e., it has the same effect as @(t s2) s1 = s1(s2(t))@ -- when applied to a term @t@. @@ -223,13 +223,30 @@ apply subst x = maybe x extractVar $ imageOf subst x where extractVar (viewTerm -> Lit (Var x')) = x' - extractVar t = - error $ "apply (LVar): variable '" ++ show x ++ + extractVar t = + error $ "apply (LVar): variable '" ++ show x ++ "' substituted with term '" ++ show t ++ "'" instance Apply LNTerm where apply subst = applyVTerm subst +instance Apply BLVar where + apply _ x@(Bound _) = x + apply subst x@(Free v) = maybe x extractVar $ imageOf subst v + where + extractVar (viewTerm -> Lit (Var v')) = Free v' + extractVar _t = + error $ "apply (BLVar): variable '" ++ show v ++ + "' substituted with term '" -- ++ show _t ++ "'" + +instance Apply BLTerm where + apply subst = (`bindTerm` applyBLLit) + where + applyBLLit :: Lit Name BLVar -> BLTerm + applyBLLit l@(Var (Free v)) = + maybe (lit l) (fmapTerm (fmap Free)) (imageOf subst v) + applyBLLit l = lit l + instance Apply () where apply _ = id @@ -245,6 +262,12 @@ instance (Apply a, Apply b) => Apply (a, b) where apply subst (x,y) = (apply subst x, apply subst y) +instance Apply a => Apply (Maybe a) where + apply subst = fmap (apply subst) + +instance (Apply a, Apply b) => Apply (Either a b) where + apply subst = either (Left . apply subst) (Right . apply subst) + instance Apply a => Apply [a] where apply subst = fmap (apply subst) @@ -266,12 +289,12 @@ ---------------------------------------------------------------------- -- | Pretty print a substitution. -prettySubst :: (Ord c, Ord v, HighlightDocument d) +prettySubst :: (Ord c, Ord v, HighlightDocument d) => (v -> d) -> (Lit c v -> d) -> Subst c v -> [d] -prettySubst ppVar ppLit = +prettySubst ppVar ppLit = map pp . M.toList . equivClasses . substToList where - pp (t, vs) = prettyTerm ppLit t <-> operator_ " <~ {" <> + pp (t, vs) = prettyTerm ppLit t <-> operator_ " <~ {" <> (fsep $ punctuate comma $ map ppVar $ S.toList vs) <> operator_ "}" -- | Pretty print a substitution with logical variables. diff --git a/src/Term/Subsumption.hs b/src/Term/Subsumption.hs --- a/src/Term/Subsumption.hs +++ b/src/Term/Subsumption.hs @@ -4,7 +4,7 @@ -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- Subsumption of terms and substitutions. @@ -23,16 +23,20 @@ , varOccurences ) where +import Control.Basics + +import Data.Monoid + +import Extension.Prelude +-- import Utils.Misc + + import Term.Term import Term.LTerm import Term.Unification import Term.Positions -import Extension.Prelude --- import Utils.Misc -import Control.Basics - ---------------------------------------------------------------------- -- Subsumption order on terms and substitutions ---------------------------------------------------------------------- @@ -40,7 +44,8 @@ -- | Compare terms @t1@ and @t2@ with respect to the subsumption order modulo AC. compareTermSubs :: LNTerm -> LNTerm -> WithMaude (Maybe Ordering) compareTermSubs t1 t2 = do - check <$> matchLNTerm [t1 `MatchWith` t2] <*> matchLNTerm [t2 `MatchWith` t1] + check <$> solveMatchLNTerm (t1 `matchWith` t2) + <*> solveMatchLNTerm (t2 `matchWith` t1) where check [] [] = Nothing check (_:_) [] = Just GT @@ -49,7 +54,7 @@ -- | Returns True if @s1@ and @s2@ are equal with respect to the subsumption order modulo AC. eqTermSubs :: LNTerm -> LNTerm -> WithMaude Bool -eqTermSubs s1 s2 = (== Just EQ) <$> compareTermSubs s1 s2 +eqTermSubs s1 s2 = (== Just EQ) <$> compareTermSubs s1 s2 -- | @factorSubstOn s1 s2 vs@ factors the free substitution @s1@ -- through free substitution @s2@ on @vs@, @@ -58,21 +63,25 @@ -- > applyVTerm s1 x =AC= applyVTerm s (applyVTerm s2 x). factorSubstVia :: [LVar] -> LNSubst -> LNSubst -> WithMaude [LNSubst] factorSubstVia vs s1 s2 = - matchLNTerm (zipWith MatchWith (substToListOn vs s1) (substToListOn vs s2)) + solveMatchLNTerm (mconcat matches) + where + matches :: [Match LNTerm] + matches = zipWith matchWith (substToListOn vs s1) (substToListOn vs s2) + {- -- | @factorSubstOnVFresh s1 s2 vs@ factors the fresh substitution @s1@ -- through the free substitution @s2@ on @vs@, -- i.e., it returns a complete set of fresh substitutions s such that -- s1 is equivalent to s.s2 modulo renaming. -factorSubstViaVFresh :: [LVar] -> LNSubstVFresh -> LNSubst +factorSubstViaVFresh :: [LVar] -> LNSubstVFresh -> LNSubst -> WithMaude [LNSubstVFresh] factorSubstViaVFresh vs s1_0 s2 = do matchers <- matchLNTerm (zipWith MatchWith l1 l2) return $ do s <- matchers when (not $ varsRange s `subsetOf` varsRange s1) $ - error $ "factorSubstOnVFresh " ++ show s1 ++ " " ++ show s2 + error $ "factorSubstOnVFresh " ++ show s1 ++ " " ++ show s2 ++ " => " ++ show s ++ " contains new variables" return $ freeToFreshRaw s where diff --git a/src/Term/Unification.hs b/src/Term/Unification.hs --- a/src/Term/Unification.hs +++ b/src/Term/Unification.hs @@ -2,7 +2,7 @@ -- | -- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- AC unification based on maude and free unification. @@ -10,14 +10,19 @@ -- * Unification modulo AC unifyLTerm , unifyLNTerm - - -- * matching modulo AC - , matchLTerm - , matchLNTerm + , unifiableLNTerms , unifyLTermFactored , unifyLNTermFactored + -- * matching modulo AC + -- ** Constructing matching problems + , matchLVar + + -- ** Solving matching problems + , solveMatchLTerm + , solveMatchLNTerm + -- * Handles to a Maude process , MaudeHandle , WithMaude @@ -109,6 +114,9 @@ -- unifyLNTerm eqs = reader $ \hnd -> (\res -> DT.trace (show ("unify", res, eqs)) res) $ unifyLTerm sortOfName eqs `runReader` hnd unifyLNTerm = unifyLTerm sortOfName +-- | 'True' iff the terms are unifiable. +unifiableLNTerms :: LNTerm -> LNTerm -> WithMaude Bool +unifiableLNTerms t1 t2 = (not . null) <$> unifyLNTerm [Equal t1 t2] -- | Flatten a factored substitution to a list of substitutions. flattenUnif :: IsConst c => (LSubst c, [LSubstVFresh c]) -> [LSubstVFresh c] @@ -117,26 +125,40 @@ -- Matching modulo AC ---------------------------------------------------------------------- +-- | Match an 'LVar' term to an 'LVar' pattern. +matchLVar :: LVar -> LVar -> Match (LTerm c) +matchLVar t p = varTerm t `matchWith` varTerm p --- | @matchLNTerm sortOf eqs@ returns a complete set of matchers for @eqs@ modulo AC. -matchLTerm :: (IsConst c , Show (Lit c LVar), Ord c) +-- | @solveMatchLNTerm sortOf eqs@ returns a complete set of matchers for +-- @eqs@ modulo AC. +solveMatchLTerm :: (IsConst c , Show (Lit c LVar), Ord c) => (c -> LSort) - -> [Match (LTerm c)] + -> Match (LTerm c) -> WithMaude [Subst c LVar] -matchLTerm sortOf eqs = - reader $ \h -> (\res -> trace (unlines $ ["matchLTerm: "++ show eqs, "result = "++ show res]) res) $ - case runState (runErrorT match) M.empty of - (Left NoMatch,_) -> [] - (Left ACProblem, _) -> unsafePerformIO (UM.matchViaMaude h sortOf eqs) - (Right _, mappings) -> [substFromMap mappings] +solveMatchLTerm sortOf matchProblem = + case flattenMatch matchProblem of + Nothing -> pure [] + Just ms -> reader $ matchTerms ms where - match = sequence [ matchRaw sortOf t p | MatchWith t p <- eqs ] + trace' res = trace + (unlines $ ["matchLTerm: "++ show matchProblem, "result = "++ show res]) + res + matchTerms ms hnd = + trace' $ case runState (runErrorT match) M.empty of + (Left NoMatcher, _) -> [] + (Left ACProblem, _) -> + unsafePerformIO (UM.matchViaMaude hnd sortOf matchProblem) + (Right (), mappings) -> [substFromMap mappings] + where + match = forM_ ms $ \(t, p) -> matchRaw sortOf t p --- | @matchLNTerm eqs@ returns a complete set of matchers for @eqs@ modulo AC. -matchLNTerm :: [Match LNTerm] -> WithMaude [Subst Name LVar] -matchLNTerm = matchLTerm sortOfName +-- | @solveMatchLNTerm eqs@ returns a complete set of matchers for @eqs@ +-- modulo AC. +solveMatchLNTerm :: Match LNTerm -> WithMaude [Subst Name LVar] +solveMatchLNTerm = solveMatchLTerm sortOfName + -- Free unification with lazy AC-equation solving. -------------------------------------------------------------------- @@ -154,7 +176,7 @@ (Lit (Var vl), Lit (Var vr)) | vl == vr -> return () | otherwise -> case (lvarSort vl, lvarSort vr) of - (sl, sr) | sl == sr -> if vl < vr then elim vr l + (sl, sr) | sl == sr -> if vl < vr then elim vr l else elim vl r _ | sortGeqLTerm sortOf vl r -> elim vl r -- If unification can succeed here, then it must work by @@ -177,7 +199,7 @@ -- all unifiable pairs of term constructors have been enumerated _ -> mzero -- no unifier where - elim v t + elim v t | v `occurs` t = mzero -- no unifier | otherwise = do sortOf <- ask @@ -185,14 +207,14 @@ modify (M.insert v t . M.map (applyVTerm (substFromList [(v,t)]))) -data MatchFailure = NoMatch | ACProblem +data MatchFailure = NoMatcher | ACProblem instance Error MatchFailure where - strMsg _ = NoMatch + strMsg _ = NoMatcher --- | Ensure that the computed substitution @sigma@ satisfies +-- | Ensure that the computed substitution @sigma@ satisfies -- @t ==_AC apply sigma p@ after the delayed equations are solved. -matchRaw :: IsConst c +matchRaw :: IsConst c => (c -> LSort) -> LTerm c -- ^ Term @t@ -> LTerm c -- ^ Pattern @p@. @@ -205,10 +227,10 @@ case M.lookup vp mappings of Nothing -> do unless (sortGeqLTerm sortOf vp t) $ - throwError NoMatch + throwError NoMatcher modify (M.insert vp t) Just tp | t == tp -> return () - | otherwise -> throwError NoMatch + | otherwise -> throwError NoMatcher (viewTerm -> Lit (Con ct), viewTerm -> Lit (Con cp)) -> guard (ct == cp) (viewTerm -> FApp (NonAC tfsym) targs, viewTerm -> FApp (NonAC pfsym) pargs) -> @@ -220,7 +242,7 @@ (viewTerm -> FApp (AC _) _, viewTerm -> FApp (AC _) _) -> throwError ACProblem -- all matchable pairs of term constructors have been enumerated - _ -> throwError NoMatch + _ -> throwError NoMatcher -- | @sortGreaterEq v t@ returns @True@ if the sort ensures that the sort of @v@ is greater or equal to diff --git a/src/Term/UnitTests.hs b/src/Term/UnitTests.hs --- a/src/Term/UnitTests.hs +++ b/src/Term/UnitTests.hs @@ -3,7 +3,7 @@ -- | -- 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. @@ -44,7 +44,7 @@ , 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) + , testTrue "e" $ null (solveMatchLNTerm (pair(x1,x2) `matchWith` pair(x1,x1)) `runReader` hnd) ] where t1 = expo (inv(pair(f1,f2)), f2 # (inv f2) # f3 # f4 # f2) @@ -52,7 +52,7 @@ 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 + where substs = solveMatchLNTerm (t1 `matchWith` p) `runReader` mhnd @@ -179,7 +179,7 @@ , 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]) diff --git a/src/Term/VTerm.hs b/src/Term/VTerm.hs --- a/src/Term/VTerm.hs +++ b/src/Term/VTerm.hs @@ -2,7 +2,7 @@ -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- Terms with variables and constants. @@ -19,6 +19,10 @@ , constsVTerm , isVar + -- ** Destructors + , termVar + , termVar' + , IsVar , IsConst , module Term.Term @@ -37,6 +41,8 @@ import Extension.Prelude +import Safe (fromJustNote) + import Term.Term ---------------------------------------------------------------------- @@ -94,7 +100,7 @@ -- | @varTerm v@ is the 'VTerm' with the variable @v@. varTerm :: v -> VTerm c v -varTerm = lit . Var +varTerm = lit . Var -- | @constTerm c@ is the 'VTerm' with the const @c@. constTerm :: c -> VTerm c v @@ -118,6 +124,21 @@ constsVTerm = sortednub . D.toList . foldMap fLit where fLit (Var _) = mempty fLit (Con n) = return n + +-- Destructors +-------------- + +-- | Extract just the variable from a term that may be variable. +termVar :: VTerm c v -> Maybe v +termVar (viewTerm -> Lit (Var v)) = Just v +termVar _ = Nothing + +-- | Extract just the variable from a term that must be variable, throw an +-- error if this fails. +termVar' :: (Show c, Show v) => VTerm c v -> v +termVar' t = + fromJustNote ("termVar': non-variable term " ++ show t) (termVar t) + -- Derived instances -------------------- 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.4.1.0 +version: 0.6.0.0 license: GPL license-file: LICENSE category: Theorem Provers @@ -15,7 +15,7 @@ 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 @@ -26,6 +26,10 @@ homepage: http://www.infsec.ethz.ch/research/software#TAMARIN +source-repository head + type: git + location: https://github.com/tamarin-prover/tamarin-prover.git + ---------------------- -- library stanzas ---------------------- @@ -51,8 +55,8 @@ , derive == 2.5.* , HUnit == 1.2.* - - , tamarin-prover-utils == 0.4.1.* + + , tamarin-prover-utils == 0.6.* hs-source-dirs: src