Initial commit

7 files changed, 770 insertions, 0 deletions

diff --git a/test/golden/byRef/encoding tasks.golden b/test/golden/byRef/encoding tasks.golden
new file mode 100644
index 0000000..75c9e78
--- /dev/null
+++ b/test/golden/byRef/encoding tasks.golden
@@ -0,0 +1,22 @@
+fof(first_proposition,conjecture,fa=fa).
+------------------
+fof(second_proposition,conjecture,fb=fb).
+fof(first_proposition,axiom,![Xa]:Xa=Xa).
+------------------
+fof(third_proposition,conjecture,fc=fc).
+fof(first_proposition,axiom,![Xa]:Xa=Xa).
+------------------
+fof(fourth_proposition,conjecture,![Xd]:Xd=Xd).
+fof(first_proposition,axiom,![Xa]:Xa=Xa).
+------------------
+fof(fourth_proposition,conjecture,fe=fe).
+fof(third_proposition,axiom,![Xc]:Xc=Xc).
+fof(second_proposition,axiom,![Xb]:Xb=Xb).
+fof(first_proposition,axiom,![Xa]:Xa=Xa).
+fof(fourth_proposition1,axiom,![Xd]:Xd=Xd).
+------------------
+fof(fifth_proposition,conjecture,ff=ff).
+fof(fourth_proposition,axiom,![Xe]:Xe=Xe).
+fof(third_proposition,axiom,![Xc]:Xc=Xc).
+fof(second_proposition,axiom,![Xb]:Xb=Xb).
+fof(first_proposition,axiom,![Xa]:Xa=Xa).
\ No newline at end of file
diff --git a/test/golden/byRef/generating tasks.golden b/test/golden/byRef/generating tasks.golden
new file mode 100644
index 0000000..3187198
--- /dev/null
+++ b/test/golden/byRef/generating tasks.golden
@@ -0,0 +1,352 @@
+[ Task
+    { taskDirectness = Direct
+    , taskHypotheses = []
+    , taskConjectureLabel = Marker "first_proposition"
+    , taskConjecture = TermSymbol
+        ( SymbolPredicate
+            ( PredicateRelation
+                ( Symbol "=" )
+            )
+        )
+        [ TermVar
+            ( NamedVar "a" )
+        , TermVar
+            ( NamedVar "a" )
+        ]
+    }
+, Task
+    { taskDirectness = Direct
+    , taskHypotheses =
+        [
+            ( Marker "first_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ]
+    , taskConjectureLabel = Marker "second_proposition"
+    , taskConjecture = TermSymbol
+        ( SymbolPredicate
+            ( PredicateRelation
+                ( Symbol "=" )
+            )
+        )
+        [ TermVar
+            ( NamedVar "b" )
+        , TermVar
+            ( NamedVar "b" )
+        ]
+    }
+, Task
+    { taskDirectness = Direct
+    , taskHypotheses =
+        [
+            ( Marker "first_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ]
+    , taskConjectureLabel = Marker "third_proposition"
+    , taskConjecture = TermSymbol
+        ( SymbolPredicate
+            ( PredicateRelation
+                ( Symbol "=" )
+            )
+        )
+        [ TermVar
+            ( NamedVar "c" )
+        , TermVar
+            ( NamedVar "c" )
+        ]
+    }
+, Task
+    { taskDirectness = Direct
+    , taskHypotheses =
+        [
+            ( Marker "first_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ]
+    , taskConjectureLabel = Marker "fourth_proposition"
+    , taskConjecture = Quantified Universally
+        ( Scope
+            ( TermSymbol
+                ( SymbolPredicate
+                    ( PredicateRelation
+                        ( Symbol "=" )
+                    )
+                )
+                [ TermVar
+                    ( B
+                        ( NamedVar "d" )
+                    )
+                , TermVar
+                    ( B
+                        ( NamedVar "d" )
+                    )
+                ]
+            )
+        )
+    }
+, Task
+    { taskDirectness = Direct
+    , taskHypotheses =
+        [
+            ( Marker "third_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "c" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "c" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ,
+            ( Marker "second_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "b" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "b" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ,
+            ( Marker "first_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ,
+            ( Marker "fourth_proposition1"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "d" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "d" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ]
+    , taskConjectureLabel = Marker "fourth_proposition"
+    , taskConjecture = TermSymbol
+        ( SymbolPredicate
+            ( PredicateRelation
+                ( Symbol "=" )
+            )
+        )
+        [ TermVar
+            ( NamedVar "e" )
+        , TermVar
+            ( NamedVar "e" )
+        ]
+    }
+, Task
+    { taskDirectness = Direct
+    , taskHypotheses =
+        [
+            ( Marker "fourth_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "e" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "e" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ,
+            ( Marker "third_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "c" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "c" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ,
+            ( Marker "second_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "b" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "b" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ,
+            ( Marker "first_proposition"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "a" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ]
+    , taskConjectureLabel = Marker "fifth_proposition"
+    , taskConjecture = TermSymbol
+        ( SymbolPredicate
+            ( PredicateRelation
+                ( Symbol "=" )
+            )
+        )
+        [ TermVar
+            ( NamedVar "f" )
+        , TermVar
+            ( NamedVar "f" )
+        ]
+    }
+]
\ No newline at end of file
diff --git a/test/golden/byRef/glossing.golden b/test/golden/byRef/glossing.golden
new file mode 100644
index 0000000..e213bc9
--- /dev/null
+++ b/test/golden/byRef/glossing.golden
@@ -0,0 +1,155 @@
+[ BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 1
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "first_proposition" )
+    ( Lemma []
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Symbol "=" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "a" )
+            , TermVar
+                ( NamedVar "a" )
+            ]
+        )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 5
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "second_proposition" )
+    ( Lemma []
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Symbol "=" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "b" )
+            , TermVar
+                ( NamedVar "b" )
+            ]
+        )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 9
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "third_proposition" )
+    ( Lemma []
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Symbol "=" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "c" )
+            , TermVar
+                ( NamedVar "c" )
+            ]
+        )
+    )
+, BlockProof
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 12
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Qed
+        ( JustificationRef
+            ( Marker "first_proposition" :| [] )
+        )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 16
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "fourth_proposition" )
+    ( Lemma []
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Symbol "=" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "e" )
+            , TermVar
+                ( NamedVar "e" )
+            ]
+        )
+    )
+, BlockProof
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 19
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Have
+        ( Quantified Universally
+            ( Scope
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateRelation
+                            ( Symbol "=" )
+                        )
+                    )
+                    [ TermVar
+                        ( B
+                            ( NamedVar "d" )
+                        )
+                    , TermVar
+                        ( B
+                            ( NamedVar "d" )
+                        )
+                    ]
+                )
+            )
+        )
+        ( JustificationRef
+            ( Marker "first_proposition" :| [] )
+        ) ( Qed JustificationEmpty )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 23
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "fifth_proposition" )
+    ( Lemma []
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Symbol "=" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "f" )
+            , TermVar
+                ( NamedVar "f" )
+            ]
+        )
+    )
+]
\ No newline at end of file
diff --git a/test/golden/byRef/parsing.golden b/test/golden/byRef/parsing.golden
new file mode 100644
index 0000000..2cf91b6
--- /dev/null
+++ b/test/golden/byRef/parsing.golden
@@ -0,0 +1,168 @@
+[ BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 1
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "first_proposition" )
+    ( Lemma []
+        ( StmtFormula
+            ( FormulaChain
+                ( ChainBase
+                    ( ExprVar
+                        ( NamedVar "a" ) :| []
+                    ) Positive
+                    ( RelationSymbol
+                        ( Symbol "=" )
+                    )
+                    ( ExprVar
+                        ( NamedVar "a" ) :| []
+                    )
+                )
+            )
+        )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 5
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "second_proposition" )
+    ( Lemma []
+        ( StmtFormula
+            ( FormulaChain
+                ( ChainBase
+                    ( ExprVar
+                        ( NamedVar "b" ) :| []
+                    ) Positive
+                    ( RelationSymbol
+                        ( Symbol "=" )
+                    )
+                    ( ExprVar
+                        ( NamedVar "b" ) :| []
+                    )
+                )
+            )
+        )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 9
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "third_proposition" )
+    ( Lemma []
+        ( StmtFormula
+            ( FormulaChain
+                ( ChainBase
+                    ( ExprVar
+                        ( NamedVar "c" ) :| []
+                    ) Positive
+                    ( RelationSymbol
+                        ( Symbol "=" )
+                    )
+                    ( ExprVar
+                        ( NamedVar "c" ) :| []
+                    )
+                )
+            )
+        )
+    )
+, BlockProof
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 12
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Qed
+        ( JustificationRef
+            ( Marker "first_proposition" :| [] )
+        )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 16
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "fourth_proposition" )
+    ( Lemma []
+        ( StmtFormula
+            ( FormulaChain
+                ( ChainBase
+                    ( ExprVar
+                        ( NamedVar "e" ) :| []
+                    ) Positive
+                    ( RelationSymbol
+                        ( Symbol "=" )
+                    )
+                    ( ExprVar
+                        ( NamedVar "e" ) :| []
+                    )
+                )
+            )
+        )
+    )
+, BlockProof
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 19
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Have Nothing
+        ( SymbolicQuantified Universally
+            ( NamedVar "d" :| [] ) Unbounded Nothing
+            ( StmtFormula
+                ( FormulaChain
+                    ( ChainBase
+                        ( ExprVar
+                            ( NamedVar "d" ) :| []
+                        ) Positive
+                        ( RelationSymbol
+                            ( Symbol "=" )
+                        )
+                        ( ExprVar
+                            ( NamedVar "d" ) :| []
+                        )
+                    )
+                )
+            )
+        )
+        ( JustificationRef
+            ( Marker "first_proposition" :| [] )
+        ) ( Qed JustificationEmpty )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/byRef.tex"
+        , sourceLine = Pos 23
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "fifth_proposition" )
+    ( Lemma []
+        ( StmtFormula
+            ( FormulaChain
+                ( ChainBase
+                    ( ExprVar
+                        ( NamedVar "f" ) :| []
+                    ) Positive
+                    ( RelationSymbol
+                        ( Symbol "=" )
+                    )
+                    ( ExprVar
+                        ( NamedVar "f" ) :| []
+                    )
+                )
+            )
+        )
+    )
+]
\ No newline at end of file
diff --git a/test/golden/byRef/scanning.golden b/test/golden/byRef/scanning.golden
new file mode 100644
index 0000000..0637a08
--- /dev/null
+++ b/test/golden/byRef/scanning.golden
@@ -0,0 +1 @@
+[]
\ No newline at end of file
diff --git a/test/golden/byRef/tokenizing.golden b/test/golden/byRef/tokenizing.golden
new file mode 100644
index 0000000..2ae8ea6
--- /dev/null
+++ b/test/golden/byRef/tokenizing.golden
@@ -0,0 +1,71 @@
+[ BeginEnv "proposition"
+, Label "first_proposition"
+, BeginEnv "math"
+, Variable "a"
+, Symbol "="
+, Variable "a"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+, BeginEnv "proposition"
+, Label "second_proposition"
+, BeginEnv "math"
+, Variable "b"
+, Symbol "="
+, Variable "b"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+, BeginEnv "proposition"
+, Label "third_proposition"
+, BeginEnv "math"
+, Variable "c"
+, Symbol "="
+, Variable "c"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+, BeginEnv "proof"
+, Word "follows"
+, Word "by"
+, Ref
+    ( "first_proposition" :| [] )
+, Symbol "."
+, EndEnv "proof"
+, BeginEnv "proposition"
+, Label "fourth_proposition"
+, BeginEnv "math"
+, Variable "e"
+, Symbol "="
+, Variable "e"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+, BeginEnv "proof"
+, Word "for"
+, Word "all"
+, BeginEnv "math"
+, Variable "d"
+, EndEnv "math"
+, Word "we"
+, Word "have"
+, BeginEnv "math"
+, Variable "d"
+, Symbol "="
+, Variable "d"
+, EndEnv "math"
+, Word "by"
+, Ref
+    ( "first_proposition" :| [] )
+, Symbol "."
+, EndEnv "proof"
+, BeginEnv "proposition"
+, Label "fifth_proposition"
+, BeginEnv "math"
+, Variable "f"
+, Symbol "="
+, Variable "f"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+]
\ No newline at end of file
diff --git a/test/golden/byRef/verification.golden b/test/golden/byRef/verification.golden
new file mode 100644
index 0000000..69b9873
--- /dev/null
+++ b/test/golden/byRef/verification.golden
@@ -0,0 +1 @@
+VerificationSuccess
\ No newline at end of file