tamarin-prover-term 0.4.1.0 → 0.6.0.0

raw patch · 10 files changed

+397/−178 lines, 10 filesdep ~tamarin-prover-utilsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: tamarin-prover-utils

API changes (from Hackage documentation)

Files

• src/Term/LTerm.hs +154/−71
• src/Term/Maude/Process.hs +19/−16
• src/Term/Rewriting/Definitions.hs +69/−18
• src/Term/Rewriting/Norm.hs +22/−19
• src/Term/Substitution/SubstVFree.hs +30/−7
• src/Term/Subsumption.hs +19/−10
• src/Term/Unification.hs +49/−27
• src/Term/UnitTests.hs +4/−4
• src/Term/VTerm.hs +23/−2
• tamarin-prover-term.cabal +8/−4

@@ -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 <beschmi@gmail.com> -- -- 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

@@ -4,7 +4,7 @@ -- | -- Copyright   : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- 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

@@ -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 <beschmi@gmail.com> -- -- 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

@@ -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 <beschmi@gmail.com> -- -- 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.

@@ -6,7 +6,7 @@ -- | -- Copyright   : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- 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.

@@ -4,7 +4,7 @@ -- | -- Copyright   : (c) 2010, 2011 Benedikt Schmidt -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- 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

@@ -2,7 +2,7 @@ -- | -- Copyright   : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- 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

@@ -3,7 +3,7 @@ -- | -- Copyright   : (c) 2012 Benedikt Schmidt -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- Unit tests for the functions dealing with term algebra and related notions.@@ -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])

@@ -2,7 +2,7 @@ -- | -- Copyright   : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- 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 --------------------

@@ -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-                    (<hackage.haskell.org/package/tamarin-prover>). +                    (<hackage.haskell.org/package/tamarin-prover>).                     .                     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