Initial commit

7 files changed, 813 insertions, 0 deletions

diff --git a/test/golden/proofdefinefunction/encoding tasks.golden b/test/golden/proofdefinefunction/encoding tasks.golden
new file mode 100644
index 0000000..36c916f
--- /dev/null
+++ b/test/golden/proofdefinefunction/encoding tasks.golden
@@ -0,0 +1,9 @@
+fof(definefunctiontest,conjecture,elem(fx,fy)=>elem(fx,fy)).
+fof(relation,axiom,![Xf]:(relation(Xf)<=>Xf=Xf)).
+fof(rightunique,axiom,![Xf]:(rightunique(Xf)<=>Xf=Xf)).
+fof(dom,axiom,![Xf]:dom(Xf)=Xf).
+fof(apply,axiom,![Xf,Xx]:apply(Xf,Xx)=Xx).
+fof(definefunctiontest1,axiom,relation(ff)).
+fof(definefunctiontest2,axiom,rightunique(ff)).
+fof(definefunctiontest3,axiom,![Xz]:(elem(Xz,fx)=>apply(ff,Xz)=Xz)).
+fof(definefunctiontest4,axiom,dom(ff)=fx).
\ No newline at end of file
diff --git a/test/golden/proofdefinefunction/generating tasks.golden b/test/golden/proofdefinefunction/generating tasks.golden
new file mode 100644
index 0000000..3ab9857
--- /dev/null
+++ b/test/golden/proofdefinefunction/generating tasks.golden
@@ -0,0 +1,332 @@
+[ Task
+    { taskDirectness = Direct
+    , taskHypotheses =
+        [
+            ( Marker "relation"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Equivalence
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateNoun
+                                    ( SgPl
+                                        { sg =
+                                            [ Just
+                                                ( Word "relation" )
+                                            ]
+                                        , pl =
+                                            [ Just
+                                                ( Word "relations" )
+                                            ]
+                                        }
+                                    )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "f" )
+                                )
+                            ]
+                        )
+                        ( Quantified Universally
+                            ( Scope
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateRelation
+                                            ( Symbol "=" )
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "f" )
+                                                )
+                                            )
+                                        )
+                                    , TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "f" )
+                                                )
+                                            )
+                                        )
+                                    ]
+                                )
+                            )
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "rightunique"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Equivalence
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateAdj
+                                    [ Just
+                                        ( Word "right-unique" )
+                                    ]
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "f" )
+                                )
+                            ]
+                        )
+                        ( Quantified Universally
+                            ( Scope
+                                ( TermSymbol
+                                    ( SymbolPredicate
+                                        ( PredicateRelation
+                                            ( Symbol "=" )
+                                        )
+                                    )
+                                    [ TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "f" )
+                                                )
+                                            )
+                                        )
+                                    , TermVar
+                                        ( F
+                                            ( TermVar
+                                                ( B
+                                                    ( NamedVar "f" )
+                                                )
+                                            )
+                                        )
+                                    ]
+                                )
+                            )
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "dom"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermSymbol
+                            ( SymbolMixfix
+                                [ Just
+                                    ( Command "dom" )
+                                , Just InvisibleBraceL
+                                , Nothing
+                                , Just InvisibleBraceR
+                                ]
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "f" )
+                                )
+                            ]
+                        , TermVar
+                            ( B
+                                ( NamedVar "f" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ,
+            ( Marker "apply"
+            , Quantified Universally
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermSymbol
+                            ( SymbolMixfix
+                                [ Just
+                                    ( Command "apply" )
+                                , Just InvisibleBraceL
+                                , Nothing
+                                , Just InvisibleBraceR
+                                , Just InvisibleBraceL
+                                , Nothing
+                                , Just InvisibleBraceR
+                                ]
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "f" )
+                                )
+                            , TermVar
+                                ( B
+                                    ( NamedVar "x" )
+                                )
+                            ]
+                        , TermVar
+                            ( B
+                                ( NamedVar "x" )
+                            )
+                        ]
+                    )
+                )
+            )
+        ,
+            ( Marker "definefunctiontest1"
+            , TermSymbol
+                ( SymbolPredicate
+                    ( PredicateNoun
+                        ( SgPl
+                            { sg =
+                                [ Just
+                                    ( Word "relation" )
+                                ]
+                            , pl =
+                                [ Just
+                                    ( Word "relations" )
+                                ]
+                            }
+                        )
+                    )
+                )
+                [ TermVar
+                    ( NamedVar "f" )
+                ]
+            )
+        ,
+            ( Marker "definefunctiontest2"
+            , TermSymbol
+                ( SymbolPredicate
+                    ( PredicateAdj
+                        [ Just
+                            ( Word "right-unique" )
+                        ]
+                    )
+                )
+                [ TermVar
+                    ( NamedVar "f" )
+                ]
+            )
+        ,
+            ( Marker "definefunctiontest3"
+            , Quantified Universally
+                ( Scope
+                    ( Connected Implication
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateRelation
+                                    ( Command "in" )
+                                )
+                            )
+                            [ TermVar
+                                ( B
+                                    ( NamedVar "z" )
+                                )
+                            , TermVar
+                                ( F
+                                    ( TermVar
+                                        ( NamedVar "x" )
+                                    )
+                                )
+                            ]
+                        )
+                        ( TermSymbol
+                            ( SymbolPredicate
+                                ( PredicateRelation
+                                    ( Symbol "=" )
+                                )
+                            )
+                            [ TermSymbol
+                                ( SymbolMixfix
+                                    [ Just
+                                        ( Command "apply" )
+                                    , Just InvisibleBraceL
+                                    , Nothing
+                                    , Just InvisibleBraceR
+                                    , Just InvisibleBraceL
+                                    , Nothing
+                                    , Just InvisibleBraceR
+                                    ]
+                                )
+                                [ TermVar
+                                    ( F
+                                        ( TermVar
+                                            ( NamedVar "f" )
+                                        )
+                                    )
+                                , TermVar
+                                    ( B
+                                        ( NamedVar "z" )
+                                    )
+                                ]
+                            , TermVar
+                                ( B
+                                    ( NamedVar "z" )
+                                )
+                            ]
+                        )
+                    )
+                )
+            )
+        ,
+            ( Marker "definefunctiontest4"
+            , TermSymbol
+                ( SymbolPredicate
+                    ( PredicateRelation
+                        ( Symbol "=" )
+                    )
+                )
+                [ TermSymbol
+                    ( SymbolMixfix
+                        [ Just
+                            ( Command "dom" )
+                        , Just InvisibleBraceL
+                        , Nothing
+                        , Just InvisibleBraceR
+                        ]
+                    )
+                    [ TermVar
+                        ( NamedVar "f" )
+                    ]
+                , TermVar
+                    ( NamedVar "x" )
+                ]
+            )
+        ]
+    , taskConjectureLabel = Marker "definefunctiontest"
+    , taskConjecture = Connected Implication
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Command "in" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "x" )
+            , TermVar
+                ( NamedVar "y" )
+            ]
+        )
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Command "in" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "x" )
+            , TermVar
+                ( NamedVar "y" )
+            ]
+        )
+    }
+]
\ No newline at end of file
diff --git a/test/golden/proofdefinefunction/glossing.golden b/test/golden/proofdefinefunction/glossing.golden
new file mode 100644
index 0000000..931e5da
--- /dev/null
+++ b/test/golden/proofdefinefunction/glossing.golden
@@ -0,0 +1,163 @@
+[ BlockDefn
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 3
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "apply" )
+    ( DefnOp
+        [ Just
+            ( Command "apply" )
+        , Just InvisibleBraceL
+        , Nothing
+        , Just InvisibleBraceR
+        , Just InvisibleBraceL
+        , Nothing
+        , Just InvisibleBraceR
+        ]
+        [ NamedVar "f"
+        , NamedVar "x"
+        ]
+        ( TermVar
+            ( NamedVar "x" )
+        )
+    )
+, BlockDefn
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 8
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "dom" )
+    ( DefnOp
+        [ Just
+            ( Command "dom" )
+        , Just InvisibleBraceL
+        , Nothing
+        , Just InvisibleBraceR
+        ]
+        [ NamedVar "f" ]
+        ( TermVar
+            ( NamedVar "f" )
+        )
+    )
+, BlockDefn
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 13
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "rightunique" )
+    ( DefnPredicate []
+        ( PredicateAdj
+            [ Just
+                ( Word "right-unique" )
+            ]
+        )
+        ( NamedVar "f" :| [] )
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Symbol "=" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "f" )
+            , TermVar
+                ( NamedVar "f" )
+            ]
+        )
+    )
+, BlockDefn
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 18
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "relation" )
+    ( DefnPredicate []
+        ( PredicateNoun
+            ( SgPl
+                { sg =
+                    [ Just
+                        ( Word "relation" )
+                    ]
+                , pl =
+                    [ Just
+                        ( Word "relations" )
+                    ]
+                }
+            )
+        )
+        ( NamedVar "f" :| [] )
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Symbol "=" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "f" )
+            , TermVar
+                ( NamedVar "f" )
+            ]
+        )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 22
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "definefunctiontest" )
+    ( Lemma []
+        ( Connected Implication
+            ( TermSymbol
+                ( SymbolPredicate
+                    ( PredicateRelation
+                        ( Command "in" )
+                    )
+                )
+                [ TermVar
+                    ( NamedVar "x" )
+                , TermVar
+                    ( NamedVar "y" )
+                ]
+            )
+            ( TermSymbol
+                ( SymbolPredicate
+                    ( PredicateRelation
+                        ( Command "in" )
+                    )
+                )
+                [ TermVar
+                    ( NamedVar "x" )
+                , TermVar
+                    ( NamedVar "y" )
+                ]
+            )
+        )
+    )
+, BlockProof
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 25
+        , sourceColumn = Pos 1
+        }
+    )
+    ( DefineFunction
+        ( NamedVar "f" )
+        ( NamedVar "z" )
+        ( TermVar
+            ( NamedVar "z" )
+        )
+        ( TermVar
+            ( NamedVar "x" )
+        ) ( Qed JustificationEmpty )
+    )
+]
\ No newline at end of file
diff --git a/test/golden/proofdefinefunction/parsing.golden b/test/golden/proofdefinefunction/parsing.golden
new file mode 100644
index 0000000..eba14ec
--- /dev/null
+++ b/test/golden/proofdefinefunction/parsing.golden
@@ -0,0 +1,184 @@
+[ BlockDefn
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 3
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "apply" )
+    ( DefnOp
+        ( SymbolPattern
+            [ Just
+                ( Command "apply" )
+            , Just InvisibleBraceL
+            , Nothing
+            , Just InvisibleBraceR
+            , Just InvisibleBraceL
+            , Nothing
+            , Just InvisibleBraceR
+            ]
+            [ NamedVar "f"
+            , NamedVar "x"
+            ]
+        )
+        ( ExprVar
+            ( NamedVar "x" )
+        )
+    )
+, BlockDefn
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 8
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "dom" )
+    ( DefnOp
+        ( SymbolPattern
+            [ Just
+                ( Command "dom" )
+            , Just InvisibleBraceL
+            , Nothing
+            , Just InvisibleBraceR
+            ]
+            [ NamedVar "f" ]
+        )
+        ( ExprVar
+            ( NamedVar "f" )
+        )
+    )
+, BlockDefn
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 13
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "rightunique" )
+    ( Defn []
+        ( DefnAdj Nothing
+            ( NamedVar "f" )
+            ( Adj
+                [ Just
+                    ( Word "right-unique" )
+                ] []
+            )
+        )
+        ( StmtFormula
+            ( FormulaChain
+                ( ChainBase
+                    ( ExprVar
+                        ( NamedVar "f" ) :| []
+                    ) Positive
+                    ( RelationSymbol
+                        ( Symbol "=" )
+                    )
+                    ( ExprVar
+                        ( NamedVar "f" ) :| []
+                    )
+                )
+            )
+        )
+    )
+, BlockDefn
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 18
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "relation" )
+    ( Defn []
+        ( DefnNoun
+            ( NamedVar "f" )
+            ( Noun
+                ( SgPl
+                    { sg =
+                        [ Just
+                            ( Word "relation" )
+                        ]
+                    , pl =
+                        [ Just
+                            ( Word "relations" )
+                        ]
+                    }
+                ) []
+            )
+        )
+        ( StmtFormula
+            ( FormulaChain
+                ( ChainBase
+                    ( ExprVar
+                        ( NamedVar "f" ) :| []
+                    ) Positive
+                    ( RelationSymbol
+                        ( Symbol "=" )
+                    )
+                    ( ExprVar
+                        ( NamedVar "f" ) :| []
+                    )
+                )
+            )
+        )
+    )
+, BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 22
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "definefunctiontest" )
+    ( Lemma []
+        ( StmtConnected Implication
+            ( StmtFormula
+                ( FormulaChain
+                    ( ChainBase
+                        ( ExprVar
+                            ( NamedVar "x" ) :| []
+                        ) Positive
+                        ( RelationSymbol
+                            ( Command "in" )
+                        )
+                        ( ExprVar
+                            ( NamedVar "y" ) :| []
+                        )
+                    )
+                )
+            )
+            ( StmtFormula
+                ( FormulaChain
+                    ( ChainBase
+                        ( ExprVar
+                            ( NamedVar "x" ) :| []
+                        ) Positive
+                        ( RelationSymbol
+                            ( Command "in" )
+                        )
+                        ( ExprVar
+                            ( NamedVar "y" ) :| []
+                        )
+                    )
+                )
+            )
+        )
+    )
+, BlockProof
+    ( SourcePos
+        { sourceName = "test/examples/proofdefinefunction.tex"
+        , sourceLine = Pos 25
+        , sourceColumn = Pos 1
+        }
+    )
+    ( DefineFunction
+        ( NamedVar "f" )
+        ( NamedVar "z" )
+        ( ExprVar
+            ( NamedVar "z" )
+        )
+        ( NamedVar "z" )
+        ( ExprVar
+            ( NamedVar "x" )
+        ) ( Qed JustificationEmpty )
+    )
+]
\ No newline at end of file
diff --git a/test/golden/proofdefinefunction/scanning.golden b/test/golden/proofdefinefunction/scanning.golden
new file mode 100644
index 0000000..e5d7748
--- /dev/null
+++ b/test/golden/proofdefinefunction/scanning.golden
@@ -0,0 +1,30 @@
+[ ScanFunctionSymbol
+    [ Just
+        ( Command "apply" )
+    , Just InvisibleBraceL
+    , Nothing
+    , Just InvisibleBraceR
+    , Just InvisibleBraceL
+    , Nothing
+    , Just InvisibleBraceR
+    ]
+    ( Marker "apply" )
+, ScanFunctionSymbol
+    [ Just
+        ( Command "dom" )
+    , Just InvisibleBraceL
+    , Nothing
+    , Just InvisibleBraceR
+    ]
+    ( Marker "dom" )
+, ScanAdj
+    [ Just
+        ( Word "right-unique" )
+    ]
+    ( Marker "rightunique" )
+, ScanNoun
+    [ Just
+        ( Word "relation" )
+    ]
+    ( Marker "relation" )
+]
\ No newline at end of file
diff --git a/test/golden/proofdefinefunction/tokenizing.golden b/test/golden/proofdefinefunction/tokenizing.golden
new file mode 100644
index 0000000..542a89c
--- /dev/null
+++ b/test/golden/proofdefinefunction/tokenizing.golden
@@ -0,0 +1,94 @@
+[ BeginEnv "definition"
+, Label "apply"
+, BeginEnv "math"
+, Command "apply"
+, InvisibleBraceL
+, Variable "f"
+, InvisibleBraceR
+, InvisibleBraceL
+, Variable "x"
+, InvisibleBraceR
+, Symbol "="
+, Variable "x"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "definition"
+, BeginEnv "definition"
+, Label "dom"
+, BeginEnv "math"
+, Command "dom"
+, InvisibleBraceL
+, Variable "f"
+, InvisibleBraceR
+, Symbol "="
+, Variable "f"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "definition"
+, BeginEnv "definition"
+, Label "rightunique"
+, BeginEnv "math"
+, Variable "f"
+, EndEnv "math"
+, Word "is"
+, Word "right-unique"
+, Word "iff"
+, BeginEnv "math"
+, Variable "f"
+, Symbol "="
+, Variable "f"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "definition"
+, BeginEnv "definition"
+, Label "relation"
+, BeginEnv "math"
+, Variable "f"
+, EndEnv "math"
+, Word "is"
+, Word "a"
+, Word "relation"
+, Word "iff"
+, BeginEnv "math"
+, Variable "f"
+, Symbol "="
+, Variable "f"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "definition"
+, BeginEnv "proposition"
+, Label "definefunctiontest"
+, Word "if"
+, BeginEnv "math"
+, Variable "x"
+, Command "in"
+, Variable "y"
+, EndEnv "math"
+, Symbol ","
+, Word "then"
+, BeginEnv "math"
+, Variable "x"
+, Command "in"
+, Variable "y"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+, BeginEnv "proof"
+, Word "let"
+, BeginEnv "math"
+, Variable "f"
+, ParenL
+, Variable "z"
+, ParenR
+, Symbol "="
+, Variable "z"
+, EndEnv "math"
+, Word "for"
+, BeginEnv "math"
+, Variable "z"
+, Command "in"
+, Variable "x"
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proof"
+]
\ No newline at end of file
diff --git a/test/golden/proofdefinefunction/verification.golden b/test/golden/proofdefinefunction/verification.golden
new file mode 100644
index 0000000..69b9873
--- /dev/null
+++ b/test/golden/proofdefinefunction/verification.golden
@@ -0,0 +1 @@
+VerificationSuccess
\ No newline at end of file