summaryrefslogtreecommitdiff
path: root/test/golden/finite-set-terms
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2024-02-10 02:22:14 +0100
committeradelon <22380201+adelon@users.noreply.github.com>2024-02-10 02:22:14 +0100
commit442d732696ad431b84f6e5c72b6ee785be4fd968 (patch)
treeb476f395e7e91d67bacb6758bc84914b8711593f /test/golden/finite-set-terms
Initial commit
Diffstat (limited to 'test/golden/finite-set-terms')
-rw-r--r--test/golden/finite-set-terms/encoding tasks.golden3
-rw-r--r--test/golden/finite-set-terms/generating tasks.golden165
-rw-r--r--test/golden/finite-set-terms/glossing.golden135
-rw-r--r--test/golden/finite-set-terms/parsing.golden124
-rw-r--r--test/golden/finite-set-terms/scanning.golden6
-rw-r--r--test/golden/finite-set-terms/tokenizing.golden48
-rw-r--r--test/golden/finite-set-terms/verification.golden1
7 files changed, 482 insertions, 0 deletions
diff --git a/test/golden/finite-set-terms/encoding tasks.golden b/test/golden/finite-set-terms/encoding tasks.golden
new file mode 100644
index 0000000..381bdf0
--- /dev/null
+++ b/test/golden/finite-set-terms/encoding tasks.golden
@@ -0,0 +1,3 @@
+fof(emptyset_in_unit,conjecture,elem(emptyset,unit)).
+fof(unit,axiom,![Xany]:(elem(Xany,unit)<=>(elem(Xany,emptyset)|Xany=emptyset))).
+fof(cons,axiom,![Xx,Xy,XX]:(elem(Xx,cons(Xy,XX))<=>(Xx=Xy|elem(Xx,XX)))). \ No newline at end of file
diff --git a/test/golden/finite-set-terms/generating tasks.golden b/test/golden/finite-set-terms/generating tasks.golden
new file mode 100644
index 0000000..84df2ba
--- /dev/null
+++ b/test/golden/finite-set-terms/generating tasks.golden
@@ -0,0 +1,165 @@
+[ Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "unit"
+ , Quantified Universally
+ ( Scope
+ ( Connected Equivalence
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "any" )
+ )
+ , TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "unit" )
+ ]
+ ) []
+ ]
+ )
+ ( Connected Disjunction
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "any" )
+ )
+ , TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "emptyset" )
+ ]
+ ) []
+ ]
+ )
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "any" )
+ )
+ , TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "emptyset" )
+ ]
+ ) []
+ ]
+ )
+ )
+ )
+ )
+ )
+ ,
+ ( Marker "cons"
+ , Quantified Universally
+ ( Scope
+ ( Connected Equivalence
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "cons" )
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ ]
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "y" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "X" )
+ )
+ ]
+ ]
+ )
+ ( Connected Disjunction
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "y" )
+ )
+ ]
+ )
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "X" )
+ )
+ ]
+ )
+ )
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "emptyset_in_unit"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "emptyset" )
+ ]
+ ) []
+ , TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "unit" )
+ ]
+ ) []
+ ]
+ }
+] \ No newline at end of file
diff --git a/test/golden/finite-set-terms/glossing.golden b/test/golden/finite-set-terms/glossing.golden
new file mode 100644
index 0000000..7bafb15
--- /dev/null
+++ b/test/golden/finite-set-terms/glossing.golden
@@ -0,0 +1,135 @@
+[ BlockAxiom
+ ( SourcePos
+ { sourceName = "test/examples/finite-set-terms.tex"
+ , sourceLine = Pos 1
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "cons" )
+ ( Axiom []
+ ( Connected Equivalence
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "x" )
+ , TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "cons" )
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ ]
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "X" )
+ ]
+ ]
+ )
+ ( Connected Disjunction
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "x" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ )
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "x" )
+ , TermVar
+ ( NamedVar "X" )
+ ]
+ )
+ )
+ )
+ )
+, BlockDefn
+ ( SourcePos
+ { sourceName = "test/examples/finite-set-terms.tex"
+ , sourceLine = Pos 5
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "unit" )
+ ( DefnOp
+ [ Just
+ ( Command "unit" )
+ ] []
+ ( TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "cons" )
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ ]
+ )
+ [ TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "emptyset" )
+ ]
+ ) []
+ , TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "emptyset" )
+ ]
+ ) []
+ ]
+ )
+ )
+, BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/finite-set-terms.tex"
+ , sourceLine = Pos 9
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "emptyset_in_unit" )
+ ( Lemma []
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "emptyset" )
+ ]
+ ) []
+ , TermSymbol
+ ( SymbolMixfix
+ [ Just
+ ( Command "unit" )
+ ]
+ ) []
+ ]
+ )
+ )
+] \ No newline at end of file
diff --git a/test/golden/finite-set-terms/parsing.golden b/test/golden/finite-set-terms/parsing.golden
new file mode 100644
index 0000000..c30f70b
--- /dev/null
+++ b/test/golden/finite-set-terms/parsing.golden
@@ -0,0 +1,124 @@
+[ BlockAxiom
+ ( SourcePos
+ { sourceName = "test/examples/finite-set-terms.tex"
+ , sourceLine = Pos 1
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "cons" )
+ ( Axiom []
+ ( StmtConnected Equivalence
+ ( StmtFormula
+ ( FormulaChain
+ ( ChainBase
+ ( ExprVar
+ ( NamedVar "x" ) :| []
+ ) Positive
+ ( RelationSymbol
+ ( Command "in" )
+ )
+ ( ExprOp
+ [ Just
+ ( Command "cons" )
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ , Just InvisibleBraceL
+ , Nothing
+ , Just InvisibleBraceR
+ ]
+ [ ExprVar
+ ( NamedVar "y" )
+ , ExprVar
+ ( NamedVar "X" )
+ ] :| []
+ )
+ )
+ )
+ )
+ ( StmtConnected Disjunction
+ ( StmtFormula
+ ( FormulaChain
+ ( ChainBase
+ ( ExprVar
+ ( NamedVar "x" ) :| []
+ ) Positive
+ ( RelationSymbol
+ ( Symbol "=" )
+ )
+ ( ExprVar
+ ( NamedVar "y" ) :| []
+ )
+ )
+ )
+ )
+ ( StmtFormula
+ ( FormulaChain
+ ( ChainBase
+ ( ExprVar
+ ( NamedVar "x" ) :| []
+ ) Positive
+ ( RelationSymbol
+ ( Command "in" )
+ )
+ ( ExprVar
+ ( NamedVar "X" ) :| []
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+, BlockDefn
+ ( SourcePos
+ { sourceName = "test/examples/finite-set-terms.tex"
+ , sourceLine = Pos 5
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "unit" )
+ ( DefnOp
+ ( SymbolPattern
+ [ Just
+ ( Command "unit" )
+ ] []
+ )
+ ( ExprFiniteSet
+ ( ExprOp
+ [ Just
+ ( Command "emptyset" )
+ ] [] :| []
+ )
+ )
+ )
+, BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/finite-set-terms.tex"
+ , sourceLine = Pos 9
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "emptyset_in_unit" )
+ ( Lemma []
+ ( StmtFormula
+ ( FormulaChain
+ ( ChainBase
+ ( ExprOp
+ [ Just
+ ( Command "emptyset" )
+ ] [] :| []
+ ) Positive
+ ( RelationSymbol
+ ( Command "in" )
+ )
+ ( ExprOp
+ [ Just
+ ( Command "unit" )
+ ] [] :| []
+ )
+ )
+ )
+ )
+ )
+] \ No newline at end of file
diff --git a/test/golden/finite-set-terms/scanning.golden b/test/golden/finite-set-terms/scanning.golden
new file mode 100644
index 0000000..1a9f920
--- /dev/null
+++ b/test/golden/finite-set-terms/scanning.golden
@@ -0,0 +1,6 @@
+[ ScanFunctionSymbol
+ [ Just
+ ( Command "unit" )
+ ]
+ ( Marker "unit" )
+] \ No newline at end of file
diff --git a/test/golden/finite-set-terms/tokenizing.golden b/test/golden/finite-set-terms/tokenizing.golden
new file mode 100644
index 0000000..761cbde
--- /dev/null
+++ b/test/golden/finite-set-terms/tokenizing.golden
@@ -0,0 +1,48 @@
+[ BeginEnv "axiom"
+, Label "cons"
+, BeginEnv "math"
+, Variable "x"
+, Command "in"
+, Command "cons"
+, InvisibleBraceL
+, Variable "y"
+, InvisibleBraceR
+, InvisibleBraceL
+, Variable "X"
+, InvisibleBraceR
+, EndEnv "math"
+, Word "iff"
+, BeginEnv "math"
+, Variable "x"
+, Symbol "="
+, Variable "y"
+, EndEnv "math"
+, Word "or"
+, BeginEnv "math"
+, Variable "x"
+, Command "in"
+, Variable "X"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "axiom"
+, BeginEnv "definition"
+, Label "unit"
+, BeginEnv "math"
+, Command "unit"
+, Symbol "="
+, VisibleBraceL
+, Command "emptyset"
+, VisibleBraceR
+, EndEnv "math"
+, Symbol "."
+, EndEnv "definition"
+, BeginEnv "proposition"
+, Label "emptyset_in_unit"
+, BeginEnv "math"
+, Command "emptyset"
+, Command "in"
+, Command "unit"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+] \ No newline at end of file
diff --git a/test/golden/finite-set-terms/verification.golden b/test/golden/finite-set-terms/verification.golden
new file mode 100644
index 0000000..69b9873
--- /dev/null
+++ b/test/golden/finite-set-terms/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 08:45:42 +0000