summaryrefslogtreecommitdiff
path: root/test/golden/coord
diff options
context:
space:
mode:
authorSimon-Kor <52245124+Simon-Kor@users.noreply.github.com>2024-05-07 18:08:34 +0200
committerGitHub <noreply@github.com>2024-05-07 18:08:34 +0200
commitfcaffbf3cb44e804fe6df25b32f09d33e1afbabb (patch)
treecf00f0039e78882353706553100398b24fd32f39 /test/golden/coord
parent08019dcdaf3b13bb8ce554dfd5377690bb508c6d (diff)
parentb2f9f7900ccb4a569ed23e9ecf327564dbba2b7d (diff)
Merge branch 'adelon:main' into main
Diffstat (limited to 'test/golden/coord')
-rw-r--r--test/golden/coord/encoding tasks.golden14
-rw-r--r--test/golden/coord/generating tasks.golden679
-rw-r--r--test/golden/coord/glossing.golden151
-rw-r--r--test/golden/coord/parsing.golden69
-rw-r--r--test/golden/coord/tokenizing.golden25
5 files changed, 936 insertions, 2 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-06 16:26:27 +0000