diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Antlr.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Antlr.cs
index 9e20fcc8360f5867cc040b565499a16fccbad751..3196f25b36066102f158700ce357222ce018a8b6 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Antlr.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Antlr.cs
@@ -9,18 +9,26 @@ namespace Eingabeverwaltung.Parser
{
public static ADT parse(string ADT_input)
{
- Container container = new Container();
-
+ // Building Architecture for Syntax analysis
ICharStream chars = new AntlrInputStream(ADT_input);
ITokenSource lexer = new ADTLexer(chars);
ITokenStream tokens = new CommonTokenStream(lexer);
ADTParser parser = new ADTParser(tokens);
- parser.BuildParseTree = true;
+ // Properties for Syntax analysis
+ parser.BuildParseTree = true;
+ parser.RemoveErrorListeners();
+ ErrorListener errorListener = new ErrorListener();
+ parser.AddErrorListener(errorListener);
+ // Syntax analysis
ADTParser.AdtContext tree = parser.adt();
- Listener_Helper LH = new Listener_Helper();
- IADTListener adt_Listener = new ADT_Listener(container,LH);
+ if (parser.NumberOfSyntaxErrors > 0) errorListener.throwErrors();
+
+ // Semantic analysis
+ Container container = new Container();
+ Listener_Helper LH = new Listener_Helper();
+ IADTListener adt_Listener = new ADT_Listener(container,LH);
ParseTreeWalker.Default.Walk(adt_Listener, tree);
LH.close();
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ErrorListener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ErrorListener.cs
new file mode 100644
index 0000000000000000000000000000000000000000..b7e7b610b29c431a54576244b5fc6182588f094f
--- /dev/null
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ErrorListener.cs
@@ -0,0 +1,24 @@
+using Antlr4.Runtime;
+using System.Collections.Generic;
+using System.IO;
+
+namespace Eingabeverwaltung.Parser
+{
+ class ErrorListener : IAntlrErrorListener<IToken>
+ {
+ public readonly List<KontextException> errors;
+
+ public ErrorListener() => errors = new List<KontextException>();
+
+ public void SyntaxError(TextWriter output, IRecognizer recognizer, IToken offendingSymbol, int line, int charPositionInLine, string msg, RecognitionException e)
+ => errors.Add(new KontextException(new Coords(line, charPositionInLine), msg));
+
+ public void throwErrors()
+ {
+ string errorMessage = "";
+ foreach (var error in errors)
+ errorMessage += error.Message+"\r\n";
+ throw new System.Exception(errorMessage);
+ }
+ }
+}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Antlr.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Antlr.cs
index 663393fe60a76dd7bcc3ffd276d67a18a3769623..b73be01205f2acc4a97447179b7a668201602cdb 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Antlr.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Antlr.cs
@@ -15,23 +15,31 @@ namespace Eingabeverwaltung.Parser
/// <returns></returns>
public static void parse(string Proof_input, Container container)
{
+ // Building Architecture for Syntax analysis
ICharStream chars = new AntlrInputStream(Proof_input);
ITokenSource lexer = new ProofLexer(chars);
ITokenStream tokens = new CommonTokenStream(lexer);
ProofParser parser = new ProofParser(tokens);
+ // Properties for Syntax analysis
parser.BuildParseTree = true;
+ parser.RemoveErrorListeners();
+ ErrorListener errorListener = new ErrorListener();
+ parser.AddErrorListener(errorListener);
+ // Syntax analysis
ProofParser.ProofContext tree = parser.proof();
+ if (parser.NumberOfSyntaxErrors > 0) errorListener.throwErrors();
+ // Semantic analysis
Listener_Helper LH = new Listener_Helper(container.ADT.sorts, container.ADT.operations, container.ADT.axioms);
// create Proof without TransformationSteps
IProofListener PL = new Proof_Listener(container,LH);
ParseTreeWalker.Default.Walk(PL, tree);
- // walk again and create all TransformationSteps: Now cycles are no Problem anymore.
- IProofListener TL = new TransformationStep_Listener(container,LH);
+ // walk again and create all TransformationSteps: Now cycles are no Problem anymore.
+ IProofListener TL = new TransformationStep_Listener(container,LH);
ParseTreeWalker.Default.Walk(TL, tree);
- LH.close();
+ LH.close();
}
}
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Antlr.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Antlr.cs
index 630e9c63ef611ae6fb3bbabbd71267441e61e744..e6547a17b00a0c6ddb05ff6241b0b20026233355 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Antlr.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Antlr.cs
@@ -15,15 +15,24 @@ namespace Eingabeverwaltung.Parser
/// <returns></returns>
public static void parse(string Task_input, Container container)
{
- ICharStream chars = new AntlrInputStream(Task_input);
+ // Building Architecture for Syntax analysis
+ ICharStream chars = new AntlrInputStream(Task_input);
ITokenSource lexer = new TaskLexer(chars);
ITokenStream tokens = new CommonTokenStream(lexer);
TaskParser parser = new TaskParser(tokens);
- parser.BuildParseTree = true;
+ // Properties for Syntax analysis
+ parser.BuildParseTree = true;
+ parser.RemoveErrorListeners();
+ ErrorListener errorListener = new ErrorListener();
+ parser.AddErrorListener(errorListener);
- Listener_Helper LH = new Listener_Helper(container.ADT.sorts, container.ADT.operations, container.ADT.axioms);
+ // Syntax analysis
TaskParser.TaskContext tree = parser.task();
+ if (parser.NumberOfSyntaxErrors > 0) errorListener.throwErrors();
+
+ // Semantic analysis
+ Listener_Helper LH = new Listener_Helper(container.ADT.sorts, container.ADT.operations, container.ADT.axioms);
ITaskListener adt_Listener = new Task_Listener(container,LH);
ParseTreeWalker.Default.Walk(adt_Listener, tree);
LH.close();
diff --git a/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs b/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs
index 11c688d356280c6245ccb58e0c892b254e3f5c09..724b44fd3acf006a39887893070fbeb1853d2806 100644
--- a/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs
+++ b/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs
@@ -70,10 +70,9 @@ namespace Testverwaltung
for (int i = 0; i < taskFileNames.Count; i++)
ExceptionTesting("Task", path + taskFileNames[i] + ".task", taskShallValues[i]);
// Test Proof
- List<string> proofFileNames = new List<string>() { "axiom", "direction", "indvar1", "indvar2" }; // wierd grammar errors:, "resulttree", "starttree", "substitution", "termpart", "transformation" };
+ List<string> proofFileNames = new List<string>() { "axiom", "indvar1", "indvar2" };
List<string> proofShallValues = new List<string>() {
"Errors:\r\nError in 4:5: The rule bla0 is not defined!\r\n",
- "Errors:\r\nError in 4:9: The Direction of the TransformationStep is undefined! Expected 'rl' or 'lr' but found \"leftright\".\r\n",
"Errors:\r\nError in 3:0: Induction variable of proof L1 is neither definied in proof nor in task!\r\nError in 16:0: Induction variable of proof L2 is neither definied in proof nor in task!\r\nError in 33:0: Induction variable of proof main proof is neither definied in proof nor in task!\r\n",
"Errors:\r\nError in 16:64: Could not find Induction variable x in current context of variables.\r\nError in 16:64: Induction variable of proof L2 is neither definied in proof nor in task!\r\n",
};
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof
deleted file mode 100644
index 368403c0be2117111761fddd726db482b99b5f4a..0000000000000000000000000000000000000000
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof
+++ /dev/null
@@ -1,46 +0,0 @@
-lemma L1: forall y:Nat : plus(null,y) = y induction y
-IA: zu zeigen: plus(null,null) = null
-plus(null,null)
- {p0, leftright, plus(null,null), [null/n]} // unknown direction
-= null
-IH: fixed y:Nat : plus(null,y) = y
-IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
-plus(null,inc(y))
- {p1, lr, plus(null,inc(y)), [null/n,y/m]}
-= inc(plus(null,y))
- {IH, lr, plus(null,y), []}
-= inc(y)
-
-lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
-IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
-plus(inc(a),null)
- {p0,lr,plus(inc(a),null),[inc(a)/n]}
-= inc(a)
- {p0,rl,a,[a/n]}
-= inc(plus(a,null))
-IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
-IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
-plus(inc(a),inc(b))
- {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
-= inc(plus(inc(a),b))
- {IH,lr,plus(inc(a),b),[]}
-= inc(inc(plus(a,b)))
- {p1,rl,inc(plus(a,b)),[a/n,b/m]}
-= inc(plus(a,inc(b)))
-
-proof induction n
-IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
-plus(null,m)
- {L1,lr,plus(null,m),[m/y]}
-= m
- {p0,rl,m,[m/n]}
-= plus(m,null)
-IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
-IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
-plus(m,inc(k))
- {p1,lr,plus(m,inc(k)),[m/n,k/m]}
-= inc(plus(m,k))
- {IH,rl,plus(m,k),[]}
-= inc(plus(k,m))
- {L2,rl,inc(plus(k,m)),[k/a,m/b]}
-= plus(inc(k),m)
\ No newline at end of file