From 3f97a7684a3b4d54013b2fa571e9634522ffa39e Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@gmail.com>
Date: Fri, 10 Nov 2023 16:37:29 +0100
Subject: [PATCH 1/2] Fix the bug that "g" was not parsed as an Atom

---
 src/parsing/fol/grammar.pest | 2 +-
 src/parsing/fol/pest.rs      | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/parsing/fol/grammar.pest b/src/parsing/fol/grammar.pest
index 6e6f34d1..883e4fb0 100644
--- a/src/parsing/fol/grammar.pest
+++ b/src/parsing/fol/grammar.pest
@@ -8,7 +8,7 @@
 
 WHITESPACE = _{ " " | NEWLINE }
 
-keyword = _{ primitive | binary_connective | unary_connective | quantifier | sort }
+keyword = _{ primitive | binary_connective | unary_connective | quantifier }
 
     primitive = _{ infimum | supremum }
         infimum  = { "#inf" }
diff --git a/src/parsing/fol/pest.rs b/src/parsing/fol/pest.rs
index 6f277694..4419f07e 100644
--- a/src/parsing/fol/pest.rs
+++ b/src/parsing/fol/pest.rs
@@ -756,6 +756,14 @@ mod tests {
                         terms: vec![],
                     },
                 ),
+                (
+                    // Parsing "g" caused issues ealier because "g" is also a sort declaration.
+                    "g",
+                    Atom {
+                        predicate: "g".into(),
+                        terms: vec![],
+                    },
+                ),
                 (
                     "p()",
                     Atom {

From 67c78318096cae48273db3d1151d435f185c31b4 Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@gmail.com>
Date: Fri, 10 Nov 2023 17:19:48 +0100
Subject: [PATCH 2/2] Ignore whitespace at the end of programs or theories...

... and accept empty theories
---
 src/parsing/asp/grammar.pest |  3 ++-
 src/parsing/asp/pest.rs      | 12 ++++++++++++
 src/parsing/fol/grammar.pest |  3 ++-
 src/parsing/fol/pest.rs      | 20 +++++++++++++++++---
 4 files changed, 33 insertions(+), 5 deletions(-)

diff --git a/src/parsing/asp/grammar.pest b/src/parsing/asp/grammar.pest
index cf266244..b347088c 100644
--- a/src/parsing/asp/grammar.pest
+++ b/src/parsing/asp/grammar.pest
@@ -51,4 +51,5 @@ body = { (atomic_formula ~ (("," | ";") ~ atomic_formula)*)? }
 
 rule = { (!"." ~ head ~ (":-" ~ body)?) ~ "." }
 
-program = { rule* }
+// TODO: Think about a proper way to handle the whitespace at the end of programs
+program = { rule* ~ WHITESPACE* }
diff --git a/src/parsing/asp/pest.rs b/src/parsing/asp/pest.rs
index 5516f7ad..85614444 100644
--- a/src/parsing/asp/pest.rs
+++ b/src/parsing/asp/pest.rs
@@ -1026,6 +1026,18 @@ mod tests {
                     ],
                 },
             ),
+            (
+                "a.\n",
+                Program {
+                    rules: vec![Rule {
+                        head: Head::Basic(Atom {
+                            predicate: "a".into(),
+                            terms: vec![],
+                        }),
+                        body: Body { formulas: vec![] },
+                    }],
+                },
+            ),
         ]);
     }
 }
diff --git a/src/parsing/fol/grammar.pest b/src/parsing/fol/grammar.pest
index 883e4fb0..0b54794a 100644
--- a/src/parsing/fol/grammar.pest
+++ b/src/parsing/fol/grammar.pest
@@ -79,4 +79,5 @@ formula = { prefix* ~ primary ~ (infix ~ prefix* ~ primary)* }
     infix   = _{ binary_connective }
     primary = _{ "(" ~ formula ~ ")" | atomic_formula }
 
-theory = { (formula ~ ".")+ }
+// TODO: Think about a proper way to handle the whitespace at the end of programs
+theory = { (formula ~ ".")* ~ WHITESPACE* }
diff --git a/src/parsing/fol/pest.rs b/src/parsing/fol/pest.rs
index 4419f07e..4b5514f2 100644
--- a/src/parsing/fol/pest.rs
+++ b/src/parsing/fol/pest.rs
@@ -480,14 +480,14 @@ mod tests {
             AtomParser, AtomicFormulaParser, BasicIntegerTermParser, BinaryConnectiveParser,
             BinaryOperatorParser, ComparisonParser, FormulaParser, GeneralTermParser, GuardParser,
             IntegerTermParser, QuantificationParser, QuantifierParser, RelationParser,
-            UnaryConnectiveParser, UnaryOperatorParser, VariableParser,
+            TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, VariableParser,
         },
         crate::{
             parsing::TestedParser,
             syntax_tree::fol::{
                 Atom, AtomicFormula, BasicIntegerTerm, BinaryConnective, BinaryOperator,
                 Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier,
-                Relation, Sort, UnaryConnective, UnaryOperator, Variable,
+                Relation, Sort, Theory, UnaryConnective, UnaryOperator, Variable,
             },
         },
     };
@@ -1147,7 +1147,21 @@ mod tests {
                 },
             ),
         ]);
+    }
 
-        // TODO Add more tests
+    #[test]
+    fn parse_theory() {
+        TheoryParser.should_parse_into([
+            ("", Theory { formulas: vec![] }),
+            (
+                "a.\n",
+                Theory {
+                    formulas: vec![Formula::AtomicFormula(AtomicFormula::Atom(Atom {
+                        predicate: "a".into(),
+                        terms: vec![],
+                    }))],
+                },
+            ),
+        ]);
     }
 }