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 @@ -1,5 +1,5 @@ -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -11,36 +11,38 @@ import Term.LTerm import Term.Builtin.Signature --- +---------------------------------------------------------------------- -- Shorter syntax for Term constructors ---------------------------------------------------------------------- (*:) :: Ord a => Term a -> Term a -> Term a -b *: e = fAppMult [b,e] +b *: e = fAppAC Mult [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] +b # e = fAppAC Union [b,e] 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] +adec (a,b) = fAppNoEq adecSym [a,b] +aenc (a,b) = fAppNoEq aencSym [a,b] +sdec (a,b) = fAppNoEq sdecSym [a,b] +senc (a,b) = fAppNoEq sencSym [a,b] +sign (a,b) = fAppNoEq signSym [a,b] verify :: Ord a => (Term a,Term a,Term a) -> Term a -verify (a,b,c) = fAppNonAC verifySym [a,b,c] +verify (a,b,c) = fAppNoEq verifySym [a,b,c] pk :: Ord a => Term a -> Term a -pk a = fAppNonAC pkSym [a] +pk a = fAppNoEq pkSym [a] trueC :: Ord a => Term a -trueC = fAppNonAC trueSym [] +trueC = fAppNoEq trueSym [] var :: String -> Integer -> LNTerm var s i = varTerm $ LVar s LSortMsg i +---------------------------------------------------------------------- +-- Predefined variables and names +---------------------------------------------------------------------- + x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 :: LNTerm x0 = var "x" 0 x1 = var "x" 1 @@ -175,25 +177,3 @@ 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 -ls2 = LVar "s2" LSortMSet 0 -ls3 = LVar "s3" LSortMSet 0 -ls4 = LVar "s4" LSortMSet 0 -ls5 = LVar "s5" LSortMSet 0 -ls6 = LVar "s6" LSortMSet 0 -ls7 = LVar "s7" LSortMSet 0 -ls8 = LVar "s8" LSortMSet 0 -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 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 @@ -1,5 +1,5 @@ -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -9,7 +9,7 @@ -- * Rewriting rules RRule(..) , dhRules - , xorRules + , bpRules , msetRules , pairRules , symEncRules @@ -54,19 +54,26 @@ inv = fAppInv one = fAppOne --- | The rewriting rules for Xor. -xorRules :: Set (RRule LNTerm) -xorRules = S.fromList - [ x1 +: x1 `RRule` zero - , x1 +: zero `RRule` x1 - , x1 +: (x1 +: x2) `RRule` x2 ] +-- | The rewriting rules for bilinear pairing. These rules extend the +-- the rules for Diffie-Hellman. +bpRules :: Set (RRule LNTerm) +bpRules = S.fromList + [ pmult(one,x1) `RRule` x1 + -- x1 and x2 are scalars, x3 is a point on an elliptic curve + , pmult(x3,pmult(x2,x1)) `RRule` pmult(x3 *: x2, x1) + + -- em is commutative, so this rule is sufficient + , em(x1, pmult(x2,x3)) `RRule` expo(em(x1,x3), x2) + ] where - zero = fAppZero + one = fAppOne + expo = fAppExp + pmult = fAppPMult + em = fAppEMap -- | The rewriting rules for multisets. msetRules :: Set (RRule LNTerm) -msetRules = S.fromList [ s1 # fAppEmpty `RRule` s1 ] - +msetRules = S.empty -- | The rewriting rules for standard subterm operators that are builtin. pairRules, symEncRules, asymEncRules, signatureRules :: Set (StRule) 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,6 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -11,44 +11,47 @@ import Term.LTerm import qualified Data.Set as S +---------------------------------------------------------------------- -- Builtin symbols (pair and inv are defined in Term.Term) ---------------------------------------------------------------------- --- | Binary builtin non-ac function symbols. -sdecSym, sencSym, adecSym, aencSym, signSym :: NonACSym -sdecSym = ("sdec",2) -sencSym = ("senc",2) -adecSym = ("adec",2) -aencSym = ("aenc",2) -signSym = ("sign",2) +-- | Binary builtin function symbols. +sdecSym, sencSym, adecSym, aencSym, signSym :: NoEqSym +sdecSym = ("sdec",(2, Public)) +sencSym = ("senc",(2, Public)) +adecSym = ("adec",(2, Public)) +aencSym = ("aenc",(2, Public)) +signSym = ("sign",(2, Public)) -verifySym :: NonACSym -verifySym = ("verify",3) +-- | Ternary builtin function symbols. +verifySym :: NoEqSym +verifySym = ("verify",(3, Public)) --- | Unary builtin non-ac function symbols. -pkSym, hashSym :: NonACSym -pkSym = ("pk",1) -hashSym = ("h",1) +-- | Unary builtin function symbols. +pkSym, hashSym :: NoEqSym +pkSym = ("pk",(1, Public)) +hashSym = ("h",(1, Public)) --- | Nullary builtin non-ac function symbols. -trueSym :: NonACSym -trueSym = ("true",0) +-- | Nullary builtin function symbols. +trueSym :: NoEqSym +trueSym = ("true",(0, Public)) +---------------------------------------------------------------------- -- Builtin signatures ---------------------------------------------------------------------- -- | The signature for symmetric encryption. -symEncFunSig :: FunSig -symEncFunSig = S.fromList [ sdecSym, sencSym ] +symEncFunSig :: NoEqFunSig +symEncFunSig = S.fromList $ [ sdecSym, sencSym ] -- | The signature for asymmetric encryption. -asymEncFunSig :: FunSig -asymEncFunSig = S.fromList [ adecSym, aencSym, pkSym ] +asymEncFunSig :: NoEqFunSig +asymEncFunSig = S.fromList $ [ adecSym, aencSym, pkSym ] -- | The signature for cryptographic signatures. -signatureFunSig :: FunSig -signatureFunSig = S.fromList [ signSym, verifySym, trueSym, pkSym ] +signatureFunSig :: NoEqFunSig +signatureFunSig = S.fromList $ [ signSym, verifySym, trueSym, pkSym ] -- | The signature for hashing. -hashFunSig :: FunSig +hashFunSig :: NoEqFunSig hashFunSig = S.fromList [ hashSym ] diff --git a/src/Term/Classes.hs b/src/Term/Classes.hs deleted file mode 100644 --- a/src/Term/Classes.hs +++ /dev/null @@ -1,14 +0,0 @@ --- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier --- License : GPL v3 (see LICENSE) --- --- Maintainer : Benedikt Schmidt --- --- | A type class for sized types. -module Term.Classes where - -class Sized a where - size :: a -> Int - -instance Sized a => Sized [a] where - size = sum . map size diff --git a/src/Term/LTerm.hs b/src/Term/LTerm.hs --- a/src/Term/LTerm.hs +++ b/src/Term/LTerm.hs @@ -11,7 +11,7 @@ {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} -- spurious warnings for view patterns -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier +-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -46,8 +46,13 @@ , sortCompare , sortOfLTerm , sortOfLNTerm + , sortOfLit , isMsgVar , isFreshVar + , isSimpleTerm + , niFactors + , containsPrivate + , neverContainsFreshPriv -- ** Destructors , ltermVar @@ -74,6 +79,8 @@ , renameAvoiding , avoidPrecise , renamePrecise + , renameDropNamehint + , varOccurences -- * BVar , BVar(..) @@ -106,12 +113,13 @@ import Data.Binary import qualified Data.DList as D import Data.DeriveTH -import Data.Foldable hiding (concatMap, elem) +import Data.Foldable hiding (concatMap, elem, notElem, any) import Data.Generics hiding (GT) import qualified Data.Map as M import Data.Monoid import qualified Data.Set as S import Data.Traversable +import qualified Data.ByteString.Char8 as BC import Safe (fromJustNote) @@ -126,21 +134,17 @@ -- | 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 +-- Partial order: Node Msg -- / \ -- Pub Fresh sortCompare :: LSort -> LSort -> Maybe Ordering @@ -149,10 +153,7 @@ -- 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 + -- Msg is greater than all sorts except Node (LSortMsg, _ ) -> Just GT (_, LSortMsg ) -> Just LT -- The remaining combinations (Pub/Fresh) are incomparable @@ -164,7 +165,6 @@ sortPrefix LSortFresh = "~" sortPrefix LSortPub = "$" sortPrefix LSortNode = "#" -sortPrefix LSortMSet = "%" -- | @sortSuffix s@ is the suffix we use for annotating variables of sort @s@. sortSuffix :: LSort -> String @@ -172,7 +172,6 @@ sortSuffix LSortFresh = "fresh" sortSuffix LSortPub = "pub" sortSuffix LSortNode = "node" -sortSuffix LSortMSet = "mset" ------------------------------------------------------------------------------ @@ -258,14 +257,18 @@ 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 sortOfLNTerm = sortOfLTerm sortOfName +-- | Returns the most precise sort of a 'Lit'. +sortOfLit :: Lit Name LVar -> LSort +sortOfLit (Con n) = sortOfName n +sortOfLit (Var v) = lvarSort v + + -- | Is a term a message variable? isMsgVar :: LNTerm -> Bool isMsgVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortMsg) @@ -276,8 +279,34 @@ isFreshVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortFresh) isFreshVar _ = False +-- | The non-inverse factors of a term. +niFactors :: LNTerm -> [LNTerm] +niFactors t = case viewTerm2 t of + FMult ts -> concatMap niFactors ts + FInv t1 -> niFactors t1 + _ -> [t] +-- | @containsPrivate t@ returns @True@ if @t@ contains private function symbols. +containsPrivate :: Term t -> Bool +containsPrivate t = case viewTerm t of + Lit _ -> False + FApp (NoEq (_,(_,Private))) _ -> True + FApp _ as -> any containsPrivate as +-- | 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, fresh variables, or private function symbols. +isSimpleTerm :: LNTerm -> Bool +isSimpleTerm t = + not (containsPrivate t) && + (getAll . foldMap (All . (LSortFresh /=) . sortOfLit) $ t) + +-- | 'True' iff no instance of this term contains fresh names or private function symbols. +neverContainsFreshPriv :: LNTerm -> Bool +neverContainsFreshPriv t = + not (containsPrivate t) && + (getAll . foldMap (All . (`notElem` [LSortMsg, LSortFresh]) . sortOfLit) $ t) + -- Destructors -------------- @@ -303,7 +332,6 @@ ltermNodeId' = ltermVar' LSortNode - -- BVar: Bound variables ------------------------ @@ -369,7 +397,7 @@ instance Eq LVar where (LVar n1 s1 i1) == (LVar n2 s2 i2) = i1 == i2 && s1 == s2 && n1 == n2 --- An ord instane that prefers the 'lvarIdx' over the 'lvarName'. +-- An ord instance that prefers the 'lvarIdx' over the 'lvarName'. instance Ord LVar where compare (LVar x1 x2 x3) (LVar y1 y2 y3) = compare x3 y3 & compare x2 y2 & compare x1 y1 & EQ @@ -392,27 +420,34 @@ -- Managing bound and free LVars ------------------------------------------------------------------------------ + +-- | This type captures the occurence of a variable in a certain context. +type Occurence = [String] + -- | 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 +-- 'LVar's and arbitrary functions. For a monotone f, if @x <= y@, then +-- @f x <= f y@. 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'. +-- be collected using 'foldFrees' and 'foldFreesOcc' and mapped in the context +-- of an applicative 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 -- Haskell types assume that all variables free in all type arguments are free. +-- The 'foldFreesOcc' is only used to define the function 'varOccurences'. See +-- below for required properties of the instance methods. -- -- Once we need it, we can use type synonym instances to parametrize over the -- variable type. -- class HasFrees t where foldFrees :: Monoid m => (LVar -> m ) -> t -> m + foldFreesOcc :: Monoid m => (Occurence -> LVar -> m) -> Occurence -> t -> m mapFrees :: Applicative f => MonotoneFunction f -> t -> f t -- | @v `occurs` t@ iff variable @v@ occurs as a free variable in @t@. @@ -432,6 +467,17 @@ frees :: HasFrees t => t -> [LVar] frees = sortednub . freesList +-- | Returns the variables occuring in @t@ together with the contexts they appear in. +-- Note that certain contexts (and variables only occuring in such contexts) are +-- ignored by this function. +-- The function is used to "guess" renamings of variables, i.e., if t is a renaming of s, +-- then variables that occur in equal contexts in t and s are probably renamings of +-- each other. +varOccurences :: HasFrees a => a -> [(LVar, S.Set Occurence)] +varOccurences t = + map (\((v,ctx1):rest) -> (v, S.fromList (ctx1:(map snd rest)))) . groupOn fst . sortOn fst + . foldFreesOcc (\ c v -> [(v,c)]) [] $ t + -- | @someInst t@ returns an instance of @t@ where all free variables whose -- binding is not yet determined by the caller are replaced with fresh -- variables. @@ -502,18 +548,28 @@ renamePrecise :: (MonadFresh m, HasFrees a) => a -> m a renamePrecise x = evalBindT (someInst x) noBindings + +renameDropNamehint :: (MonadFresh m, MonadBind LVar LVar m, HasFrees a) => a -> m a +renameDropNamehint = + mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x "") + + -- Instances ------------ instance HasFrees LVar where foldFrees = id - mapFrees (Arbitrary f) = f - mapFrees (Monotone f) = f + foldFreesOcc f c v = f c v + 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 + foldFreesOcc f c (Var x) = foldFreesOcc f c x + foldFreesOcc _ _ _ = mempty + mapFrees f (Var x) = Var <$> mapFrees f x mapFrees _ l = pure l @@ -521,86 +577,117 @@ foldFrees _ (Bound _) = mempty foldFrees f (Free v) = foldFrees f v + foldFreesOcc _ _ (Bound _) = mempty + foldFreesOcc f c (Free v) = foldFreesOcc f c v + mapFrees _ b@(Bound _) = pure b mapFrees f (Free v) = Free <$> mapFrees f v instance (HasFrees l, Ord l) => HasFrees (Term l) where - foldFrees f = foldMap (foldFrees 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 + foldFrees f = foldMap (foldFrees f) + foldFreesOcc f c t = case viewTerm t of + Lit l -> foldFreesOcc f c l + FApp (NoEq o) as -> foldFreesOcc f ((BC.unpack . fst $ o):c) as + FApp o as -> mconcat $ map (foldFreesOcc f (show o:c)) as + -- AC or C symbols + + 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) - mapFrees f = traverse (mapFrees f) + foldFrees f = foldMap (foldFrees f) + foldFreesOcc f p (Equal a b) = foldFreesOcc f p (a,b) + mapFrees f = traverse (mapFrees f) instance HasFrees a => HasFrees (Match a) where - foldFrees f = foldMap (foldFrees f) - mapFrees f = traverse (mapFrees f) + foldFrees f = foldMap (foldFrees f) + foldFreesOcc _ _ NoMatch = mempty + foldFreesOcc f p (DelayedMatches ms) = foldFreesOcc f p ms + mapFrees f = traverse (mapFrees f) instance HasFrees a => HasFrees (RRule a) where - foldFrees f = foldMap (foldFrees f) - mapFrees f = traverse (mapFrees f) - + foldFrees f = foldMap (foldFrees f) + foldFreesOcc f p (RRule a b) = foldFreesOcc f p (a,b) + mapFrees f = traverse (mapFrees f) instance HasFrees () where - foldFrees _ = const mempty - mapFrees _ = pure + foldFrees _ = const mempty + foldFreesOcc _ _ = const mempty + mapFrees _ = pure instance HasFrees Int where - foldFrees _ = const mempty - mapFrees _ = pure + foldFrees _ = const mempty + foldFreesOcc _ _ = const mempty + mapFrees _ = pure instance HasFrees Integer where - foldFrees _ = const mempty - mapFrees _ = pure + foldFrees _ = const mempty + foldFreesOcc _ _ = const mempty + mapFrees _ = pure instance HasFrees Bool where - foldFrees _ = const mempty - mapFrees _ = pure + foldFrees _ = const mempty + foldFreesOcc _ _ = const mempty + mapFrees _ = pure instance HasFrees Char where - foldFrees _ = const mempty - mapFrees _ = pure + foldFrees _ = const mempty + foldFreesOcc _ _ = const mempty + mapFrees _ = pure instance HasFrees a => HasFrees (Maybe a) where - foldFrees f = foldMap (foldFrees f) - mapFrees f = traverse (mapFrees f) + foldFrees f = foldMap (foldFrees f) + foldFreesOcc _ _ Nothing = mempty + foldFreesOcc f p (Just x) = foldFreesOcc f p x + mapFrees f = traverse (mapFrees f) instance (HasFrees a, HasFrees b) => HasFrees (Either a b) where - foldFrees f = either (foldFrees f) (foldFrees f) - mapFrees f = either (fmap Left . mapFrees f) (fmap Right . mapFrees f) + foldFrees f = either (foldFrees f) (foldFrees f) + foldFreesOcc f p = either (foldFreesOcc f ("0":p)) (foldFreesOcc f ("1":p)) + mapFrees f = either (fmap Left . mapFrees f) (fmap Right . mapFrees f) instance (HasFrees a, HasFrees b) => HasFrees (a, b) where - foldFrees f (x, y) = foldFrees f x `mappend` foldFrees f y - mapFrees f (x, y) = (,) <$> mapFrees f x <*> mapFrees f y + foldFrees f (x, y) = foldFrees f x `mappend` foldFrees f y + foldFreesOcc f p (x, y) = foldFreesOcc f ("0":p) x `mappend` foldFreesOcc f ("1":p) y + mapFrees f (x, y) = (,) <$> mapFrees f x <*> mapFrees f y 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) = + foldFrees f (x, y, z) = foldFrees f (x, (y, z)) + foldFreesOcc f p (x, y, z) = + foldFreesOcc f ("0":p) x `mappend` foldFreesOcc f ("1":p) y `mappend` foldFreesOcc f ("2":p) z + mapFrees f (x0, y0, z0) = (\(x, (y, z)) -> (x, y, z)) <$> mapFrees f (x0, (y0, z0)) instance HasFrees a => HasFrees [a] where - foldFrees f = foldMap (foldFrees f) - mapFrees f = traverse (mapFrees f) + foldFrees f = foldMap (foldFrees f) + foldFreesOcc f c xs = mconcat $ (map (\(i,x) -> foldFreesOcc f (show i:c) x)) $ zip [(0::Int)..] xs + mapFrees f = traverse (mapFrees f) instance HasFrees a => HasFrees (Disj a) where - foldFrees f = foldMap (foldFrees f) - mapFrees f = traverse (mapFrees f) + foldFrees f = foldMap (foldFrees f) + foldFreesOcc f p d = foldFreesOcc f p (getDisj d) + mapFrees f = traverse (mapFrees f) instance HasFrees a => HasFrees (Conj a) where - foldFrees f = foldMap (foldFrees f) - mapFrees f = traverse (mapFrees f) + foldFrees f = foldMap (foldFrees f) + foldFreesOcc f p c = foldFreesOcc f p (getConj c) + mapFrees f = traverse (mapFrees f) instance (Ord a, HasFrees a) => HasFrees (S.Set a) where - foldFrees f = foldMap (foldFrees f) - mapFrees f = fmap S.fromList . mapFrees f . S.toList + foldFrees f = foldMap (foldFrees f) + foldFreesOcc f p = foldMap (foldFreesOcc f ("0":p)) + mapFrees f = fmap S.fromList . mapFrees f . S.toList instance (Ord k, HasFrees k, HasFrees v) => HasFrees (M.Map k v) where - foldFrees f = M.foldrWithKey combine mempty + foldFrees f = M.foldrWithKey combine mempty where combine k v m = foldFrees f k `mappend` (foldFrees f v `mappend` m) - mapFrees f = fmap M.fromList . mapFrees f . M.toList + foldFreesOcc f p = M.foldrWithKey combine mempty + where + combine k v m = foldFreesOcc f p (k,v) `mappend` m + mapFrees f = fmap M.fromList . mapFrees f . M.toList ------------------------------------------------------------------------------ diff --git a/src/Term/Maude/Parser.hs b/src/Term/Maude/Parser.hs --- a/src/Term/Maude/Parser.hs +++ b/src/Term/Maude/Parser.hs @@ -1,6 +1,4 @@ -{-# OPTIONS_GHC -fno-warn-unused-do-bind #-} -{-# LANGUAGE TemplateHaskell, FlexibleContexts, TupleSections #-} -{-# LANGUAGE ViewPatterns, NamedFieldPuns #-} +{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE OverloadedStrings #-} -- | -- Copyright : (c) 2010, 2011 Benedikt Schmidt @@ -50,7 +48,6 @@ LSortFresh -> "Fresh" LSortMsg -> "Msg" LSortNode -> "Node" - LSortMSet -> "MSet" ppLSortSym :: LSort -> ByteString ppLSortSym lsort = case lsort of @@ -58,7 +55,6 @@ LSortPub -> "p" LSortMsg -> "c" LSortNode -> "n" - LSortMSet -> "m" parseLSortSym :: ByteString -> Maybe LSort parseLSortSym s = case s of @@ -66,7 +62,6 @@ "p" -> Just LSortPub "c" -> Just LSortMsg "n" -> Just LSortNode - "m" -> Just LSortMSet _ -> Nothing -- | Used to prevent clashes with predefined Maude function symbols @@ -74,37 +69,43 @@ funSymPrefix :: ByteString funSymPrefix = "tamX" +-- | Prefix for private function symbols. +funSymPrefixPriv :: ByteString +funSymPrefixPriv = "tamP" + -- | 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" + funSymPrefix <> case o of + Mult -> "mult" + Union -> "mun" --- | Pretty print an AC symbol for Maude. -ppMaudeNonACSym :: NonACSym -> ByteString -ppMaudeNonACSym (o,_) = funSymPrefix <> o +-- | Pretty print a non-AC symbol for Maude. +ppMaudeNoEqSym :: NoEqSym -> ByteString +ppMaudeNoEqSym (o,(_,Private)) = funSymPrefixPriv <> o +ppMaudeNoEqSym (o,(_,Public)) = funSymPrefix <> o +-- | Pretty print a C symbol for Maude. +ppMaudeCSym :: CSym -> ByteString +ppMaudeCSym EMap = funSymPrefix <> emapSymString + -- | @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 <> ")" + FApp (NoEq fsym) [] -> ppMaudeNoEqSym fsym + FApp (NoEq fsym) as -> ppMaudeNoEqSym fsym <> ppArgs as + FApp (C fsym) as -> ppMaudeCSym fsym <> ppArgs as + FApp (AC op) as -> ppMaudeACSym op <> ppArgs as + FApp List as -> "list(" <> ppList as <> ")" where + ppArgs as = "(" <> (B.intercalate "," (map ppMaude as)) <> ")" ppInt = BC.pack . show - ppList [] = funSymPrefix <> "nil" - ppList (x:xs) = funSymPrefix <> "cons(" <> ppMaude x <> "," <> ppList xs <> ")" + ppList [] = "nil" + ppList (x:xs) = "cons(" <> ppMaude x <> "," <> ppList xs <> ")" ------------------------------------------------------------------------------ -- Pretty printing a 'MaudeSig' as a Maude functional module. @@ -114,19 +115,9 @@ 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 ." + , " protecting NAT ." + , " sort Pub Fresh Msg Node TOP ." + , " subsort Pub < Msg ." , " subsort Fresh < Msg ." , " subsort Msg < TOP ." , " subsort Node < TOP ." @@ -137,32 +128,40 @@ , " 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 ." ] + , " op list : TOP -> TOP ." + , " op cons : TOP TOP -> TOP ." + , " op nil : -> TOP ." ] ++ + (if enableMSet msig + then + [ theoryOp "mun : Msg Msg -> Msg [comm assoc]" ] + else []) + ++ (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 ." ] + [ theoryOp "one : -> Msg" + , theoryOp "exp : Msg Msg -> Msg" + , theoryOp "mult : Msg Msg -> Msg [comm assoc]" + , theoryOp "inv : Msg -> Msg" ] else []) ++ - (if enableXor msig + (if enableBP msig then - [ " op " <> funSymPrefix <> "zero : -> Msg ." - , " op " <> funSymPrefix <> "xor : Msg Msg -> Msg [comm assoc] ."] + [ theoryOp "pmult : Msg Msg -> Msg" + , theoryOp "em : Msg Msg -> Msg [comm]" ] else []) ++ - map theoryFunSym (S.toList $ functionSymbols msig) + map theoryFunSym (S.toList $ stFunSyms msig) ++ map theoryRule (S.toList $ rrulesForMaudeSig msig) ++ [ "endfm" ] where - theoryFunSym (s,ar) = - " op " <> funSymPrefix <> s <> " : " <> (B.concat $ replicate ar "Msg ") <> " -> Msg ." + theoryOpNoEq priv fsort = + " op " <> (if (priv==Private) then funSymPrefixPriv else funSymPrefix) <> fsort <>" ." + theoryOp = theoryOpNoEq Public + theoryFunSym (s,(ar,priv)) = + theoryOpNoEq priv (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 @@ -197,31 +196,26 @@ 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) - - + <|> string "M" *> -- FIXME: why? + ( string "sg" *> return LSortMsg ) -- | @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 "(" + choice [ do _ <- string "(" case parseLSortSym ident of Just s -> parseConst s Nothing -> parseFApp ident @@ -230,33 +224,42 @@ ] ] where + consSym = ("cons",(2,Public)) + nilSym = ("nil",(0,Public)) + + parseFunSym ident args + | op `elem` allowedfunSyms = op + | otherwise = + error $ "Maude.Parser.parseTerm: unknown function " + ++ "symbol `"++ show op ++"', not in " + ++show allowedfunSyms + where prefixLen = BC.length funSymPrefix + special = ident `elem` ["list", "cons", "nil" ] + priv = if (not special) && BC.isPrefixOf funSymPrefixPriv ident + then Private else Public + op = (if special then ident else BC.drop prefixLen ident + , ( length args, priv)) + allowedfunSyms = [consSym, nilSym]++(S.toList $ noEqFunSyms msig) + 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) + appIdent args | ident == ppMaudeACSym Mult = fAppAC Mult args + | ident == ppMaudeACSym Union = fAppAC Union args + | ident == ppMaudeCSym EMap = fAppC EMap args + appIdent [arg] | ident == "list" = fAppList (flattenCons arg) + appIdent args = fAppNoEq op args + where op = parseFunSym ident args - flattenCons (viewTerm -> FApp (NonAC ("cons",2)) [x,xs]) = x:flattenCons xs - flattenCons (viewTerm -> FApp (NonAC ("nil",0)) []) = [] - flattenCons t = [t] + flattenCons (viewTerm -> FApp (NoEq s) [x,xs]) | s == consSym = x:flattenCons xs + flattenCons (viewTerm -> FApp (NoEq s) []) | s == nilSym = [] + flattenCons t = [t] - parseFAppConst ident = return $ ensureValidOp op (fAppNonAC op []) - where op = (BC.drop prefixLen ident,0) + parseFAppConst ident = return $ fAppNoEq (parseFunSym ident []) [] 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,8 +1,8 @@ -{-# LANGUAGE TemplateHaskell, DeriveDataTypeable, DeriveFunctor #-} -{-# LANGUAGE FlexibleContexts, NamedFieldPuns, BangPatterns #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE BangPatterns #-} {-# LANGUAGE OverloadedStrings #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier +-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -182,7 +182,6 @@ Left e -> fail $ "\ncomputeViaMaude:\nParse error: `" ++ e ++"'"++ "\nFor Maude Output: `" ++ BC.unpack reply ++"'"++ "\nFor query: `" ++ BC.unpack cmd++"'" - ------------------------------------------------------------------------------ -- Unification modulo AC diff --git a/src/Term/Maude/Signature.hs b/src/Term/Maude/Signature.hs --- a/src/Term/Maude/Signature.hs +++ b/src/Term/Maude/Signature.hs @@ -1,39 +1,39 @@ -{-# OPTIONS_GHC -fno-warn-unused-do-bind #-} -{-# LANGUAGE TemplateHaskell, FlexibleContexts, TupleSections #-} -{-# LANGUAGE ViewPatterns, NamedFieldPuns #-} -{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE NamedFieldPuns #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt -- --- Euqatiuonal signatures for Maude. +-- Equational signatures for Maude. module Term.Maude.Signature ( -- * Maude signatures MaudeSig , enableDH - , enableXor + , enableBP , enableMSet - , functionSymbols + , stFunSyms , stRules - , allFunctionSymbols - , irreducibleFunctionSymbols + , funSyms + , irreducibleFunSyms , rrulesForMaudeSig + , noEqFunSyms -- * predefined maude signatures , dhMaudeSig - , xorMaudeSig , pairMaudeSig , asymEncMaudeSig , symEncMaudeSig , signatureMaudeSig , hashMaudeSig , msetMaudeSig + , bpMaudeSig , minimalMaudeSig -- * extend maude signatures - , addFunctionSymbol + , addFunSym , addStRule -- * pretty printing @@ -66,57 +66,65 @@ -- | 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 + { enableDH :: Bool + , enableBP :: Bool + , enableMSet :: Bool + , stFunSyms :: S.Set NoEqSym -- ^ function signature for subterm theory + , stRules :: S.Set StRule -- ^ rewriting rules for subterm theory + + , funSyms :: FunSig -- ^ function signature including the + -- function symbols for DH, BP, and Multiset + -- can be computed from enableX and stFunSyms + , irreducibleFunSyms :: FunSig -- ^ irreducible function symbols (can be computed) } 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 +-- | Smart constructor for maude signatures. Computes funSyms and irreducibleFunSyms. +maudeSig :: MaudeSig -> MaudeSig +maudeSig msig@(MaudeSig {enableDH,enableBP,enableMSet,stFunSyms,stRules}) = + msig {enableDH=enableDH||enableBP, funSyms=allfuns, irreducibleFunSyms=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) + allfuns = (S.map NoEq stFunSyms) + `S.union` (if enableDH || enableBP then dhFunSig else S.empty) + `S.union` (if enableBP then bpFunSig else S.empty) + `S.union` (if enableMSet 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 + S.fromList [ o | StRule (viewTerm -> FApp o _) _ <- S.toList stRules ] + `S.union` dhReducibleFunSig `S.union` bpReducibleFunSig -- | 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 + (MaudeSig dh1 bp1 mset1 stFunSyms1 stRules1 _ _) `mappend` + (MaudeSig dh2 bp2 mset2 stFunSyms2 stRules2 _ _) = + maudeSig (mempty {enableDH=dh1||dh2 + ,enableBP=bp1||bp2 + ,enableMSet=mset1||mset2 + ,stFunSyms=S.union stFunSyms1 stFunSyms2 + ,stRules=S.union stRules1 stRules2}) + mempty = MaudeSig False False False S.empty S.empty S.empty S.empty +-- | Non-AC function symbols. +noEqFunSyms :: MaudeSig -> NoEqFunSig +noEqFunSyms msig = S.fromList [ o | NoEq o <- S.toList (funSyms msig) ] + -- | 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 +addFunSym :: NoEqSym -> MaudeSig -> MaudeSig +addFunSym funsym msig = + msig `mappend` mempty {stFunSyms=S.fromList [funsym]} -- | 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]) + msig `mappend` mempty {stRules=S.fromList [str]} --- | @rrulesForMaudeSig msig@ returns all rewriting rules including the rules --- for xor, dh, and multiset. +-- | Returns all rewriting rules including the rules +-- for DH, BP, and multiset. rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm) -rrulesForMaudeSig (MaudeSig {enableXor, enableDH, enableMSet, stRules}) = +rrulesForMaudeSig (MaudeSig {enableDH, enableBP, 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 enableBP then bpRules else S.empty) `S.union` (if enableMSet then msetRules else S.empty) ------------------------------------------------------------------------------ @@ -124,18 +132,18 @@ ------------------------------------------------------------------------------ -- | 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 +dhMaudeSig, bpMaudeSig, msetMaudeSig :: MaudeSig +dhMaudeSig = maudeSig $ mempty {enableDH=True} +bpMaudeSig = maudeSig $ mempty {enableBP=True} +msetMaudeSig = maudeSig $ mempty {enableMSet=True} -- | 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 +pairMaudeSig = maudeSig $ mempty {stFunSyms=pairFunSig,stRules=pairRules} +symEncMaudeSig = maudeSig $ mempty {stFunSyms=symEncFunSig,stRules=symEncRules} +asymEncMaudeSig = maudeSig $ mempty {stFunSyms=asymEncFunSig,stRules=asymEncRules} +signatureMaudeSig = maudeSig $ mempty {stFunSyms=signatureFunSig,stRules=signatureRules} +hashMaudeSig = maudeSig $ mempty {stFunSyms=hashFunSig} -- | The minimal maude signature. minimalMaudeSig :: MaudeSig @@ -148,7 +156,7 @@ prettyMaudeSig :: P.HighlightDocument d => MaudeSig -> d prettyMaudeSig sig = P.vcat [ ppNonEmptyList' "builtins:" P.text builtIns - , ppNonEmptyList' "functions:" ppFunSymb $ S.toList (functionSymbols sig) + , ppNonEmptyList' "functions:" ppFunSymb $ S.toList (stFunSyms sig) , ppNonEmptyList (\ds -> P.sep (P.keyword_ "equations:" : map (P.nest 2) ds)) prettyStRule $ S.toList (stRules sig) @@ -160,11 +168,13 @@ builtIns = asum $ map (\(f, x) -> guard (f sig) *> pure x) [ (enableDH, "diffie-hellman") - , (enableXor, "xor") + , (enableBP, "bilinear-pairing") , (enableMSet, "multiset") ] - ppFunSymb (f,k) = P.text $ BC.unpack f ++ "/" ++ show k + ppFunSymb (f,(k,priv)) = P.text $ BC.unpack f ++ "/" ++ show k ++ showPriv priv + where showPriv Private = " [private]" + showPriv Public = "" -- derived instances 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,9 +1,6 @@ -{-# OPTIONS_GHC -fno-warn-unused-do-bind #-} -{-# LANGUAGE TemplateHaskell, FlexibleContexts, TupleSections #-} -{-# LANGUAGE ViewPatterns, NamedFieldPuns #-} -{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE FlexibleContexts #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -25,20 +22,20 @@ ) where -import Term.Term -import Term.LTerm -import Term.Substitution +import Term.Term +import Term.LTerm +import Term.Substitution -import Utils.Misc +import Utils.Misc -import Control.Monad.Fresh -import Control.Monad.Bind -import Control.Applicative +import Control.Monad.Fresh +import Control.Monad.Bind +import Control.Applicative -import Data.Traversable hiding (mapM) -import Data.Maybe +import Data.Traversable hiding (mapM) +import Data.Maybe import qualified Data.Map as M -import Data.Map ( Map ) +import Data.Map (Map) -- Maude Terms ---------------------------------------------------------------------- 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 @@ -1,6 +1,5 @@ -{-# LANGUAGE FlexibleInstances #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -10,15 +9,15 @@ narrowSubsts ) where -import Term.Unification -import Term.Positions +import Term.Unification +import Term.Positions -import Control.Monad.Reader +import Control.Monad.Reader -import Extension.Prelude +import Extension.Prelude import qualified Data.Set as S -import Debug.Trace.Ignore +import Debug.Trace.Ignore -- Narrowing ---------------------------------------------------------------------- diff --git a/src/Term/Narrowing/Variants.hs b/src/Term/Narrowing/Variants.hs --- a/src/Term/Narrowing/Variants.hs +++ b/src/Term/Narrowing/Variants.hs @@ -1,5 +1,5 @@ -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt diff --git a/src/Term/Narrowing/Variants/Check.hs b/src/Term/Narrowing/Variants/Check.hs --- a/src/Term/Narrowing/Variants/Check.hs +++ b/src/Term/Narrowing/Variants/Check.hs @@ -1,5 +1,5 @@ -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -18,7 +18,7 @@ import Term.Substitution import Term.Unification import Term.Rewriting.Norm -import Term.Subsumption ( factorSubstVia, canonizeSubst ) +import Term.Subsumption (factorSubstVia,canonizeSubst) import Term.Narrowing.Narrow import Extension.Prelude @@ -94,7 +94,8 @@ -- in substs with s' <=_Var^t s. isMaximalIn :: LNSubstVFresh -> [LNSubstVFresh] -> LNTerm -> WithMaude Bool isMaximalIn s substs t = reader $ \hnd -> - all (\s' -> (\res -> trace (show ("isMaximal:", not res , "=", s, "<=", s')) res ) $not (leqSubstVariant t s s' `runReader` hnd)) substs + all (\s' -> (\res -> trace (show ("isMaximal:", not res , "=", s, "<=", s')) res ) $ + not (leqSubstVariant t s s' `runReader` hnd)) substs -- Minimality checking for a set of variants ---------------------------------------------------------------------- @@ -105,4 +106,5 @@ checkMinimal :: LNTerm -> [LNSubstVFresh] -> WithMaude Bool checkMinimal t substs = reader $ \hnd -> noDuplicates substs && - all (\s -> (\res -> trace (show (s,substs,res)) res) $ (`runReader` hnd) $ isMaximalIn s (delete s substs) t) substs + all (\s -> (\res -> trace (show (s,substs,res)) res) $ + (`runReader` hnd) $ isMaximalIn s (delete s substs) t) substs diff --git a/src/Term/Narrowing/Variants/Compute.hs b/src/Term/Narrowing/Variants/Compute.hs --- a/src/Term/Narrowing/Variants/Compute.hs +++ b/src/Term/Narrowing/Variants/Compute.hs @@ -1,6 +1,5 @@ -{-# LANGUAGE FlexibleInstances #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -17,7 +16,7 @@ import Term.LTerm import Term.Substitution import Term.Unification -import Term.Narrowing.Variants.Check (leqSubstVariant, variantsFrom) +import Term.Narrowing.Variants.Check (leqSubstVariant,variantsFrom) import Extension.Prelude @@ -122,12 +121,10 @@ -- x is maximal, start comparing a new element to the others go x ([],y:done) = x:(go y (reverse done,[])) - -- | This is used to sort narrowing steps such that similar steps are close narrowSeqStepComplexity :: (Bool,Variant) -> (Bool,Int,Int,Int) narrowSeqStepComplexity (checked, var@(Variant _ subst)) = (not checked, length (varPos var), size subst, length (varsRangeVFresh subst)) - -- | @computeVariants t d@ compute the variants of term @t@ with bound @d@. -- The rewriting rules are taken from the Maude context. diff --git a/src/Term/Positions.hs b/src/Term/Positions.hs --- a/src/Term/Positions.hs +++ b/src/Term/Positions.hs @@ -28,7 +28,7 @@ atPos t [] = t atPos (viewTerm -> FApp (AC _) (a:_)) (0:ps) = a `atPos` ps -atPos (viewTerm -> FApp (AC _) [_]) _ = +atPos (viewTerm -> FApp (AC _) [_]) _ = error "Term.Positions.atPos: invalid position given" atPos (viewTerm -> FApp fsym@(AC _) (_:as)) (1:ps) = (fApp fsym as) `atPos` ps @@ -52,26 +52,27 @@ 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 _) _) _ = +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" +replacePos (viewTerm -> Lit _) (_,_:_) = + error "Term.Positions.replacePos: invalid position given" -- | @positionsNonVar t@ returns all the non-variable positions in the term @t@. -- 'positionsNonVar' accounts for AC symbols in the same ways as 'atPos'. positionsNonVar :: (Show a, Show b) => VTerm a b -> [Position] -positionsNonVar t = - go t +positionsNonVar = + go 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) + 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) + 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 --- a/src/Term/Rewriting/Definitions.hs +++ b/src/Term/Rewriting/Definitions.hs @@ -1,6 +1,5 @@ -{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable #-} -- | --- Copyright : (c) 2010 - 2012 Benedikt Schmidt, Simon Meier +-- Copyright : (c) 2010-2012 Benedikt Schmidt, Simon Meier -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -11,13 +10,13 @@ Equal (..) , evalEqual - -- * Matching Problems + -- * Matching problems , Match(..) , flattenMatch , matchWith , matchOnlyIf - -- * Rewriting Rules + -- * Rewriting rules , 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,20 +1,13 @@ -{-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} - -- spurious warnings for view patterns -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 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. +-- This module implements normalization and normal-form checks of terms. module Term.Rewriting.Norm ( --- norm norm' , nf' , nfSubstVFresh' @@ -39,6 +32,7 @@ import System.IO.Unsafe (unsafePerformIO) +---------------------------------------------------------------------- -- Normalization using Maude ---------------------------------------------------------------------- @@ -53,6 +47,10 @@ norm' = norm sortOfName +---------------------------------------------------------------------- +-- Normal-form check using Maude and Haskell +---------------------------------------------------------------------- + -- | @nfViaHaskell t@ returns @True@ if the term @t@ is in normal form. nfViaHaskell :: LNTerm -> WithMaude Bool nfViaHaskell t0 = reader $ \hnd -> check hnd @@ -61,36 +59,38 @@ 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 + FAppNoEq o ts | (NoEq o) `S.member` irreducible -> all go ts + FList ts -> all go ts + FPair t1 t2 -> go t1 && go t2 + One -> True + Lit2 _ -> True -- subterm rules - FAppNonAC _ _ | setAny (struleApplicable t) strules -> False + FAppNoEq _ _ | setAny (struleApplicable t) strules -> False -- exponentiation - FExp (viewTerm2 -> FExp _ _) _ | dh -> False - FExp _ (viewTerm2 -> One) | dh -> False + FExp (viewTerm2 -> FExp _ _) _ -> False + FExp _ (viewTerm2 -> One) -> False -- inverses - FInv (viewTerm2 -> FInv _) | dh -> False - FInv (viewTerm2 -> FMult ts) | dh && any isInverse ts -> False - FInv (viewTerm2 -> One) | dh -> False + FInv (viewTerm2 -> FInv _) -> False + FInv (viewTerm2 -> FMult ts) | any isInverse ts -> False + FInv (viewTerm2 -> One) -> 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 + -- point multiplication + FPMult _ (viewTerm2 -> FPMult _ _) -> False + FPMult (viewTerm2 -> One) _ -> False + -- bilinear map + FEMap _ (viewTerm2 -> FPMult _ _) -> False + FEMap (viewTerm2 -> FPMult _ _) _ -> 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 + FExp t1 t2 -> go t1 && go t2 + FPMult t1 t2 -> go t1 && go t2 + FEMap t1 t2 -> go t1 && go t2 + FInv t1 -> go t1 + FMult ts -> all go ts + FUnion ts -> all go ts + FAppNoEq _ ts -> all go ts + FAppC _ ts -> all go ts struleApplicable t (StRule lhs rhs) = case solveMatchLNTerm (t `matchWith` lhs) `runReader` hnd of @@ -110,9 +110,7 @@ msig = mhMaudeSig hnd strules = stRules msig - irreducible = irreducibleFunctionSymbols msig - dh = enableDH msig - + irreducible = irreducibleFunSyms msig -- | @nf' t@ returns @True@ if the term @t@ is in normal form. nf' :: LNTerm -> WithMaude Bool @@ -135,28 +133,22 @@ ++" maude: " ++ show x ++ " haskell: "++show y --- Normalization ----------------------------------------------------- +-- Utility functions for normalization and normal-form checks +------------------------------------------------------------ -- | @nfSubst s@ returns @True@ if the substitution @s@ is in normal form. nfSubstVFresh' :: LNSubstVFresh -> WithMaude Bool nfSubstVFresh' s = reader $ \hnd -> all (\t -> runReader (nf' t) hnd) (rangeVFresh s) -{- -- | @normSubst s@ normalizes the substitution @s@. -normSubst :: (IsConst c, IsVar v, Show (Lit c v)) => Subst c v -> Subst c v -normSubst s = mapRange norm s - --} - --- | @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] + where irreducible = irreducibleFunSyms msig + go t = case viewTerm t of + Lit (Con _) -> [] + (FApp o as) | o `S.member` irreducible -> concatMap go as + _ -> [t] diff --git a/src/Term/Substitution.hs b/src/Term/Substitution.hs --- a/src/Term/Substitution.hs +++ b/src/Term/Substitution.hs @@ -1,8 +1,7 @@ -{-# LANGUAGE TupleSections, TypeSynonymInstances, GADTs,FlexibleContexts,EmptyDataDecls #-} -{-# LANGUAGE StandaloneDeriving, DeriveDataTypeable, FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses, DeriveFunctor, ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE FlexibleContexts #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -67,14 +66,12 @@ Lit (Var _) -> lvarName lv -- keep name of oldvar _ -> lvarName v - -- | @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. @@ -83,7 +80,6 @@ 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,10 +1,9 @@ -{-# LANGUAGE TupleSections, GeneralizedNewtypeDeriving #-} -{-# LANGUAGE ViewPatterns, TypeSynonymInstances, FlexibleContexts #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} -{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} - -- spurious warnings for view patterns -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier +-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -41,7 +40,7 @@ , substToListOn , substToList - -- * + -- *Apply class , Apply(..) -- * Pretty printing @@ -54,23 +53,24 @@ ) where -import Term.LTerm -import Term.Rewriting.Definitions --- import Term.Rewriting.NormAC -import Text.PrettyPrint.Highlight -import Logic.Connectives +import Term.LTerm +import Term.Rewriting.Definitions -import Utils.Misc +import Text.PrettyPrint.Highlight +import Logic.Connectives -import Data.Maybe -import Data.Map ( Map ) +import Utils.Misc + +import Data.Maybe +import Data.Map ( Map ) import qualified Data.Map as M import qualified Data.Set as S -import Data.List -import Data.Binary +import Data.List +import Data.Binary +import Data.Monoid (mempty) -import Control.Applicative -import Control.DeepSeq +import Control.Applicative +import Control.DeepSeq ---------------------------------------------------------------------- -- Substitutions @@ -101,10 +101,11 @@ -- | @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) + Lit l -> applyLit subst l + FApp (AC o) ts -> fAppAC o (map (applyVTerm subst) ts) + FApp (C o) ts -> fAppC o (map (applyVTerm subst) ts) + FApp (NoEq o) ts -> fAppNoEq o (map (applyVTerm subst) ts) + FApp List ts -> fAppList (map (applyVTerm subst) ts) -- Construction @@ -213,6 +214,7 @@ instance Ord c => HasFrees (LSubst c) where foldFrees f = foldFrees f . sMap + foldFreesOcc = mempty -- we ignore occurences in substitutions for now mapFrees f = (substFromList <$>) . mapFrees f . substToList -- | Types that support the application of 'LSubst's. @@ -289,7 +291,7 @@ ---------------------------------------------------------------------- -- | Pretty print a substitution. -prettySubst :: (Ord c, Ord v, HighlightDocument d) +prettySubst :: (Ord c, Ord v, HighlightDocument d, Show c, Show v) => (v -> d) -> (Lit c v -> d) -> Subst c v -> [d] prettySubst ppVar ppLit = map pp . M.toList . equivClasses . substToList @@ -298,6 +300,6 @@ (fsep $ punctuate comma $ map ppVar $ S.toList vs) <> operator_ "}" -- | Pretty print a substitution with logical variables. -prettyLNSubst :: (Show (Lit c LVar), Ord c, HighlightDocument d) +prettyLNSubst :: (Show (Lit c LVar), Ord c, HighlightDocument d, Show c) => LSubst c -> d prettyLNSubst = vcat . prettySubst (text . show) (text . show) 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 @@ -1,17 +1,10 @@ -{-# LANGUAGE TupleSections - , TypeSynonymInstances - , GADTs - , FlexibleContexts - , EmptyDataDecls - , StandaloneDeriving - , DeriveDataTypeable - , FlexibleInstances - , MultiParamTypeClasses - , GeneralizedNewtypeDeriving - , ScopedTypeVariables - #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier +-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -57,23 +50,24 @@ ) where -import Term.LTerm -import Text.PrettyPrint.Highlight +import Term.LTerm +import Text.PrettyPrint.Highlight -import Control.Applicative -import Control.Monad.Fresh -import Control.DeepSeq +import Control.Applicative +import Control.Monad.Fresh +import Control.DeepSeq -import Logic.Connectives +import Logic.Connectives -import Utils.Misc +import Utils.Misc -import Data.Map ( Map ) +import Data.Map ( Map ) import qualified Data.Map as M import qualified Data.Set as S -import Data.List -import Data.Traversable hiding ( mapM ) -import Data.Binary +import Data.List +import Data.Traversable hiding ( mapM ) +import Data.Binary +import Data.Monoid ( mempty ) ---------------------------------------------------------------------- -- Substitutions @@ -92,9 +86,6 @@ -- | Fresh substitution with logical variables and names type LNSubstVFresh = SubstVFresh Name LVar --- Instances ------------- - -- Smart constructors for substitutions ---------------------------------------------------------------------- @@ -106,7 +97,6 @@ emptySubstVFresh :: SubstVFresh c v emptySubstVFresh = SubstVFresh M.empty - -- Operations ---------------------------------------------------------------------- @@ -132,7 +122,6 @@ where s2 = substFromListVFresh [(v, lit (Var v)) | v <- vs ] vs = vs0 \\ domVFresh s - -- Queries ---------------------------------------------------------------------- @@ -208,6 +197,7 @@ instance HasFrees (SubstVFresh n LVar) where foldFrees f = foldFrees f . M.keys . svMap + foldFreesOcc _ _ = const mempty -- we ignore occurences in substitutions for now mapFrees f = (substFromListVFresh <$>) . traverse mapDomain . substToListVFresh where @@ -218,7 +208,7 @@ ---------------------------------------------------------------------- -- | Pretty print a substitution. -prettySubstVFresh :: (Ord c, Ord v, HighlightDocument d) +prettySubstVFresh :: (Ord c, Ord v, HighlightDocument d, Show c, Show v) => (v -> d) -> (Lit c v -> d) -> SubstVFresh c v -> [d] prettySubstVFresh ppVar ppLit = map pp . M.toList . equivClasses . substToListVFresh @@ -227,7 +217,8 @@ (fsep $ punctuate comma $ map ppVar $ S.toList vs) <> operator_ "}" -- | Pretty print a substitution with logical variables. -prettyLSubstVFresh :: (Show (Lit c LVar), Ord c, HighlightDocument d) => LSubstVFresh c -> d +prettyLSubstVFresh :: (Show (Lit c LVar), Ord c, HighlightDocument d, Show c) + => LSubstVFresh c -> d prettyLSubstVFresh = vcat . prettySubstVFresh (text . show) (text . show) -- | Pretty print a disjunction of substitutions. diff --git a/src/Term/Subsumption.hs b/src/Term/Subsumption.hs --- a/src/Term/Subsumption.hs +++ b/src/Term/Subsumption.hs @@ -1,8 +1,6 @@ -{-# LANGUAGE GADTs, FlexibleContexts, ViewPatterns #-} -{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} - -- spurious warnings for view patterns +{-# LANGUAGE ViewPatterns #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt +-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -13,9 +11,8 @@ , eqTermSubs , factorSubstVia --- , factorSubstOnVFresh - -- * canonical representations for substitutions + -- * Canonical representations for substitutions -- modulo renaming , canonizeSubst @@ -28,13 +25,9 @@ import Data.Monoid import Extension.Prelude --- import Utils.Misc - -import Term.Term import Term.LTerm import Term.Unification -import Term.Positions ---------------------------------------------------------------------- @@ -68,28 +61,6 @@ 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 - -> 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 - ++ " => " ++ show s ++ " contains new variables" - return $ freeToFreshRaw s - where - s1 = freshToFreeAvoiding s1_0 (vs, varsRange s2) - l1 = substToListOn vs s1 - l2 = substToListOn vs s2 --} - ---------------------------------------------------------------------- -- Equality of substitutions modulo AC and renaming ---------------------------------------------------------------------- @@ -99,21 +70,8 @@ canonizeSubst subst = mapRangeVFresh (applyVTerm renaming) subst where - vrangeSorted = sortOn (varOccurences subst) (varsRangeVFresh subst) + occs = varOccurences $ rangeVFresh subst + vrangeSorted = sortOn (`lookup` occs) (varsRangeVFresh subst) renaming = substFromList $ zipWith (\lv i -> (lv, varTerm $ LVar "x" (lvarSort lv) i)) vrangeSorted [1..] - --- | @varOccurences v t@ returns a sorted list of positions where the --- variable @v@ occurs in @t@. The function returns the same result for --- terms that are equal modulo AC since the flattened term representation --- is used. -varOccurences :: LNSubstVFresh -> LVar -> [[Position]] -varOccurences subst v = map (go []) $ rangeVFresh subst - where - go pos (viewTerm -> Lit (Var v')) | v == v' = [pos] - | otherwise = [] - 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 @@ -2,7 +2,7 @@ {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} -- spurious warnings for view patterns -- | --- Copyright : (c) 2011, 2012 Benedikt Schmidt +-- Copyright : (c) 2011-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -57,13 +57,6 @@ stRuleToRRule (StRule lhs rhs) = case rhs of RhsGround t -> lhs `RRule` t RhsPosition p -> lhs `RRule` (lhs `atPos` p) - -{- - -test: -xorRules == map (stRuleToRRule . fromJust . rRuleToStRule) xorRules - --} ------------------------------------------------------------------------------ -- Pretty Printing diff --git a/src/Term/Term.hs b/src/Term/Term.hs --- a/src/Term/Term.hs +++ b/src/Term/Term.hs @@ -1,395 +1,149 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE TemplateHaskell, FlexibleInstances #-} -{-# LANGUAGE DeriveDataTypeable, ViewPatterns #-} +{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE OverloadedStrings #-} -- for ByteString -- | --- 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 Algebra and related notions. module Term.Term ( - -- * Signatures and function symbols - FunSym(..) - , ACSym(..) - , NonACSym - , FunSig - , dhFunSig - , xorFunSig - , msetFunSig - , pairFunSig - , dhReducibleFunSig - , implicitFunSig - -- * Terms - , Term - , TermView (..) - , viewTerm - , TermView2 (..) - , viewTerm2 - - , traverseTerm - , fmapTerm - , bindTerm - , lits + -- ** Pretty printing and query functions. + prettyTerm , showFunSymName - , prettyTerm + , lits -- ** Smart constructors - , lit - , fApp - , fAppAC - , fAppNonAC - , fAppList - , unsafefApp - - , fAppMult , fAppOne , fAppExp , fAppInv - , fAppXor - , fAppZero - , fAppUnion - , fAppEmpty + , fAppPMult + , fAppEMap , fAppPair , fAppFst , fAppSnd - -- ** exp symbol - , expSymString - , invSymString - -- ** Destructors and classifiers - , destPair - , destInverse - , destProduct - , destXor - , destUnion - , isPair , isInverse , isProduct - , isXor , isUnion - , isNullaryFunction - - , module Term.Classes - ) where - -import Data.List -import Data.Monoid -import Data.Foldable (Foldable, foldMap) -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 Data.ByteString (ByteString) -import qualified Data.ByteString.Char8 as BC -import Extension.Data.ByteString () - -import Data.Set (Set) -import qualified Data.Set as S - -import Text.PrettyPrint.Class - -import Term.Classes + , isEMap + , isNullaryPublicFunction + , isPrivateFunction ----------------------------------------------------------------------- --- AC operators for terms ----------------------------------------------------------------------- + -- * AC, C, and NonAC funcion symbols + , FunSym(..) + , ACSym(..) + , CSym(..) + , Privacy(..) + , NoEqSym --- | AC function symbols. -data ACSym = Union | Xor | Mult - deriving (Eq, Ord, Typeable, Data, Show) + -- ** Signatures + , FunSig + , NoEqFunSig --- | non-AC function symbols -type NonACSym = (ByteString, Int) + -- ** concrete symbols strings + , expSymString + , invSymString + , pmultSymString + , emapSymString + , unionSymString + + -- ** Function symbols + , expSym + , pmultSym --- | Function symbols -data FunSym = NonAC NonACSym -- ^ a non-AC function function symbol of a given arity - | AC ACSym -- ^ an AC function symbol, can be used n-ary - | List -- ^ a non-AC n-ary function symbol of TOP sort - deriving (Eq, Ord, Typeable, Data, Show) + -- ** concrete signatures + , dhFunSig + , bpFunSig + , msetFunSig + , pairFunSig + , dhReducibleFunSig + , bpReducibleFunSig + , implicitFunSig --- | Function signatures. -type FunSig = Set NonACSym + , module Term.Term.Classes + , module Term.Term.Raw -expSymString :: ByteString -expSymString = "exp" + ) where -invSymString :: ByteString -invSymString = "inv" +import Data.Monoid +import Data.Foldable (Foldable, foldMap) -pairSym, expSym, invSym, oneSym, zeroSym, emptySym, fstSym, sndSym :: NonACSym --- | Pairing. -pairSym = ("pair",2) --- | Exponentiation. -expSym = (expSymString,2) --- | The inverse in the groups of exponents. -invSym = (invSymString,1) --- | The one in the group of exponents. -oneSym = ("one", 0) --- | The zero for Xor. -zeroSym = ("zero",0) --- | The empty multiset. -emptySym = ("empty",0) --- | 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) +import qualified Data.ByteString.Char8 as BC +import Extension.Data.ByteString () --- | The signature for the non-AC Diffie-Hellman function symbols. -dhFunSig :: FunSig -dhFunSig = S.fromList [ expSym, oneSym, invSym ] - --- | 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 ] - --- | The signature for pairing. -pairFunSig :: FunSig -pairFunSig = S.fromList [ pairSym, fstSym, sndSym ] - --- | Reducible non-AC symbols for DH. -dhReducibleFunSig :: FunSig -dhReducibleFunSig = S.fromList [ expSym, invSym ] - --- | Implicit non-AC symbols. -implicitFunSig :: FunSig -implicitFunSig = S.fromList [ invSym, pairSym ] +import Text.PrettyPrint.Class +import Term.Term.Classes +import Term.Term.FunctionSymbols +import Term.Term.Raw ---------------------------------------------------------------------- --- Terms +-- Smart Constructors ---------------------------------------------------------------------- --- | 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 ) - --- | 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) +-- | Smart constructors for one, zero. +fAppOne :: Term a +fAppOne = fAppNoEq oneSym [] --- | 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 +-- | Smart constructors for pair, exp, pmult, and emap. +fAppPair, fAppExp,fAppPMult, fAppEMap :: Ord a => (Term a, Term a) -> Term a +fAppPair (x,y) = fAppNoEq pairSym [x, y] +fAppExp (b,e) = fAppNoEq expSym [b, e] +fAppPMult (s,p) = fAppNoEq pmultSym [s, p] +fAppEMap (x,y) = fAppC EMap [x, y] --- | Destruct a top-level product. -destProduct :: Term a -> Maybe [Term a] -destProduct (FAPP (AC Mult) ts) = return ts -destProduct _ = Nothing +-- | Smart constructors for inv, fst, and snd. +fAppInv, fAppFst, fAppSnd :: Term a -> Term a +fAppInv e = fAppNoEq invSym [e] +fAppFst a = fAppNoEq fstSym [a] +fAppSnd a = fAppNoEq sndSym [a] --- | Destruct a top-level product. -destXor :: Term a -> Maybe [Term a] -destXor (FAPP (AC Xor) ts) = return ts -destXor _ = Nothing +-- | @lits t@ returns all literals that occur in term @t@. List can contain duplicates. +lits :: Ord a => Term a -> [a] +lits = foldMap return --- | Destruct a top-level multiset union. -destUnion :: Term a -> Maybe [Term a] -destUnion (FAPP (AC Union) ts) = return ts -destUnion _ = Nothing +---------------------------------------------------------------------- +-- Classifiers +---------------------------------------------------------------------- -- | 'True' iff the term is a well-formed pair. -isPair :: Term a -> Bool -isPair = isJust . destPair +isPair :: Show a => Term a -> Bool +isPair (viewTerm2 -> FPair _ _) = True +isPair _ = False -- | 'True' iff the term is a well-formed inverse. -isInverse :: Term a -> Bool -isInverse = isJust . destInverse +isInverse :: Show a => Term a -> Bool +isInverse (viewTerm2 -> FInv _) = True +isInverse _ = False -- | 'True' iff the term is a well-formed product. -isProduct :: Term a -> Bool -isProduct = isJust . destProduct +isProduct :: Show a => Term a -> Bool +isProduct (viewTerm2 -> FMult _) = True +isProduct _ = False --- | 'True' iff the term is a well-formed xor'ing. -isXor :: Term a -> Bool -isXor = isJust . destXor +-- | 'True' iff the term is a well-formed emap. +isEMap :: Show a => Term a -> Bool +isEMap (viewTerm2 -> FEMap _ _) = True +isEMap _ = False --- | 'True' iff the term is a well-formed xor'ing. -isUnion :: Term a -> Bool -isUnion = isJust . destXor +-- | 'True' iff the term is a well-formed union. +isUnion :: Show a => Term a -> Bool +isUnion (viewTerm2 -> FUnion _) = True +isUnion _ = False -- | 'True' iff the term is a nullary, public function. -isNullaryFunction :: Term a -> Bool -isNullaryFunction (viewTerm -> FApp (NonAC (_, 0)) _) = True -isNullaryFunction _ = False - --- | View on terms that corresponds to representation. -data TermView a = Lit a - | FApp FunSym [Term a] - deriving (Show, Eq, Ord) - -{-# 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 - --- | @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 - --- | 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 ] - --- | Smart constructor for non-AC terms. -{-# INLINE fAppNonAC #-} -fAppNonAC :: NonACSym -> [Term a] -> Term a -fAppNonAC nacsym = FAPP (NonAC nacsym) - --- | Smart constructor for list terms. -{-# INLINE fAppList #-} -fAppList :: [Term a] -> Term a -fAppList = FAPP List - --- | @lit l@ creates a term from the literal @l@. -{-# INLINE lit #-} -lit :: a -> Term a -lit l = LIT l - --- | @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 - - --- | 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) - --- | 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 ] - - --- | 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 - --- | Smart constructors for one, zero, and empty. -fAppOne, fAppZero, fAppEmpty :: Term a -fAppOne = fAppNonAC oneSym [] -fAppZero = fAppNonAC zeroSym [] -fAppEmpty = fAppNonAC emptySym [] - --- | 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] - --- | 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] - - --- Instances ------------- - -{-# 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 - -{-# 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 - -instance Foldable Term where - {-# INLINE foldMap #-} - foldMap f = foldTerm f (const mconcat) - -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))++")" - - - --- | 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 Sized a => Sized (Term a) where - size = foldTerm size (const $ \xs -> sum xs + 1) +isNullaryPublicFunction :: Term a -> Bool +isNullaryPublicFunction (viewTerm -> FApp (NoEq (_, (0, Public))) _) = True +isNullaryPublicFunction _ = False --- | @lits t@ returns all literals that occur in term @t@. List can contain duplicates. -lits :: Ord a => Term a -> [a] -lits = foldMap return +isPrivateFunction :: Term a -> Bool +isPrivateFunction (viewTerm -> FApp (NoEq (_, (_,Private))) _) = True +isPrivateFunction _ = False ---------------------------------------------------------------------- -- Pretty printing @@ -397,43 +151,34 @@ -- | Convert a function symbol to its name. showFunSymName :: FunSym -> String -showFunSymName (NonAC (bs, _)) = BC.unpack bs -showFunSymName (AC op) = show op -showFunSymName List = "List" +showFunSymName (NoEq (bs, _)) = BC.unpack bs +showFunSymName (AC op) = show op +showFunSymName (C op ) = show op +showFunSymName List = "List" -- | Pretty print a term. -prettyTerm :: Document d => (l -> d) -> Term l -> d +prettyTerm :: (Document d, Show l) => (l -> d) -> Term l -> d 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 + ppTerm t = case viewTerm t of + Lit l -> ppLit l + FApp (AC o) ts -> ppTerms (ppACOp o) 1 "(" ")" ts + FApp (NoEq s) [t1,t2] | s == expSym -> ppTerm t1 <> text "^" <> ppTerm t2 + FApp (NoEq s) _ | s == pairSym -> ppTerms ", " 1 "<" ">" (split t) + FApp (NoEq (f, _)) [] -> text (BC.unpack f) + FApp (NoEq (f, _)) ts -> ppFun f ts + FApp (C EMap) ts -> ppFun emapSymString ts + FApp List ts -> ppFun "LIST" ts ppACOp Mult = "*" - ppACOp Union = "#" - ppACOp Xor = "+" + ppACOp Union = "+" 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 t = [t] + split (viewTerm2 -> FPair t1 t2) = t1 : split t2 + split t = [t] ppFun f ts = text (BC.unpack f ++"(") <> fsep (punctuate comma (map ppTerm ts)) <> text ")" - --- Derived instances --------------------- - -$( derive makeNFData ''FunSym) -$( derive makeNFData ''ACSym) -$( derive makeNFData ''Term ) - -$( derive makeBinary ''FunSym) -$( derive makeBinary ''ACSym) -$( derive makeBinary ''Term ) diff --git a/src/Term/Term/Classes.hs b/src/Term/Term/Classes.hs new file mode 100644 --- /dev/null +++ b/src/Term/Term/Classes.hs @@ -0,0 +1,14 @@ +-- | +-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier +-- License : GPL v3 (see LICENSE) +-- +-- Maintainer : Benedikt Schmidt +-- +-- | A type class for sized types. +module Term.Term.Classes where + +class Sized a where + size :: a -> Int + +instance Sized a => Sized [a] where + size = sum . map size diff --git a/src/Term/Term/FunctionSymbols.hs b/src/Term/Term/FunctionSymbols.hs new file mode 100644 --- /dev/null +++ b/src/Term/Term/FunctionSymbols.hs @@ -0,0 +1,172 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE OverloadedStrings #-} + -- for ByteString +-- | +-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier +-- License : GPL v3 (see LICENSE) +-- +-- Maintainer : Benedikt Schmidt +-- +-- Function Symbols and Signatures. +module Term.Term.FunctionSymbols ( + -- ** AC, C, and NonAC funcion symbols + FunSym(..) + , ACSym(..) + , CSym(..) + , Privacy(..) + , NoEqSym + + -- ** Signatures + , FunSig + , NoEqFunSig + + -- ** concrete symbols strings + , expSymString + , invSymString + , pmultSymString + , emapSymString + , unionSymString + + -- ** concrete symbols + , expSym + , pmultSym + , oneSym + , invSym + , pairSym + , fstSym + , sndSym + + -- ** concrete signatures + , dhFunSig + , bpFunSig + , msetFunSig + , pairFunSig + , dhReducibleFunSig + , bpReducibleFunSig + , implicitFunSig + ) where + +import Data.Typeable +import Data.Generics +import Data.DeriveTH +import Data.Binary + +import Control.DeepSeq + +import Data.ByteString (ByteString) +import Extension.Data.ByteString () +import Data.ByteString.Char8 () + +import Data.Set (Set) +import qualified Data.Set as S + +---------------------------------------------------------------------- +-- Function symbols +---------------------------------------------------------------------- + +-- | AC function symbols. +data ACSym = Union | Mult + deriving (Eq, Ord, Typeable, Data, Show) + +-- | A function symbol can be either Private (unknown to adversary) or Public. +data Privacy = Private | Public + deriving (Eq, Ord, Typeable, Data, Show) + +-- | NoEq function symbols (with respect to the background theory). +type NoEqSym = (ByteString, (Int, Privacy)) -- ^ operator name, arity, private + +-- | C(ommutative) function symbols +data CSym = EMap + deriving (Eq, Ord, Typeable, Data, Show) + +-- | Function symbols +data FunSym = NoEq NoEqSym -- ^ a free function function symbol of a given arity + | AC ACSym -- ^ an AC function symbol, can be used n-ary + | C CSym -- ^ a C function symbol of a given arity + | List -- ^ a free n-ary function symbol of TOP sort + deriving (Eq, Ord, Typeable, Data, Show) + +-- | Function signatures. +type FunSig = Set FunSym + +-- | NoEq function signatures. +type NoEqFunSig = Set NoEqSym + +---------------------------------------------------------------------- +-- Fixed function symbols +---------------------------------------------------------------------- + +expSymString, invSymString :: ByteString +expSymString = "exp" +invSymString = "inv" + +unionSymString :: ByteString +unionSymString = "union" + +emapSymString, pmultSymString :: ByteString +emapSymString = "em" +pmultSymString = "pmult" + +pairSym, expSym, invSym, oneSym, fstSym, sndSym, pmultSym :: NoEqSym +-- | Pairing. +pairSym = ("pair",(2,Public)) +-- | Exponentiation. +expSym = (expSymString,(2,Public)) +-- | The inverse in the groups of exponents. +invSym = (invSymString,(1,Public)) +-- | The one in the group of exponents. +oneSym = ("one",(0,Public)) +-- | Projection of first component of pair. +fstSym = ("fst",(1,Public)) +-- | Projection of second component of pair. +sndSym = ("snd",(1,Public)) +-- | Multiplication of points (in G1) on elliptic curve by scalars. +pmultSym = (pmultSymString,(2,Public)) + +---------------------------------------------------------------------- +-- Fixed signatures +---------------------------------------------------------------------- + +-- | The signature for Diffie-Hellman function symbols. +dhFunSig :: FunSig +dhFunSig = S.fromList [ AC Mult, NoEq expSym, NoEq oneSym, NoEq invSym ] + +-- | The signature for the bilinear pairing function symbols. +bpFunSig :: FunSig +bpFunSig = S.fromList [ NoEq pmultSym, C EMap ] + +-- | The signature for the multiset function symbols. +msetFunSig :: FunSig +msetFunSig = S.fromList [AC Union] + +-- | The signature for pairing. +pairFunSig :: NoEqFunSig +pairFunSig = S.fromList [ pairSym, fstSym, sndSym ] + +-- | Reducible function symbols for DH. +dhReducibleFunSig :: FunSig +dhReducibleFunSig = S.fromList [ NoEq expSym, NoEq invSym ] + +-- | Reducible function symbols for BP. +bpReducibleFunSig :: FunSig +bpReducibleFunSig = S.fromList [ NoEq pmultSym, C EMap ] + +-- | Implicit function symbols. +implicitFunSig :: FunSig +implicitFunSig = S.fromList [ NoEq invSym, NoEq pairSym + , AC Mult, AC Union ] + +---------------------------------------------------------------------- +-- Derived instances +---------------------------------------------------------------------- + +$( derive makeNFData ''Privacy) +$( derive makeNFData ''CSym) +$( derive makeNFData ''FunSym) +$( derive makeNFData ''ACSym) + +$( derive makeBinary ''Privacy) +$( derive makeBinary ''CSym) +$( derive makeBinary ''FunSym) +$( derive makeBinary ''ACSym) diff --git a/src/Term/Term/Raw.hs b/src/Term/Term/Raw.hs new file mode 100644 --- /dev/null +++ b/src/Term/Term/Raw.hs @@ -0,0 +1,207 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE DeriveDataTypeable #-} +-- | +-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier +-- License : GPL v3 (see LICENSE) +-- +-- Maintainer : Benedikt Schmidt +-- +-- Term Algebra and related notions. +module Term.Term.Raw ( + -- * Terms + Term + , TermView (..) + , viewTerm + , TermView2 (..) + , viewTerm2 + + -- ** Standard function + , traverseTerm + , fmapTerm + , bindTerm + + -- ** Smart constructors + , lit + , fApp + , fAppAC + , fAppC + , fAppNoEq + , fAppList + , unsafefApp + + ) where + +import Data.List +import Data.Monoid +import Data.Foldable (Foldable, foldMap) +import Data.Traversable +import Data.Typeable +import Data.Generics +import Data.DeriveTH +import Data.Binary + +import Control.DeepSeq +import Control.Basics + +import qualified Data.ByteString.Char8 as BC +import Extension.Data.ByteString () + +import Term.Term.Classes +import Term.Term.FunctionSymbols + +---------------------------------------------------------------------- +-- 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 ) + +---------------------------------------------------------------------- +-- Views and smart constructors +---------------------------------------------------------------------- + +-- | View on terms that corresponds to representation. +data TermView a = Lit a + | FApp FunSym [Term a] + deriving (Show, Eq, Ord) + +{-# 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 + +-- | @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 (C o) ts = fAppC o ts +fApp List ts = FAPP List ts +fApp s@(NoEq _) ts = FAPP s ts + +-- | 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 ] + +-- | Smart constructor for AC terms. +fAppC :: Ord a => CSym -> [Term a] -> Term a +fAppC nacsym as = FAPP (C nacsym) (sort as) + +-- | Smart constructor for non-AC terms. +{-# INLINE fAppNoEq #-} +fAppNoEq :: NoEqSym -> [Term a] -> Term a +fAppNoEq freesym = FAPP (NoEq freesym) + +-- | Smart constructor for list terms. +{-# INLINE fAppList #-} +fAppList :: [Term a] -> Term a +fAppList = FAPP List + +-- | @lit l@ creates a term from the literal @l@. +{-# INLINE lit #-} +lit :: a -> Term a +lit l = LIT l + +-- | @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 + +-- | 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 + | FPMult (Term a) (Term a) | FEMap (Term a) (Term a) + | FUnion [Term a] + | FPair (Term a) (Term a) + | FAppNoEq NoEqSym [Term a] + | FAppC CSym [Term a] + | FList [Term a] + | Lit2 a + deriving (Show, Eq, Ord) + +-- | 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 Union = FUnion +viewTerm2 (FAPP (C EMap) [ t1 ,t2 ]) = FEMap t1 t2 +viewTerm2 t@(FAPP (C _) _) = error $ "viewTerm2: malformed term `"++show t++"'" +viewTerm2 t@(FAPP (NoEq o) ts) = case ts of + [ t1, t2 ] | o == expSym -> FExp t1 t2 -- ensure here that FExp is always exp, never a user-defined symbol + [ t1, t2 ] | o == pmultSym -> FPMult t1 t2 + [ t1, t2 ] | o == pairSym -> FPair t1 t2 + [ t1 ] | o == invSym -> FInv t1 + [] | o == oneSym -> One + _ | o `elem` ssyms -> error $ "viewTerm2: malformed term `"++show t++"'" + _ -> FAppNoEq o ts + where + -- special symbols + ssyms = [ expSym, pairSym, invSym, oneSym, pmultSym ] + +---------------------------------------------------------------------- +-- Instances +---------------------------------------------------------------------- + +{-# 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 + +{-# 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 + +instance Foldable Term where + {-# INLINE foldMap #-} + foldMap f = foldTerm f (const mconcat) + +instance Show a => Show (Term a) where + show t = + case viewTerm t of + Lit l -> show l + FApp (NoEq (s,_)) [] -> BC.unpack s + FApp (NoEq (s,_)) as -> BC.unpack s++"("++(intercalate "," (map show as))++")" + FApp (C EMap) as -> BC.unpack emapSymString++"("++(intercalate "," (map show as))++")" + FApp List as -> "LIST"++"("++(intercalate "," (map show as))++")" + FApp (AC o) as -> show o++"("++(intercalate "," (map show as))++")" + +-- | 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 Sized a => Sized (Term a) where + size = foldTerm size (const $ \xs -> sum xs + 1) + +---------------------------------------------------------------------- +-- Derived Instances +---------------------------------------------------------------------- + +$( derive makeNFData ''Term ) + +$( derive makeBinary ''Term ) 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, ViewPatterns #-} +{-# LANGUAGE FlexibleContexts #-} -- | -- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) @@ -34,11 +34,11 @@ -- * Maude signatures , MaudeSig , enableDH - , enableXor + , enableBP , enableMSet , minimalMaudeSig , dhMaudeSig - , xorMaudeSig + , bpMaudeSig , msetMaudeSig , pairMaudeSig , symEncMaudeSig @@ -46,10 +46,12 @@ , signatureMaudeSig , hashMaudeSig , rrulesForMaudeSig - , allFunctionSymbols + , stFunSyms + , funSyms , stRules - , irreducibleFunctionSymbols - , addFunctionSymbol + , irreducibleFunSyms + , noEqFunSyms + , addFunSym , addStRule -- * Convenience exports @@ -186,7 +188,7 @@ (Lit (Var vl), _ ) -> elim vl r (_, Lit (Var vr) ) -> elim vr l (Lit (Con cl), Lit (Con cr) ) -> guard (cl == cr) - (FApp (NonAC lfsym) largs, FApp (NonAC rfsym) rargs) -> + (FApp (NoEq lfsym) largs, FApp (NoEq rfsym) rargs) -> guard (lfsym == rfsym && length largs == length rargs) >> sequence_ (zipWith unifyRaw largs rargs) (FApp List largs, FApp List rargs) -> @@ -196,6 +198,10 @@ (FApp (AC lacsym) _, FApp (AC racsym) _) -> guard (lacsym == racsym) >> tell [Equal l r] -- delay unification + (FApp (C lsym) largs, FApp (C rsym) rargs) -> + guard (lsym == rsym && length largs == length rargs) + >> tell [Equal l r] -- delay unification + -- all unifiable pairs of term constructors have been enumerated _ -> mzero -- no unifier where @@ -222,8 +228,8 @@ matchRaw sortOf t p = do mappings <- get guard (trace (show (mappings,t,p)) True) - case (t, p) of - (_, viewTerm -> Lit (Var vp)) -> + case (viewTerm t, viewTerm p) of + (_, Lit (Var vp)) -> case M.lookup vp mappings of Nothing -> do unless (sortGeqLTerm sortOf vp t) $ @@ -232,14 +238,15 @@ Just tp | t == tp -> return () | otherwise -> throwError NoMatcher - (viewTerm -> Lit (Con ct), viewTerm -> Lit (Con cp)) -> guard (ct == cp) - (viewTerm -> FApp (NonAC tfsym) targs, viewTerm -> FApp (NonAC pfsym) pargs) -> + (Lit (Con ct), Lit (Con cp)) -> guard (ct == cp) + (FApp (NoEq tfsym) targs, FApp (NoEq pfsym) pargs) -> guard (tfsym == pfsym && length targs == length pargs) >> sequence_ (zipWith (matchRaw sortOf) targs pargs) - (viewTerm -> FApp List targs, viewTerm -> FApp List pargs) -> + (FApp List targs, FApp List pargs) -> guard (length targs == length pargs) >> sequence_ (zipWith (matchRaw sortOf) targs pargs) - (viewTerm -> FApp (AC _) _, viewTerm -> FApp (AC _) _) -> throwError ACProblem + (FApp (AC _) _, FApp (AC _) _) -> throwError ACProblem + (FApp (C _) _, FApp (C _) _) -> throwError ACProblem -- all matchable pairs of term constructors have been enumerated _ -> throwError NoMatcher diff --git a/src/Term/UnitTests.hs b/src/Term/UnitTests.hs --- a/src/Term/UnitTests.hs +++ b/src/Term/UnitTests.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-} +{-# LANGUAGE FlexibleContexts #-} {-# OPTIONS_GHC -fno-warn-unused-binds #-} -- | -- Copyright : (c) 2012 Benedikt Schmidt @@ -7,7 +7,8 @@ -- Maintainer : Benedikt Schmidt -- -- Unit tests for the functions dealing with term algebra and related notions. -module Term.UnitTests (tests) where +module Term.UnitTests -- (tests) + where import Term.Substitution import Term.Subsumption @@ -63,11 +64,11 @@ 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))) + [ testTrue "a" (propUnifySound mhnd (pair(f1,inv(f2))) (pair(f1,inv(f2)))) + , testTrue "b" (propUnifySound mhnd t1 t2) + , testTrue "c" (propUnifySound mhnd u1 u2) + , testTrue "d" (propUnifySound mhnd (sdec(x1,y1)) (sdec(senc(x2,x3), x4))) + , testTrue "e" (propUnifySound mhnd (fAppEMap (p2,x1)) (fAppEMap (p1,x2))) ] where t1 = expo (inv(pair(f1,f2)), f2 *: (inv f2) *: f3 *: f4 *: x2) @@ -76,8 +77,9 @@ 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 +propUnifySound hnd t1 t2 = all (\s -> let s' = freshToFreeAvoiding s [t1,t2] in applyVTerm s' t1 == applyVTerm s' t2) substs + && not (null substs) where substs = unifyLNTerm [Equal t1 t2] `runReader` hnd @@ -253,22 +255,6 @@ , [(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) @@ -299,7 +285,7 @@ -- | Maude signatures with all builtin symbols. allMaudeSig :: MaudeSig allMaudeSig = mconcat - [ dhMaudeSig, xorMaudeSig, msetMaudeSig + [ bpMaudeSig, msetMaudeSig , pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig ] @@ -325,25 +311,6 @@ 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]) ] @@ -357,19 +324,16 @@ -- convenience abbreviations ---------------------------------------------------------------------------------- -pair, expo :: (Term a, Term a) -> Term a +pair, expo :: Ord a => (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 +union, mult :: Ord a => [Term a] -> Term a +union = fAppAC Union +mult = fAppAC Mult -one, zero, emptyMSet :: Term a -one = fAppOne -zero = fAppZero -emptyMSet = fAppEmpty +one :: Term a +one = fAppOne diff --git a/src/Term/VTerm.hs b/src/Term/VTerm.hs --- a/src/Term/VTerm.hs +++ b/src/Term/VTerm.hs @@ -1,6 +1,8 @@ -{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable, ViewPatterns #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE ViewPatterns #-} -- | --- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier +-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt @@ -48,7 +50,6 @@ ---------------------------------------------------------------------- -- 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 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.8.2.0 +version: 0.8.4.0 license: GPL license-file: LICENSE category: Theorem Provers @@ -58,7 +58,7 @@ , HUnit == 1.2.* - , tamarin-prover-utils >= 0.8.2 && < 0.9 + , tamarin-prover-utils >= 0.8.4 && < 0.9 hs-source-dirs: src @@ -92,7 +92,9 @@ other-modules: Term.Term - Term.Classes + Term.Term.Classes + Term.Term.Raw + Term.Term.FunctionSymbols Term.Narrowing.Narrow