diff options
Diffstat (limited to 'source/Felix/Syntax')
| -rw-r--r-- | source/Felix/Syntax/Concrete.hs | 104 |
1 files changed, 74 insertions, 30 deletions
diff --git a/source/Felix/Syntax/Concrete.hs b/source/Felix/Syntax/Concrete.hs index 8be8ab6..d6cf957 100644 --- a/source/Felix/Syntax/Concrete.hs +++ b/source/Felix/Syntax/Concrete.hs @@ -259,53 +259,91 @@ grammar lexicon@Lexicon{..} = mdo <|> stmtStruct <|> stmtFormula <|> stmtFormualNeg + <|> symbolicExistsBare <|> paren stmt -- Textual connectives use the same precedence and associativity as - -- symbolic connectives. Prefix negation and quantifiers scope over the - -- complete statement that follows them. + -- symbolic connectives. A prefix form that takes a statement body is a + -- terminal operand: its body consumes every following connective unless + -- an explicit delimiter (such as a parenthesis or "then") ends it. The + -- plain/scoped split at each precedence level prevents an enclosing level + -- from resuming after such an operand. let connect conn lhs rhs = StmtConnected conn Nothing lhs rhs - appendScoped conn lhs rhs scoped = - let connected = foldl' (connect conn) lhs rhs - in maybe connected (connect conn connected) scoped - stmtAnd <- rule do + connectMany conn lhs rhs = + foldl' (connect conn) lhs rhs + stmtAndPlain <- rule do lhs <- stmtAtom rhs <- many (_and *> stmtAtom) - scoped <- optional (_and *> stmtScoped) - pure (appendScoped Conjunction lhs rhs scoped) - stmtXor <- rule $ + pure (connectMany Conjunction lhs rhs) + stmtAndScoped <- rule $ + connect Conjunction <$> stmtAndPlain <* _and <*> stmtScoped + stmtAnd <- rule $ stmtAndScoped <|> stmtAndPlain + stmtXorPlain <- rule $ StmtConnected ExclusiveOr <$> (Just <$> _either) <*> stmtAnd <* _or + <*> stmtAndPlain + stmtXorScoped <- rule $ + StmtConnected ExclusiveOr + <$> (Just <$> _either) <*> stmtAnd - stmtNor <- rule $ + <* _or + <*> stmtAndScoped + stmtNorPlain <- rule $ StmtConnected NegatedDisjunction <$> (Just <$> _neither) <*> stmtAnd <* _nor + <*> stmtAndPlain + stmtNorScoped <- rule $ + StmtConnected NegatedDisjunction + <$> (Just <$> _neither) <*> stmtAnd - stmtOrBase <- rule $ stmtXor <|> stmtNor <|> stmtAnd - stmtOr <- rule do - lhs <- stmtOrBase - rhs <- many (_or *> stmtOrBase) - scoped <- optional (_or *> stmtScoped) - pure (appendScoped Disjunction lhs rhs scoped) - stmtIf <- rule $ + <* _nor + <*> stmtAndScoped + stmtOrBasePlain <- rule $ stmtXorPlain <|> stmtNorPlain <|> stmtAndPlain + stmtOrBaseScoped <- rule $ stmtXorScoped <|> stmtNorScoped <|> stmtAndScoped + stmtOrPlain <- rule do + lhs <- stmtOrBasePlain + rhs <- many (_or *> stmtOrBasePlain) + pure (connectMany Disjunction lhs rhs) + stmtOrScoped <- rule $ + stmtOrBaseScoped + <|> (connect Disjunction + <$> stmtOrPlain + <* _or + <*> (stmtOrBaseScoped <|> stmtScoped)) + stmtOr <- rule $ stmtOrScoped <|> stmtOrPlain + stmtIfPlain <- rule $ StmtConnected Implication <$> (Just <$> _if) <*> stmtIfAntecedent <* optional _comma <* _then - <*> stmtImpRhs - stmtImp <- rule $ stmtIf <|> stmtOr - stmtIff <- rule do - lhs <- stmtImp - rhs <- optional (_iff *> stmtImpRhs) + <*> stmtImpPlain + stmtIfScoped <- rule $ + StmtConnected Implication + <$> (Just <$> _if) + <*> stmtIfAntecedent + <* optional _comma + <* _then + <*> (stmtScoped <|> stmtImpScoped) + stmtImpPlain <- rule $ stmtIfPlain <|> stmtOrPlain + stmtImpScoped <- rule $ stmtIfScoped <|> stmtOrScoped + stmtIffPlain <- rule do + lhs <- stmtImpPlain + rhs <- optional (_iff *> stmtImpPlain) pure case rhs of Nothing -> lhs Just rhs' -> connect Equivalence lhs rhs' + stmtIffScoped <- rule $ + stmtImpScoped + <|> (connect Equivalence + <$> stmtImpPlain + <* _iff + <*> (stmtScoped <|> stmtImpScoped)) stmtNeg <- rule $ StmtNeg <$> _itIsWrong <*> stmt stmtQuantPhrase <- rule $ StmtQuantPhrase <$> _for <*> quant <* optional _comma <* optional _have <*> stmt @@ -320,13 +358,20 @@ grammar lexicon@Lexicon{..} = mdo ms <- optional suchStmt s <- optional _have *> stmt pure (SymbolicForall p xs b ms s) - symbolicExists <- rule do + symbolicExistsHead <- rule do loc1 <- _exists <|> _exist xs <- beginMath *> varSymbols b <- maybeBounded loc2 <- endMath - ms <- optional (_suchThat *> stmt) - pure (SymbolicExists loc1 xs b (ms ?? StmtFormula (PropositionalConstant loc2 IsTop))) + pure (loc1, xs, b, loc2) + symbolicExistsBare <- rule $ + (\(loc1, xs, b, loc2) -> + SymbolicExists loc1 xs b (StmtFormula (PropositionalConstant loc2 IsTop))) + <$> symbolicExistsHead + symbolicExistsScoped <- rule $ + (\(loc1, xs, b, _loc2) -> SymbolicExists loc1 xs b) + <$> symbolicExistsHead + <*> (_suchThat *> stmt) symbolicNotExists <- rule do p <- _exists *> _no xs <- beginMath *> varSymbols @@ -336,8 +381,6 @@ grammar lexicon@Lexicon{..} = mdo symbolicBound <- rule $ (\sign rel e -> Bounded (locate rel) sign rel e) <$> relationSign <*> relation <*> expr maybeBounded <- rule (pure Unbounded <|> symbolicBound) - symbolicQuantified <- rule $ symbolicForall <|> symbolicExists <|> symbolicNotExists - stmtScoped <- rule $ asum [ stmtNeg @@ -345,12 +388,13 @@ grammar lexicon@Lexicon{..} = mdo , stmtExist , stmtExistsNot , stmtQuantPhrase - , symbolicQuantified + , symbolicForall + , symbolicExistsScoped + , symbolicNotExists ] stmtIfAntecedent <- rule $ stmtScoped <|> stmtOr - stmtImpRhs <- rule $ stmtScoped <|> stmtImp stmt :: Prod r Text (Located Token) Stmt <- rule $ - (stmtScoped <|> stmtIff) <?> "a statement" + (stmtScoped <|> stmtIffScoped <|> stmtIffPlain) <?> "a statement" asmLetIn <- rule $ uncurry AsmLetIn <$> (_let *> math typing) |