diff --git a/BewerterStrukturellerInduktion/Bewertung/AbstractBewerter.cs b/BewerterStrukturellerInduktion/Bewertung/AbstractBewerter.cs
index 51c639968f598ade773f6005ab828d67aee50d78..5806c364e43724ce8abad98f17006b9cc20ffaa0 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 14356aeaa5379f5482b7121312e5192b08fce7a9..dbf94f841576655e6558a7e51d76c4f93d9e00a0 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 14b790c81765f236749f49d3a94c1227b416d257..deadf6266005d1a34d3315ea027ffd9318386fd5 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 ec0591e533841677e34fd73b5aa5cb35d8191024..23b6268d96e32d52e3240084b9975beccfd67cf7 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 895de887640983c085656594abe2447fa456c35a..085f41ec5fee0e3733038280b363e28172afd7ad 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 7b184662824b173de713cca726652341081cab49..8c46629ef9880c48a1cb6c597cd7c20b4dc237f9 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 101b8c32813c233c33ae126fb1cfea27e60ad69b..868e4441a677de3ce78edf3f5fdcabc0007d108b 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 14ecc419c5ce6304c8f0abbeb6beb9f6a4fafa15..e51c3a0e4ee6a199b4969f6ced03dcb5018f7930 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 ef1c6dfdca092362a728ffa84b9ee3a7ce38b89e..65de424974aebd3a951c7b27239210871f8e0c75 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 7c1ddc2b91c7f7e803198fa8ec0be33a60f3683b..3c63a6c369192230d84f09774cf4368ea56167ea 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 2b1f0926b2836a2dc3c84a0180bfbaddf47e1ded..89a24e09610b12c29d43db0db2e3470d5b03d5bd 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 6aebfa05c9447353d05154e1537985b579971039..1214aa78b193490820955e0cac23034c01e4486e 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 b2cf076074b48d935def059718ef020db648c2e7..81258737803f2324e7950b0d272639fe1afb0aa8 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 010f61455ed4ea59aac9e78ca4f1a8965bde0139..e5eb7466a2f6a64348adf2659485a844cd779b3e 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 288c63c63c21e7c39376a0ef4c2a5f3665680247..ffdc68b9c8776008bb58f1e3a3954680335e83e2 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 6129541e190a58d2d8ebf51f127dab82f0aa8aa0..e620e88ef9006c4eff791fc69d5b5f01d3b10f4e 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 219501daea8bd90830aa2316d863566196c94194..1c347001d3f06dcd0f1b1243d0707f38cd1ed2d2 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 e221e66643d9467240e67579cbe4dc9653a922df..11ec7bb63dee8a2b4344e380229ef7dc1f1a93cf 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 4d7715863b89bdef8fb2203283094c11e96446ac..abdf539e331e8e4030c09ecbf6885e6449f9a353 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 97fbf46b3aef0daea20cbf210420217070002ed2..96d0911b56128aebf95a5ea8f93226fe2b8f27bc 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 4eb72270b240e995eebfb14bb36b89730ff04c93..eeaa777cbea65af52682ea82c1e50af0a90f4479 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 2d11e8bef116d152f3c63a10f607b9a3bf776dc4..e81a66440b7b5e6d262c3bd8c7d3df41aea01896 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 75f0b64715cde0812d0378131da66966b95c1b5c..02a33297843e375937aa1509fc88eb40ac7f2b5a 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 bc6c9454a29c114b115352dbdf779cef6a43e88b..efb88183418793400a82c29d39e720e69cbb905f 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 dd668e6ef577276f2f37e1f56112f3e8d55abf97..2db9e6be951a0daf87878b21b43dfe5e63a5e03c 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 9b01ccbe84a40c5cc38501801de38475355eb234..53acee790eb099a7f5c7a9f22ba24e9b917d20d5 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 25f92e9d833ad0aceedb8406e8494def2b7743f5..2d0e87081c69da91a05a68ee387bcf965f6101d0 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 7ffd2093e028d1227d1b6e5fd70e9639dc61d9f2..26f33ac950c966c90af1de75502984cc38fcaa72 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);
}
}