Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

fix #96: parse and check (partial) proofs

  • Loading branch information...
commit 320965cb13fdd81610666bcd34fd8a3a4ccf2532 1 parent c6f664c
Simon Meier meiersi authored
Showing with 112 additions and 82 deletions.
  1. +112 −82 src/Theory/Text/Parser.hs
194 src/Theory/Text/Parser.hs
View
@@ -20,7 +20,7 @@ import Data.Char (isUpper, toUpper)
import Data.Foldable (asum)
import Data.Label
import qualified Data.Map as M
-import Data.Monoid
+import Data.Monoid hiding (Last)
import qualified Data.Set as S
import Control.Applicative hiding (empty, many, optional)
@@ -179,7 +179,7 @@ tupleterm plit = chainr1 (multterm plit) ((\a b -> fAppPair (a,b)) <$ comma)
-- | Parse a fact.
fact :: Ord l => Parser (Term l) -> Parser (Fact (Term l))
-fact plit =
+fact plit = try (
do multi <- option Linear (opBang *> pure Persistent)
i <- identifier
case i of
@@ -188,7 +188,7 @@ fact plit =
| otherwise -> fail "facts must start with upper-case letters"
ts <- parens (commaSep (multterm plit))
mkProtoFact multi i ts
- <?> "protocol fact"
+ <?> "fact" )
where
singleTerm _ constr [t] = return $ constr t
singleTerm f _ ts = fail $ "fact '" ++ f ++ "' used with arity " ++
@@ -357,91 +357,23 @@ transferProto = do
-}
------------------------------------------------------------------------------
--- Parsing Proofs
-------------------------------------------------------------------------------
-
--- | Parse a node premise.
-nodePrem :: Parser NodePrem
-nodePrem = parens ((,) <$> nodevar
- <*> (comma *> fmap (PremIdx . fromIntegral) natural))
-
--- | Parse a node conclusion.
-nodeConc :: Parser NodeConc
-nodeConc = parens ((,) <$> nodevar
- <*> (comma *> fmap (ConcIdx .fromIntegral) natural))
-
--- | Parse a goal.
-goal :: Parser Goal
-goal = asum
- [ -- splitGoal
- premiseGoal
- , actionGoal
- , ChainG <$> nodeConc <*> nodePrem
- ]
- 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
- -- splitGoal = do
- -- split <- (symbol "splitEqsOn" *> pure SplitEqs) <|>
- -- (symbol "splitTypingOn" *> pure SplitTyping)
- -- SplitGoal split <$> parens natural
-
--- | Parse a proof method.
-proofMethod :: Parser ProofMethod
-proofMethod = asum
- [ symbol "sorry" *> pure (Sorry "not yet proven")
- , symbol "simplify" *> pure Simplify
- , symbol "solve" *> (SolveGoal <$> parens goal)
- , symbol "contradiction" *> pure (Contradiction Nothing)
- ]
-
--- | Parse a proof skeleton.
-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
-
-------------------------------------------------------------------------------
--- Parsing Formulas and Lemmas
+-- Parsing Standard and Guarded Formulas
------------------------------------------------------------------------------
-- | Parse an atom with possibly bound logical variables.
blatom :: Parser BLAtom
blatom = (fmap (fmapTerm (fmap Free))) <$> asum
- [ flip Action <$> try (fact llit <* opAt) <*> nodevarTerm <?> "action"
- , Less <$> try (nodevarTerm <* opLess) <*> nodevarTerm <?> "less"
+ [ 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
- -- nodePrem = annNode PremIdx
- -- nodeConc = annNode ConcIdx
- -- annNode mkAnn = parens ((,) <$> (nodevarTerm <* kw COMMA)
- -- <*> (mkAnn <$> natural))
-- | Parse an atom of a formula.
-fatom :: Parser (LFormula Name)
+fatom :: Parser LNFormula
fatom = asum
[ pure lfalse <* opLFalse
, pure ltrue <* opLTrue
@@ -462,30 +394,50 @@ fatom = asum
-- | Parse a negation.
-negation :: Parser (LFormula Name)
+negation :: Parser LNFormula
negation = opLNot *> (Not <$> fatom) <|> fatom
-- | Parse a left-associative sequence of conjunctions.
-conjuncts :: Parser (LFormula Name)
+conjuncts :: Parser LNFormula
conjuncts = chainl1 negation ((.&&.) <$ opLAnd)
-- | Parse a left-associative sequence of disjunctions.
-disjuncts :: Parser (LFormula Name)
+disjuncts :: Parser LNFormula
disjuncts = chainl1 conjuncts ((.||.) <$ opLOr)
-- | An implication.
-imp :: Parser (LFormula Name)
+imp :: Parser LNFormula
imp = do
lhs <- disjuncts
asum [ opImplies *> ((lhs .==>.) <$> imp)
, pure lhs ]
-- | An logical equivalence.
-iff :: Parser (LFormula Name)
+iff :: Parser LNFormula
iff = do
lhs <- imp
asum [opLEquiv *> ((lhs .<=>.) <$> imp), pure lhs ]
+-- | Parse a standard formula.
+standardFormula :: Parser LNFormula
+standardFormula = iff
+
+-- | Parse a guarded formula using the hack of parsing a standard formula and
+-- converting it afterwards.
+--
+-- FIXME: Write a proper parser.
+guardedFormula :: Parser LNGuarded
+guardedFormula = try $ do
+ res <- formulaToGuarded <$> standardFormula
+ case res of
+ Left d -> fail $ render d
+ Right gf -> return gf
+
+
+------------------------------------------------------------------------------
+-- Parsing Lemmas
+------------------------------------------------------------------------------
+
-- | Parse a 'LemmaAttribute'.
lemmaAttribute :: Parser LemmaAttribute
lemmaAttribute = asum
@@ -506,9 +458,87 @@ lemma :: Parser (Lemma ProofSkeleton)
lemma = skeletonLemma <$> (symbol "lemma" *> optional moduloE *> identifier)
<*> (option [] $ list lemmaAttribute)
<*> (colon *> option AllTraces traceQuantifier)
- <*> doubleQuoted iff
+ <*> doubleQuoted standardFormula
<*> (proofSkeleton <|> pure (unproven ()))
+
+------------------------------------------------------------------------------
+-- Parsing Proofs
+------------------------------------------------------------------------------
+
+-- | Parse a node premise.
+nodePrem :: Parser NodePrem
+nodePrem = parens ((,) <$> nodevar
+ <*> (comma *> fmap (PremIdx . fromIntegral) natural))
+
+-- | Parse a node conclusion.
+nodeConc :: Parser NodeConc
+nodeConc = parens ((,) <$> nodevar
+ <*> (comma *> fmap (ConcIdx .fromIntegral) natural))
+
+-- | Parse a goal.
+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
+
+
+-- | Parse a proof method.
+proofMethod :: Parser ProofMethod
+proofMethod = asum
+ [ symbol "sorry" *> pure (Sorry "not yet proven")
+ , symbol "simplify" *> pure Simplify
+ , symbol "solve" *> (SolveGoal <$> parens goal)
+ , symbol "contradiction" *> pure (Contradiction Nothing)
+ , symbol "induction" *> pure Induction
+ ]
+
+-- | Parse a proof skeleton.
+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
+
+------------------------------------------------------------------------------
+-- Parsing Signatures
+------------------------------------------------------------------------------
+
-- | Builtin signatures.
builtins :: Parser ()
builtins =
Please sign in to comment.
Something went wrong with that request. Please try again.