module Theory.Model.Rule (
Rule(..)
, PremIdx(..)
, ConcIdx(..)
, rInfo
, rPrems
, rConcs
, rActs
, rPrem
, rConc
, lookupPrem
, lookupConc
, enumPrems
, enumConcs
, RuleInfo(..)
, ruleInfo
, ProtoRuleName(..)
, ProtoRuleACInfo(..)
, pracName
, pracVariants
, pracLoopBreakers
, ProtoRuleACInstInfo(..)
, praciName
, praciLoopBreakers
, RuleACConstrs
, IntrRuleACInfo(..)
, ProtoRuleE
, ProtoRuleAC
, IntrRuleAC
, RuleAC
, RuleACInst
, HasRuleName(..)
, isIntruderRule
, isDestrRule
, isConstrRule
, isFreshRule
, isIRecvRule
, isISendRule
, isCoerceRule
, nfRule
, isTrivialProtoVariantAC
, ruleACToIntrRuleAC
, ruleACIntrToRuleAC
, ruleACIntrToRuleACInst
, someRuleACInst
, unifyRuleACInstEqs
, unifiableRuleACInsts
, reservedRuleNames
, showRuleCaseName
, prettyProtoRuleName
, prettyRuleName
, prettyProtoRuleE
, prettyProtoRuleAC
, prettyIntrRuleAC
, prettyIntrRuleACInfo
, prettyRuleAC
, prettyLoopBreakers
, prettyRuleACInst
) where
import Prelude hiding (id, (.))
import Data.Binary
import qualified Data.ByteString.Char8 as BC
import Data.DeriveTH
import Data.Foldable (foldMap)
import Data.Generics
import Data.List
import Data.Monoid
import Safe
import Control.Basics
import Control.Category
import Control.DeepSeq
import Control.Monad.Bind
import Control.Monad.Reader
import Extension.Data.Label hiding (get)
import qualified Extension.Data.Label as L
import Logic.Connectives
import Term.LTerm
import Term.Rewriting.Norm (nf')
import Term.Unification
import Theory.Model.Fact
import Theory.Text.Pretty
data Rule i = Rule {
_rInfo :: i
, _rPrems :: [LNFact]
, _rConcs :: [LNFact]
, _rActs :: [LNFact]
}
deriving( Eq, Ord, Show, Data, Typeable )
$(mkLabels [''Rule])
newtype PremIdx = PremIdx { getPremIdx :: Int }
deriving( Eq, Ord, Show, Enum, Data, Typeable, Binary, NFData )
newtype ConcIdx = ConcIdx { getConcIdx :: Int }
deriving( Eq, Ord, Show, Enum, Data, Typeable, Binary, NFData )
lookupPrem :: PremIdx -> Rule i -> Maybe LNFact
lookupPrem i = (`atMay` getPremIdx i) . L.get rPrems
lookupConc :: ConcIdx -> Rule i -> Maybe LNFact
lookupConc i = (`atMay` getConcIdx i) . L.get rConcs
rPrem :: PremIdx -> (Rule i :-> LNFact)
rPrem i = nthL (getPremIdx i) . rPrems
rConc :: ConcIdx -> (Rule i :-> LNFact)
rConc i = nthL (getConcIdx i) . rConcs
enumPrems :: Rule i -> [(PremIdx, LNFact)]
enumPrems = zip [(PremIdx 0)..] . L.get rPrems
enumConcs :: Rule i -> [(ConcIdx, LNFact)]
enumConcs = zip [(ConcIdx 0)..] . L.get rConcs
instance Functor Rule where
fmap f (Rule i ps cs as) = Rule (f i) ps cs as
instance (Show i, HasFrees i) => HasFrees (Rule i) where
foldFrees f (Rule i ps cs as) =
(foldFrees f i `mappend`) $
(foldFrees f ps `mappend`) $
(foldFrees f cs `mappend`) $
(foldFrees f as)
foldFreesOcc f c (Rule i ps cs as) =
foldFreesOcc f ((show i):c) (ps, cs, as)
mapFrees f (Rule i ps cs as) =
Rule <$> mapFrees f i
<*> mapFrees f ps <*> mapFrees f cs <*> mapFrees f as
instance Apply i => Apply (Rule i) where
apply subst (Rule i ps cs as) =
Rule (apply subst i) (apply subst ps) (apply subst cs) (apply subst as)
instance Sized (Rule i) where
size (Rule _ ps cs as) = size ps + size cs + size as
data RuleInfo p i =
ProtoInfo p
| IntrInfo i
deriving( Eq, Ord, Show )
ruleInfo :: (p -> c) -> (i -> c) -> RuleInfo p i -> c
ruleInfo proto _ (ProtoInfo x) = proto x
ruleInfo _ intr (IntrInfo x) = intr x
instance (HasFrees p, HasFrees i) => HasFrees (RuleInfo p i) where
foldFrees f = ruleInfo (foldFrees f) (foldFrees f)
foldFreesOcc _ _ = const mempty
mapFrees f = ruleInfo (fmap ProtoInfo . mapFrees f)
(fmap IntrInfo . mapFrees f)
instance (Apply p, Apply i) => Apply (RuleInfo p i) where
apply subst = ruleInfo (ProtoInfo . apply subst) (IntrInfo . apply subst)
data ProtoRuleName =
FreshRule
| StandRule String
deriving( Eq, Ord, Show, Data, Typeable )
data ProtoRuleACInfo = ProtoRuleACInfo
{ _pracName :: ProtoRuleName
, _pracVariants :: Disj (LNSubstVFresh)
, _pracLoopBreakers :: [PremIdx]
}
deriving( Eq, Ord, Show )
data ProtoRuleACInstInfo = ProtoRuleACInstInfo
{ _praciName :: ProtoRuleName
, _praciLoopBreakers :: [PremIdx]
}
deriving( Eq, Ord, Show )
$(mkLabels [''ProtoRuleACInfo, ''ProtoRuleACInstInfo])
instance Apply ProtoRuleName where
apply _ = id
instance HasFrees ProtoRuleName where
foldFrees _ = const mempty
foldFreesOcc _ _ = const mempty
mapFrees _ = pure
instance Apply PremIdx where
apply _ = id
instance HasFrees PremIdx where
foldFrees _ = const mempty
foldFreesOcc _ _ = const mempty
mapFrees _ = pure
instance Apply ConcIdx where
apply _ = id
instance HasFrees ConcIdx where
foldFrees _ = const mempty
foldFreesOcc _ _ = const mempty
mapFrees _ = pure
instance HasFrees ProtoRuleACInfo where
foldFrees f (ProtoRuleACInfo na vari breakers) =
foldFrees f na `mappend` foldFrees f vari
`mappend` foldFrees f breakers
foldFreesOcc _ _ = const mempty
mapFrees f (ProtoRuleACInfo na vari breakers) =
ProtoRuleACInfo na <$> mapFrees f vari <*> mapFrees f breakers
instance Apply ProtoRuleACInstInfo where
apply _ = id
instance HasFrees ProtoRuleACInstInfo where
foldFrees f (ProtoRuleACInstInfo na breakers) =
foldFrees f na `mappend` foldFrees f breakers
foldFreesOcc _ _ = const mempty
mapFrees f (ProtoRuleACInstInfo na breakers) =
ProtoRuleACInstInfo na <$> mapFrees f breakers
data IntrRuleACInfo =
ConstrRule BC.ByteString
| DestrRule BC.ByteString
| CoerceRule
| IRecvRule
| ISendRule
| PubConstrRule
| FreshConstrRule
deriving( Ord, Eq, Show, Data, Typeable )
type IntrRuleAC = Rule IntrRuleACInfo
ruleACToIntrRuleAC :: RuleAC -> Maybe IntrRuleAC
ruleACToIntrRuleAC (Rule (IntrInfo i) ps cs as) = Just (Rule i ps cs as)
ruleACToIntrRuleAC _ = Nothing
ruleACIntrToRuleAC :: IntrRuleAC -> RuleAC
ruleACIntrToRuleAC (Rule ri ps cs as) = Rule (IntrInfo ri) ps cs as
ruleACIntrToRuleACInst :: IntrRuleAC -> RuleACInst
ruleACIntrToRuleACInst (Rule ri ps cs as) = Rule (IntrInfo ri) ps cs as
instance Apply IntrRuleACInfo where
apply _ = id
instance HasFrees IntrRuleACInfo where
foldFrees _ = const mempty
foldFreesOcc _ _ = const mempty
mapFrees _ = pure
type ProtoRuleE = Rule ProtoRuleName
type ProtoRuleAC = Rule ProtoRuleACInfo
type RuleAC = Rule (RuleInfo ProtoRuleACInfo IntrRuleACInfo)
type RuleACInst = Rule (RuleInfo ProtoRuleACInstInfo IntrRuleACInfo)
class HasRuleName t where
ruleName :: t -> RuleInfo ProtoRuleName IntrRuleACInfo
instance HasRuleName ProtoRuleE where
ruleName = ProtoInfo . L.get rInfo
instance HasRuleName RuleAC where
ruleName = ruleInfo (ProtoInfo . L.get pracName) IntrInfo . L.get rInfo
instance HasRuleName ProtoRuleAC where
ruleName = ProtoInfo . L.get (pracName . rInfo)
instance HasRuleName IntrRuleAC where
ruleName = IntrInfo . L.get rInfo
instance HasRuleName RuleACInst where
ruleName = ruleInfo (ProtoInfo . L.get praciName) IntrInfo . L.get rInfo
isDestrRule :: HasRuleName r => r -> Bool
isDestrRule ru = case ruleName ru of
IntrInfo (DestrRule _) -> True
_ -> False
isConstrRule :: HasRuleName r => r -> Bool
isConstrRule ru = case ruleName ru of
IntrInfo (ConstrRule _) -> True
IntrInfo FreshConstrRule -> True
IntrInfo PubConstrRule -> True
IntrInfo CoerceRule -> True
_ -> False
isFreshRule :: HasRuleName r => r -> Bool
isFreshRule = (ProtoInfo FreshRule ==) . ruleName
isIRecvRule :: HasRuleName r => r -> Bool
isIRecvRule = (IntrInfo IRecvRule ==) . ruleName
isISendRule :: HasRuleName r => r -> Bool
isISendRule = (IntrInfo ISendRule ==) . ruleName
isCoerceRule :: HasRuleName r => r -> Bool
isCoerceRule = (IntrInfo CoerceRule ==) . ruleName
nfRule :: Rule i -> WithMaude Bool
nfRule (Rule _ ps cs as) = reader $ \hnd ->
all (nfFactList hnd) [ps, cs, as]
where
nfFactList hnd xs =
getAll $ foldMap (foldMap (All . (\t -> nf' t `runReader` hnd))) xs
isIntruderRule :: HasRuleName r => r -> Bool
isIntruderRule ru =
case ruleName ru of IntrInfo _ -> True; ProtoInfo _ -> False
isTrivialProtoVariantAC :: ProtoRuleAC -> ProtoRuleE -> Bool
isTrivialProtoVariantAC (Rule info ps as cs) (Rule _ ps' as' cs') =
L.get pracVariants info == Disj [emptySubstVFresh]
&& ps == ps' && as == as' && cs == cs'
type RuleACConstrs = Disj LNSubstVFresh
someRuleACInst :: MonadFresh m
=> RuleAC
-> m (RuleACInst, Maybe RuleACConstrs)
someRuleACInst =
fmap extractInsts . rename
where
extractInsts (Rule (ProtoInfo i) ps cs as) =
( Rule (ProtoInfo i') ps cs as
, Just (L.get pracVariants i)
)
where
i' = ProtoRuleACInstInfo (L.get pracName i) (L.get pracLoopBreakers i)
extractInsts (Rule (IntrInfo i) ps cs as) =
( Rule (IntrInfo i) ps cs as, Nothing )
unifyRuleACInstEqs :: [Equal RuleACInst] -> WithMaude [LNSubstVFresh]
unifyRuleACInstEqs eqs
| all unifiable eqs = unifyLNFactEqs $ concatMap ruleEqs eqs
| otherwise = return []
where
unifiable (Equal ru1 ru2) =
L.get rInfo ru1 == L.get rInfo ru2
&& length (L.get rPrems ru1) == length (L.get rPrems ru2)
&& length (L.get rConcs ru1) == length (L.get rConcs ru2)
ruleEqs (Equal ru1 ru2) =
zipWith Equal (L.get rPrems ru1) (L.get rPrems ru2) ++
zipWith Equal (L.get rConcs ru1) (L.get rConcs ru2)
unifiableRuleACInsts :: RuleACInst -> RuleACInst -> WithMaude Bool
unifiableRuleACInsts ru1 ru2 =
(not . null) <$> unifyRuleACInstEqs [Equal ru1 ru2]
prefixIfReserved :: String -> String
prefixIfReserved n
| n `elem` reservedRuleNames = "_" ++ n
| "_" `isPrefixOf` n = "_" ++ n
| otherwise = n
reservedRuleNames :: [String]
reservedRuleNames = ["Fresh", "irecv", "isend", "coerce", "fresh", "pub"]
prettyProtoRuleName :: Document d => ProtoRuleName -> d
prettyProtoRuleName rn = text $ case rn of
FreshRule -> "Fresh"
StandRule n -> prefixIfReserved n
prettyRuleName :: (HighlightDocument d, HasRuleName (Rule i)) => Rule i -> d
prettyRuleName = ruleInfo prettyProtoRuleName prettyIntrRuleACInfo . ruleName
showRuleCaseName :: HasRuleName (Rule i) => Rule i -> String
showRuleCaseName =
render . ruleInfo prettyProtoRuleName prettyIntrRuleACInfo . ruleName
prettyIntrRuleACInfo :: Document d => IntrRuleACInfo -> d
prettyIntrRuleACInfo rn = text $ case rn of
IRecvRule -> "irecv"
ISendRule -> "isend"
CoerceRule -> "coerce"
FreshConstrRule -> "fresh"
PubConstrRule -> "pub"
ConstrRule name -> prefixIfReserved ('c' : BC.unpack name)
DestrRule name -> prefixIfReserved ('d' : BC.unpack name)
prettyNamedRule :: (HighlightDocument d, HasRuleName (Rule i))
=> d
-> (i -> d)
-> Rule i -> d
prettyNamedRule prefix ppInfo ru =
prefix <-> prettyRuleName ru <> colon $-$
nest 2 (sep [ nest 1 $ ppFactsList rPrems
, if null (L.get rActs ru)
then operator_ "-->"
else fsep [operator_ "--[", ppFacts rActs, operator_ "]->"]
, nest 1 $ ppFactsList rConcs]) $-$
nest 2 (ppInfo $ L.get rInfo ru)
where
ppList pp = fsep . punctuate comma . map pp
ppFacts proj = ppList prettyLNFact $ L.get proj ru
ppFactsList proj = fsep [operator_ "[", ppFacts proj, operator_ "]"]
prettyProtoRuleACInfo :: HighlightDocument d => ProtoRuleACInfo -> d
prettyProtoRuleACInfo i =
(ppVariants $ L.get pracVariants i) $-$
prettyLoopBreakers i
where
ppVariants (Disj [subst]) | subst == emptySubstVFresh = emptyDoc
ppVariants substs = kwVariantsModulo "AC" $-$ prettyDisjLNSubstsVFresh substs
prettyLoopBreakers :: HighlightDocument d => ProtoRuleACInfo -> d
prettyLoopBreakers i = case breakers of
[] -> emptyDoc
[_] -> lineComment_ $ "loop breaker: " ++ show breakers
_ -> lineComment_ $ "loop breakers: " ++ show breakers
where
breakers = getPremIdx <$> L.get pracLoopBreakers i
prettyProtoRuleE :: HighlightDocument d => ProtoRuleE -> d
prettyProtoRuleE = prettyNamedRule (kwRuleModulo "E") (const emptyDoc)
prettyRuleAC :: HighlightDocument d => RuleAC -> d
prettyRuleAC =
prettyNamedRule (kwRuleModulo "AC")
(ruleInfo prettyProtoRuleACInfo (const emptyDoc))
prettyIntrRuleAC :: HighlightDocument d => IntrRuleAC -> d
prettyIntrRuleAC = prettyNamedRule (kwRuleModulo "AC") (const emptyDoc)
prettyProtoRuleAC :: HighlightDocument d => ProtoRuleAC -> d
prettyProtoRuleAC = prettyNamedRule (kwRuleModulo "AC") prettyProtoRuleACInfo
prettyRuleACInst :: HighlightDocument d => RuleACInst -> d
prettyRuleACInst = prettyNamedRule (kwInstanceModulo "AC") (const emptyDoc)
$( derive makeBinary ''Rule)
$( derive makeBinary ''ProtoRuleName)
$( derive makeBinary ''ProtoRuleACInfo)
$( derive makeBinary ''ProtoRuleACInstInfo)
$( derive makeBinary ''RuleInfo)
$( derive makeBinary ''IntrRuleACInfo)
$( derive makeNFData ''Rule)
$( derive makeNFData ''ProtoRuleName)
$( derive makeNFData ''ProtoRuleACInfo)
$( derive makeNFData ''ProtoRuleACInstInfo)
$( derive makeNFData ''RuleInfo)
$( derive makeNFData ''IntrRuleACInfo)