summaryrefslogtreecommitdiff
path: root/test/golden/abbr
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/abbr')
-rw-r--r--test/golden/abbr/encoding tasks.golden26
-rw-r--r--test/golden/abbr/generating tasks.golden836
-rw-r--r--test/golden/abbr/glossing.golden384
-rw-r--r--test/golden/abbr/parsing.golden408
-rw-r--r--test/golden/abbr/scanning.golden19
-rw-r--r--test/golden/abbr/tokenizing.golden164
-rw-r--r--test/golden/abbr/verification.golden1
7 files changed, 1838 insertions, 0 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-06 10:28:20 +0000