From d92b6032a774ee898a6812cbbd5f8e58113b29ab Mon Sep 17 00:00:00 2001
From: Edward Sabinus <edward.sabinus@informatik.uni-halle.de>
Date: Fri, 24 Nov 2023 15:39:59 +0100
Subject: [PATCH] added coords to element, so every Part of the proof got
coords. Changed all Exceptions related to elements to print its coords to the
message. Maybe do the same for Trees?
---
.../Bewertung/AbstractBewerter.cs | 2 +-
.../Eingabeverwaltung/{Parser => }/Coords.cs | 6 ++--
.../{Parser => }/KontextException.cs | 2 +-
.../Eingabeverwaltung/Metamodell/ADT/Axiom.cs | 2 +-
.../Metamodell/Beweis/Induction.cs | 2 +-
.../Metamodell/Beweis/InductionCase.cs | 6 ++--
.../Metamodell/Beweis/InductionHypothesis.cs | 4 +--
.../Metamodell/Beweis/Lemma.cs | 6 ++--
.../Metamodell/Beweis/SingleProof.cs | 1 +
.../Metamodell/Beweis/Substitution.cs | 13 +++++++--
.../Metamodell/Beweis/Transformation.cs | 2 +-
.../Metamodell/Beweis/TransformationStep.cs | 6 ++--
.../Eingabeverwaltung/Metamodell/Container.cs | 2 +-
.../Eingabeverwaltung/Metamodell/Rule.cs | 2 +-
.../Metamodell/Task/SingleTask.cs | 2 +-
.../Metamodell/Task/TaskLemma.cs | 2 +-
.../Parser/Listener_Helper.cs | 1 -
.../Parser/Proof_Listener.cs | 28 +++++++++----------
.../Eingabeverwaltung/Parser/Task_Listener.cs | 4 +--
.../Parser/TransformationStep_Listener.cs | 9 +++---
.../Ueberpruefung/CheckHelper.cs | 6 ++--
.../CheckInduction/CheckIndCaseType.cs | 5 ++--
.../CheckInduction/CheckIndTask_Satisfied.cs | 5 ++--
.../Ueberpruefung/CheckLemmaTaskIsUsed.cs | 3 +-
.../CheckTask_Satisfied.cs | 7 +++--
.../CheckUsedLemmaIsProved.cs | 7 +++--
.../Ueberpruefung/Element.cs | 15 ++++++++--
.../Ueberpruefung/Ueberpruefer.cs | 11 ++++----
28 files changed, 92 insertions(+), 69 deletions(-)
rename BewerterStrukturellerInduktion/Eingabeverwaltung/{Parser => }/Coords.cs (80%)
rename BewerterStrukturellerInduktion/Eingabeverwaltung/{Parser => }/KontextException.cs (86%)
diff --git a/BewerterStrukturellerInduktion/Bewertung/AbstractBewerter.cs b/BewerterStrukturellerInduktion/Bewertung/AbstractBewerter.cs
index 51c6399..5806c36 100644
--- a/BewerterStrukturellerInduktion/Bewertung/AbstractBewerter.cs
+++ b/BewerterStrukturellerInduktion/Bewertung/AbstractBewerter.cs
@@ -38,7 +38,7 @@ namespace Bewertung
};
// Init Bewertung
List<AssessmentObject> bewertung = new List<AssessmentObject>();
- Lemma mainProofLemma = new Lemma("main proof", con.Task.task.eq, con.Task.task.fixedVars, con.Proof.proof);
+ Lemma mainProofLemma = new Lemma(con.Proof.proof.coords,"main proof", con.Task.task.eq, con.Task.task.fixedVars, con.Proof.proof);
mainProofLemma.OwnTask = con.Task.task;
mainProofLemma.usefulFor.Add(new TaskAssignment(con.Task.task));
mainProofLemma.IsProved = true;
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Coords.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Coords.cs
similarity index 80%
rename from BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Coords.cs
rename to BewerterStrukturellerInduktion/Eingabeverwaltung/Coords.cs
index 14356ae..dbf94f8 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Coords.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Coords.cs
@@ -1,7 +1,7 @@
using Antlr4.Runtime;
-namespace Eingabeverwaltung.Parser
-{
+namespace Eingabeverwaltung
+{
public class Coords
{
public readonly int line;
@@ -13,7 +13,7 @@ namespace Eingabeverwaltung.Parser
this.column = column;
}
- public Coords(ParserRuleContext context)
+ public Coords(ParserRuleContext context)
{
line = context.Start.Line;
column = context.Start.Column;
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/KontextException.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/KontextException.cs
similarity index 86%
rename from BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/KontextException.cs
rename to BewerterStrukturellerInduktion/Eingabeverwaltung/KontextException.cs
index 14b790c..deadf62 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/KontextException.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/KontextException.cs
@@ -1,6 +1,6 @@
using System;
-namespace Eingabeverwaltung.Parser
+namespace Eingabeverwaltung
{
internal class KontextException : Exception
{
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/ADT/Axiom.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/ADT/Axiom.cs
index ec0591e..23b6268 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/ADT/Axiom.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/ADT/Axiom.cs
@@ -2,7 +2,7 @@
{
public class Axiom : Rule
{
- public Axiom(string name, Equation equation) :base(name,equation) { }
+ public Axiom(string name, Equation equation) :base(new Coords(-1,-1),name,equation) { }
public override bool IsFixed(Variable variable) => false;
}
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Induction.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Induction.cs
index 895de88..085f41e 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Induction.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Induction.cs
@@ -10,7 +10,7 @@ namespace Eingabeverwaltung.Metamodell
public readonly List<InductionCase> indCases;
public readonly List<InductionHypothesis> indHyps;
public readonly List<Error> errors;
- public Induction(Equation eq, List<Variable> fixedVars, Variable indVar, List<InductionCase> indCases, List<InductionHypothesis> indHyps)
+ public Induction(Coords coords, Equation eq, List<Variable> fixedVars, Variable indVar, List<InductionCase> indCases, List<InductionHypothesis> indHyps) : base(coords)
{
this.eq = eq;
this.fixedVars = fixedVars;
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/InductionCase.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/InductionCase.cs
index 7b18466..8c46629 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/InductionCase.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/InductionCase.cs
@@ -12,7 +12,7 @@ namespace Eingabeverwaltung.Metamodell
private Constructor constructor;
private List<Variable> buildingParameterVariables;
- public InductionCase(string type, Equation eq, List<Variable> fixedVars, Transformation proof)
+ public InductionCase(Coords coords,string type, Equation eq, List<Variable> fixedVars, Transformation proof) : base(coords)
{
this.type = type;
this.fixedVars = fixedVars;
@@ -26,13 +26,13 @@ namespace Eingabeverwaltung.Metamodell
public Constructor Constructor
{
get { return constructor; }
- set { if (constructor == null) constructor = value; else throw new System.Exception("Tried to reset constructor in InductionCase!"); }
+ set { if (constructor == null) constructor = value; else throw new KontextException(coords,"Tried to reset constructor in InductionCase!"); }
}
public List<Variable> BuildingParameterVariables
{
get { return buildingParameterVariables; }
set { if (buildingParameterVariables == null) buildingParameterVariables = value;
- else throw new System.Exception("Tried to reset buildingParameterVariables in InductionCase!");
+ else throw new KontextException(coords, "Tried to reset buildingParameterVariables in InductionCase!");
}
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/InductionHypothesis.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/InductionHypothesis.cs
index 101b8c3..868e444 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/InductionHypothesis.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/InductionHypothesis.cs
@@ -8,7 +8,7 @@ namespace Eingabeverwaltung.Metamodell
public readonly List<Variable> fixedVars;
private Nullable<bool> isProved;
public readonly List<Error> errors;
- public InductionHypothesis(string name, Equation eq, List<Variable> fixedVars) : base(name,eq)
+ public InductionHypothesis(Coords coords, string name, Equation eq, List<Variable> fixedVars) : base(coords,name,eq)
{
this.fixedVars = fixedVars;
errors = new List<Error>();
@@ -17,7 +17,7 @@ namespace Eingabeverwaltung.Metamodell
public Nullable<bool> IsProved
{
get { return isProved; }
- set { if (isProved == null) isProved = value; else throw new Exception("Tried to change existing isProved in Inductionhypothesis!"); }
+ set { if (isProved == null) isProved = value; else throw new KontextException(coords, "Tried to change existing isProved in Inductionhypothesis!"); }
}
public override bool IsFixed(Variable variable) => fixedVars.Contains(variable);
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Lemma.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Lemma.cs
index 14ecc41..e51c3a0 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Lemma.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Lemma.cs
@@ -13,7 +13,7 @@ namespace Eingabeverwaltung.Metamodell
public readonly List<TaskAssignment> usefulFor;
public readonly List<Error> errors;
- public Lemma(string name, Equation equation, List<Variable> fixedVars, SingleProof proof) : base(name,equation)
+ public Lemma(Coords coords, string name, Equation equation, List<Variable> fixedVars, SingleProof proof) : base(coords, name,equation)
{
this.fixedVars = fixedVars;
this.proof = proof;
@@ -28,13 +28,13 @@ namespace Eingabeverwaltung.Metamodell
public Nullable<bool> IsProved
{
get { return isProved; }
- set { if (isProved == null) isProved = value; else throw new Exception("Tried to change existing isProved in Lemma!"); }
+ set { if (isProved == null) isProved = value; else throw new KontextException(coords, "Tried to change existing isProved in Lemma!"); }
}
public SingleTask OwnTask
{
get { return ownTask; }
- set { if (ownTask == null) ownTask = value; else throw new Exception("Tried to change existing ownTask in Lemma!"); }
+ set { if (ownTask == null) ownTask = value; else throw new KontextException(coords, "Tried to change existing ownTask in Lemma!"); }
}
/// <summary>
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/SingleProof.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/SingleProof.cs
index ef1c6df..65de424 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/SingleProof.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/SingleProof.cs
@@ -4,6 +4,7 @@ namespace Eingabeverwaltung.Metamodell
{
public abstract class SingleProof : Element
{
+ public SingleProof(Coords coords) : base(coords) { }
public abstract string ToString(bool showMetadata);
}
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Substitution.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Substitution.cs
index 7c1ddc2..3c63a6c 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Substitution.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Substitution.cs
@@ -11,14 +11,21 @@ namespace Eingabeverwaltung.Metamodell
public readonly Tree tree;
public readonly List<Error> errors;
+ /// <summary>
+ /// Use this Constructor only for Substitutions that are not from the input.
+ /// </summary>
+ /// <param name="variable"></param>
+ /// <param name="tree"></param>
+ public Substitution(Variable variable, Tree tree) : this(new Coords(-1, -1), variable, tree) { }
+
/// <summary>
/// This Constructor throws Exception if variable is null.
/// </summary>
/// <param name="variable"></param>
/// <param name="tree"></param>
- public Substitution(Variable variable, Tree tree)
+ public Substitution(Coords coords,Variable variable, Tree tree) :base(coords)
{
- if (variable == null) throw new Exception("Error: It was tried to build a Substitution with a null-variable and without variableName!");
+ if (variable == null) throw new KontextException(coords, "Error: It was tried to build a Substitution with a null-variable and without variableName!");
variableName = variable.name;
this.variable = variable;
this.tree = tree;
@@ -31,7 +38,7 @@ namespace Eingabeverwaltung.Metamodell
/// <param name="variableName"></param>
/// <param name="variable"></param>
/// <param name="tree"></param>
- public Substitution(string variableName, Variable variable, Tree tree)
+ public Substitution(Coords coords, string variableName, Variable variable, Tree tree) : base(coords)
{
this.variableName = variableName;
this.variable = variable;
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Transformation.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Transformation.cs
index 2b1f092..89a24e0 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Transformation.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/Transformation.cs
@@ -9,7 +9,7 @@ namespace Eingabeverwaltung.Metamodell
public readonly List<TransformationStep> transformationSteps;
public readonly List<Error> errors;
- public Transformation(Tree startTree, List<TransformationStep> transformationSteps)
+ public Transformation(Coords coords, Tree startTree, List<TransformationStep> transformationSteps) : base(coords)
{
this.startTree = startTree;
this.transformationSteps = transformationSteps;
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/TransformationStep.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/TransformationStep.cs
index 6aebfa0..1214aa7 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/TransformationStep.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Beweis/TransformationStep.cs
@@ -13,7 +13,7 @@ namespace Eingabeverwaltung.Metamodell
public readonly List<Substitution> substitutions;
public readonly List<Error> errors;
- public TransformationStep(Tree startTree, Rule rule, char direction, Tree termPart, Tree resultTree, List<Substitution> substitutions)
+ public TransformationStep(Coords coords, Tree startTree, Rule rule, char direction, Tree termPart, Tree resultTree, List<Substitution> substitutions) : base(coords)
{
this.startTree = startTree;
this.rule = rule;
@@ -30,7 +30,7 @@ namespace Eingabeverwaltung.Metamodell
{
case '>': return rule.eq.leftTree;
case '<': return rule.eq.rightTree;
- default: throw new System.Exception("A TransformationStep has an undefined direction: " + direction);
+ default: throw new KontextException(coords, "A TransformationStep has an undefined direction: " + direction);
}
}
public Tree ruleEndTree()
@@ -39,7 +39,7 @@ namespace Eingabeverwaltung.Metamodell
{
case '>': return rule.eq.rightTree;
case '<': return rule.eq.leftTree;
- default: throw new System.Exception("A TransformationStep has an undefined direction: " + direction);
+ default: throw new KontextException(coords, "A TransformationStep has an undefined direction: " + direction);
}
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Container.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Container.cs
index b2cf076..8125873 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Container.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Container.cs
@@ -9,7 +9,7 @@ namespace Eingabeverwaltung.Metamodell
private Task task;
private Proof proof;
- public Container() {}
+ public Container() : base(new Coords(0, 0)) { }
public ADT ADT
{
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Rule.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Rule.cs
index 010f614..e5eb746 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Rule.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Rule.cs
@@ -7,7 +7,7 @@ namespace Eingabeverwaltung.Metamodell
{
public readonly string name;
public readonly Equation eq;
- public Rule(string name, Equation equation)
+ public Rule(Coords coords, string name, Equation equation) :base(coords)
{
this.name = name;
eq = equation;
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Task/SingleTask.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Task/SingleTask.cs
index 288c63c..ffdc68b 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Task/SingleTask.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Task/SingleTask.cs
@@ -9,7 +9,7 @@ namespace Eingabeverwaltung.Metamodell
public readonly IConfig config;
public readonly Variable indVariable;
- public SingleTask(string name, Equation eq, List<Variable> fixedVars, IConfig config, Variable indVariable) : base(name, eq)
+ public SingleTask(string name, Equation eq, List<Variable> fixedVars, IConfig config, Variable indVariable) : base(new Coords(-1,-1),name, eq)
{
this.fixedVars = fixedVars;
this.config = config;
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Task/TaskLemma.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Task/TaskLemma.cs
index 6129541..e620e88 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Task/TaskLemma.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Task/TaskLemma.cs
@@ -5,7 +5,7 @@ namespace Eingabeverwaltung.Metamodell
public class TaskLemma : Rule
{
public readonly List<Variable> fixedVars;
- public TaskLemma(string name, Equation eq, List<Variable> fixedVars) : base(name, eq)
+ public TaskLemma(string name, Equation eq, List<Variable> fixedVars) : base(new Coords(-1, -1), name, eq)
{
this.fixedVars = fixedVars;
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
index 219501d..1c34700 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
@@ -2,7 +2,6 @@
using System.Linq;
using System.Collections.Generic;
using Eingabeverwaltung.Metamodell;
-using Antlr4.Runtime;
namespace Eingabeverwaltung.Parser
{
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
index e221e66..11ec7bb 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
@@ -4,9 +4,6 @@ using Antlr4.Runtime.Tree;
using Antlr4.Runtime;
using Antlr4.Runtime.Misc;
using System.Collections.Generic;
-using System;
-using Eingabeverwaltung.Parser.ADT_Parser;
-using Eingabeverwaltung.Parser.Task_Parser;
namespace Eingabeverwaltung.Parser
{
@@ -79,15 +76,16 @@ namespace Eingabeverwaltung.Parser
public void EnterLemma([NotNull] ProofParser.LemmaContext context) { }
public void ExitLemma([NotNull] ProofParser.LemmaContext context)
{
- lemmata.Add(new Lemma(lemmaDef.name, lemmaDef.eq, lemmaDef.fixedVars, SP));
+ lemmata.Add(new Lemma(new Coords(context),lemmaDef.name, lemmaDef.eq, lemmaDef.fixedVars, SP));
lemmaDef = null; // notwendig, damit SP weis, ob es gerade nicht in einem Lemma ist
}
public void EnterLemmaDef([NotNull] ProofParser.LemmaDefContext context) { }
public void ExitLemmaDef([NotNull] ProofParser.LemmaDefContext context)
{
+ Coords coords = new Coords(context);
string lemmaName = context.BEZ().GetText();
- Test_Lemmata_all_Unique(lemmaName,"Lemma",new Coords(context));
- lemmaDef = new Lemma(lemmaName, LH.equation, LH.fixedVars,null);
+ Test_Lemmata_all_Unique(lemmaName,"Lemma",coords);
+ lemmaDef = new Lemma(coords,lemmaName, LH.equation, LH.fixedVars,null);
// Im Beweis des Lemmas gelten zuerst die Variablen des Lemmas (gilt bereits durch das Bauen der Gleichung)
List<List<Variable>> variableDefinitionContext;
variableDefinitionContext = new List<List<Variable>>() { LH.adt_vars };
@@ -107,7 +105,7 @@ namespace Eingabeverwaltung.Parser
public void EnterTransformation([NotNull] ProofParser.TransformationContext context) { }
public void ExitTransformation([NotNull] ProofParser.TransformationContext context)
{
- SP = new Transformation(startTree, new List<TransformationStep>());
+ SP = new Transformation(new Coords(context),startTree, new List<TransformationStep>());
}
public void EnterStart_tree([NotNull] ProofParser.Start_treeContext context) => LH.trees = new List<Tree>();
@@ -177,7 +175,7 @@ namespace Eingabeverwaltung.Parser
if (tv.variable == indVar) { indVar = renaming.variable; changed = true; break; }
if (!changed) indVar = null;
}
- SP = new Induction(eq,fixedVars,indVar,indCases, indHyps);
+ SP = new Induction(coords,eq, fixedVars,indVar,indCases, indHyps);
}
public void EnterInd_var([NotNull] ProofParser.Ind_varContext context)
{
@@ -188,18 +186,20 @@ namespace Eingabeverwaltung.Parser
}
public void ExitInd_var([NotNull] ProofParser.Ind_varContext context) { }
public void EnterInd_basis([NotNull] ProofParser.Ind_basisContext context) => SP = null;
- public void ExitInd_basis([NotNull] ProofParser.Ind_basisContext context)
+ public void ExitInd_basis([NotNull] ProofParser.Ind_basisContext context)
{
+ Coords coords = new Coords(context);
if (SP is Transformation tr)
- indCases.Add(new InductionCase("IA", LH.equation, LH.fixedVars, tr));
- else throw new KontextException(new Coords(context),"Found Singleproof in induction basis that is not a transformation!");
+ indCases.Add(new InductionCase(coords,"IA", LH.equation, LH.fixedVars, tr));
+ else throw new KontextException(coords,"Found Singleproof in induction basis that is not a transformation!");
}
public void EnterInd_step([NotNull] ProofParser.Ind_stepContext context) => SP = null;
public void ExitInd_step([NotNull] ProofParser.Ind_stepContext context)
{
+ Coords coords = new Coords(context);
if (SP is Transformation tr)
- indCases.Add(new InductionCase("IS", LH.equation, LH.fixedVars, tr));
- else throw new KontextException(new Coords(context),"Found Singleproof in induction step that is not a transformation!");
+ indCases.Add(new InductionCase(coords, "IS", LH.equation, LH.fixedVars, tr));
+ else throw new KontextException(coords,"Found Singleproof in induction step that is not a transformation!");
}
public void EnterInd_hyp([NotNull] ProofParser.Ind_hypContext context) { }
public void ExitInd_hyp([NotNull] ProofParser.Ind_hypContext context)
@@ -212,7 +212,7 @@ namespace Eingabeverwaltung.Parser
foreach (InductionHypothesis ih in indHyps)
if (ih.name == name) throw new KontextException(coords,"There are more then 1 inductionhypothesis with name "+name+"!");
Test_Lemmata_all_Unique(name,"InductionHypothesis",coords);
- indHyps.Add(new InductionHypothesis(name,LH.equation, LH.fixedVars));
+ indHyps.Add(new InductionHypothesis(coords,name,LH.equation, LH.fixedVars));
}
public void EnterInd_case([NotNull] ProofParser.Ind_caseContext context) { }
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Listener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Listener.cs
index 4d77158..abdf539 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Listener.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Listener.cs
@@ -4,12 +4,10 @@ using Antlr4.Runtime.Misc;
using Eingabeverwaltung.Metamodell;
using Eingabeverwaltung.Parser.Task_Parser;
using System.Collections.Generic;
-using System;
-using Eingabeverwaltung.Parser.ADT_Parser;
namespace Eingabeverwaltung.Parser
{
- public class Task_Listener : ITaskListener
+ public class Task_Listener : ITaskListener
{
// object on which will be build
private Container container;
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
index 97fbf46..96d0911 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
@@ -6,7 +6,6 @@ using Antlr4.Runtime.Misc;
using System.Collections.Generic;
using System;
using System.Linq;
-using Eingabeverwaltung.Parser.ADT_Parser;
namespace Eingabeverwaltung.Parser
{
@@ -28,6 +27,7 @@ namespace Eingabeverwaltung.Parser
private class Transformation_Step
{
+ public Coords coords;
public Rule rule;
public char direction;
public Tree termpart;
@@ -107,7 +107,7 @@ namespace Eingabeverwaltung.Parser
Tree startT = currentTR.startTree;
for (int i = 0; i < TSs.Count; i++)
{
- currentTR.transformationSteps.Add(new TransformationStep(startT, TSs[i].rule, TSs[i].direction, TSs[i].termpart, TSs[i].resultTree, TSs[i].subs));
+ currentTR.transformationSteps.Add(new TransformationStep(TSs[i].coords,startT, TSs[i].rule, TSs[i].direction, TSs[i].termpart, TSs[i].resultTree, TSs[i].subs));
startT = TSs[i].resultTree;
}
}
@@ -118,6 +118,7 @@ namespace Eingabeverwaltung.Parser
public void EnterTransformation_step([NotNull] ProofParser.Transformation_stepContext context) => TS = new Transformation_Step();
public void ExitTransformation_step([NotNull] ProofParser.Transformation_stepContext context)
{
+ TS.coords = new Coords(context);
TSs.Add(TS);
TS = null;
}
@@ -206,7 +207,7 @@ namespace Eingabeverwaltung.Parser
foreach (Variable RV in ruleVars)
foreach (Variable CV in allContextVars)
if (CV.name == RV.name && CV != RV) // do trivial subs even if it means sub of fixed var
- TS.subs.Add(new Substitution(RV, new TreeVariable(CV)));
+ TS.subs.Add(new Substitution(new Coords(context.Stop.Line,context.Stop.Column),RV, new TreeVariable(CV)));
}
public void EnterSub([NotNull] ProofParser.SubContext context) => LH.trees = new List<Tree>();
@@ -217,7 +218,7 @@ namespace Eingabeverwaltung.Parser
string variableName = context.BEZ().GetText();
Variable variable = LH.findVariable(variableName, TS.rule.eq.variables);
Test_Substitution_Variable_isCorrect(variableName, variable,coords);
- TS.subs.Add(new Substitution(variableName, variable, LH.trees[0]));
+ TS.subs.Add(new Substitution(coords,variableName, variable, LH.trees[0]));
}
public void EnterResult_tree([NotNull] ProofParser.Result_treeContext context) => LH.trees = new List<Tree>();
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/CheckHelper.cs b/BewerterStrukturellerInduktion/Ueberpruefung/CheckHelper.cs
index 4eb7227..eeaa777 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/CheckHelper.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/CheckHelper.cs
@@ -26,7 +26,7 @@ namespace Ueberpruefung
substitutedChildren.Add(substitute(workingTree.children[i], sub));
tree = new ComposedTree(workingTree.operation, substitutedChildren);
}
- else throw new Exception("Found a tree that is wether TreeVariable nor ComposedTree: " + tree.ToString());
+ else throw new Exception("Found a tree that is neither TreeVariable nor ComposedTree: " + tree.ToString());
}
}
return tree;
@@ -145,7 +145,7 @@ namespace Ueberpruefung
return null;
}
else if (forTree as ComposedTree != null && toTree as TreeVariable != null) return null;
- else throw new Exception("Found a tree that is wether TreeVariable nor ComposedTree: forTree: " + forTree.ToString() + ", toTree: " + toTree.ToString());
+ else throw new Exception("Found a tree that is neither TreeVariable nor ComposedTree: forTree: " + forTree.ToString() + ", toTree: " + toTree.ToString());
}
/// <summary>
@@ -208,7 +208,7 @@ namespace Ueberpruefung
if (foundSubTree) return cTree;
else return null;
}
- else throw new Exception("Found a tree that is wether TreeVariable nor ComposedTree: " + tree.ToString());
+ else throw new Exception("Found a tree that is neither TreeVariable nor ComposedTree: " + tree.ToString());
}
}
}
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndCaseType.cs b/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndCaseType.cs
index 2d11e8b..e81a664 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndCaseType.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndCaseType.cs
@@ -1,4 +1,5 @@
-using Eingabeverwaltung.Metamodell;
+using Eingabeverwaltung;
+using Eingabeverwaltung.Metamodell;
using System;
namespace Ueberpruefung.CheckInduction
@@ -23,7 +24,7 @@ namespace Ueberpruefung.CheckInduction
{ if (indC.Constructor != null) result = indC.Constructor is BasicConstructor; }
else if (indC.type == "IS")
{ if (indC.Constructor != null) result = indC.Constructor is BuildingConstructor; }
- else throw new Exception("Found an unknown induction case type: " + indC.type);
+ else throw new KontextException(indC.coords,"Found an unknown induction case type: " + indC.type);
if (!result) indC.errors.Add(new Error(41));
return result;
}
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndTask_Satisfied.cs b/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndTask_Satisfied.cs
index 75f0b64..02a3329 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndTask_Satisfied.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndTask_Satisfied.cs
@@ -1,4 +1,5 @@
-using Eingabeverwaltung.Metamodell;
+using Eingabeverwaltung;
+using Eingabeverwaltung.Metamodell;
using System;
using System.Collections.Generic;
@@ -44,7 +45,7 @@ namespace Ueberpruefung.CheckInduction
if (ind.indVar != taskRenaming.variable)
{ result = false; ind.errors.Add(new Error(38)); }
}
- else throw new Exception("Found a single proof that is neither Transformation nor Induction!");
+ else throw new KontextException(proof.coords,"Found a single proof that is neither Transformation nor Induction!");
return result;
}
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/CheckLemmaTaskIsUsed.cs b/BewerterStrukturellerInduktion/Ueberpruefung/CheckLemmaTaskIsUsed.cs
index bc6c945..efb8818 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/CheckLemmaTaskIsUsed.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/CheckLemmaTaskIsUsed.cs
@@ -1,5 +1,6 @@
using System;
using System.Collections.Generic;
+using Eingabeverwaltung;
using Eingabeverwaltung.Metamodell;
namespace Ueberpruefung
@@ -42,7 +43,7 @@ namespace Ueberpruefung
else if (proof is Induction ind)
foreach (InductionCase indC in ind.indCases)
RemoveAllUsefulLemmataTR(visited, newLemmata, indC.proof);
- else throw new Exception("Found a proof that is neither Transformation nor Induction!");
+ else throw new KontextException(proof.coords,"Found a proof that is neither Transformation nor Induction!");
foreach (Lemma newLemma in newLemmata)
RemoveAllUsefulLemmata(visited, newLemma.proof);
}
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/CheckTransformation/CheckTask_Satisfied.cs b/BewerterStrukturellerInduktion/Ueberpruefung/CheckTransformation/CheckTask_Satisfied.cs
index dd668e6..2db9e6b 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/CheckTransformation/CheckTask_Satisfied.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/CheckTransformation/CheckTask_Satisfied.cs
@@ -1,4 +1,5 @@
-using Eingabeverwaltung.Metamodell;
+using Eingabeverwaltung;
+using Eingabeverwaltung.Metamodell;
using System;
using System.Collections.Generic;
using System.Linq;
@@ -15,12 +16,12 @@ namespace Ueberpruefung.CheckTransformation
if (con.Proof.proof is Transformation tr)
return check(con.Task.task.eq, tr);
else if (con.Proof.proof is Induction) return true; // is true by creation of Induction
- else throw new Exception("Found a Singleproof that is either Transformation nor Induction");
+ else throw new KontextException(con.Proof.proof.coords,"Found a Singleproof that is neither Transformation nor Induction");
else if (e is Lemma l)
if (l.proof is Transformation tr)
return check(l.eq, tr);
else if (l.proof is Induction) return true; // is true by creation of Induction
- else throw new Exception("Found a Singleproof that is either Transformation nor Induction");
+ else throw new KontextException(l.proof.coords,"Found a Singleproof that is neither Transformation nor Induction");
else if (e is InductionCase ic) return check(ic.eq, ic.proof);
else throw new InvalidOperationException();
}
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/CheckTransformation/CheckUsedLemmaIsProved.cs b/BewerterStrukturellerInduktion/Ueberpruefung/CheckTransformation/CheckUsedLemmaIsProved.cs
index 9b01ccb..53acee7 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/CheckTransformation/CheckUsedLemmaIsProved.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/CheckTransformation/CheckUsedLemmaIsProved.cs
@@ -1,4 +1,5 @@
-using Eingabeverwaltung.Metamodell;
+using Eingabeverwaltung;
+using Eingabeverwaltung.Metamodell;
using System;
namespace Ueberpruefung.CheckTransformation
@@ -15,7 +16,7 @@ namespace Ueberpruefung.CheckTransformation
{
bool result; string output = "";
if (l.IsProved is bool p) result = p;
- else throw new Exception("Tried to check if lemma " + l.name + " is proved while isProved is not set.");
+ else throw new KontextException(l.coords,"Tried to check if lemma " + l.name + " is proved while isProved is not set.");
if (result)
{
// This error must occure also when a main proof of a task has cyclic dependencies,
@@ -36,7 +37,7 @@ namespace Ueberpruefung.CheckTransformation
{
bool result;
if (ih.IsProved is bool p) result = p;
- else throw new Exception("Tried to check if inductionhypothesis is proved while isProved is not set.");
+ else throw new KontextException(ih.coords,"Tried to check if inductionhypothesis is proved while isProved is not set.");
return result;
}
else return true;
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/Element.cs b/BewerterStrukturellerInduktion/Ueberpruefung/Element.cs
index 25f92e9..2d0e870 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/Element.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/Element.cs
@@ -1,7 +1,18 @@
-namespace Ueberpruefung
+using Eingabeverwaltung;
+
+namespace Ueberpruefung
{
- public abstract class Element
+ public abstract class Element
{
+ /// <summary>
+ /// Coords of the start token of this element
+ /// </summary>
+ public readonly Coords coords;
+
+ public Element(Coords coords)
+ {
+ this.coords = coords;
+ }
public bool accept(ElementChecker e) => e.check(this);
}
}
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/Ueberpruefer.cs b/BewerterStrukturellerInduktion/Ueberpruefung/Ueberpruefer.cs
index 7ffd209..26f33ac 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/Ueberpruefer.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/Ueberpruefer.cs
@@ -3,6 +3,7 @@ using System;
using System.Collections.Generic;
using Ueberpruefung.CheckTransformation;
using Ueberpruefung.CheckInduction;
+using Eingabeverwaltung;
namespace Ueberpruefung
{
@@ -186,7 +187,7 @@ namespace Ueberpruefung
if (!lemma.cyclicDependencies.Contains(usedLemma)) lemma.cyclicDependencies.Add(usedLemma);
found = true; break;
}
- if (!found) throw new Exception("Error in Ueberpruefung: Could not find Lemma " + usedLemma.name + " in Lemmata!");
+ if (!found) throw new KontextException(ts.rule.coords, "Error in Ueberpruefung: Could not find Lemma " + usedLemma.name + " in Lemmata!");
}
}
}
@@ -197,7 +198,7 @@ namespace Ueberpruefung
else if (lemma.proof is Induction ind)
foreach (InductionCase indC in ind.indCases)
writeDirectCyclicDependencies(lemma, indC.proof);
- else throw new Exception("Found a proof in Lemma that is neither Transformation nor Induction!");
+ else throw new KontextException(lemma.proof.coords,"Found a proof in Lemma that is neither Transformation nor Induction!");
}
//Console.WriteLine("After 1."); print(lemmata,true);
// 2. remove Lemmata not depending from cyclic Lemmata by topological sort
@@ -314,7 +315,7 @@ namespace Ueberpruefung
private static void analyseUsefulnessToIndCases(List<SingleTask> tasks, Proof proof)
{
// 1. get all lemmata inclusive a lemma for main proof
- Lemma mainProofLemma = new Lemma("main proof", tasks[0].eq, tasks[0].fixedVars, proof.proof);
+ Lemma mainProofLemma = new Lemma(proof.proof.coords,"main proof", tasks[0].eq, tasks[0].fixedVars, proof.proof);
mainProofLemma.OwnTask = tasks[0];
mainProofLemma.usefulFor.Add(new TaskAssignment(tasks[0]));
List<Lemma> allLemmata = new List<Lemma>() { mainProofLemma };
@@ -330,13 +331,13 @@ namespace Ueberpruefung
{
foreach(InductionCase ic in ind.indCases)
{
- if (ic.Constructor == null) continue;
+ if (ic.Constructor == null) continue; // those inductioncases don't get assessed, so it should not count to the usefulness
foreach (Lemma usefulLemma in GetAllUsefulLemmata(new List<Lemma>(), ic.proof))
{
TaskAssignment ta = null;
foreach(TaskAssignment currentTa in usefulLemma.usefulFor)
if (currentTa.task == mainIndLemma.OwnTask) { ta = currentTa; break; }
- if (ta == null) throw new Exception("Could not find Task Assignment to task "+mainIndLemma.OwnTask.name+" for Lemma "+usefulLemma.name+" in its Task Assignments!");
+ if (ta == null) throw new Exception("Could not find Task Assignment to task "+mainIndLemma.OwnTask.name+" for Lemma "+usefulLemma.name+" in its Task Assignments!"); // there are no useful coords
ta.AddIndCase(ic.Constructor);
}
}
--
GitLab