summaryrefslogtreecommitdiff
path: root/test/golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden')
-rw-r--r--test/golden/abbr/encoding tasks.golden2
-rw-r--r--test/golden/abbr/generating tasks.golden26
-rw-r--r--test/golden/abbr/glossing.golden38
-rw-r--r--test/golden/abbr/parsing.golden41
-rw-r--r--test/golden/abbr/tokenizing.golden7
-rw-r--r--test/golden/relparam/scanning.golden4
-rw-r--r--test/golden/relparam/tokenizing.golden38
7 files changed, 111 insertions, 45 deletions
diff --git a/test/golden/abbr/encoding tasks.golden b/test/golden/abbr/encoding tasks.golden
index 18ba749..365aa3d 100644
--- a/test/golden/abbr/encoding tasks.golden
+++ b/test/golden/abbr/encoding tasks.golden
@@ -1,6 +1,6 @@
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_noun,conjecture,![Xx]:Xx=Xx).
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).
diff --git a/test/golden/abbr/generating tasks.golden b/test/golden/abbr/generating tasks.golden
index 397fafe..d438481 100644
--- a/test/golden/abbr/generating tasks.golden
+++ b/test/golden/abbr/generating tasks.golden
@@ -117,17 +117,25 @@
)
]
, taskConjectureLabel = Marker "dummy_abbr_test_noun"
- , taskConjecture = TermSymbol
- ( SymbolPredicate
- ( PredicateRelation
- ( Symbol "=" )
+ , taskConjecture = Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
)
)
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "x" )
- ]
}
, Task
{ taskDirectness = Direct
diff --git a/test/golden/abbr/glossing.golden b/test/golden/abbr/glossing.golden
index 152fbe1..0efddcd 100644
--- a/test/golden/abbr/glossing.golden
+++ b/test/golden/abbr/glossing.golden
@@ -125,25 +125,31 @@
)
( Marker "dummy_abbr_test_noun" )
( Lemma []
- ( TermSymbol
- ( SymbolPredicate
- ( PredicateNoun
- ( SgPl
- { sg =
- [ Just
- ( Word "function" )
- ]
- , pl =
- [ Just
- ( Word "functions" )
- ]
- }
+ ( Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateNoun
+ ( SgPl
+ { sg =
+ [ Just
+ ( Word "function" )
+ ]
+ , pl =
+ [ Just
+ ( Word "functions" )
+ ]
+ }
+ )
+ )
)
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
)
)
- [ TermVar
- ( NamedVar "x" )
- ]
)
)
, BlockAbbr
diff --git a/test/golden/abbr/parsing.golden b/test/golden/abbr/parsing.golden
index 77a4c47..21e4c60 100644
--- a/test/golden/abbr/parsing.golden
+++ b/test/golden/abbr/parsing.golden
@@ -122,25 +122,28 @@
)
( Marker "dummy_abbr_test_noun" )
( Lemma []
- ( StmtNoun
- ( TermExpr
- ( ExprVar
- ( NamedVar "x" )
- ) :| []
- ) NounPhrase ( [] )
- ( Noun
- ( SgPl
- { sg =
- [ Just
- ( Word "function" )
- ]
- , pl =
- [ Just
- ( Word "functions" )
- ]
- }
- ) []
- ) ( Nothing ) ( [] ) ( Nothing )
+ ( SymbolicQuantified Universally
+ ( NamedVar "x" :| [] ) Unbounded Nothing
+ ( StmtNoun
+ ( TermExpr
+ ( ExprVar
+ ( NamedVar "x" )
+ ) :| []
+ ) NounPhrase ( [] )
+ ( Noun
+ ( SgPl
+ { sg =
+ [ Just
+ ( Word "function" )
+ ]
+ , pl =
+ [ Just
+ ( Word "functions" )
+ ]
+ }
+ ) []
+ ) ( Nothing ) ( [] ) ( Nothing )
+ )
)
)
, BlockAbbr
diff --git a/test/golden/abbr/tokenizing.golden b/test/golden/abbr/tokenizing.golden
index 8da4b07..10b17fb 100644
--- a/test/golden/abbr/tokenizing.golden
+++ b/test/golden/abbr/tokenizing.golden
@@ -56,6 +56,13 @@
, EndEnv "abbreviation"
, BeginEnv "proposition"
, Label "dummy_abbr_test_noun"
+, Word "for"
+, Word "all"
+, BeginEnv "math"
+, Variable "x"
+, EndEnv "math"
+, Word "we"
+, Word "have"
, BeginEnv "math"
, Variable "x"
, EndEnv "math"
diff --git a/test/golden/relparam/scanning.golden b/test/golden/relparam/scanning.golden
new file mode 100644
index 0000000..7c72985
--- /dev/null
+++ b/test/golden/relparam/scanning.golden
@@ -0,0 +1,4 @@
+[ ScanRelationSymbol
+ ( Command "EQUAL" )
+ ( Marker "equalparam" )
+] \ No newline at end of file
diff --git a/test/golden/relparam/tokenizing.golden b/test/golden/relparam/tokenizing.golden
new file mode 100644
index 0000000..95290d5
--- /dev/null
+++ b/test/golden/relparam/tokenizing.golden
@@ -0,0 +1,38 @@
+[ BeginEnv "abbreviation"
+, Label "equalparam"
+, BeginEnv "math"
+, Variable "x"
+, Command "EQUAL"
+, InvisibleBraceL
+, Variable "y"
+, InvisibleBraceR
+, Variable "z"
+, EndEnv "math"
+, Word "iff"
+, BeginEnv "math"
+, Variable "x"
+, Symbol "="
+, Variable "z"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "abbreviation"
+, BeginEnv "proposition"
+, Label "dummy_abbr_test_noun"
+, Word "for"
+, Word "all"
+, BeginEnv "math"
+, Variable "x"
+, EndEnv "math"
+, Word "we"
+, Word "have"
+, BeginEnv "math"
+, Variable "x"
+, Command "EQUAL"
+, InvisibleBraceL
+, Variable "y"
+, InvisibleBraceR
+, Variable "x"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+] \ No newline at end of file