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/separation/encoding tasks.golden   |  1 +
 test/golden/separation/generating tasks.golden | 65 ++++++++++++++++++++++++++
 test/golden/separation/glossing.golden         | 40 ++++++++++++++++
 test/golden/separation/parsing.golden          | 44 +++++++++++++++++
 test/golden/separation/scanning.golden         |  1 +
 test/golden/separation/tokenizing.golden       | 18 +++++++
 test/golden/separation/verification.golden     |  1 +
 7 files changed, 170 insertions(+)
 create mode 100644 test/golden/separation/encoding tasks.golden
 create mode 100644 test/golden/separation/generating tasks.golden
 create mode 100644 test/golden/separation/glossing.golden
 create mode 100644 test/golden/separation/parsing.golden
 create mode 100644 test/golden/separation/scanning.golden
 create mode 100644 test/golden/separation/tokenizing.golden
 create mode 100644 test/golden/separation/verification.golden

(limited to 'test/golden/separation')

diff --git a/test/golden/separation/encoding tasks.golden b/test/golden/separation/encoding tasks.golden
new file mode 100644
index 0000000..5d0994b
--- /dev/null
+++ b/test/golden/separation/encoding tasks.golden	
@@ -0,0 +1 @@
+fof(sep_test,conjecture,![Xx]:(elem(Xx,fX)<=>(elem(Xx,fX)&Xx=Xx))).
\ No newline at end of file
diff --git a/test/golden/separation/generating tasks.golden b/test/golden/separation/generating tasks.golden
new file mode 100644
index 0000000..889906b
--- /dev/null
+++ b/test/golden/separation/generating tasks.golden	
@@ -0,0 +1,65 @@
+[ Task
+    { taskDirectness = Direct
+    , taskHypotheses = []
+    , taskConjectureLabel = Marker "sep_test"
+    , taskConjecture = Quantified Universally
+        ( Scope
+            ( Connected Equivalence
+                ( TermSymbol
+                    ( SymbolPredicate
+                        ( PredicateRelation
+                            ( Command "in" )
+                        )
+                    )
+                    [ TermVar
+                        ( B
+                            ( NamedVar "x" )
+                        )
+                    , TermVar
+                        ( F
+                            ( TermVar
+                                ( NamedVar "X" )
+                            )
+                        )
+                    ]
+                )
+                ( Connected Conjunction
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Command "in" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "x" )
+                            )
+                        , TermVar
+                            ( F
+                                ( TermVar
+                                    ( NamedVar "X" )
+                                )
+                            )
+                        ]
+                    )
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B
+                                ( NamedVar "x" )
+                            )
+                        , TermVar
+                            ( B
+                                ( NamedVar "x" )
+                            )
+                        ]
+                    )
+                )
+            )
+        )
+    }
+]
\ No newline at end of file
diff --git a/test/golden/separation/glossing.golden b/test/golden/separation/glossing.golden
new file mode 100644
index 0000000..47d574b
--- /dev/null
+++ b/test/golden/separation/glossing.golden
@@ -0,0 +1,40 @@
+[ BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/separation.tex"
+        , sourceLine = Pos 1
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "sep_test" )
+    ( Lemma []
+        ( TermSymbol
+            ( SymbolPredicate
+                ( PredicateRelation
+                    ( Symbol "=" )
+                )
+            )
+            [ TermVar
+                ( NamedVar "X" )
+            , TermSep
+                ( NamedVar "x" )
+                ( TermVar
+                    ( NamedVar "X" )
+                )
+                ( Scope
+                    ( TermSymbol
+                        ( SymbolPredicate
+                            ( PredicateRelation
+                                ( Symbol "=" )
+                            )
+                        )
+                        [ TermVar
+                            ( B () )
+                        , TermVar
+                            ( B () )
+                        ]
+                    )
+                )
+            ]
+        )
+    )
+]
\ No newline at end of file
diff --git a/test/golden/separation/parsing.golden b/test/golden/separation/parsing.golden
new file mode 100644
index 0000000..2a2110f
--- /dev/null
+++ b/test/golden/separation/parsing.golden
@@ -0,0 +1,44 @@
+[ BlockLemma
+    ( SourcePos
+        { sourceName = "test/examples/separation.tex"
+        , sourceLine = Pos 1
+        , sourceColumn = Pos 1
+        }
+    )
+    ( Marker "sep_test" )
+    ( Lemma []
+        ( StmtFormula
+            ( FormulaChain
+                ( ChainBase
+                    ( ExprVar
+                        ( NamedVar "X" ) :| []
+                    ) Positive
+                    ( RelationSymbol
+                        ( Symbol "=" )
+                    )
+                    ( ExprSep
+                        ( NamedVar "x" )
+                        ( ExprVar
+                            ( NamedVar "X" )
+                        )
+                        ( StmtFormula
+                            ( FormulaChain
+                                ( ChainBase
+                                    ( ExprVar
+                                        ( NamedVar "x" ) :| []
+                                    ) Positive
+                                    ( RelationSymbol
+                                        ( Symbol "=" )
+                                    )
+                                    ( ExprVar
+                                        ( NamedVar "x" ) :| []
+                                    )
+                                )
+                            )
+                        ) :| []
+                    )
+                )
+            )
+        )
+    )
+]
\ No newline at end of file
diff --git a/test/golden/separation/scanning.golden b/test/golden/separation/scanning.golden
new file mode 100644
index 0000000..0637a08
--- /dev/null
+++ b/test/golden/separation/scanning.golden
@@ -0,0 +1 @@
+[]
\ No newline at end of file
diff --git a/test/golden/separation/tokenizing.golden b/test/golden/separation/tokenizing.golden
new file mode 100644
index 0000000..40b30d8
--- /dev/null
+++ b/test/golden/separation/tokenizing.golden
@@ -0,0 +1,18 @@
+[ BeginEnv "proposition"
+, Label "sep_test"
+, BeginEnv "math"
+, Variable "X"
+, Symbol "="
+, VisibleBraceL
+, Variable "x"
+, Command "in"
+, Variable "X"
+, Command "mid"
+, Variable "x"
+, Symbol "="
+, Variable "x"
+, VisibleBraceR
+, EndEnv "math"
+, Symbol "."
+, EndEnv "proposition"
+]
\ No newline at end of file
diff --git a/test/golden/separation/verification.golden b/test/golden/separation/verification.golden
new file mode 100644
index 0000000..69b9873
--- /dev/null
+++ b/test/golden/separation/verification.golden
@@ -0,0 +1 @@
+VerificationSuccess
\ No newline at end of file
-- 
cgit v1.2.3