module Scyther.Theory.Parser (
Token
, Keyword(..)
, scanString
, scanFile
, Parser
, parseFile
, liftMaybe
, liftMaybe'
, token
, kw
, betweenKWs
, commaSep
, commaSep1
, list
, braced
, parens
, brackets
, singleQuoted
, doubleQuoted
, identifier
, string
, strings
, integer
, genFunOpen
, genFunApp
, funOpen
, funApp
, protocol
, claims
, theory
, parseTheory
, mkLTSPat
, mkMultIdentityPat
, mkExpPat
, mkMultPat
, destLTSPat
, destMultIdentityPat
, destExpPat
, destMultPat
) where
import Data.Char
import Data.List
import qualified Data.Set as S
import Data.DAG.Simple
import Data.Foldable (asum)
import Control.Arrow ( (***) )
import Control.Monad hiding (sequence)
import Control.Applicative hiding (empty, many, optional)
import Text.Parsec hiding (token, (<|>), string )
import qualified Text.Parsec as P
import Text.Parsec.Pos
import qualified Scyther.Equalities as E
import Scyther.Facts as F hiding (protocol)
import Scyther.Sequent
import Scyther.Proof
import Scyther.Theory
import Scyther.Theory.Lexer
type Token = (SourcePos, Keyword)
scanString :: FilePath -> String -> [Token]
scanString filename s =
case runAlex s gatherUntilEOF of
Left err -> error err
Right kws -> kws
where
gatherUntilEOF = do
AlexPn _ line col <- alexGetPos
let pos = newPos filename line col
k <- alexMonadScan
case k of
EOF -> return [(pos,EOF)]
_ -> do kws <- gatherUntilEOF
return $ (pos,k) : kws
type Parser s a = Parsec [Token] s a
liftMaybe :: MonadPlus m => Maybe a -> m a
liftMaybe = maybe mzero return
liftMaybe' :: Monad m => String -> Maybe a -> m a
liftMaybe' msg = maybe (fail msg) return
token :: (Keyword -> Maybe a) -> Parser s a
token p = P.token (show . snd) fst (p . snd)
kw :: Keyword -> Parser s ()
kw t = token check
where
check t' | t == t' = Just () | otherwise = Nothing
betweenKWs :: Keyword -> Keyword -> Parser s a -> Parser s a
betweenKWs l r = between (kw l) (kw r)
braced :: Parser s a -> Parser s a
braced = betweenKWs LBRACE RBRACE
parens :: Parser s a -> Parser s a
parens = betweenKWs LPAREN RPAREN
brackets :: Parser s a -> Parser s a
brackets = betweenKWs LBRACKET RBRACKET
singleQuoted :: Parser s a -> Parser s a
singleQuoted = betweenKWs SQUOTE SQUOTE
doubleQuoted :: Parser s a -> Parser s a
doubleQuoted = betweenKWs DQUOTE DQUOTE
identifier :: Parser s String
identifier = token extract
where extract (IDENT name) = Just $ name
extract _ = Nothing
string :: String -> Parser s ()
string cs = (try $ do { i <- identifier; guard (i == cs) }) <?> ('`' : cs ++ "'")
strings :: [String] -> Parser s ()
strings = mapM_ string
integer :: Parser s Int
integer = do i <- identifier
guard (all isDigit i)
return (read i)
commaSep :: Parser s a -> Parser s [a]
commaSep = (`sepBy` kw COMMA)
commaSep1 :: Parser s a -> Parser s [a]
commaSep1 = (`sepBy1` kw COMMA)
list :: Parser s a -> Parser s [a]
list p = kw LBRACKET *> commaSep p <* kw RBRACKET
scanFile :: FilePath -> IO [Token]
scanFile f = do
s <- readFile f
return $ scanString f s
parseFile :: Parser s a -> s -> FilePath -> IO a
parseFile parser state f = do
s <- readFile f
case runParser parser state f (scanString f s) of
Right p -> return p
Left err -> error $ show err
parseTheory :: FilePath -> IO Theory
parseTheory = parseFile theory ()
ident :: Parser s Id
ident = Id <$> identifier
genFunOpen :: Parser s a -> Parser s b -> Parser s a
genFunOpen ldelim f = try $ f *> ldelim
genFunApp :: Parser s a -> Parser s b -> Parser s d -> Parser s c -> Parser s c
genFunApp ldelim rdelim f arg = genFunOpen ldelim f *> arg <* rdelim
funOpen :: String -> Parser s ()
funOpen = genFunOpen (kw LPAREN) . string
funApp :: String -> Parser s a -> Parser s a
funApp = genFunApp (kw LPAREN) (kw RPAREN) . string
mkLTSPat :: Pattern -> Pattern
mkLTSPat x = PHash (PTup (PConst (Id "PARSE_LTS")) x)
mkMultIdentityPat :: Pattern
mkMultIdentityPat = PHash (PConst (Id "PARSE_MULT_IDENTITY"))
mkExpPat :: Pattern -> Pattern -> Pattern
mkExpPat x y = PHash (PTup (PConst (Id "PARSE_EXP")) (PTup x y))
mkMultPat :: Pattern -> Pattern -> Pattern
mkMultPat x y = PHash (PTup (PConst (Id "PARSE_MULT")) (PTup x y))
destLTSPat :: Pattern -> Maybe Pattern
destLTSPat (PHash (PTup (PConst (Id "PARSE_LTS")) x)) = return x
destLTSPat _ = mzero
destMultIdentityPat :: Pattern -> Maybe ()
destMultIdentityPat (PHash (PConst (Id "PARSE_MULT_IDENTITY"))) = return ()
destMultIdentityPat _ = mzero
destExpPat :: Pattern -> Maybe (Pattern, Pattern)
destExpPat (PHash (PTup (PConst (Id "PARSE_EXP")) (PTup x y))) = return (x,y)
destExpPat _ = mzero
destMultPat :: Pattern -> Maybe (Pattern, Pattern)
destMultPat (PHash (PTup (PConst (Id "PARSE_MULT")) (PTup x y))) = return (x,y)
destMultPat _ = mzero
pattern :: Parser s Pattern
pattern = asum
[ string "1" *> pure mkMultIdentityPat
, PConst <$> singleQuoted ident
, PMVar <$> (kw QUESTIONMARK *> ident)
, PAVar <$> (kw DOLLAR *> ident)
, PFresh <$> (kw TILDE *> ident)
, parens tuplepattern
, PHash <$> funApp "h" tuplepattern
, mkLTSPat <$> funApp "lts" tuplepattern
, PSymK <$> (try (funOpen "k") *> multpattern <* kw COMMA) <*> (multpattern <* kw RPAREN)
, PShrK <$> (try (string "k" *> kw LBRACKET) *> multpattern <* kw COMMA)
<*> (multpattern <* kw RBRACKET)
, PAsymPK <$> funApp "pk" tuplepattern
, PAsymSK <$> funApp "sk" tuplepattern
, PEnc <$> braced tuplepattern <*> pattern
, PSign <$> genFunApp (kw LBRACE) (kw RBRACE) (string "sign") tuplepattern <*> pattern
, PMVar <$> tempIdentifier
]
where
tempIdentifier = do i <- identifier
if isLetter (head i)
then return (Id (' ':i))
else fail $ "invalid variable name '" ++ i ++
"': variable names must start with a letter"
exppattern :: Parser s Pattern
exppattern = chainl1 pattern (mkExpPat <$ kw HAT)
multpattern :: Parser s Pattern
multpattern = chainl1 exppattern (mkMultPat <$ kw STAR)
tuplepattern :: Parser s Pattern
tuplepattern = chainr1 multpattern (PTup <$ kw COMMA)
dropSpacePrefix :: Id -> Id
dropSpacePrefix (Id (' ':i)) = Id i
dropSpacePrefix i = i
resolveId :: S.Set Id -> S.Set Id -> Id -> Pattern
resolveId avars mvars i
| i `S.member` avars = PAVar i
| i `S.member` mvars = PMVar i
| otherwise = PFresh i
resolveIds :: S.Set Id -> S.Set Id -> Pattern -> Pattern
resolveIds avars mvars = go
where
resolve = resolveId avars mvars
go pt@(PConst _) = pt
go pt@(PFresh _) = pt
go pt@(PAVar _) = pt
go pt@(PMVar i) = case getId i of
' ':i' -> resolve (Id i')
_ -> pt
go (PHash pt) = PHash (go pt)
go (PTup pt1 pt2) = PTup (go pt1) (go pt2)
go (PEnc pt1 pt2) = PEnc (go pt1) (go pt2)
go (PSign pt1 pt2) = PSign (go pt1) (go pt2)
go (PSymK pt1 pt2) = PSymK (go pt1) (go pt2)
go (PShrK pt1 pt2) = PShrK (go pt1) (go pt2)
go (PAsymPK pt) = PAsymPK (go pt)
go (PAsymSK pt) = PAsymSK (go pt)
resolveIdsLocalToRole :: Role -> Pattern -> Pattern
resolveIdsLocalToRole role = resolveIds (roleFAV role) (roleFMV role)
threadId :: Parser s TID
threadId = TID <$> (kw SHARP *> integer)
localIdentifier :: Parser s LocalId
localIdentifier = LocalId <$> ((,) <$> ident <*> threadId)
resolveTID :: MonadPlus m => E.Mapping -> TID -> m Role
resolveTID mapping tid =
liftMaybe' ("resolveTID: no role assigned to thread "++show tid)
(E.threadRole tid (E.getMappingEqs mapping))
resolveLocalId :: MonadPlus m => E.Mapping -> LocalId -> m Message
resolveLocalId mapping (LocalId (i, tid)) =
do role <- resolveTID mapping tid
return $ inst tid (resolveId (roleFAV role) (roleFMV role) i)
`mplus`
(fail $ "resolveLocalId: no role defined for thread " ++ show tid)
resolveStep :: MonadPlus m => E.Mapping -> TID -> String -> m RoleStep
resolveStep mapping tid stepId = do
role <- resolveTID mapping tid
let roleId = roleName role
if isPrefixOf roleId stepId
then liftMaybe' ("resolveStep: step '"++stepId++"' not part of role '"++roleName role++"'")
(lookupRoleStep (drop (length roleId + 1) stepId) role)
else fail ("resolveStep: role of step '"++stepId++"' does not agree to role '"
++roleName role++"' of thread "++show tid)
instantiation :: MonadPlus m => Parser s (E.Mapping -> m Message)
instantiation = do
tid <- TID <$> (funOpen "inst" *> integer <* kw COMMA)
m <- (do i <- identifier
let (stepId, iTyp) = splitAt (length i 3) i
when (iTyp /= "_pt") (fail $ "inst: could not resolve pattern '"++i++"'")
return $ \mapping -> do
step <- resolveStep mapping tid stepId
return (inst tid $ stepPat step)
`mplus`
do pt <- pattern
return $ \mapping -> do
role <- resolveTID mapping tid
return (inst tid $ resolveIds (roleFAV role) (roleFMV role) pt)
)
kw RPAREN
return m
message :: MonadPlus m => Parser s (E.Mapping -> m Message)
message = asum
[ instantiation
, (pure . return . MConst) <$> betweenKWs SQUOTE SQUOTE ident
, parens tuplemessage
, (liftA $ liftM MHash) <$> funApp "h" tuplemessage
, (liftA2 $ liftM2 MSymK) <$> (funOpen "k" *> message) <*> (kw COMMA *> message <* kw RPAREN)
, (liftA $ liftM MAsymPK) <$> funApp "pk" message
, (liftA $ liftM MAsymSK) <$> funApp "sk" message
, (liftA2 $ liftM2 MEnc) <$> braced tuplemessage <*> message
, (liftA $ liftM MInvKey) <$> funApp "inv" tuplemessage
, (flip resolveLocalId) <$> localIdentifier
]
tuplemessage :: MonadPlus m => Parser s (E.Mapping -> m Message)
tuplemessage = chainr1 message ((liftA2 $ liftM2 MTup) <$ kw COMMA)
transfer :: Parser s [(Id, RoleStep)]
transfer = do
lbl <- Label <$> identifier <* kw DOT
(do right <- kw RIGHTARROW *> ident <* kw COLON
pt <- tuplepattern
return [(right, Recv lbl pt)]
<|>
do right <- kw LEFTARROW *> ident <* kw COLON
ptr <- tuplepattern
(do left <- try $ ident <* kw LEFTARROW <* kw COLON
ptl <- tuplepattern
return [(left, Recv lbl ptl),(right, Send lbl ptr)]
<|>
return [(right, Send lbl ptr)]
)
<|>
do left <- ident
(do kw RIGHTARROW
(do right <- ident <* kw COLON
pt <- tuplepattern
return [(left,Send lbl pt), (right, Recv lbl pt)]
<|>
do ptl <- kw COLON *> tuplepattern
(do right <- kw RIGHTARROW *> ident <* kw COLON
ptr <- tuplepattern
return [(left,Send lbl ptl), (right, Recv lbl ptr)]
<|>
do return [(left, Send lbl ptl)]
)
)
<|>
do kw LEFTARROW
(do pt <- kw COLON *> tuplepattern
return [(left, Recv lbl pt)]
<|>
do right <- ident <* kw COLON
pt <- tuplepattern
return [(left, Recv lbl pt), (right, Send lbl pt)]
)
)
)
protocol :: Parser s Protocol
protocol = do
name <- string "protocol" *> identifier
transfers <- concat <$> braced (many1 transfer)
let roleIds = S.fromList $ map fst transfers
roles = do
actor <- S.toList roleIds
let steps = [ step | (i, step) <- transfers, i == actor ]
return $ Role (getId actor)
(ensureFreshSteps actor (S.map addSpacePrefix roleIds) steps)
return $ Protocol name roles
where
addSpacePrefix = Id . (' ':) . getId
dropSpacePrefixes = S.map dropSpacePrefix
ensureFreshSteps actor possibleAvars =
go (S.singleton (addSpacePrefix actor)) S.empty S.empty
where
go _ _ _ [] = []
go avars mvars fresh (Send l pt : rs) =
let avars' = avars `S.union` (((patFMV pt `S.intersection` possibleAvars)
`S.difference` mvars) `S.difference` fresh)
fresh' = fresh `S.union` ((patFMV pt `S.difference` avars') `S.difference` mvars)
pt' = resolveIds (dropSpacePrefixes avars') (dropSpacePrefixes mvars) pt
in Send l pt' : go avars' mvars fresh' rs
go avars mvars fresh (Recv l pt : rs) =
let mvars' = mvars `S.union` ((patFMV pt `S.difference` avars) `S.difference` fresh)
pt' = resolveIds (dropSpacePrefixes avars) (dropSpacePrefixes mvars') pt
in Recv l pt' : go avars mvars' fresh rs
claims :: (String -> Maybe Protocol) -> Parser s [ThyItem]
claims protoMap = do
let mkAxiom (name, se) = ThyTheorem (name, Axiom se)
(multiplicity, mkThyItem) <-
(string "property" *> pure (id, ThySequent)) <|>
(string "properties" *> pure ((concat <$>) . many1, ThySequent)) <|>
(string "axiom" *> pure (id, mkAxiom ))
protoId <- kw LPAREN *> string "of" *> identifier
proto <- liftMaybe' ("unknown protocol '"++protoId++"'") $ protoMap protoId
kw RPAREN
multiplicity $ do
claimId <- try $ identifier <* kw COLON
when ('-' `elem` claimId) (fail $ "hyphen '-' not allowed in property name '"++claimId++"'")
let mkThySequent (mkClaimId, se) = mkThyItem (mkClaimId claimId, se)
singleSequents = map (liftM (return . (,) id) . ($ proto))
[ niagreeSequent, secrecySequent, parseAtomicitySequent, implicationSequent ]
multiSequents = map ($ proto)
[ parseNonceSecrecy, parseFirstSends
, parseTransferTyping, parseAutoProps ]
sequents <- asum $ multiSequents ++ singleSequents
return $ map mkThySequent sequents
parseAutoProps :: Protocol -> Parser s [(String -> String,Sequent)]
parseAutoProps proto =
string "auto" *> kw MINUS *> string "properties" *>
pure (concat
[ transferTyping proto, firstSendSequents proto, nonceSecrecySequents proto ])
parseNonceSecrecy :: Protocol -> Parser s [(String -> String,Sequent)]
parseNonceSecrecy proto =
string "nonce" *> kw MINUS *> string "secrecy" *> pure (nonceSecrecySequents proto)
nonceSecrecySequents :: Protocol -> [(String -> String,Sequent)]
nonceSecrecySequents proto =
concatMap mkSequent . toposort $ protoOrd proto
where
mkSequent (step, role) = case step of
Send _ pt -> do
n@(PFresh i) <- S.toList $ subpatterns pt
guard (not (plainUse pt n) && firstUse n)
return $ secrecySe (MFresh . Fresh) i
Recv _ pt -> do
v@(PMVar i) <- S.toList $ subpatterns pt
guard (not (plainUse pt v) && firstUse v)
return $ secrecySe (MMVar . MVar) i
where
(tid, prem0) = freshTID (empty proto)
(prefix, _) = break (step ==) $ roleSteps role
firstUse = (`S.notMember` (S.unions $ map (subpatterns . stepPat) prefix))
plainUse pt = (`S.member` splitpatterns pt)
avars = [ MAVar (AVar (LocalId (v,tid)))
| (PAVar v) <- S.toList . S.unions . map (subpatterns.stepPat) $ roleSteps role ]
secrecySe constr i =
( (++("_"++roleName role++"_sec_"++getId i))
, Sequent prem (FAtom AFalse)
)
where
Just (Just prem) = conjoinAtoms atoms prem0
atoms = [ AEq (E.TIDRoleEq (tid, role))
, AEv (Step tid step)
, AEv (Learn (constr (LocalId (i, tid))))
] ++ map AUncompr avars
parseFirstSends :: Protocol -> Parser s [(String -> String,Sequent)]
parseFirstSends proto =
string "first" *> kw MINUS *> string "sends" *> pure (firstSendSequents proto)
firstSendSequents :: Protocol -> [(String -> String,Sequent)]
firstSendSequents proto =
concatMap mkRoleSequents $ protoRoles proto
where
mkRoleSequents role =
concatMap mkStepSequents $ zip (inits steps) steps
where
steps = roleSteps role
(tid, prem0) = freshTID (empty proto)
mkStepSequents (_, Recv _ _ ) = []
mkStepSequents (prefix, step@(Send _ pt)) = do
n@(PFresh i) <- S.toList $ splitpatterns pt
guard (n `S.notMember` S.unions (map (subpatterns.stepPat) prefix))
let learn = (Learn (MFresh (Fresh (LocalId (i, tid)))))
atoms = [ AEq (E.TIDRoleEq (tid, role)), AEv learn ]
Just (Just prem) = conjoinAtoms atoms prem0
concl = FAtom (AEvOrd (Step tid step, learn))
return ( (++("_" ++ getId i)), Sequent prem concl)
parseTransferTyping :: Protocol -> Parser s [(String -> String, Sequent)]
parseTransferTyping proto =
string "msc" *> kw MINUS *> string "typing" *> pure (transferTyping proto)
transferTyping :: Protocol -> [(String -> String, Sequent)]
transferTyping proto = case mscTyping proto of
Just typing -> pure
((++"_msc_typing"), Sequent (empty proto) (FAtom (ATyping typing)))
Nothing -> fail "transferTyping: failed to construct typing"
secrecySequent :: Protocol -> Parser s Sequent
secrecySequent proto = do
let (tid, prem0) = freshTID (empty proto)
roleId <- funOpen "secret" *> identifier
role <- liftMaybe' ("could not find role '"++roleId++"'") $ lookupRole roleId proto
lbl <- kw COMMA *> (identifier <|> kw MINUS *> pure "-")
stepAtoms <-
(do step <- liftMaybe $ lookupRoleStep lbl role
return $ [AEv (Step tid step)]
`mplus` return [])
kw COMMA
(msgMod, pt) <- asum
[ ((,) MInvKey) <$> funApp "inv" tuplepattern
, ((,) id) <$> pattern ]
let m = msgMod . inst tid . resolveIdsLocalToRole role $ pt
kw COMMA
uncompromised <- map (inst tid . resolveIdsLocalToRole role) <$> msgSet
kw RPAREN
let atoms = [ AEq (E.TIDRoleEq (tid, role)), AEv (Learn m) ] ++ stepAtoms ++
map AUncompr uncompromised
prem = case conjoinAtoms atoms prem0 of
Just (Just prem1) -> prem1
Just Nothing -> error "secrecySequent: secrecy claim is trivially true"
Nothing -> error "secrecySequent: failed to construct secrecy claim"
return $ Sequent prem (FAtom AFalse)
where
msgSet = braced $ sepBy pattern (kw COMMA)
niagreeSequent :: Protocol -> Parser s Sequent
niagreeSequent proto = do
funOpen "niagree"
(roleCom, stepCom, patCom) <- roleStepPattern
kw RIGHTARROW
(roleRun, stepRun, patRun) <- roleStepPattern
kw COMMA
uncompromised <- map (AUncompr . instPat tidCom roleCom) <$> patSet
kw RPAREN
let premAtoms = [ AEq (E.TIDRoleEq (tidCom, roleCom))
, AEv (Step tidCom stepCom)
] ++
uncompromised
conclAtoms = [ AEq (E.TIDRoleEq (tidRun, roleRun))
, AEv (Step tidRun stepRun)
, AEq (E.MsgEq ( instPat tidRun roleRun patRun
, instPat tidCom roleCom patCom ))
]
concl = FExists (Left tidRun) (foldr1 FConj $ map FAtom conclAtoms)
prem = case conjoinAtoms premAtoms prem0 of
Just (Just prem1) -> prem1
Just Nothing -> error "niagreeSequent: claim is trivially true"
Nothing -> error "niagreeSequent: failed to construct claim"
return (Sequent prem concl)
where
(tidCom, prem0) = freshTID (empty proto)
tidRun = succ tidCom
patSet = braced $ sepBy pattern (kw COMMA)
instPat tid role = inst tid . resolveIdsLocalToRole role
roleStepPattern = do
stepId <- identifier
let (lbl, roleId) = (reverse *** (init . reverse)) (break ('_' ==) $ reverse stepId)
role <- liftMaybe' ("could not find role '" ++ roleId ++
"' in protocol '" ++ protoName proto ++ "'")
(lookupRole roleId proto)
step <- liftMaybe' ("unknown label '" ++ lbl ++ "' in role '" ++ roleId ++ "'")
(lookupRoleStep lbl role)
pat <- kw LBRACKET *> tuplepattern <* kw RBRACKET
return (role, step, pat)
parseAtomicitySequent :: Protocol -> Parser s Sequent
parseAtomicitySequent proto =
string "weakly" *> kw MINUS *> string "atomic" *> pure (atomicitySequent proto)
atomicitySequent :: Protocol -> Sequent
atomicitySequent proto = Sequent (empty proto) (FAtom (ATyping WeaklyAtomic))
data RawFact m =
RawAtom (E.Mapping -> m Atom)
| RawTIDRoleEq TID String
extractRoleEqs :: MonadPlus m => Protocol -> [RawFact m] -> m [(TID, Role)]
extractRoleEqs proto facts =
mapM mkEq [(tid, roleId) | RawTIDRoleEq tid roleId <- facts]
where
mkEq (tid, roleId) = case lookupRole roleId proto of
Just role -> return (tid, role)
Nothing -> fail $ "mkRoleEqs: role '"++roleId++"' does not occur in protocol '"
++protoName proto++"'"
roleEqFact :: MonadPlus m => Parser s (RawFact m)
roleEqFact = RawTIDRoleEq <$> (TID <$> (string "role" *> parens integer))
<*> (kw EQUAL *> identifier)
knowsFact :: MonadPlus m => Parser s (RawFact m)
knowsFact = do
m <- funApp "knows" message
return $ RawAtom (liftM (AEv . Learn) <$> m)
rawStep :: MonadPlus m => Parser s (E.Mapping -> m Event)
rawStep = parens $ do
tid <- TID <$> integer
stepId <- kw COMMA *> identifier
let step = resolveStep <*> pure tid <*> pure stepId
return $ (liftM (Step tid) <$> step)
stepFact :: MonadPlus m => Parser s (RawFact m)
stepFact = do
step <- string "step" *> rawStep
return $ RawAtom (liftM AEv <$> step)
honestFact :: MonadPlus m => Parser s [RawFact m]
honestFact = do
string "uncompromised"
msgs <- parens (sepBy1 message (kw COMMA))
return $ [RawAtom (liftM AUncompr <$> m) | m <- msgs]
event :: MonadPlus m => Parser s (E.Mapping -> m Event)
event = asum [ string "St" *> rawStep
, (liftM Learn <$>) <$> (string "Ln" *> message)
, (liftM Learn <$>) <$> instantiation ]
orderFacts :: MonadPlus m => Parser s [RawFact m]
orderFacts = do
ev <- event <* kw LESS
evs <- sepBy1 event (kw LESS)
let mkAtom e1 e2 = RawAtom $ \mapping -> do
e1' <- e1 mapping
e2' <- e2 mapping
return $ AEvOrd (e1', e2')
return $ zipWith mkAtom (ev:evs) evs
eqFact :: MonadPlus m => Parser s (RawFact m)
eqFact = do
m1 <- message <* kw EQUAL
m2 <- message
return $ RawAtom (liftM2 (\x y -> AEq (E.MsgEq (x , y))) <$> m1 <*> m2)
rawFacts :: MonadPlus m => Parser s [RawFact m]
rawFacts = foldl1 (<|>)
( [try orderFacts, honestFact] ++
map (liftM return) [roleEqFact, knowsFact, stepFact, eqFact] )
falseConcl :: Parser s Formula
falseConcl = doubleQuoted (string "False" *> pure (FAtom AFalse))
existenceConcl :: Protocol -> E.Mapping -> Parser s Formula
existenceConcl proto mapping = do
tids <- map (Left . TID) <$> (threads <|> pure [])
facts <- concat <$> doubleQuoted (sepBy1 rawFacts (kw AND))
roleeqs <- extractRoleEqs proto facts
let mapping' = foldr (uncurry E.addTIDRoleMapping) mapping roleeqs
atoms <- (map (AEq . E.TIDRoleEq) roleeqs ++) `liftM`
sequence [ mkAtom mapping' | RawAtom mkAtom <- facts ]
return $ foldr FExists (foldr1 FConj . map FAtom $ atoms) tids
where
singleThread = pure <$> (strings ["a", "thread"] *> integer)
multiThreads = strings ["threads"] *> sepBy1 integer (kw COMMA)
threads = (singleThread <|> multiThreads) <* strings ["such","that"]
conclusion :: Protocol -> E.Mapping -> Parser s Formula
conclusion proto mapping = asum
[try falseConcl, existenceConcl proto mapping]
implicationSequent :: Protocol -> Parser s Sequent
implicationSequent proto = do
facts <- concat <$> (string "premises" *> many (doubleQuoted rawFacts))
roleeqs <- extractRoleEqs proto facts
let mapping = foldr (uncurry E.addTIDRoleMapping) (E.Mapping E.empty) roleeqs
quantifiers = map fst roleeqs
atoms <- (map (AEq . E.TIDRoleEq) roleeqs ++) `liftM`
sequence [ mkAtom mapping | RawAtom mkAtom <- facts ]
prems0 <- foldM (flip quantifyTID) (F.empty proto) quantifiers
optPrems <- conjoinAtoms atoms prems0
prems <- maybe (fail "contradictory premises") return optPrems
string "imply"
concl <- conclusion proto mapping
return $ Sequent prems concl
theory :: Parser s Theory
theory = do
string "theory"
thyId <- identifier
string "begin" *> addItems (Theory thyId []) <* string "end"
where
addItems :: Theory -> Parser s (Theory)
addItems thy =
do p <- protocol
case lookupProtocol (protoName p) thy of
Just _ -> fail $ "duplicate protocol '" ++ protoName p ++ "'"
Nothing -> addItems (insertItem (ThyProtocol p) thy)
<|>
do cs <- claims (flip lookupProtocol thy)
addItems (foldl' (flip insertItem) thy cs)
<|>
do return thy