tamarin-prover-term 0.8.2.0 → 0.8.4.0
raw patch · 29 files changed
+1043/−929 lines, 29 filesdep ~tamarin-prover-utilsnew-uploader
Dependency ranges changed: tamarin-prover-utils
Files
- src/Term/Builtin/Convenience.hs +16/−36
- src/Term/Builtin/Rules.hs +18/−11
- src/Term/Builtin/Signature.hs +27/−24
- src/Term/Classes.hs +0/−14
- src/Term/LTerm.hs +149/−62
- src/Term/Maude/Parser.hs +78/−75
- src/Term/Maude/Process.hs +3/−4
- src/Term/Maude/Signature.hs +66/−56
- src/Term/Maude/Types.hs +12/−15
- src/Term/Narrowing/Narrow.hs +6/−7
- src/Term/Narrowing/Variants.hs +1/−1
- src/Term/Narrowing/Variants/Check.hs +6/−4
- src/Term/Narrowing/Variants/Compute.hs +2/−5
- src/Term/Positions.hs +11/−10
- src/Term/Rewriting/Definitions.hs +3/−4
- src/Term/Rewriting/Norm.hs +40/−48
- src/Term/Substitution.hs +3/−7
- src/Term/Substitution/SubstVFree.hs +26/−24
- src/Term/Substitution/SubstVFresh.hs +22/−31
- src/Term/Subsumption.hs +5/−47
- src/Term/SubtermRule.hs +1/−8
- src/Term/Term.hs +109/−364
- src/Term/Term/Classes.hs +14/−0
- src/Term/Term/FunctionSymbols.hs +172/−0
- src/Term/Term/Raw.hs +207/−0
- src/Term/Unification.hs +20/−13
- src/Term/UnitTests.hs +17/−53
- src/Term/VTerm.hs +4/−3
- tamarin-prover-term.cabal +5/−3
src/Term/Builtin/Convenience.hs view
@@ -1,5 +1,5 @@ -- |--- Copyright : (c) 2010, 2011 Benedikt Schmidt+-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt <beschmi@gmail.com>@@ -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
src/Term/Builtin/Rules.hs view
@@ -1,5 +1,5 @@ -- |--- Copyright : (c) 2010, 2011 Benedikt Schmidt+-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt <beschmi@gmail.com>@@ -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)
src/Term/Builtin/Signature.hs view
@@ -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 <beschmi@gmail.com>@@ -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 ]
− src/Term/Classes.hs
@@ -1,14 +0,0 @@--- |--- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier--- License : GPL v3 (see LICENSE)--- --- Maintainer : Benedikt Schmidt <beschmi@gmail.com>------ | 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
src/Term/LTerm.hs view
@@ -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 <beschmi@gmail.com>@@ -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 ------------------------------------------------------------------------------
src/Term/Maude/Parser.hs view
@@ -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 ++"'"
src/Term/Maude/Process.hs view
@@ -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 <beschmi@gmail.com>@@ -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
src/Term/Maude/Signature.hs view
@@ -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 <beschmi@gmail.com> ----- 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
src/Term/Maude/Types.hs view
@@ -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 <beschmi@gmail.com>@@ -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 ----------------------------------------------------------------------
src/Term/Narrowing/Narrow.hs view
@@ -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 <beschmi@gmail.com>@@ -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 ----------------------------------------------------------------------
src/Term/Narrowing/Variants.hs view
@@ -1,5 +1,5 @@ -- |--- Copyright : (c) 2010, 2011 Benedikt Schmidt+-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt <beschmi@gmail.com>
src/Term/Narrowing/Variants/Check.hs view
@@ -1,5 +1,5 @@ -- |--- Copyright : (c) 2010, 2011 Benedikt Schmidt+-- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt <beschmi@gmail.com>@@ -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
src/Term/Narrowing/Variants/Compute.hs view
@@ -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 <beschmi@gmail.com>@@ -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.
src/Term/Positions.hs view
@@ -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]
src/Term/Rewriting/Definitions.hs view
@@ -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 <beschmi@gmail.com>@@ -11,13 +10,13 @@ Equal (..) , evalEqual - -- * Matching Problems+ -- * Matching problems , Match(..) , flattenMatch , matchWith , matchOnlyIf - -- * Rewriting Rules+ -- * Rewriting rules , RRule(..) ) where
src/Term/Rewriting/Norm.hs view
@@ -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 <beschmi@gmail.com> ----- This module implements normalization with respect to DH u AC using class--- rewriting and an ad-hoc function that uses the @TermAC@ representation of--- terms modulo AC.+-- 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]
src/Term/Substitution.hs view
@@ -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 <beschmi@gmail.com>@@ -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
src/Term/Substitution/SubstVFree.hs view
@@ -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 <beschmi@gmail.com>@@ -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)
src/Term/Substitution/SubstVFresh.hs view
@@ -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 <beschmi@gmail.com>@@ -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.
src/Term/Subsumption.hs view
@@ -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 <beschmi@gmail.com>@@ -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)
src/Term/SubtermRule.hs view
@@ -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 <beschmi@gmail.com>@@ -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
src/Term/Term.hs view
@@ -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 <beschmi@gmail.com> -- -- 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 )
+ src/Term/Term/Classes.hs view
@@ -0,0 +1,14 @@+-- |+-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier+-- License : GPL v3 (see LICENSE)+-- +-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>+--+-- | 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
+ src/Term/Term/FunctionSymbols.hs view
@@ -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 <beschmi@gmail.com>+--+-- 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)
+ src/Term/Term/Raw.hs view
@@ -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 <beschmi@gmail.com>+--+-- 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 )
src/Term/Unification.hs view
@@ -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
src/Term/UnitTests.hs view
@@ -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 <beschmi@gmail.com> -- -- 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
src/Term/VTerm.hs view
@@ -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 <beschmi@gmail.com>@@ -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
tamarin-prover-term.cabal view
@@ -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