module Term.Maude.Signature (
MaudeSig
, enableDH
, enableBP
, enableMSet
, stFunSyms
, stRules
, funSyms
, irreducibleFunSyms
, rrulesForMaudeSig
, noEqFunSyms
, dhMaudeSig
, pairMaudeSig
, asymEncMaudeSig
, symEncMaudeSig
, signatureMaudeSig
, hashMaudeSig
, msetMaudeSig
, bpMaudeSig
, minimalMaudeSig
, addFunSym
, addStRule
, prettyMaudeSig
) where
import Term.Term
import Term.LTerm
import Term.Builtin.Rules
import Term.SubtermRule
import Control.Monad.Fresh
import Control.Applicative
import Control.DeepSeq
import Data.DeriveTH
import Data.Binary
import Data.Foldable (asum)
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as S
import qualified Data.ByteString.Char8 as BC
import qualified Text.PrettyPrint.Highlight as P
data MaudeSig = MaudeSig
{ enableDH :: Bool
, enableBP :: Bool
, enableMSet :: Bool
, stFunSyms :: S.Set NoEqSym
, stRules :: S.Set StRule
, funSyms :: FunSig
, irreducibleFunSyms :: FunSig
}
deriving (Ord, Show, Eq)
maudeSig :: MaudeSig -> MaudeSig
maudeSig msig@(MaudeSig {enableDH,enableBP,enableMSet,stFunSyms,stRules}) =
msig {enableDH=enableDH||enableBP, funSyms=allfuns, irreducibleFunSyms=irreduciblefuns}
where
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 o _) _ <- S.toList stRules ]
`S.union` dhReducibleFunSig `S.union` bpReducibleFunSig
instance Monoid MaudeSig where
(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
noEqFunSyms :: MaudeSig -> NoEqFunSig
noEqFunSyms msig = S.fromList [ o | NoEq o <- S.toList (funSyms msig) ]
addFunSym :: NoEqSym -> MaudeSig -> MaudeSig
addFunSym funsym msig =
msig `mappend` mempty {stFunSyms=S.fromList [funsym]}
addStRule :: StRule -> MaudeSig -> MaudeSig
addStRule str msig =
msig `mappend` mempty {stRules=S.fromList [str]}
rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)
rrulesForMaudeSig (MaudeSig {enableDH, enableBP, enableMSet, stRules}) =
(S.map stRuleToRRule stRules)
`S.union` (if enableDH then dhRules else S.empty)
`S.union` (if enableBP then bpRules else S.empty)
`S.union` (if enableMSet then msetRules else S.empty)
dhMaudeSig, bpMaudeSig, msetMaudeSig :: MaudeSig
dhMaudeSig = maudeSig $ mempty {enableDH=True}
bpMaudeSig = maudeSig $ mempty {enableBP=True}
msetMaudeSig = maudeSig $ mempty {enableMSet=True}
pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig :: MaudeSig
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}
minimalMaudeSig :: MaudeSig
minimalMaudeSig = pairMaudeSig
prettyMaudeSig :: P.HighlightDocument d => MaudeSig -> d
prettyMaudeSig sig = P.vcat
[ ppNonEmptyList' "builtins:" P.text builtIns
, ppNonEmptyList' "functions:" ppFunSymb $ S.toList (stFunSyms sig)
, ppNonEmptyList
(\ds -> P.sep (P.keyword_ "equations:" : map (P.nest 2) ds))
prettyStRule $ S.toList (stRules sig)
]
where
ppNonEmptyList' name = ppNonEmptyList ((P.keyword_ name P.<->) . P.fsep)
ppNonEmptyList _ _ [] = P.emptyDoc
ppNonEmptyList hdr pp xs = hdr $ P.punctuate P.comma $ map pp xs
builtIns = asum $ map (\(f, x) -> guard (f sig) *> pure x)
[ (enableDH, "diffie-hellman")
, (enableBP, "bilinear-pairing")
, (enableMSet, "multiset")
]
ppFunSymb (f,(k,priv)) = P.text $ BC.unpack f ++ "/" ++ show k ++ showPriv priv
where showPriv Private = " [private]"
showPriv Public = ""
$(derive makeBinary ''MaudeSig)
$(derive makeNFData ''MaudeSig)