From 01597efdfedc4d4919c445eafba2eb15582ed1cb Mon Sep 17 00:00:00 2001
From: Edward Sabinus <edward.sabinus@informatik.uni-halle.de>
Date: Fri, 24 Nov 2023 16:11:26 +0100
Subject: [PATCH] added coords to trees; changed all Exceptions related to
trees to show its coords
---
.../Metamodell/ComposedTree.cs | 15 +++++---
.../Eingabeverwaltung/Metamodell/Tree.cs | 6 +++-
.../Metamodell/TreeVariable.cs | 15 ++++++--
.../Parser/Listener_Helper.cs | 10 +++---
.../Parser/TransformationStep_Listener.cs | 5 ++-
.../Ueberpruefung/CheckHelper.cs | 35 +++++++++++--------
.../CheckInduction/CheckIndPartEquation.cs | 5 +--
7 files changed, 61 insertions(+), 30 deletions(-)
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/ComposedTree.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/ComposedTree.cs
index 8f1addb..4ed626f 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/ComposedTree.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/ComposedTree.cs
@@ -9,14 +9,21 @@ namespace Eingabeverwaltung.Metamodell
/// OperationName is the name of the operation.
/// </summary>
public readonly Operation operation;
- public readonly List<Tree> children;
+ public readonly List<Tree> children;
/// <summary>
- /// Creates a ComposedTree. Base gets operation.name as name and operation.sorts.Last() as sort.
+ /// Use this only for Trees without Coords.
/// </summary>
/// <param name="operation"></param>
/// <param name="children"></param>
- public ComposedTree(Operation operation, List<Tree> children) : base(operation.name, operation.sorts.Last())
+ public ComposedTree(Operation operation, List<Tree> children) : this(new Coords(-1,-1), operation, children) { }
+
+ /// <summary>
+ /// Creates a ComposedTree. Base gets operation.name as name and operation.sorts.Last() as sort.
+ /// </summary>
+ /// <param name="operation"></param>
+ /// <param name="children"></param>
+ public ComposedTree(Coords coords, Operation operation, List<Tree> children) : base(coords,operation.name, operation.sorts.Last())
{
this.operation = operation;
this.children = children;
@@ -83,7 +90,7 @@ namespace Eingabeverwaltung.Metamodell
// Not a foreach because the order is important and its safer when order is defined explicitly.
for (int i = 0; i < children.Count; i++)
copiedChildren.Add(children[i].Copy());
- return new ComposedTree(operation, copiedChildren);
+ return new ComposedTree(coords, operation, copiedChildren);
}
}
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Tree.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Tree.cs
index a6b6f8c..2026c8e 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Tree.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Tree.cs
@@ -4,7 +4,11 @@ namespace Eingabeverwaltung.Metamodell
{
public abstract class Tree : Sorthaver
{
- public Tree(string name, Sort sort) : base(name, sort) { }
+ public readonly Coords coords;
+ public Tree(Coords coords, string name, Sort sort) : base(name, sort)
+ {
+ this.coords = coords;
+ }
public override abstract string ToString();
public abstract List<Tree> findSubTree(Tree tree);
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/TreeVariable.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/TreeVariable.cs
index 0a8d399..a186ed1 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/TreeVariable.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/TreeVariable.cs
@@ -6,7 +6,18 @@ namespace Eingabeverwaltung.Metamodell
{
public readonly Variable variable;
- public TreeVariable(Variable variable) : base(variable.name, variable.sort)
+ /// <summary>
+ /// Use this only for Trees without Coords.
+ /// </summary>
+ /// <param name="variable"></param>
+ public TreeVariable(Variable variable) : this(new Coords(-1,-1), variable) { }
+
+ /// <summary>
+ /// The regular Constructor of TreeVariable
+ /// </summary>
+ /// <param name="coords"></param>
+ /// <param name="variable"></param>
+ public TreeVariable(Coords coords, Variable variable) : base(coords, variable.name, variable.sort)
{
this.variable = variable;
}
@@ -26,6 +37,6 @@ namespace Eingabeverwaltung.Metamodell
public override bool Equals(Tree tree) => findSubTree(tree).Count > 0;
- public override Tree Copy() => new TreeVariable(variable);
+ public override Tree Copy() => new TreeVariable(coords, variable);
}
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
index 1c34700..29c368d 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
@@ -72,12 +72,12 @@ namespace Eingabeverwaltung.Parser
Tree result = null;
Variable variable = findVariableInADT_Vars(treeName);
if (variable != null)
- result = new TreeVariable(variable);
+ result = new TreeVariable(coords,variable);
else
{
Operation operation = findOperationInADT_Ops(treeName, 0, coords);
if (operation != null)
- result = new ComposedTree(operation, new List<Tree>());
+ result = new ComposedTree(coords, operation, new List<Tree>());
}
if (result == null) throw new KontextException(coords,"The Tree " + treeName + " could not be found in Vars or Operations of the ADT!");
trees.Add(result);
@@ -100,7 +100,7 @@ namespace Eingabeverwaltung.Parser
}
children.Reverse();
Test_ComposedTree_Children_Sorts_are_correct(operation, children);
- Tree currentTree = new ComposedTree(operation, children);
+ Tree currentTree = new ComposedTree(coords, operation, children);
trees.Add(currentTree);
}
else
@@ -121,12 +121,12 @@ namespace Eingabeverwaltung.Parser
Tree result = null;
Variable variable = findVariableInADT_Vars(treeName);
if (variable != null)
- result = new TreeVariable(variable);
+ result = new TreeVariable(coords, variable);
else
{
Operation operation = findOperationInADT_Ops(treeName, -1, false, coords); // can't test it here because of structure of fTrees
if (operation != null)
- result = new ComposedTree(operation, new List<Tree>());
+ result = new ComposedTree(coords, operation, new List<Tree>());
}
if (result == null) throw new KontextException(coords,"The Tree " + treeName + " could not be found in Vars or Operations of the ADT!");
trees.Add(result);
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
index 96d0911..1926baa 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
@@ -207,7 +207,10 @@ 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(new Coords(context.Stop.Line,context.Stop.Column),RV, new TreeVariable(CV)));
+ {
+ Coords coords = new Coords(context.Stop.Line, context.Stop.Column);
+ TS.subs.Add(new Substitution(coords, RV, new TreeVariable(coords,CV)));
+ }
}
public void EnterSub([NotNull] ProofParser.SubContext context) => LH.trees = new List<Tree>();
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/CheckHelper.cs b/BewerterStrukturellerInduktion/Ueberpruefung/CheckHelper.cs
index eeaa777..cce922c 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/CheckHelper.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/CheckHelper.cs
@@ -1,6 +1,7 @@
using Eingabeverwaltung.Metamodell;
using System.Collections.Generic;
using System;
+using Eingabeverwaltung;
namespace Ueberpruefung
{
@@ -24,9 +25,9 @@ namespace Ueberpruefung
List<Tree> substitutedChildren = new List<Tree>();
for (int i = 0; i < workingTree.children.Count; i++)
substitutedChildren.Add(substitute(workingTree.children[i], sub));
- tree = new ComposedTree(workingTree.operation, substitutedChildren);
+ tree = new ComposedTree(new Coords(-1,-1),workingTree.operation, substitutedChildren);
}
- else throw new Exception("Found a tree that is neither TreeVariable nor ComposedTree: " + tree.ToString());
+ else throw new KontextException(tree.coords,"Found a tree that is neither TreeVariable nor ComposedTree: " + tree.ToString());
}
}
return tree;
@@ -128,24 +129,28 @@ namespace Ueberpruefung
{
if (forTree as TreeVariable != null)
return new List<Substitution>() { new Substitution(((TreeVariable)forTree).variable, toTree) };
- else if (forTree as ComposedTree != null && toTree as ComposedTree != null)
+ else if (forTree as ComposedTree != null)
{
- ComposedTree forCTree = forTree as ComposedTree;
- ComposedTree toCTree = toTree as ComposedTree;
- if (forCTree.operation == toCTree.operation)
+ if (toTree as TreeVariable != null) return null;
+ else if (toTree as ComposedTree != null)
{
- List<Substitution> result = new List<Substitution>();
- for (int forChild = 0; forChild < forCTree.children.Count; forChild++)
+ ComposedTree forCTree = forTree as ComposedTree;
+ ComposedTree toCTree = toTree as ComposedTree;
+ if (forCTree.operation == toCTree.operation)
{
- List<Substitution> childResult = findSubstitution(forCTree.children[forChild], toCTree.children[forChild]);
- if (unionSubstitutions(result, childResult) == null) return null;
+ List<Substitution> result = new List<Substitution>();
+ for (int forChild = 0; forChild < forCTree.children.Count; forChild++)
+ {
+ List<Substitution> childResult = findSubstitution(forCTree.children[forChild], toCTree.children[forChild]);
+ if (unionSubstitutions(result, childResult) == null) return null;
+ }
+ return result;
}
- return result;
+ return null;
}
- return null;
+ else throw new KontextException(forTree.coords, "Found a tree that is neither TreeVariable nor ComposedTree: "+ toTree.ToString());
}
- else if (forTree as ComposedTree != null && toTree as TreeVariable != null) return null;
- else throw new Exception("Found a tree that is neither TreeVariable nor ComposedTree: forTree: " + forTree.ToString() + ", toTree: " + toTree.ToString());
+ else throw new KontextException(forTree.coords,"Found a tree that is neither TreeVariable nor ComposedTree: " + forTree.ToString());
}
/// <summary>
@@ -208,7 +213,7 @@ namespace Ueberpruefung
if (foundSubTree) return cTree;
else return null;
}
- else throw new Exception("Found a tree that is neither TreeVariable nor ComposedTree: " + tree.ToString());
+ else throw new KontextException(tree.coords,"Found a tree that is neither TreeVariable nor ComposedTree: " + tree.ToString());
}
}
}
diff --git a/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndPartEquation.cs b/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndPartEquation.cs
index 8cc4a13..f8501ad 100644
--- a/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndPartEquation.cs
+++ b/BewerterStrukturellerInduktion/Ueberpruefung/CheckInduction/CheckIndPartEquation.cs
@@ -1,4 +1,5 @@
-using Eingabeverwaltung.Metamodell;
+using Eingabeverwaltung;
+using Eingabeverwaltung.Metamodell;
using System;
using System.Collections.Generic;
@@ -60,7 +61,7 @@ namespace Ueberpruefung.CheckInduction
else // instead of inductionvariable an inner Tree or constant is used
variableIsOnBuildingParameter = false;
if (variableIsOnBuildingParameter && ic.BuildingParameterVariables.Count == 0)
- throw new Exception("Found building constructor " + bc.name + " without building parameters!");
+ throw new KontextException(cTree.coords,"Found building constructor " + bc.name + " without building parameters!");
result &= variableIsOnBuildingParameter;
}
}
--
GitLab