diff options
| -rw-r--r-- | library/lexicon.csv | 6 | ||||
| -rw-r--r-- | library/test-lexicon.tex | 3 | ||||
| -rw-r--r-- | source/Api.hs | 9 | ||||
| -rw-r--r-- | source/Meaning.hs | 7 | ||||
| -rw-r--r-- | source/Syntax/Abstract.hs | 2 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 16 | ||||
| -rw-r--r-- | source/Syntax/Lexicon.hs | 8 | ||||
| -rw-r--r-- | source/Syntax/LexiconFile.hs | 58 | ||||
| -rw-r--r-- | test/examples/coord.tex | 5 | ||||
| -rw-r--r-- | test/examples/formula.tex | 4 | ||||
| -rw-r--r-- | test/examples/signature.tex | 19 | ||||
| -rw-r--r-- | test/golden/abbr/parsing.golden | 4 | ||||
| -rw-r--r-- | test/golden/coord/encoding tasks.golden | 14 | ||||
| -rw-r--r-- | test/golden/coord/generating tasks.golden | 679 | ||||
| -rw-r--r-- | test/golden/coord/glossing.golden | 151 | ||||
| -rw-r--r-- | test/golden/coord/parsing.golden | 69 | ||||
| -rw-r--r-- | test/golden/coord/tokenizing.golden | 25 | ||||
| -rw-r--r-- | test/golden/formula/encoding tasks.golden | 4 | ||||
| -rw-r--r-- | test/golden/formula/generating tasks.golden | 111 | ||||
| -rw-r--r-- | test/golden/formula/glossing.golden | 54 | ||||
| -rw-r--r-- | test/golden/formula/parsing.golden | 52 | ||||
| -rw-r--r-- | test/golden/formula/tokenizing.golden | 27 | ||||
| -rw-r--r-- | test/golden/indefinite-terms/parsing.golden | 4 |
23 files changed, 1291 insertions, 40 deletions
diff --git a/library/lexicon.csv b/library/lexicon.csv new file mode 100644 index 0000000..b9f8a09 --- /dev/null +++ b/library/lexicon.csv @@ -0,0 +1,6 @@ +reals,const,\reals +rplus,infix,\rplus +rminus,infix,\rminus +rmul,infix,\rmul +rfrac,infix,\rfrac +rless,rel,\rless diff --git a/library/test-lexicon.tex b/library/test-lexicon.tex new file mode 100644 index 0000000..ced585e --- /dev/null +++ b/library/test-lexicon.tex @@ -0,0 +1,3 @@ +\begin{axiom}\label{ax1} + If $x$ is even, then $x$ is even. +\end{axiom} 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 '?') diff --git a/test/examples/coord.tex b/test/examples/coord.tex index 6dc8d5a..9987506 100644 --- a/test/examples/coord.tex +++ b/test/examples/coord.tex @@ -35,3 +35,8 @@ \begin{proposition}\label{adjs} $x$ is foo and baz. \end{proposition} + +\begin{proposition}\label{are_nouns} + Let $x, y$ be foo bars. + Then $x$ and $y$ are foo bars. +\end{proposition} diff --git a/test/examples/formula.tex b/test/examples/formula.tex index c029402..e3b1e29 100644 --- a/test/examples/formula.tex +++ b/test/examples/formula.tex @@ -5,3 +5,7 @@ \begin{proposition}\label{formula_test_exists} $\exists x, y. x = y$. \end{proposition} + +\begin{proposition}\label{formula_test_not_exists} + $\exists x, y. x = y$ if and only if not $\exists x. x \neq x$. +\end{proposition} diff --git a/test/examples/signature.tex b/test/examples/signature.tex deleted file mode 100644 index 4d794a9..0000000 --- a/test/examples/signature.tex +++ /dev/null @@ -1,19 +0,0 @@ -\begin{signature}\label{triangle} - $x$ can be a number. -\end{signature} - -\begin{signature}\label{even} - $x$ can be even. -\end{signature} - -\begin{signature}\label{div} - $x$ can divide $y$. -\end{signature} - -\begin{signature}\label{square} - The square of $x$ is a number. -\end{signature} - -\begin{signature}\label{nless} - $x \nless y$ is a proposition. -\end{signature} diff --git a/test/golden/abbr/parsing.golden b/test/golden/abbr/parsing.golden index bad58c3..2bc8148 100644 --- a/test/golden/abbr/parsing.golden +++ b/test/golden/abbr/parsing.golden @@ -126,7 +126,7 @@ ( TermExpr ( ExprVar ( NamedVar "x" ) - ) + ) :| [] ) NounPhrase ( [] ) ( Noun ( SgPl @@ -305,7 +305,7 @@ ( TermExpr ( ExprVar ( NamedVar "x" ) - ) + ) :| [] ) NounPhrase ( [] ) ( Noun ( SgPl diff --git a/test/golden/coord/encoding tasks.golden b/test/golden/coord/encoding tasks.golden index 3776aed..08eb73e 100644 --- a/test/golden/coord/encoding tasks.golden +++ b/test/golden/coord/encoding tasks.golden @@ -38,4 +38,16 @@ fof(adj_nouns,axiom,![Xx,Xy]:((bar(Xx)&foo(Xx)&bar(Xy)&foo(Xy))=>Xx=Xx)). fof(nouns,axiom,![Xx,Xy]:((bar(Xx)&bar(Xy))=>Xx=Xx)). fof(baz,axiom,![Xx]:(baz(Xx)<=>Xx=Xx)). fof(foo,axiom,![Xx]:(foo(Xx)<=>Xx=Xx)). -fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)).
\ No newline at end of file +fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)). +------------------ +fof(are_nouns,conjecture,bar(fx)&foo(fx)&bar(fy)&foo(fy)). +fof(adjs,axiom,![Xx]:(foo(Xx)&baz(Xx))). +fof(noun_verb,axiom,![Xx,Xy]:(Xx=Xy<=>(bar(Xx)&Xx=Xy))). +fof(nouns_suchthat,axiom,![Xx,Xy]:((foo(Xx)&baz(Xy)&bar(Xx)&bar(Xy))=>Xx=Xx)). +fof(adj_nouns,axiom,![Xx,Xy]:((bar(Xx)&foo(Xx)&bar(Xy)&foo(Xy))=>Xx=Xx)). +fof(nouns,axiom,![Xx,Xy]:((bar(Xx)&bar(Xy))=>Xx=Xx)). +fof(baz,axiom,![Xx]:(baz(Xx)<=>Xx=Xx)). +fof(foo,axiom,![Xx]:(foo(Xx)<=>Xx=Xx)). +fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)). +fof(are_nouns1,axiom,bar(fy)&foo(fy)). +fof(are_nouns2,axiom,bar(fx)&foo(fx)).
\ No newline at end of file diff --git a/test/golden/coord/generating tasks.golden b/test/golden/coord/generating tasks.golden index 0e43d0e..df07901 100644 --- a/test/golden/coord/generating tasks.golden +++ b/test/golden/coord/generating tasks.golden @@ -1965,4 +1965,683 @@ ] ) } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "adjs" + , Quantified Universally + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "baz" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "noun_verb" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "nouns_suchthat" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "baz" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "adj_nouns" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "nouns" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "baz" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "baz" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + , + ( Marker "foo" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + , + ( Marker "bar" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + , + ( Marker "are_nouns1" + , Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + ) + , + ( Marker "are_nouns2" + , Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ) + ] + , taskConjectureLabel = Marker "are_nouns" + , taskConjecture = Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + ) + } ]
\ No newline at end of file diff --git a/test/golden/coord/glossing.golden b/test/golden/coord/glossing.golden index c051fe9..0ae9b95 100644 --- a/test/golden/coord/glossing.golden +++ b/test/golden/coord/glossing.golden @@ -434,4 +434,155 @@ ) ) ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/coord.tex" + , sourceLine = Pos 39 + , sourceColumn = Pos 1 + } + ) + ( Marker "are_nouns" ) + ( Lemma + [ Asm + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ) + , Asm + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + ) + ] + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "foo" ) + ] + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + ) + ) + ) ]
\ No newline at end of file diff --git a/test/golden/coord/parsing.golden b/test/golden/coord/parsing.golden index 555b86b..65fa82f 100644 --- a/test/golden/coord/parsing.golden +++ b/test/golden/coord/parsing.golden @@ -302,7 +302,7 @@ ( TermExpr ( ExprVar ( NamedVar "x" ) - ) + ) :| [] ) NounPhrase ( [] ) ( Noun ( SgPl @@ -364,4 +364,71 @@ ) ) ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/coord.tex" + , sourceLine = Pos 39 + , sourceColumn = Pos 1 + } + ) + ( Marker "are_nouns" ) + ( Lemma + [ AsmLetNoun + ( NamedVar "x" :| + [ NamedVar "y" ] + ) NounPhrase + ( + [ AdjL + [ Just + ( Word "foo" ) + ] [] + ] + ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtNoun + ( TermExpr + ( ExprVar + ( NamedVar "x" ) + ) :| + [ TermExpr + ( ExprVar + ( NamedVar "y" ) + ) + ] + ) NounPhrase + ( + [ AdjL + [ Just + ( Word "foo" ) + ] [] + ] + ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "bar" ) + ] + , pl = + [ Just + ( Word "bars" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) + ) ]
\ No newline at end of file diff --git a/test/golden/coord/tokenizing.golden b/test/golden/coord/tokenizing.golden index 0516d7a..b993832 100644 --- a/test/golden/coord/tokenizing.golden +++ b/test/golden/coord/tokenizing.golden @@ -147,4 +147,29 @@ , Word "baz" , Symbol "." , EndEnv "proposition" +, BeginEnv "proposition" +, Label "are_nouns" +, Word "let" +, BeginEnv "math" +, Variable "x" +, Symbol "," +, Variable "y" +, EndEnv "math" +, Word "be" +, Word "foo" +, Word "bars" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Variable "y" +, EndEnv "math" +, Word "are" +, Word "foo" +, Word "bars" +, Symbol "." +, EndEnv "proposition" ]
\ No newline at end of file diff --git a/test/golden/formula/encoding tasks.golden b/test/golden/formula/encoding tasks.golden index ab149dd..64f4883 100644 --- a/test/golden/formula/encoding tasks.golden +++ b/test/golden/formula/encoding tasks.golden @@ -1,4 +1,8 @@ fof(formula_test_forall,conjecture,![Xx,Xy]:(Xx=Xx&Xy=Xy)). ------------------ fof(formula_test_exists,conjecture,?[Xx,Xy]:Xx=Xy). +fof(formula_test_forall,axiom,![Xx,Xy]:(Xx=Xx&Xy=Xy)). +------------------ +fof(formula_test_not_exists,conjecture,?[Xx,Xy]:Xx=Xy<=>~?[Xx]:Xx!=Xx). +fof(formula_test_exists,axiom,?[Xx,Xy]:Xx=Xy). fof(formula_test_forall,axiom,![Xx,Xy]:(Xx=Xx&Xy=Xy)).
\ No newline at end of file diff --git a/test/golden/formula/generating tasks.golden b/test/golden/formula/generating tasks.golden index db5d39e..04b4a7d 100644 --- a/test/golden/formula/generating tasks.golden +++ b/test/golden/formula/generating tasks.golden @@ -105,4 +105,115 @@ ) ) } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "formula_test_exists" + , Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + , + ( Marker "formula_test_forall" + , Quantified Universally + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "formula_test_not_exists" + , taskConjecture = Connected Equivalence + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) + } ]
\ No newline at end of file diff --git a/test/golden/formula/glossing.golden b/test/golden/formula/glossing.golden index bb72370..f282b2e 100644 --- a/test/golden/formula/glossing.golden +++ b/test/golden/formula/glossing.golden @@ -76,4 +76,58 @@ ) ) ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/formula.tex" + , sourceLine = Pos 9 + , sourceColumn = Pos 1 + } + ) + ( Marker "formula_test_not_exists" ) + ( Lemma [] + ( Connected Equivalence + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) + ) + ) ]
\ No newline at end of file diff --git a/test/golden/formula/parsing.golden b/test/golden/formula/parsing.golden index 4c6321d..7de1fb7 100644 --- a/test/golden/formula/parsing.golden +++ b/test/golden/formula/parsing.golden @@ -73,4 +73,56 @@ ) ) ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/formula.tex" + , sourceLine = Pos 9 + , sourceColumn = Pos 1 + } + ) + ( Marker "formula_test_not_exists" ) + ( Lemma [] + ( StmtConnected Equivalence + ( StmtFormula + ( FormulaQuantified Existentially + ( NamedVar "x" :| + [ NamedVar "y" ] + ) Unbounded + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ) + ( StmtNeg + ( StmtFormula + ( FormulaQuantified Existentially + ( NamedVar "x" :| [] ) Unbounded + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "neq" ) + ) + ( ExprVar + ( NamedVar "x" ) :| [] + ) + ) + ) + ) + ) + ) + ) + ) ]
\ No newline at end of file diff --git a/test/golden/formula/tokenizing.golden b/test/golden/formula/tokenizing.golden index 3cb9b0e..1abe20a 100644 --- a/test/golden/formula/tokenizing.golden +++ b/test/golden/formula/tokenizing.golden @@ -30,4 +30,31 @@ , EndEnv "math" , Symbol "." , EndEnv "proposition" +, BeginEnv "proposition" +, Label "formula_test_not_exists" +, BeginEnv "math" +, Command "exists" +, Variable "x" +, Symbol "," +, Variable "y" +, Symbol "." +, Variable "x" +, Symbol "=" +, Variable "y" +, EndEnv "math" +, Word "if" +, Word "and" +, Word "only" +, Word "if" +, Word "not" +, BeginEnv "math" +, Command "exists" +, Variable "x" +, Symbol "." +, Variable "x" +, Command "neq" +, Variable "x" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" ]
\ No newline at end of file diff --git a/test/golden/indefinite-terms/parsing.golden b/test/golden/indefinite-terms/parsing.golden index 8c468ab..2beb5ca 100644 --- a/test/golden/indefinite-terms/parsing.golden +++ b/test/golden/indefinite-terms/parsing.golden @@ -21,7 +21,7 @@ ] } ) [] - ) ( Nothing ) ( [] ) ( Nothing ) + ) ( Nothing ) ( [] ) ( Nothing ) :| [] ) NounPhrase ( [] ) ( Noun ( SgPl @@ -61,7 +61,7 @@ ] } ) [] - ) ( Nothing ) ( [] ) ( Nothing ) + ) ( Nothing ) ( [] ) ( Nothing ) :| [] ) NounPhrase ( [] ) ( Noun ( SgPl |