module Theory.Text.Parser (
parseOpenTheory
, parseOpenTheoryString
, parseLemma
, parseIntruderRules
) where
import Prelude hiding (id, (.))
import qualified Data.ByteString.Char8 as BC
import Data.Char (isUpper, toUpper)
import Data.Foldable (asum)
import Data.Label
import qualified Data.Map as M
import Data.Monoid hiding (Last)
import qualified Data.Set as S
import Control.Applicative hiding (empty, many, optional)
import Control.Category
import Control.Monad
import Text.Parsec hiding ((<|>))
import Text.PrettyPrint.Class (render)
import Term.Substitution
import Term.SubtermRule
import Theory
import Theory.Text.Parser.Token
parseOpenTheory :: [String]
-> FilePath
-> IO OpenTheory
parseOpenTheory flags = parseFile (theory flags)
parseIntruderRules :: MaudeSig -> FilePath -> IO [IntrRuleAC]
parseIntruderRules msig = parseFile (setState msig >> many intrRule)
parseOpenTheoryString :: [String]
-> String -> Either ParseError OpenTheory
parseOpenTheoryString flags = parseString "<unknown source>" (theory flags)
parseLemma :: String -> Either ParseError (Lemma ProofSkeleton)
parseLemma = parseString "<unknown source>" lemma
llit :: Parser LNTerm
llit = asum [freshTerm <$> freshName, pubTerm <$> pubName, varTerm <$> msgvar]
lookupArity :: String -> Parser (Int, Privacy)
lookupArity op = do
maudeSig <- getState
case lookup (BC.pack op) (S.toList (noEqFunSyms maudeSig) ++ [(emapSymString, (2,Public))]) of
Nothing -> fail $ "unknown operator `" ++ op ++ "'"
Just (k,priv) -> return (k,priv)
naryOpApp :: Ord l => Parser (Term l) -> Parser (Term l)
naryOpApp plit = do
op <- identifier
(k,priv) <- lookupArity op
ts <- parens $ if k == 1
then return <$> tupleterm plit
else commaSep (multterm plit)
let k' = length ts
when (k /= k') $
fail $ "operator `" ++ op ++"' has arity " ++ show k ++
", but here it is used with arity " ++ show k'
let app o = if BC.pack op == emapSymString then fAppC EMap else fAppNoEq o
return $ app (BC.pack op, (k,priv)) ts
binaryAlgApp :: Ord l => Parser (Term l) -> Parser (Term l)
binaryAlgApp plit = do
op <- identifier
(k,priv) <- lookupArity op
arg1 <- braced (tupleterm plit)
arg2 <- term plit
when (k /= 2) $ fail $
"only operators of arity 2 can be written using the `op{t1}t2' notation"
return $ fAppNoEq (BC.pack op, (2,priv)) [arg1, arg2]
term :: Ord l => Parser (Term l) -> Parser (Term l)
term plit = asum
[ pairing <?> "pairs"
, parens (multterm plit)
, symbol "1" *> pure fAppOne
, application <?> "function application"
, nullaryApp
, plit
]
<?> "term"
where
application = asum $ map (try . ($ plit)) [naryOpApp, binaryAlgApp]
pairing = angled (tupleterm plit)
nullaryApp = do
maudeSig <- getState
asum [ try (symbol (BC.unpack sym)) *> pure (fApp (NoEq (sym,(0,priv))) [])
| NoEq (sym,(0,priv)) <- S.toList $ funSyms maudeSig ]
expterm :: Ord l => Parser (Term l) -> Parser (Term l)
expterm plit = chainl1 (msetterm plit) ((\a b -> fAppExp (a,b)) <$ opExp)
multterm :: Ord l => Parser (Term l) -> Parser (Term l)
multterm plit = do
dh <- enableDH <$> getState
if dh
then chainl1 (expterm plit) ((\a b -> fAppAC Mult [a,b]) <$ opMult)
else msetterm plit
msetterm :: Ord l => Parser (Term l) -> Parser (Term l)
msetterm plit = do
mset <- enableMSet <$> getState
if mset
then chainl1 (term plit) ((\a b -> fAppAC Union [a,b]) <$ opPlus)
else term plit
tupleterm :: Ord l => Parser (Term l) -> Parser (Term l)
tupleterm plit = chainr1 (multterm plit) ((\a b -> fAppPair (a,b)) <$ comma)
fact :: Ord l => Parser (Term l) -> Parser (Fact (Term l))
fact plit = try (
do multi <- option Linear (opBang *> pure Persistent)
i <- identifier
case i of
[] -> fail "empty identifier"
(c:_) | isUpper c -> return ()
| otherwise -> fail "facts must start with upper-case letters"
ts <- parens (commaSep (multterm plit))
mkProtoFact multi i ts
<?> "fact" )
where
singleTerm _ constr [t] = return $ constr t
singleTerm f _ ts = fail $ "fact '" ++ f ++ "' used with arity " ++
show (length ts) ++ " instead of arity one"
mkProtoFact multi f = case map toUpper f of
"OUT" -> singleTerm f outFact
"IN" -> singleTerm f inFact
"KU" -> singleTerm f kuFact
"KD" -> return . Fact KDFact
"DED" -> return . Fact DedFact
"FR" -> singleTerm f freshFact
_ -> return . protoFact multi f
modulo :: String -> Parser ()
modulo thy = parens $ symbol_ "modulo" *> symbol_ thy
moduloE, moduloAC :: Parser ()
moduloE = modulo "E"
moduloAC = modulo "AC"
protoRule :: Parser (ProtoRuleE)
protoRule = do
name <- try (symbol "rule" *> optional moduloE *> identifier <* colon)
when (name `elem` reservedRuleNames) $
fail $ "cannot use reserved rule name '" ++ name ++ "'"
subst <- option emptySubst letBlock
(ps,as,cs) <- genericRule
return $ apply subst $ Rule (StandRule name) ps cs as
letBlock :: Parser LNSubst
letBlock = do
toSubst <$> (symbol "let" *> many1 definition <* symbol "in")
where
toSubst = foldr1 compose . map (substFromList . return)
definition = (,) <$> (sortedLVar [LSortMsg] <* equalSign) <*> multterm llit
intrRule :: Parser IntrRuleAC
intrRule = do
info <- try (symbol "rule" *> moduloAC *> intrInfo <* colon)
(ps,as,cs) <- genericRule
return $ Rule info ps cs as
where
intrInfo = do
name <- identifier
case name of
'c':cname -> return $ ConstrRule (BC.pack cname)
'd':dname -> return $ DestrRule (BC.pack dname)
_ -> fail $ "invalid intruder rule name '" ++ name ++ "'"
genericRule :: Parser ([LNFact], [LNFact], [LNFact])
genericRule =
(,,) <$> list (fact llit)
<*> ((pure [] <* symbol "-->") <|>
(symbol "--[" *> commaSep (fact llit) <* symbol "]->"))
<*> list (fact llit)
blatom :: Parser BLAtom
blatom = (fmap (fmapTerm (fmap Free))) <$> asum
[ Last <$> try (symbol "last" *> parens nodevarTerm) <?> "last atom"
, flip Action <$> try (fact llit <* opAt) <*> nodevarTerm <?> "action atom"
, Less <$> try (nodevarTerm <* opLess) <*> nodevarTerm <?> "less atom"
, EqE <$> try (multterm llit <* opEqual) <*> multterm llit <?> "term equality"
, EqE <$> (nodevarTerm <* opEqual) <*> nodevarTerm <?> "node equality"
]
where
nodevarTerm = (lit . Var) <$> nodevar
fatom :: Parser LNFormula
fatom = asum
[ pure lfalse <* opLFalse
, pure ltrue <* opLTrue
, Ato <$> try blatom
, quantification
, parens iff
]
where
quantification = do
q <- (pure forall <* opForall) <|> (pure exists <* opExists)
vs <- many1 lvar <* dot
f <- iff
return $ foldr (hinted q) f vs
hinted :: ((String, LSort) -> LVar -> a) -> LVar -> a
hinted f v@(LVar n s _) = f (n,s) v
negation :: Parser LNFormula
negation = opLNot *> (Not <$> fatom) <|> fatom
conjuncts :: Parser LNFormula
conjuncts = chainl1 negation ((.&&.) <$ opLAnd)
disjuncts :: Parser LNFormula
disjuncts = chainl1 conjuncts ((.||.) <$ opLOr)
imp :: Parser LNFormula
imp = do
lhs <- disjuncts
asum [ opImplies *> ((lhs .==>.) <$> imp)
, pure lhs ]
iff :: Parser LNFormula
iff = do
lhs <- imp
asum [opLEquiv *> ((lhs .<=>.) <$> imp), pure lhs ]
standardFormula :: Parser LNFormula
standardFormula = iff
guardedFormula :: Parser LNGuarded
guardedFormula = try $ do
res <- formulaToGuarded <$> standardFormula
case res of
Left d -> fail $ render d
Right gf -> return gf
axiom :: Parser Axiom
axiom = Axiom <$> (symbol "axiom" *> identifier <* colon)
<*> doubleQuoted standardFormula
lemmaAttribute :: Parser LemmaAttribute
lemmaAttribute = asum
[ symbol "typing" *> pure TypingLemma
, symbol "reuse" *> pure ReuseLemma
, symbol "use_induction" *> pure InvariantLemma
]
traceQuantifier :: Parser TraceQuantifier
traceQuantifier = asum
[ symbol "all-traces" *> pure AllTraces
, symbol "exists-trace" *> pure ExistsTrace
]
lemma :: Parser (Lemma ProofSkeleton)
lemma = skeletonLemma <$> (symbol "lemma" *> optional moduloE *> identifier)
<*> (option [] $ list lemmaAttribute)
<*> (colon *> option AllTraces traceQuantifier)
<*> doubleQuoted standardFormula
<*> (proofSkeleton <|> pure (unproven ()))
nodePrem :: Parser NodePrem
nodePrem = parens ((,) <$> nodevar
<*> (comma *> fmap (PremIdx . fromIntegral) natural))
nodeConc :: Parser NodeConc
nodeConc = parens ((,) <$> nodevar
<*> (comma *> fmap (ConcIdx .fromIntegral) natural))
goal :: Parser Goal
goal = asum
[ premiseGoal
, actionGoal
, chainGoal
, disjSplitGoal
, eqSplitGoal
]
where
actionGoal = do
fa <- try (fact llit <* opAt)
i <- nodevar
return $ ActionG i fa
premiseGoal = do
(fa, v) <- try ((,) <$> fact llit <*> opRequires)
i <- nodevar
return $ PremiseG (i, v) fa
chainGoal = ChainG <$> (try (nodeConc <* opChain)) <*> nodePrem
disjSplitGoal = (DisjG . Disj) <$> sepBy1 guardedFormula (symbol "∥")
eqSplitGoal = try $ do
symbol_ "split"
parens $ (SplitG . SplitId . fromIntegral) <$> natural
proofMethod :: Parser ProofMethod
proofMethod = asum
[ symbol "sorry" *> pure (Sorry Nothing)
, symbol "simplify" *> pure Simplify
, symbol "solve" *> (SolveGoal <$> parens goal)
, symbol "contradiction" *> pure (Contradiction Nothing)
, symbol "induction" *> pure Induction
]
proofSkeleton :: Parser ProofSkeleton
proofSkeleton =
solvedProof <|> finalProof <|> interProof
where
solvedProof =
symbol "SOLVED" *> pure (LNode (ProofStep Solved ()) M.empty)
finalProof = do
method <- symbol "by" *> proofMethod
return (LNode (ProofStep method ()) M.empty)
interProof = do
method <- proofMethod
cases <- (sepBy oneCase (symbol "next") <* symbol "qed") <|>
((return . (,) "") <$> proofSkeleton )
return (LNode (ProofStep method ()) (M.fromList cases))
oneCase = (,) <$> (symbol "case" *> identifier) <*> proofSkeleton
builtins :: Parser ()
builtins =
symbol "builtins" *> colon *> commaSep1 builtinTheory *> pure ()
where
extendSig msig = modifyState (`mappend` msig)
builtinTheory = asum
[ try (symbol "diffie-hellman")
*> extendSig dhMaudeSig
, try (symbol "bilinear-pairing")
*> extendSig bpMaudeSig
, try (symbol "multiset")
*> extendSig msetMaudeSig
, try (symbol "symmetric-encryption")
*> extendSig symEncMaudeSig
, try (symbol "asymmetric-encryption")
*> extendSig asymEncMaudeSig
, try (symbol "signing")
*> extendSig signatureMaudeSig
, symbol "hashing"
*> extendSig hashMaudeSig
]
functions :: Parser ()
functions =
symbol "functions" *> colon *> commaSep1 functionSymbol *> pure ()
where
functionSymbol = do
f <- BC.pack <$> identifier <* opSlash
k <- fromIntegral <$> natural
priv <- option Public (symbol "[private]" *> pure Private)
sig <- getState
case lookup f [ o | o <- (S.toList $ stFunSyms sig)] of
Just kp' | kp' /= (k,priv) ->
fail $ "conflicting arities/private " ++
show kp' ++ " and " ++ show (k,priv) ++
" for `" ++ BC.unpack f
_ -> setState (addFunSym (f,(k,priv)) sig)
equations :: Parser ()
equations =
symbol "equations" *> colon *> commaSep1 equation *> pure ()
where
equation = do
rrule <- RRule <$> term llit <*> (equalSign *> term llit)
case rRuleToStRule rrule of
Just str ->
modifyState (addStRule str)
Nothing ->
fail $ "Not a subterm rule: " ++ show rrule
theory :: [String]
-> Parser OpenTheory
theory flags0 = do
symbol_ "theory"
thyId <- identifier
symbol_ "begin"
*> addItems (S.fromList flags0) (set thyName thyId defaultOpenTheory)
<* symbol "end"
where
addItems :: S.Set String -> OpenTheory -> Parser OpenTheory
addItems flags thy = asum
[ do builtins
msig <- getState
addItems flags $ set (sigpMaudeSig . thySignature) msig thy
, do functions
msig <- getState
addItems flags $ set (sigpMaudeSig . thySignature) msig thy
, do equations
msig <- getState
addItems flags $ set (sigpMaudeSig . thySignature) msig thy
, do thy' <- liftedAddAxiom thy =<< axiom
addItems flags thy'
, do thy' <- liftedAddLemma thy =<< lemma
addItems flags thy'
, do ru <- protoRule
thy' <- liftedAddProtoRule thy ru
addItems flags thy'
, do r <- intrRule
addItems flags (addIntrRuleACs [r] thy)
, do c <- formalComment
addItems flags (addFormalComment c thy)
, do ifdef flags thy
, do define flags thy
, do return thy
]
define :: S.Set String -> OpenTheory -> Parser OpenTheory
define flags thy = do
flag <- try (symbol "#define") *> identifier
addItems (S.insert flag flags) thy
ifdef :: S.Set String -> OpenTheory -> Parser OpenTheory
ifdef flags thy = do
flag <- symbol_ "#ifdef" *> identifier
thy' <- addItems flags thy
symbol_ "#endif"
if flag `S.member` flags
then addItems flags thy'
else addItems flags thy
liftedAddProtoRule thy ru = case addProtoRule ru thy of
Just thy' -> return thy'
Nothing -> fail $ "duplicate rule: " ++ render (prettyRuleName ru)
liftedAddLemma thy lem = case addLemma lem thy of
Just thy' -> return thy'
Nothing -> fail $ "duplicate lemma: " ++ get lName lem
liftedAddAxiom thy ax = case addAxiom ax thy of
Just thy' -> return thy'
Nothing -> fail $ "duplicate axiom: " ++ get axName ax