Merge branch 'adelon:main' into main

6 files changed, 85 insertions, 15 deletions

diff --git a/source/Api.hs b/source/Api.hs
index ac277f5..9dfa0e1 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -36,21 +36,22 @@ import Base
 import Checking
 import Checking.Cache
 import Encoding
+import Filter(filterTask)
 import Meaning (meaning, GlossError(..))
+import Megalodon qualified
 import Provers
 import Syntax.Abstract qualified as Raw
 import Syntax.Adapt (adaptChunks, scanChunk, ScannedLexicalItem)
+import Syntax.Chunk
 import Syntax.Concrete
 import Syntax.Import
-import Syntax.Chunk
 import Syntax.Internal qualified as Internal
 import Syntax.Lexicon (Lexicon, builtins)
+import Syntax.LexiconFile
 import Syntax.Token
 import TheoryGraph (TheoryGraph, Precedes(..))
 import TheoryGraph qualified
 import Tptp.UnsortedFirstOrder qualified as Tptp
-import Filter(filterTask)
-import Megalodon qualified
 
 import Control.Monad.Logger
 import Data.List (intercalate)
@@ -120,6 +121,8 @@ scan :: MonadIO io => FilePath -> io [ScannedLexicalItem]
 scan input = do
     tokenStream <- tokenize input
     let chunks = chunkify (unTokStream tokenStream)
+    -- TODO items <- liftIO parseLexiconFile
+    --pure ((concatMap scanChunk chunks) <> items)
     pure (concatMap scanChunk chunks)
 
 
diff --git a/source/Meaning.hs b/source/Meaning.hs
index d32e8ac..834d8a6 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -389,13 +389,14 @@ glossStmt = \case
         vp' <- glossVP vp
         let phi = Sem.makeConjunction (vp' <$> toList ts')
         pure (compose quantifies phi)
-    Raw.StmtNoun t np -> do
-        (t', quantify) <- glossTerm t
+    Raw.StmtNoun ts np -> do
+        (ts', quantifies) <- NonEmpty.unzip <$> glossTerm `each` ts
         (np', maySuchThat) <- glossNPMaybe np
         let andSuchThat phi = case maySuchThat of
                 Just suchThat -> phi `Sem.And` suchThat
                 Nothing -> phi
-        pure (quantify (andSuchThat (np' t')))
+            psi = Sem.makeConjunction (andSuchThat . np' <$> toList ts')
+        pure (compose quantifies psi)
     Raw.StmtStruct t sp -> do
         (t', quantify) <- glossTerm t
         pure (quantify (Sem.TermSymbol (Sem.SymbolPredicate (Sem.PredicateNounStruct sp)) [t']))
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 \<Formula\>@/.
     | StmtVerbPhrase (NonEmpty Term) VerbPhrase -- ^ E.g.: /@\<Term\> and \<Term\> \<verb\>@/.
-    | StmtNoun Term (NounPhrase Maybe) -- ^ E.g.: /@\<Term\> is a(n) \<NP\>@/.
+    | StmtNoun (NonEmpty Term) (NounPhrase Maybe) -- ^ E.g.: /@\<Term\> is a(n) \<NP\>@/.
     | StmtStruct Term StructPhrase
     | StmtNeg Stmt -- ^ E.g.: /@It is not the case that \<Stmt\>@/.
     | StmtExists (NounPhrase []) -- ^ E.g.: /@There exists a(n) \<NP\>@/.
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
new file mode 100644
index 0000000..b700621
--- /dev/null
+++ b/source/Syntax/LexiconFile.hs
@@ -0,0 +1,58 @@
+module Syntax.LexiconFile where
+
+import Base hiding (many)
+import Syntax.Adapt
+import Syntax.LexicalPhrase
+import Syntax.Abstract
+
+import Data.Char (isAlphaNum, isAsciiLower, isLetter, isDigit)
+import Data.Text qualified as Text
+import Data.Text.IO qualified as Text
+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 </> "library" </> "lexicon.csv")
+    csv <- Text.readFile csvPath
+    case runParser lexiconFile csvPath csv of
+        Left err -> fail (errorBundlePretty err)
+        Right entries -> pure entries
+
+lexiconFile :: LexiconFileParser [ScannedLexicalItem]
+lexiconFile = many line <* eof
+
+line :: LexiconFileParser ScannedLexicalItem
+line = do
+    c <- satisfy isAsciiLower
+    cs <- takeWhileP Nothing (\x -> isAsciiLower x || isDigit x || x == '_')
+    let marker = Marker (Text.cons c cs)
+    Char.char ','
+    kind <- takeWhile1P Nothing isLetter
+    Char.char ','
+    item <- case kind of
+        "adj" -> do
+            entry <- takeWhile1P Nothing (\x -> isAlphaNum x || x == '\'' || x == '-' || x == ' ')
+            pure (ScanAdj (unsafeReadPhrase (Text.unpack entry)) marker)
+        "rel" -> do
+            entry <- tokenSingle
+            pure (ScanRelationSymbol entry marker)
+        "const" -> do
+            entry <- tokenPattern
+            pure (ScanFunctionSymbol entry marker)
+        _ -> error "Unrecognized lexical item kind in lexicon file."
+    optional Char.eol
+    pure item
+
+tokenSingle :: LexiconFileParser Token
+tokenSingle = Command <$> (single '\\' *> takeWhile1P Nothing (\x -> isAlphaNum x))
+
+-- TODO allow spaces
+tokenPattern :: LexiconFileParser (Holey Token)
+tokenPattern = some (Just <$> tokenSingle <|> Nothing <$ single '?')