From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Sat, 10 Feb 2024 02:22:14 +0100 Subject: Initial commit --- test/golden/calc/encoding tasks.golden | 30 ++ test/golden/calc/generating tasks.golden | 464 +++++++++++++++++++++++++++++++ test/golden/calc/glossing.golden | 160 +++++++++++ test/golden/calc/parsing.golden | 174 ++++++++++++ test/golden/calc/scanning.golden | 1 + test/golden/calc/tokenizing.golden | 71 +++++ test/golden/calc/verification.golden | 1 + 7 files changed, 901 insertions(+) create mode 100644 test/golden/calc/encoding tasks.golden create mode 100644 test/golden/calc/generating tasks.golden create mode 100644 test/golden/calc/glossing.golden create mode 100644 test/golden/calc/parsing.golden create mode 100644 test/golden/calc/scanning.golden create mode 100644 test/golden/calc/tokenizing.golden create mode 100644 test/golden/calc/verification.golden (limited to 'test/golden/calc') 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 -- cgit v1.2.3