summaryrefslogtreecommitdiff
path: root/test/golden/calc
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/calc')
-rw-r--r--test/golden/calc/encoding tasks.golden30
-rw-r--r--test/golden/calc/generating tasks.golden464
-rw-r--r--test/golden/calc/glossing.golden160
-rw-r--r--test/golden/calc/parsing.golden174
-rw-r--r--test/golden/calc/scanning.golden1
-rw-r--r--test/golden/calc/tokenizing.golden71
-rw-r--r--test/golden/calc/verification.golden1
7 files changed, 901 insertions, 0 deletions
diff --git a/test/golden/calc/encoding tasks.golden b/test/golden/calc/encoding tasks.golden
new file mode 100644
index 0000000..d4104e6
--- /dev/null
+++ b/test/golden/calc/encoding tasks.golden
@@ -0,0 +1,30 @@
+fof(trivial,conjecture,fx=fx).
+------------------
+fof(irrelevant,conjecture,fz=fz).
+fof(trivial,axiom,![Xx]:Xx=Xx).
+------------------
+fof(alsotrivial,conjecture,fy=fy).
+fof(irrelevant,axiom,![Xz]:Xz=Xz).
+fof(trivial,axiom,![Xx]:Xx=Xx).
+------------------
+fof(alsotrivial,conjecture,fy=fy).
+fof(trivial,axiom,![Xx]:Xx=Xx).
+------------------
+fof(alsotrivial,conjecture,fy=fy).
+fof(irrelevant,axiom,![Xz]:Xz=Xz).
+fof(trivial,axiom,![Xx]:Xx=Xx).
+fof(alsotrivial1,axiom,fy=fy).
+------------------
+fof(trivial_biconditionals,conjecture,fy=fy).
+fof(alsotrivial,axiom,![Xy]:Xy=Xy).
+fof(irrelevant,axiom,![Xz]:Xz=Xz).
+fof(trivial,axiom,![Xx]:Xx=Xx).
+------------------
+fof(trivial_biconditionals,conjecture,fy=fy).
+fof(trivial,axiom,![Xx]:Xx=Xx).
+------------------
+fof(trivial_biconditionals,conjecture,fy=fy).
+fof(alsotrivial,axiom,![Xy]:Xy=Xy).
+fof(irrelevant,axiom,![Xz]:Xz=Xz).
+fof(trivial,axiom,![Xx]:Xx=Xx).
+fof(trivial_biconditionals1,axiom,fy=fy<=>fy=fy). \ No newline at end of file
diff --git a/test/golden/calc/generating tasks.golden b/test/golden/calc/generating tasks.golden
new file mode 100644
index 0000000..6bd518c
--- /dev/null
+++ b/test/golden/calc/generating tasks.golden
@@ -0,0 +1,464 @@
+[ Task
+ { taskDirectness = Direct
+ , taskHypotheses = []
+ , taskConjectureLabel = Marker "trivial"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "x" )
+ , TermVar
+ ( NamedVar "x" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "trivial"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "irrelevant"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "z" )
+ , TermVar
+ ( NamedVar "z" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "irrelevant"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "z" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "z" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "trivial"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "alsotrivial"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "trivial"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "alsotrivial"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "irrelevant"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "z" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "z" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "trivial"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "alsotrivial1"
+ , TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ )
+ ]
+ , taskConjectureLabel = Marker "alsotrivial"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "alsotrivial"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "y" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "y" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "irrelevant"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "z" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "z" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "trivial"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "trivial_biconditionals"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "trivial"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "trivial_biconditionals"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "alsotrivial"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "y" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "y" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "irrelevant"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "z" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "z" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "trivial"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "trivial_biconditionals1"
+ , Connected Equivalence
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ )
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "trivial_biconditionals"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ }
+] \ No newline at end of file
diff --git a/test/golden/calc/glossing.golden b/test/golden/calc/glossing.golden
new file mode 100644
index 0000000..96366d4
--- /dev/null
+++ b/test/golden/calc/glossing.golden
@@ -0,0 +1,160 @@
+[ BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 1
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "trivial" )
+ ( Lemma []
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "x" )
+ , TermVar
+ ( NamedVar "x" )
+ ]
+ )
+ )
+, BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 5
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "irrelevant" )
+ ( Lemma []
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "z" )
+ , TermVar
+ ( NamedVar "z" )
+ ]
+ )
+ )
+, BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 9
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "alsotrivial" )
+ ( Lemma []
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ )
+ )
+, BlockProof
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 12
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Calc
+ ( Equation
+ ( TermVar
+ ( NamedVar "y" )
+ )
+ (
+ ( TermVar
+ ( NamedVar "y" )
+ , JustificationEmpty
+ ) :|
+ [
+ ( TermVar
+ ( NamedVar "y" )
+ , JustificationRef
+ ( Marker "trivial" :| [] )
+ )
+ ]
+ )
+ ) ( Qed JustificationEmpty )
+ )
+, BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 22
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "trivial_biconditionals" )
+ ( Lemma []
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ )
+ )
+, BlockProof
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 25
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Calc
+ ( Biconditionals
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ )
+ (
+ ( PropositionalConstant IsTop
+ , JustificationEmpty
+ ) :|
+ [
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "y" )
+ , TermVar
+ ( NamedVar "y" )
+ ]
+ , JustificationRef
+ ( Marker "trivial" :| [] )
+ )
+ ]
+ )
+ ) ( Qed JustificationEmpty )
+ )
+] \ No newline at end of file
diff --git a/test/golden/calc/parsing.golden b/test/golden/calc/parsing.golden
new file mode 100644
index 0000000..3d86683
--- /dev/null
+++ b/test/golden/calc/parsing.golden
@@ -0,0 +1,174 @@
+[ BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 1
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "trivial" )
+ ( Lemma []
+ ( StmtFormula
+ ( FormulaChain
+ ( ChainBase
+ ( ExprVar
+ ( NamedVar "x" ) :| []
+ ) Positive
+ ( RelationSymbol
+ ( Symbol "=" )
+ )
+ ( ExprVar
+ ( NamedVar "x" ) :| []
+ )
+ )
+ )
+ )
+ )
+, BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 5
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "irrelevant" )
+ ( Lemma []
+ ( StmtFormula
+ ( FormulaChain
+ ( ChainBase
+ ( ExprVar
+ ( NamedVar "z" ) :| []
+ ) Positive
+ ( RelationSymbol
+ ( Symbol "=" )
+ )
+ ( ExprVar
+ ( NamedVar "z" ) :| []
+ )
+ )
+ )
+ )
+ )
+, BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 9
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "alsotrivial" )
+ ( Lemma []
+ ( StmtFormula
+ ( FormulaChain
+ ( ChainBase
+ ( ExprVar
+ ( NamedVar "y" ) :| []
+ ) Positive
+ ( RelationSymbol
+ ( Symbol "=" )
+ )
+ ( ExprVar
+ ( NamedVar "y" ) :| []
+ )
+ )
+ )
+ )
+ )
+, BlockProof
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 12
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Calc
+ ( Equation
+ ( ExprVar
+ ( NamedVar "y" )
+ )
+ (
+ ( ExprVar
+ ( NamedVar "y" )
+ , JustificationEmpty
+ ) :|
+ [
+ ( ExprVar
+ ( NamedVar "y" )
+ , JustificationRef
+ ( Marker "trivial" :| [] )
+ )
+ ]
+ )
+ ) ( Qed JustificationEmpty )
+ )
+, BlockLemma
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 22
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Marker "trivial_biconditionals" )
+ ( Lemma []
+ ( StmtFormula
+ ( FormulaChain
+ ( ChainBase
+ ( ExprVar
+ ( NamedVar "y" ) :| []
+ ) Positive
+ ( RelationSymbol
+ ( Symbol "=" )
+ )
+ ( ExprVar
+ ( NamedVar "y" ) :| []
+ )
+ )
+ )
+ )
+ )
+, BlockProof
+ ( SourcePos
+ { sourceName = "test/examples/calc.tex"
+ , sourceLine = Pos 25
+ , sourceColumn = Pos 1
+ }
+ )
+ ( Calc
+ ( Biconditionals
+ ( FormulaChain
+ ( ChainBase
+ ( ExprVar
+ ( NamedVar "y" ) :| []
+ ) Positive
+ ( RelationSymbol
+ ( Symbol "=" )
+ )
+ ( ExprVar
+ ( NamedVar "y" ) :| []
+ )
+ )
+ )
+ (
+ ( PropositionalConstant IsTop
+ , JustificationEmpty
+ ) :|
+ [
+ ( FormulaChain
+ ( ChainBase
+ ( ExprVar
+ ( NamedVar "y" ) :| []
+ ) Positive
+ ( RelationSymbol
+ ( Symbol "=" )
+ )
+ ( ExprVar
+ ( NamedVar "y" ) :| []
+ )
+ )
+ , JustificationRef
+ ( Marker "trivial" :| [] )
+ )
+ ]
+ )
+ ) ( Qed JustificationEmpty )
+ )
+] \ No newline at end of file
diff --git a/test/golden/calc/scanning.golden b/test/golden/calc/scanning.golden
new file mode 100644
index 0000000..0637a08
--- /dev/null
+++ b/test/golden/calc/scanning.golden
@@ -0,0 +1 @@
+[] \ No newline at end of file
diff --git a/test/golden/calc/tokenizing.golden b/test/golden/calc/tokenizing.golden
new file mode 100644
index 0000000..a99980c
--- /dev/null
+++ b/test/golden/calc/tokenizing.golden
@@ -0,0 +1,71 @@
+[ BeginEnv "proposition"
+, Label "trivial"
+, BeginEnv "math"
+, Variable "x"
+, Symbol "="
+, Variable "x"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+, BeginEnv "proposition"
+, Label "irrelevant"
+, BeginEnv "math"
+, Variable "z"
+, Symbol "="
+, Variable "z"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+, BeginEnv "proposition"
+, Label "alsotrivial"
+, BeginEnv "math"
+, Variable "y"
+, Symbol "="
+, Variable "y"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+, BeginEnv "proof"
+, BeginEnv "align*"
+, Variable "y"
+, Symbol "&="
+, Variable "y"
+, Symbol "&="
+, Variable "y"
+, BeginEnv "text"
+, Word "by"
+, Ref
+ ( "trivial" :| [] )
+, EndEnv "text"
+, EndEnv "align*"
+, EndEnv "proof"
+, BeginEnv "proposition"
+, Label "trivial_biconditionals"
+, BeginEnv "math"
+, Variable "y"
+, Symbol "="
+, Variable "y"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+, BeginEnv "proof"
+, BeginEnv "align*"
+, Variable "y"
+, Symbol "="
+, Variable "y"
+, Symbol "&"
+, Command "iff"
+, Command "top"
+, Symbol "&"
+, Command "iff"
+, Variable "y"
+, Symbol "="
+, Variable "y"
+, BeginEnv "text"
+, Word "by"
+, Ref
+ ( "trivial" :| [] )
+, EndEnv "text"
+, EndEnv "align*"
+, EndEnv "proof"
+] \ No newline at end of file
diff --git a/test/golden/calc/verification.golden b/test/golden/calc/verification.golden
new file mode 100644
index 0000000..69b9873
--- /dev/null
+++ b/test/golden/calc/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 13:19:39 +0000