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 --- test/golden/abbr/parsing.golden | 4 +- test/golden/coord/encoding tasks.golden | 14 +- test/golden/coord/generating tasks.golden | 679 ++++++++++++++++++++++++++++ test/golden/coord/glossing.golden | 151 +++++++ test/golden/coord/parsing.golden | 69 ++- test/golden/coord/tokenizing.golden | 25 + test/golden/formula/encoding tasks.golden | 4 + test/golden/formula/generating tasks.golden | 111 +++++ test/golden/formula/glossing.golden | 54 +++ test/golden/formula/parsing.golden | 52 +++ test/golden/formula/tokenizing.golden | 27 ++ test/golden/indefinite-terms/parsing.golden | 4 +- 12 files changed, 1188 insertions(+), 6 deletions(-) (limited to 'test/golden') 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 -- cgit v1.2.3