From b2f9f7900ccb4a569ed23e9ecf327564dbba2b7d Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Tue, 7 May 2024 18:07:23 +0200 Subject: Sketch noun coord, symbols for reals --- source/Syntax/Abstract.hs | 2 +- source/Syntax/Concrete.hs | 16 +++++++++++----- source/Syntax/Lexicon.hs | 8 +++++--- source/Syntax/LexiconFile.hs | 4 ++-- 4 files changed, 19 insertions(+), 11 deletions(-) (limited to 'source/Syntax') diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 6f30612..4aa8623 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -269,7 +269,7 @@ data Term data Stmt = StmtFormula Formula -- ^ E.g.: /@We have \@/. | StmtVerbPhrase (NonEmpty Term) VerbPhrase -- ^ E.g.: /@\ and \ \@/. - | StmtNoun Term (NounPhrase Maybe) -- ^ E.g.: /@\ is a(n) \@/. + | StmtNoun (NonEmpty Term) (NounPhrase Maybe) -- ^ E.g.: /@\ is a(n) \@/. | StmtStruct Term StructPhrase | StmtNeg Stmt -- ^ E.g.: /@It is not the case that \@/. | StmtExists (NounPhrase []) -- ^ E.g.: /@There exists a(n) \@/. diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 8c6962d..bad9635 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -123,6 +123,7 @@ grammar lexicon@Lexicon{..} = mdo nounPl <- rule $ nounOf lexicon pl term nounNames nounPlMay <- rule $ nounOf lexicon pl term nounName + structNoun <- rule $ structNounOf lexicon sg var var structNounNameless <- rule $ fst <$> structNounOf lexicon sg var (pure Nameless) @@ -180,19 +181,24 @@ grammar lexicon@Lexicon{..} = mdo -- Basic statements @stmt'@ are statements without any conjunctions or quantifiers. -- - stmtVerbSg <- rule $ StmtVerbPhrase <$> ((:| []) <$> term) <*> verbPhraseSg + let singletonTerm = (:| []) <$> term + nonemptyTerms = andList1 term + stmtVerbSg <- rule $ StmtVerbPhrase <$> singletonTerm <*> verbPhraseSg stmtVerbPl <-rule $ StmtVerbPhrase <$> andList1 term <*> verbPhrasePl stmtVerb <- rule $ stmtVerbSg <|> stmtVerbPl - stmtNounIs <- rule $ StmtNoun <$> term <* _is <* _an <*> nounPhrase - stmtNounIsNot <- rule $ StmtNeg <$> (StmtNoun <$> term <* _is <* _not <* _an <*> nounPhrase) - stmtNoun <- rule $ stmtNounIs <|> stmtNounIsNot + stmtNounIs <- rule $ StmtNoun <$> singletonTerm <* _is <* _an <*> nounPhrase + stmtNounAre <- rule $ StmtNoun <$> (nonemptyTerms <* _are) <*> nounPhrasePlMay + stmtNounIsNot <- rule $ StmtNeg <$> (StmtNoun <$> singletonTerm <* _is <* _not <* _an <*> nounPhrase) + stmtNounAreNot <- rule $ StmtNeg <$> (StmtNoun <$> nonemptyTerms <* (_are *> _not) <*> nounPhrasePlMay) + stmtNoun <- rule $ stmtNounIs <|> stmtNounIsNot <|> stmtNounAre <|> stmtNounAreNot stmtStruct <- rule $ StmtStruct <$> (term <* _is <* _an) <*> structNounNameless stmtExists <- rule $ StmtExists <$> (_exists *> _an *> nounPhrase') stmtExist <- rule $ StmtExists <$> (_exist *> nounPhrasePl) stmtExistsNot <- rule $ StmtNeg . StmtExists <$> (_exists *> _no *> nounPhrase') stmtFormula <- rule $ StmtFormula <$> math formula + stmtFormualNeg <- rule $ StmtNeg . StmtFormula <$> (_not *> math formula) stmtBot <- rule $ StmtFormula (PropositionalConstant IsBottom) <$ _contradiction - stmt' <- rule $ stmtVerb <|> stmtNoun <|> stmtStruct <|> stmtFormula <|> stmtBot + stmt' <- rule $ stmtVerb <|> stmtNoun <|> stmtStruct <|> stmtFormula <|> stmtFormualNeg <|> stmtBot stmtOr <- rule $ stmt' <|> (StmtConnected Disjunction <$> stmt' <* _or <*> stmt) stmtAnd <- rule $ stmtOr <|> (StmtConnected Conjunction <$> stmtOr <* _and <*> stmt) stmtIff <- rule $ stmtAnd <|> (StmtConnected Equivalence <$> stmtAnd <* _iff <*> stmt) diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index 805b875..b5e4f58 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -80,10 +80,10 @@ builtins = Lexicon builtinMixfix :: Seq (HashMap FunctionSymbol (Associativity, Marker)) builtinMixfix = Seq.fromList $ (HM.fromList <$>) [ [] - , [binOp (Symbol "+") LeftAssoc "add", binOp (Command "union") LeftAssoc "union", binOp (Command "monus") LeftAssoc "monus"] + , [binOp (Symbol "+") LeftAssoc "add", binOp (Command "union") LeftAssoc "union", binOp (Symbol "-") LeftAssoc "minus", binOp (Command "rminus") LeftAssoc "rminus", binOp (Command "monus") LeftAssoc "monus"] , [binOp (Command "relcomp") LeftAssoc "relcomp"] , [binOp (Command "circ") LeftAssoc "circ"] - , [binOp (Command "mul") LeftAssoc "mul", binOp (Command "inter") LeftAssoc "inter"] + , [binOp (Command "mul") LeftAssoc "mul", binOp (Command "inter") LeftAssoc "inter", binOp (Command "rmul") LeftAssoc "rmul"] , [binOp (Command "setminus") LeftAssoc "setminus"] , [binOp (Command "times") RightAssoc "times"] , [] @@ -103,7 +103,8 @@ builtinMixfix = Seq.fromList $ (HM.fromList <$>) prefixOps :: [(FunctionSymbol, (Associativity, Marker))] prefixOps = - [ ([Just (Command "unions"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "unions")) + [ ([Just (Command "rfrac"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "rfrac")) + , ([Just (Command "unions"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "unions")) , ([Just (Command "cumul"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "cumul")) , ([Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "fst")) , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd")) @@ -126,6 +127,7 @@ identifier cmd = ([Just (Command cmd)], (NonAssoc, Marker cmd)) builtinRelationSymbols :: LexicalItems RelationSymbol builtinRelationSymbols = HM.fromList [ (Symbol "=", "eq") + , (Command "rless", "rless") , (Command "neq", "neq") , (Command "in", "elem") , (Command "notin", "notelem") -- Alternative to @\not\in@. diff --git a/source/Syntax/LexiconFile.hs b/source/Syntax/LexiconFile.hs index be70a6b..b700621 100644 --- a/source/Syntax/LexiconFile.hs +++ b/source/Syntax/LexiconFile.hs @@ -12,14 +12,14 @@ import Text.Earley.Mixfix (Holey) import Text.Megaparsec hiding (Token, Label, label) import Text.Megaparsec.Char qualified as Char import UnliftIO.Directory - +import System.FilePath type LexiconFileParser = Parsec Void Text parseLexiconFile :: IO [ScannedLexicalItem] parseLexiconFile = do currentDir <- getCurrentDirectory - let csvPath = (currentDir <> "lexicon.csv") + let csvPath = (currentDir "library" "lexicon.csv") csv <- Text.readFile csvPath case runParser lexiconFile csvPath csv of Left err -> fail (errorBundlePretty err) -- cgit v1.2.3