From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Sat, 10 Feb 2024 02:22:14 +0100 Subject: Initial commit --- test/golden/abbr/encoding tasks.golden | 26 + test/golden/abbr/generating tasks.golden | 836 +++++++++++++++++++++++++++++++ test/golden/abbr/glossing.golden | 384 ++++++++++++++ test/golden/abbr/parsing.golden | 408 +++++++++++++++ test/golden/abbr/scanning.golden | 19 + test/golden/abbr/tokenizing.golden | 164 ++++++ test/golden/abbr/verification.golden | 1 + 7 files changed, 1838 insertions(+) create mode 100644 test/golden/abbr/encoding tasks.golden create mode 100644 test/golden/abbr/generating tasks.golden create mode 100644 test/golden/abbr/glossing.golden create mode 100644 test/golden/abbr/parsing.golden create mode 100644 test/golden/abbr/scanning.golden create mode 100644 test/golden/abbr/tokenizing.golden create mode 100644 test/golden/abbr/verification.golden (limited to 'test/golden/abbr') diff --git a/test/golden/abbr/encoding tasks.golden b/test/golden/abbr/encoding tasks.golden new file mode 100644 index 0000000..18ba749 --- /dev/null +++ b/test/golden/abbr/encoding tasks.golden @@ -0,0 +1,26 @@ +fof(dummy_abbr_test_adj,conjecture,~?[Xy]:elem(Xy,fx)=>~?[Xy]:elem(Xy,fx)). +------------------ +fof(dummy_abbr_test_noun,conjecture,fx=fx). +fof(dummy_abbr_test_adj,axiom,![Xx]:(~?[Xy]:elem(Xy,Xx)=>~?[Xy]:elem(Xy,Xx))). +------------------ +fof(dummy_abbr_test_verb,conjecture,fx=fy=>fx=fy). +fof(dummy_abbr_test_noun,axiom,![Xx]:Xx=Xx). +fof(dummy_abbr_test_adj,axiom,![Xx]:(~?[Xy]:elem(Xy,Xx)=>~?[Xy]:elem(Xy,Xx))). +------------------ +fof(abbr_test_notin,conjecture,~elem(fx,fy)=>~elem(fx,fy)). +fof(dummy_abbr_test_verb,axiom,![Xx,Xy]:(Xx=Xy=>Xx=Xy)). +fof(dummy_abbr_test_noun,axiom,![Xx]:Xx=Xx). +fof(dummy_abbr_test_adj,axiom,![Xx]:(~?[Xy]:elem(Xy,Xx)=>~?[Xy]:elem(Xy,Xx))). +------------------ +fof(abbr_test_elementof_is_in,conjecture,elem(fx,fy)=>elem(fx,fy)). +fof(abbr_test_notin,axiom,![Xx,Xy]:(~elem(Xx,Xy)=>~elem(Xx,Xy))). +fof(dummy_abbr_test_verb,axiom,![Xx,Xy]:(Xx=Xy=>Xx=Xy)). +fof(dummy_abbr_test_noun,axiom,![Xx]:Xx=Xx). +fof(dummy_abbr_test_adj,axiom,![Xx]:(~?[Xy]:elem(Xy,Xx)=>~?[Xy]:elem(Xy,Xx))). +------------------ +fof(abbr_test_equals_is_eq,conjecture,fx=fy=>fx=fy). +fof(abbr_test_elementof_is_in,axiom,![Xx,Xy]:(elem(Xx,Xy)=>elem(Xx,Xy))). +fof(abbr_test_notin,axiom,![Xx,Xy]:(~elem(Xx,Xy)=>~elem(Xx,Xy))). +fof(dummy_abbr_test_verb,axiom,![Xx,Xy]:(Xx=Xy=>Xx=Xy)). +fof(dummy_abbr_test_noun,axiom,![Xx]:Xx=Xx). +fof(dummy_abbr_test_adj,axiom,![Xx]:(~?[Xy]:elem(Xy,Xx)=>~?[Xy]:elem(Xy,Xx))). \ No newline at end of file diff --git a/test/golden/abbr/generating tasks.golden b/test/golden/abbr/generating tasks.golden new file mode 100644 index 0000000..397fafe --- /dev/null +++ b/test/golden/abbr/generating tasks.golden @@ -0,0 +1,836 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = [] + , taskConjectureLabel = Marker "dummy_abbr_test_adj" + , taskConjecture = Connected Implication + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "x" ) + ) + ) + ] + ) + ) + ) + ) + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "x" ) + ) + ) + ] + ) + ) + ) + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "dummy_abbr_test_adj" + , Quantified Universally + ( Scope + ( Connected Implication + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "dummy_abbr_test_noun" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "x" ) + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "dummy_abbr_test_noun" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + , + ( Marker "dummy_abbr_test_adj" + , Quantified Universally + ( Scope + ( Connected Implication + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "dummy_abbr_test_verb" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "dummy_abbr_test_verb" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "dummy_abbr_test_noun" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + , + ( Marker "dummy_abbr_test_adj" + , Quantified Universally + ( Scope + ( Connected Implication + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "abbr_test_notin" + , taskConjecture = Connected Implication + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "abbr_test_notin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "dummy_abbr_test_verb" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "dummy_abbr_test_noun" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + , + ( Marker "dummy_abbr_test_adj" + , Quantified Universally + ( Scope + ( Connected Implication + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "abbr_test_elementof_is_in" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "abbr_test_elementof_is_in" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "abbr_test_notin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "dummy_abbr_test_verb" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "dummy_abbr_test_noun" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + , + ( Marker "dummy_abbr_test_adj" + , Quantified Universally + ( Scope + ( Connected Implication + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "abbr_test_equals_is_eq" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + } +] \ No newline at end of file diff --git a/test/golden/abbr/glossing.golden b/test/golden/abbr/glossing.golden new file mode 100644 index 0000000..152fbe1 --- /dev/null +++ b/test/golden/abbr/glossing.golden @@ -0,0 +1,384 @@ +[ BlockAbbr + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "empty" ) + ( Abbreviation + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "empty" ) + ] + ) + ) + ( Scope + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( F + ( TermVar + ( B 0 ) + ) + ) + ] + ) + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 5 + , sourceColumn = Pos 1 + } + ) + ( Marker "dummy_abbr_test_adj" ) + ( Lemma [] + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "empty" ) + ] + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "empty" ) + ] + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ) + ) +, BlockAbbr + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 11 + , sourceColumn = Pos 1 + } + ) + ( Marker "function" ) + ( Abbreviation + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "function" ) + ] + , pl = + [ Just + ( Word "functions" ) + ] + } + ) + ) + ) + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B 0 ) + , TermVar + ( B 0 ) + ] + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "dummy_abbr_test_noun" ) + ( Lemma [] + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "function" ) + ] + , pl = + [ Just + ( Word "functions" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + ) +, BlockAbbr + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 21 + , sourceColumn = Pos 1 + } + ) + ( Marker "converges" ) + ( Abbreviation + ( SymbolPredicate + ( PredicateVerb + ( SgPl + { sg = + [ Just + ( Word "converges" ) + , Just + ( Word "to" ) + , Nothing + ] + , pl = + [ Just + ( Word "converge" ) + , Just + ( Word "to" ) + , Nothing + ] + } + ) + ) + ) + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B 0 ) + , TermVar + ( B 1 ) + ] + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 25 + , sourceColumn = Pos 1 + } + ) + ( Marker "dummy_abbr_test_verb" ) + ( Lemma [] + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateVerb + ( SgPl + { sg = + [ Just + ( Word "converges" ) + , Just + ( Word "to" ) + , Nothing + ] + , pl = + [ Just + ( Word "converge" ) + , Just + ( Word "to" ) + , Nothing + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 31 + , sourceColumn = Pos 1 + } + ) + ( Marker "abbr_test_notin" ) + ( Lemma [] + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "notin" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 37 + , sourceColumn = Pos 1 + } + ) + ( Marker "abbr_test_elementof_is_in" ) + ( Lemma [] + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "element" ) + , Just + ( Word "of" ) + , Nothing + ] + , pl = + [ Just + ( Word "elements" ) + , Just + ( Word "of" ) + , Nothing + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 43 + , sourceColumn = Pos 1 + } + ) + ( Marker "abbr_test_equals_is_eq" ) + ( Lemma [] + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateVerb + ( SgPl + { sg = + [ Just + ( Word "equals" ) + , Nothing + ] + , pl = + [ Just + ( Word "equal" ) + , Nothing + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ) + ) +] \ No newline at end of file diff --git a/test/golden/abbr/parsing.golden b/test/golden/abbr/parsing.golden new file mode 100644 index 0000000..bad58c3 --- /dev/null +++ b/test/golden/abbr/parsing.golden @@ -0,0 +1,408 @@ +[ BlockAbbr + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "empty" ) + ( AbbreviationAdj + ( NamedVar "x" ) + ( Adj + [ Just + ( Word "empty" ) + ] [] + ) + ( StmtNeg + ( SymbolicQuantified Existentially + ( NamedVar "y" :| [] ) Unbounded Nothing + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "y" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "x" ) :| [] + ) + ) + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 5 + , sourceColumn = Pos 1 + } + ) + ( Marker "dummy_abbr_test_adj" ) + ( Lemma [] + ( StmtConnected Implication + ( StmtVerbPhrase + ( TermExpr + ( ExprVar + ( NamedVar "x" ) + ) :| [] + ) + ( VPAdj + ( Adj + [ Just + ( Word "empty" ) + ] [] :| [] + ) + ) + ) + ( StmtVerbPhrase + ( TermExpr + ( ExprVar + ( NamedVar "x" ) + ) :| [] + ) + ( VPAdj + ( Adj + [ Just + ( Word "empty" ) + ] [] :| [] + ) + ) + ) + ) + ) +, BlockAbbr + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 11 + , sourceColumn = Pos 1 + } + ) + ( Marker "function" ) + ( AbbreviationNoun + ( NamedVar "x" ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "function" ) + ] + , pl = + [ Just + ( Word "functions" ) + ] + } + ) [] + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "x" ) :| [] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "dummy_abbr_test_noun" ) + ( Lemma [] + ( StmtNoun + ( TermExpr + ( ExprVar + ( NamedVar "x" ) + ) + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "function" ) + ] + , pl = + [ Just + ( Word "functions" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) + ) +, BlockAbbr + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 21 + , sourceColumn = Pos 1 + } + ) + ( Marker "converges" ) + ( AbbreviationVerb + ( NamedVar "x" ) + ( Verb + ( SgPl + { sg = + [ Just + ( Word "converges" ) + , Just + ( Word "to" ) + , Nothing + ] + , pl = + [ Just + ( Word "converge" ) + , Just + ( Word "to" ) + , Nothing + ] + } + ) + [ NamedVar "y" ] + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 25 + , sourceColumn = Pos 1 + } + ) + ( Marker "dummy_abbr_test_verb" ) + ( Lemma [] + ( StmtConnected Implication + ( StmtVerbPhrase + ( TermExpr + ( ExprVar + ( NamedVar "x" ) + ) :| [] + ) + ( VPVerb + ( Verb + ( SgPl + { sg = + [ Just + ( Word "converges" ) + , Just + ( Word "to" ) + , Nothing + ] + , pl = + [ Just + ( Word "converge" ) + , Just + ( Word "to" ) + , Nothing + ] + } + ) + [ TermExpr + ( ExprVar + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 31 + , sourceColumn = Pos 1 + } + ) + ( Marker "abbr_test_notin" ) + ( Lemma [] + ( StmtConnected Implication + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "notin" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Negative + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 37 + , sourceColumn = Pos 1 + } + ) + ( Marker "abbr_test_elementof_is_in" ) + ( Lemma [] + ( StmtConnected Implication + ( StmtNoun + ( TermExpr + ( ExprVar + ( NamedVar "x" ) + ) + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "element" ) + , Just + ( Word "of" ) + , Nothing + ] + , pl = + [ Just + ( Word "elements" ) + , Just + ( Word "of" ) + , Nothing + ] + } + ) + [ TermExpr + ( ExprVar + ( NamedVar "y" ) + ) + ] + ) ( Nothing ) ( [] ) ( Nothing ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/abbr.tex" + , sourceLine = Pos 43 + , sourceColumn = Pos 1 + } + ) + ( Marker "abbr_test_equals_is_eq" ) + ( Lemma [] + ( StmtConnected Implication + ( StmtVerbPhrase + ( TermExpr + ( ExprVar + ( NamedVar "x" ) + ) :| [] + ) + ( VPVerb + ( Verb + ( SgPl + { sg = + [ Just + ( Word "equals" ) + , Nothing + ] + , pl = + [ Just + ( Word "equal" ) + , Nothing + ] + } + ) + [ TermExpr + ( ExprVar + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ) + ) +] \ No newline at end of file diff --git a/test/golden/abbr/scanning.golden b/test/golden/abbr/scanning.golden new file mode 100644 index 0000000..397e257 --- /dev/null +++ b/test/golden/abbr/scanning.golden @@ -0,0 +1,19 @@ +[ ScanAdj + [ Just + ( Word "empty" ) + ] + ( Marker "empty" ) +, ScanNoun + [ Just + ( Word "function" ) + ] + ( Marker "function" ) +, ScanVerb + [ Just + ( Word "converges" ) + , Just + ( Word "to" ) + , Nothing + ] + ( Marker "converges" ) +] \ No newline at end of file diff --git a/test/golden/abbr/tokenizing.golden b/test/golden/abbr/tokenizing.golden new file mode 100644 index 0000000..8da4b07 --- /dev/null +++ b/test/golden/abbr/tokenizing.golden @@ -0,0 +1,164 @@ +[ BeginEnv "abbreviation" +, Label "empty" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "is" +, Word "empty" +, Word "iff" +, Word "there" +, Word "exists" +, Word "no" +, BeginEnv "math" +, Variable "y" +, EndEnv "math" +, Word "such" +, Word "that" +, BeginEnv "math" +, Variable "y" +, Command "in" +, Variable "x" +, EndEnv "math" +, Symbol "." +, EndEnv "abbreviation" +, BeginEnv "proposition" +, Label "dummy_abbr_test_adj" +, Word "if" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "is" +, Word "empty" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "is" +, Word "empty" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "abbreviation" +, Label "function" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "is" +, Word "a" +, Word "function" +, Word "iff" +, BeginEnv "math" +, Variable "x" +, Symbol "=" +, Variable "x" +, EndEnv "math" +, Symbol "." +, EndEnv "abbreviation" +, BeginEnv "proposition" +, Label "dummy_abbr_test_noun" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "is" +, Word "a" +, Word "function" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "abbreviation" +, Label "converges" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "converges" +, Word "to" +, BeginEnv "math" +, Variable "y" +, EndEnv "math" +, Word "iff" +, BeginEnv "math" +, Variable "x" +, Symbol "=" +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "abbreviation" +, BeginEnv "proposition" +, Label "dummy_abbr_test_verb" +, Word "if" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "converges" +, Word "to" +, BeginEnv "math" +, Variable "y" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "x" +, Symbol "=" +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proposition" +, Label "abbr_test_notin" +, Word "if" +, BeginEnv "math" +, Variable "x" +, Command "notin" +, Variable "y" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "x" +, Command "not" +, Command "in" +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proposition" +, Label "abbr_test_elementof_is_in" +, Word "if" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "is" +, Word "an" +, Word "element" +, Word "of" +, BeginEnv "math" +, Variable "y" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proposition" +, Label "abbr_test_equals_is_eq" +, Word "if" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "equals" +, BeginEnv "math" +, Variable "y" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "x" +, Symbol "=" +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +] \ No newline at end of file diff --git a/test/golden/abbr/verification.golden b/test/golden/abbr/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/abbr/verification.golden @@ -0,0 +1 @@ +VerificationSuccess \ No newline at end of file -- cgit v1.2.3