module Scyther.Sequent (
Sequent(..)
, seProto
, wellTypedCases
, saturate
, frule
, fruleInst
, chainRule
, splitEq
, exploitTyping
, uniqueTIDQuantifiers
) where
import Data.Maybe
import qualified Data.Map as M
import qualified Data.Set as S
import Data.Data
import Control.Arrow
import Control.Monad
import qualified Scyther.Equalities as E
import Scyther.Facts
import Scyther.Formula
data Sequent = Sequent {
sePrem :: Facts
, seConcl :: Formula
}
deriving( Eq, Show, Ord, Data, Typeable )
seProto :: Sequent -> Protocol
seProto = protocol . sePrem
uniqueTIDQuantifiers :: Sequent -> Sequent
uniqueTIDQuantifiers (Sequent prem concl) =
Sequent prem (relabelTIDs [nextTID prem..] concl)
changePrem :: MonadPlus m => (Facts -> m Facts) -> Sequent -> m Sequent
changePrem f se = do
let prem0 = sePrem se
prem1 <- f prem0
guard (prem0 /= prem1)
return $ se { sePrem = prem1 }
wellTypedCases :: MonadPlus m => Sequent -> m [(String, Sequent)]
wellTypedCases se = case seConcl se of
FAtom (ATyping someTyp) ->
return $ protoRoles (seProto se) >>= roleProofs someTyp
_ -> mzero
where
roleProofs someTyp role = proveRecvs S.empty (roleSteps role)
where
proveRecvs _ [] = []
proveRecvs recv ( Send _ _ : steps) = proveRecvs recv steps
proveRecvs recv ((Recv _ (PMVar lid)) : steps) =
proveRecvs (S.insert lid recv) steps
proveRecvs recv (step@(Recv _ pt) : steps) =
let mvars = patFMV pt
in (S.toList mvars >>= proveVar) `mplus`
(proveRecvs (recv `S.union` mvars) steps)
where
proveVar v
| v `S.member` recv = fail "proveVar: not first receive"
| otherwise = do
return (name, Sequent prem concl)
where
name = roleName role ++ "_" ++ stepLabel step ++ "_" ++ getId v
(tid, prem0) = freshTID (sePrem se)
mv = MVar (LocalId (v, tid))
premErr = error $ "wellTypedCases: could not add thread " ++ show tid ++ ". This should not happen."
prem1 = maybe premErr saturateFacts . join $
conjoinAtoms [AEv (Step tid step), AEq (E.TIDRoleEq (tid, role))] prem0
prem = fromMaybe (error "failed to set typing") $ setTyping someTyp prem1
concl = FAtom $
case someTyp of
WeaklyAtomic -> AHasType mv Nothing
Typing typ -> case M.lookup (v, role) typ of
Just ty -> AHasType mv (Just ty)
Nothing -> error $
"wellTypedCases: no type given for '"++show v++"' in role '"++roleName role++"'"
fruleInst :: MonadPlus m
=> Sequent
-> E.Mapping
-> Sequent
-> m (Maybe Sequent)
fruleInst rule mapping state = do
atoms <- conjunctionToAtoms $ seConcl rule
let statePrem = sePrem state
guard (proveFacts statePrem (sePrem rule) mapping)
optStatePrem' <- conjoinAtoms (map (substAtom (E.getMappingEqs mapping)) atoms) statePrem
case optStatePrem' of
Nothing -> do return Nothing
Just statePrem' -> do guard (statePrem /= statePrem')
return . Just $ Sequent statePrem' (seConcl state)
frule :: MonadPlus m
=> Sequent
-> Sequent
-> m (E.Mapping, Maybe Sequent)
frule rule state = case resolutions of
[] -> mzero
res : _ -> return res
where
resolutions = do
mapping <- freeVariableMappings (sePrem rule) (sePrem state)
((,) mapping) `liftM` fruleInst rule mapping state
saturate :: MonadPlus m => Sequent -> m Sequent
saturate = changePrem (return . saturateFacts)
chainRule :: MonadPlus m
=> Sequent -> Message
-> m [((String, [Either TID AgentId]), Sequent)]
chainRule se m =
map (second mkSequent) `liftM` chainRuleFacts m (sePrem se)
where
mkSequent prem = Sequent prem (seConcl se)
exploitTyping :: MonadPlus m => Sequent -> m Sequent
exploitTyping = changePrem exploitTypingFacts
splitEq :: E.MsgEq -> Sequent -> [Maybe Sequent]
splitEq eq se
| eq `elem` splittableEqs prems = map (fmap updPrem) $ splitEqFacts eq prems
| otherwise = error $ "splitEq: equality not present"
where
prems = sePrem se
updPrem prem' = se {sePrem = prem'}