Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • amxgg/bewerter-struktureller-induktion
1 result
Show changes
Commits on Source (6)
Hide whitespace changes
Inline Side-by-side
Showing
with 372 additions and 167 deletions
BewerterStrukturellerInduktion/Eingabeverwaltung/AbstactEingabeverwalter.cs → BewerterStrukturellerInduktion/Eingabeverwaltung/AbstractEingabeverwalter.cs
View file @ 11691f38
......@@ -3,11 +3,11 @@
namespace Eingabeverwaltung
{
public abstract class AbstactEingabeverwalter
public abstract class AbstractEingabeverwalter
{
protected Container inputContainer;
public AbstactEingabeverwalter()
public AbstractEingabeverwalter()
{
inputContainer = null;
}
......
BewerterStrukturellerInduktion/Eingabeverwaltung/Eingabeverwalter.cs
View file @ 11691f38
......@@ -7,7 +7,7 @@ using System.Collections.Generic;
namespace Eingabeverwaltung
{
public class Eingabeverwalter : AbstactEingabeverwalter
public class Eingabeverwalter : AbstractEingabeverwalter
{
public Eingabeverwalter() : base() { }
......@@ -135,7 +135,8 @@ namespace Eingabeverwaltung
Console.WriteLine(a.Message);
verwalteEingabe();
}
}
}
public void Eingabe_Interface(string action, string path)
{
ImmutableDictionary<string, Action<string>> eingabe = new Dictionary<string, Action<string>>
......
BewerterStrukturellerInduktion/Eingabeverwaltung/KontextException.cs
View file @ 11691f38
......@@ -2,7 +2,7 @@
namespace Eingabeverwaltung
{
internal class KontextException : Exception
public class KontextException : Exception
{
public KontextException(Coords coords, string message) : base("Error in " + coords.line + ":" + coords.column + ": " + message) { }
}
......
BewerterStrukturellerInduktion/Eingabeverwaltung/Metamodell/Error.cs
View file @ 11691f38
using System;
public class Error
namespace Eingabeverwaltung.Metamodell
{
public readonly int errorCode;
private string output;
public Error(int errorCode)
{
this.errorCode = errorCode;
output = null;
}
public Error(int errorCode, string output)
public class Error
{
this.errorCode = errorCode;
this.output = output;
}
public readonly int errorCode;
private string output;
public string Output
{
get
public Error(int errorCode)
{
return output;
this.errorCode = errorCode;
output = null;
}
set
public Error(int errorCode, string output)
{
this.errorCode = errorCode;
this.output = output;
}
public string Output
{
if (output == null) output = value;
else throw new Exception("ERROR: It was tried to change Error.output while it was set!");
get
{
return output;
}
set
{
if (output == null) output = value;
else throw new Exception("ERROR: It was tried to change Error.output while it was set!");
}
}
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Antlr.cs
View file @ 11691f38
......@@ -19,10 +19,12 @@ namespace Eingabeverwaltung.Parser
parser.BuildParseTree = true;
ADTParser.AdtContext tree = parser.adt();
IADTListener adt_Listener = new ADT_Listener(container);
Listener_Helper LH = new Listener_Helper();
IADTListener adt_Listener = new ADT_Listener(container,LH);
ParseTreeWalker.Default.Walk(adt_Listener, tree);
LH.close();
return container.ADT;
return container.ADT;
}
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Listener.cs
View file @ 11691f38
......@@ -19,23 +19,23 @@ namespace Eingabeverwaltung.Parser
private Listener_Helper LH;
public ADT_Listener(Container container)
public ADT_Listener(Container container, Listener_Helper LH)
{
this.container = container;
op_sorts = null;
LH = new Listener_Helper(null, null, null, null, null, null);
this.LH = LH;
}
public void EnterAdt([NotNull] ADTParser.AdtContext context) { }
public void ExitAdt([NotNull] ADTParser.AdtContext context)
{
Coords coords = new Coords(context);
if (LH.adt_sorts == null) throw new KontextException(coords,"adt_sorts = null at ExitAdt");
if (LH.adt_ops == null) throw new KontextException(coords,"adt_ops = null at ExitAdt");
if (LH.adt_sorts == null) LH.errors.Add(new SemanticAnalysisError(coords,"adt_sorts = null at ExitAdt"));
if (LH.adt_ops == null) LH.errors.Add(new SemanticAnalysisError(coords,"adt_ops = null at ExitAdt"));
if (LH.adt_axioms == null) LH.adt_axioms = new List<Axiom>();
if (LH.adt_sorts.Count < 1) throw new KontextException(coords,"adt_sorts is empty at ExitAdt");
if (LH.adt_ops.Count < 1) throw new KontextException(coords,"adt_ops is empty at ExitAdt");
if (LH.adt_sorts.Count < 1) LH.errors.Add(new SemanticAnalysisError(coords, "adt_sorts is empty at ExitAdt"));
if (LH.adt_ops.Count < 1) LH.errors.Add(new SemanticAnalysisError(coords, "adt_ops is empty at ExitAdt"));
container.ADT = new ADT(LH.adt_sorts, LH.adt_ops, LH.adt_axioms);
}
public void EnterName([NotNull] ADTParser.NameContext context) { }
......@@ -44,7 +44,7 @@ namespace Eingabeverwaltung.Parser
public void EnterSorts([NotNull] ADTParser.SortsContext context) => LH.adt_sorts = new List<Sort>();
public void ExitSorts([NotNull] ADTParser.SortsContext context)
{
if (LH.adt_sorts.Count < 1) throw new KontextException(new Coords(context),"adt_sorts is empty at ExitSorts");
if (LH.adt_sorts.Count < 1) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"adt_sorts is empty at ExitSorts"));
}
public void EnterSort([NotNull] ADTParser.SortContext context) { }
......@@ -66,17 +66,17 @@ namespace Eingabeverwaltung.Parser
return;
}
if (context.Parent.Parent.GetChild(0).GetText() == "vars") return; // this job is done in ExitVar
throw new KontextException(coords,"ExitSort with Context = " + context.GetText() + " in parent "+ context.Parent.GetChild(0).GetText() + " was not able to find the sense of its life.");
throw new SemanticAnalysisDeadlyError(coords,"ExitSort with Context = " + context.GetText() + " in parent "+ context.Parent.GetChild(0).GetText() + " was not able to find the sense of its life.");
}
public void EnterConstructors([NotNull] ADTParser.ConstructorsContext context) => LH.adt_ops = new List<Operation>();
public void ExitConstructors([NotNull] ADTParser.ConstructorsContext context)
{
Coords coords = new Coords(context);
if (LH.adt_ops.Count < 1) throw new KontextException(coords,"adt_ops is empty at ExitConstructors");
if (LH.adt_ops.Count < 1) LH.errors.Add(new SemanticAnalysisError(coords, "adt_ops is empty at ExitConstructors"));
// check for each sort: numer & type of constructors is ok
foreach (Sort sort in LH.adt_sorts)
if (sort.GetBuildingConstructors().Count > 0 && sort.GetBasicConstructors().Count == 0)
throw new KontextException(coords,"The sort "+sort.name+" has building constructors, but no basic constructors.");
LH.errors.Add(new SemanticAnalysisError(coords,"The sort "+sort.name+" has building constructors, but no basic constructors."));
}
public void EnterOperations([NotNull] ADTParser.OperationsContext context)
......@@ -85,14 +85,14 @@ namespace Eingabeverwaltung.Parser
}
public void ExitOperations([NotNull] ADTParser.OperationsContext context)
{
if (LH.adt_ops.Count < 1) throw new KontextException(new Coords(context),"adt_ops is empty at ExitOperations");
if (LH.adt_ops.Count < 1) LH.errors.Add(new SemanticAnalysisError(new Coords(context), "adt_ops is empty at ExitOperations"));
}
public void EnterOperation(ADTParser.OperationContext context) => op_sorts = new List<Sort>();
public void ExitOperation(ADTParser.OperationContext context)
{
Coords coords = new Coords(context);
if (op_sorts.Count < 1) throw new KontextException(coords,"op_sorts is empty at ExitOperation");
if (op_sorts.Count < 1) LH.errors.Add(new SemanticAnalysisError(coords, "op_sorts is empty at ExitOperation"));
string operationName = context.BEZ().GetText();
Test_Operations_all_unique(operationName,new Coords(context));
Operation operation;
......@@ -107,7 +107,7 @@ namespace Eingabeverwaltung.Parser
else operation = new BuildingConstructor(operationName, op_sorts);
op_sorts.Last().SetConstructor((Constructor)operation);
}
else throw new KontextException(coords,"ExitOperation with Context = " + context.GetText() + " in parent " + context.Parent.GetChild(0).GetText() + " was not able to find the sense of its life.");
else throw new SemanticAnalysisDeadlyError(coords,"ExitOperation with Context = " + context.GetText() + " in parent " + context.Parent.GetChild(0).GetText() + " was not able to find the sense of its life.");
LH.adt_ops.Add(operation);
}
......@@ -121,7 +121,7 @@ namespace Eingabeverwaltung.Parser
public void EnterAxioms([NotNull] ADTParser.AxiomsContext context) => LH.adt_axioms = new List<Axiom>();
public void ExitAxioms([NotNull] ADTParser.AxiomsContext context)
{
if (LH.adt_axioms.Count < 1) throw new KontextException(new Coords(context),"adt_axioms is empty at ExitAxioms");
if (LH.adt_axioms.Count < 1) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"adt_axioms is empty at ExitAxioms"));
}
public void EnterAxiom([NotNull] ADTParser.AxiomContext context) => LH.trees = new List<Tree>();
......@@ -185,7 +185,7 @@ namespace Eingabeverwaltung.Parser
/// <param name="sortName"></param>
private void Test_Sorts_all_unique(string sortName, Coords coords)
{
if (LH.findSortInADT_Sorts(sortName) != null) throw new KontextException(coords,"The Sort " + sortName + " was defined more than 1 times in Sorts of ADT!");
if (LH.findSortInADT_Sorts(sortName) != null) LH.errors.Add(new SemanticAnalysisError(coords,"The Sort " + sortName + " was defined more than 1 times in Sorts of ADT!"));
}
/// <summary>
/// This Test is activated always when a new Operation gets added to the operationList of the ADT,
......@@ -194,7 +194,7 @@ namespace Eingabeverwaltung.Parser
/// <param name="operationName"></param>
private void Test_Operations_all_unique(string operationName, Coords coords)
{
if (LH.findOperationInADT_Ops(operationName,0,false,coords) != null) throw new KontextException(coords,"The Operation " + operationName + " was defined more than 1 times in Operations of ADT!");
if (LH.findOperationInADT_Ops(operationName,0,false,coords) != null) LH.errors.Add(new SemanticAnalysisError(coords, "The Operation " + operationName + " was defined more than 1 times in Operations of ADT!"));
}
/// <summary>
/// This Test is activated always when a new Sort gets added to the sortList of an Operation,
......@@ -203,7 +203,7 @@ namespace Eingabeverwaltung.Parser
/// <param name="sortName"></param>
private void Test_Operation_all_Sorts_were_defined_in_ADT(string sortName, Coords coords)
{
if (LH.findSortInADT_Sorts(sortName) == null) throw new KontextException(coords,"Found a Sort " + sortName + " in Operations that was not defined in Sorts!");
if (LH.findSortInADT_Sorts(sortName) == null) LH.errors.Add(new SemanticAnalysisError(coords, "Found a Sort " + sortName + " in Operations that was not defined in Sorts!"));
}
/// <summary>
/// This Test is activated always when a new Axiom gets added to the axiomList of the ADT,
......@@ -214,7 +214,7 @@ namespace Eingabeverwaltung.Parser
{
foreach (Axiom axiom in LH.adt_axioms)
{
if (axiom.name == axiomName) throw new KontextException(coords,"The Axiom " + axiomName + " was defined more than 1 times in Axioms of ADT!");
if (axiom.name == axiomName) LH.errors.Add(new SemanticAnalysisError(coords, "The Axiom " + axiomName + " was defined more than 1 times in Axioms of ADT!"));
}
}
/// <summary>
......
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
View file @ 11691f38
......@@ -21,17 +21,44 @@ namespace Eingabeverwaltung.Parser
public Equation equation;
// Tree
public List<Tree> trees;
public Listener_Helper(List<Sort> adt_sorts, List<Operation> adt_ops, List<Variable> adt_vars, List<Axiom> adt_axioms, Equation equation, List<Tree> trees)
// Errors and Warnings
public List<SemanticAnalysisError> errors;
public List<SemanticAnalysisWarning> warnings;
public Listener_Helper() : this(null,null,null) { }
public Listener_Helper(List<Sort> adt_sorts, List<Operation> adt_ops, List<Axiom> adt_axioms)
{
this.adt_sorts = adt_sorts;
this.adt_ops = adt_ops;
this.adt_vars = adt_vars;
this.adt_vars = null;
this.adt_axioms = adt_axioms;
this.equation = equation;
this.trees = trees;
this.equation = null;
this.trees = null;
allQVars = new List<Variable>();
fixedVars = new List<Variable>();
}
errors = new List<SemanticAnalysisError>();
warnings = new List<SemanticAnalysisWarning>();
}
/// <summary>
/// Closes the Listener_Helper printing all errors and warnings
/// </summary>
public void close()
{
string errorMessage = "Errors:\r\n";
foreach(SemanticAnalysisError error in errors)
errorMessage += error.message+"\r\n";
string warningMessage = "Warnings:\r\n";
foreach(SemanticAnalysisWarning warning in warnings)
warningMessage += warning.message + "\r\n";
if (errors.Count != 0)
if (warnings.Count != 0) throw new Exception(errorMessage+warningMessage);
else throw new Exception(errorMessage);
// TODO: How warnings?
// print warnings in Ausgabeverwalter of ProgramForHuman / ProgramForYapex
}
// Equation
public void EnterEq()
{
......@@ -41,8 +68,14 @@ namespace Eingabeverwaltung.Parser
}
public void ExitEq(Coords coords)
{
if (trees.Count != 2) throw new KontextException(coords,"Calculated " + trees.Count + " Trees in Equation! The Trees are: " + TreeListToString(trees));
Test_Equation_both_sides_have_same_Sort(trees[0], trees[1],coords);
if (trees.Count == 2) Test_Equation_both_sides_have_same_Sort(trees[0], trees[1], coords);
else
{
errors.Add(new SemanticAnalysisError(coords, "Calculated " + trees.Count + " Trees in Equation! The Trees are: " + TreeListToString(trees)));
while (trees.Count < 2)
trees.Add(null);
}
equation = new Equation(trees[0], trees[1], adt_vars);
}
......@@ -79,34 +112,32 @@ namespace Eingabeverwaltung.Parser
if (operation != null)
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!");
if (result == null) errors.Add(new SemanticAnalysisError(coords,"The Tree " + treeName + " could not be found in Vars or Operations of the ADT!"));
trees.Add(result);
}
public void ExitTreeNode(string treeName, int context_ChildCount, string context_Text, Coords coords)
{
int childCount = (int)Math.Ceiling(((double)(context_ChildCount - 3)) / 2); // -1 for BEZ, -1 for "(", -1 for ")", ceiling(/2) = -1 for each "," between 2 children
// All children of current tree are in this.trees because inner trees 1st, but sure is sure
if (trees.Count >= childCount)
Operation operation = findOperationInADT_Ops(treeName, childCount,coords);
if (operation == null) throw new SemanticAnalysisDeadlyError(coords,"The Tree " + treeName + " could not be found in Operations of the ADT!"); // deadly because how much trees to remove from trees then?
List<Tree> children = new List<Tree>();
for (int i = 0; i < childCount; i++) // childCount because to better coordinate with the input
{
Operation operation = findOperationInADT_Ops(treeName, childCount,coords);
if (operation == null) throw new KontextException(coords,"The Tree " + treeName + " could not be found in Operations of the ADT!");
List<Tree> children = new List<Tree>();
for (int i = 0; i < operation.sorts.Count - 1; i++)
if (trees.Count == 0)
{
if (trees.Count == 0)
throw new KontextException(coords,"Not enough created trees for the current tree! CurrentTreeName: " + treeName + "\n Context: " + context_Text + "\n added children: " + TreeListToString(children));
children.Add(trees.Last());
trees.RemoveAt(trees.Count - 1);
errors.Add(new SemanticAnalysisError(coords, "Not enough created trees for the current tree! CurrentTreeName: " + treeName + "\n Context: " + context_Text + "\n added children: " + TreeListToString(children)));
for (int j = i; j < operation.sorts.Count -1; j++)
children.Add(null);
break;
}
children.Reverse();
Test_ComposedTree_Children_Sorts_are_correct(operation, children);
Tree currentTree = new ComposedTree(coords, operation, children);
trees.Add(currentTree);
}
else
{
throw new KontextException(coords,"Not all childen of the current Tree " + treeName + " are in trees!");
children.Add(trees.Last());
trees.RemoveAt(trees.Count - 1);
}
children.Reverse();
Test_ComposedTree_Children_Sorts_are_correct(operation, children,coords);
Tree currentTree = new ComposedTree(coords, operation, children);
trees.Add(currentTree);
}
// function Trees
......@@ -115,7 +146,6 @@ namespace Eingabeverwaltung.Parser
/// </summary>
/// <param name="treeName"></param>
/// <param name="coords"></param>
/// <exception cref="KontextException"></exception>
public void ExitFTreeBez(string treeName, Coords coords)
{
Tree result = null;
......@@ -128,7 +158,7 @@ namespace Eingabeverwaltung.Parser
if (operation != null)
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!");
if (result == null) errors.Add(new SemanticAnalysisError(coords,"The Tree " + treeName + " could not be found in Vars or Operations of the ADT!"));
trees.Add(result);
}
......@@ -137,6 +167,7 @@ namespace Eingabeverwaltung.Parser
/// ExitFTreeRoot builds the next incomplete Composed Tree.
/// </summary>
/// <param name="coords"></param>
/// <exception cref="SemanticAnalysisDeadlyError"> </exception>
public void ExitFTreeRoot(Coords coords)
{
for (int rootPos = trees.Count - 1; rootPos>= 0; rootPos--)
......@@ -162,10 +193,10 @@ namespace Eingabeverwaltung.Parser
}
}
break;
default: throw new KontextException(coords, "Found a Tree " + currentTree.name+ " that is neither TreeVariable nor ComposedTree!");
default: throw new SemanticAnalysisDeadlyError(coords, "Found a Tree " + currentTree.name+ " that is neither TreeVariable nor ComposedTree!");
}
}
throw new KontextException(coords, "ExitFTreeRoot could not find the composed tree which needs to be build.");
throw new SemanticAnalysisDeadlyError(coords, "ExitFTreeRoot could not find the composed tree which needs to be build.");
}
// Helping functions
......@@ -314,19 +345,24 @@ namespace Eingabeverwaltung.Parser
private void Test_ComposedTree_ChildCount_is_corrent(Operation operation, int inputtedChildCount, Coords coords)
{
if (operation.sorts.Count != inputtedChildCount + 1)
throw new KontextException(coords,"The Operation_Tree " + operation.name + " was inputted with " + inputtedChildCount + " children, expected " + (operation.sorts.Count - 1) + " children!");
errors.Add(new SemanticAnalysisError(coords,"The Operation_Tree " + operation.name + " was inputted with " + inputtedChildCount + " children, expected " + (operation.sorts.Count - 1) + " children!"));
}
private void Test_ComposedTree_Children_Sorts_are_correct(Operation operation, List<Tree> children) => Test_ComposedTree_Children_Sorts_are_correct(operation, children, new Coords(-1,-1));
private void Test_ComposedTree_Children_Sorts_are_correct(Operation operation, List<Tree> children, Coords coords)
{
for (int i = 0; i < children.Count; i++)
{
string type = "";
if (children[i] as ComposedTree != null) type = "ComposedTree";
else type = "Variable";
if (children[i] is ComposedTree) type = "ComposedTree";
else if (children[i] is TreeVariable) type = "Variable";
else if (children[i] == null) { if (errors.Count == 0) errors.Add(new SemanticAnalysisError(coords, "The child number "+i+" of the tree "+operation.name+" is null.")); continue; }
else throw new SemanticAnalysisDeadlyError(coords, "Found a Tree " + children[i].name + " that is neither TreeVariable nor ComposedTree!");
if (children[i].sort == null) { if (errors.Count == 0) errors.Add(new SemanticAnalysisError(coords, "The sort child number " + i + " of the tree " + operation.name + " is null.")); continue; }
if (operation.sorts[i] == null) { if (errors.Count == 0) errors.Add(new SemanticAnalysisError(coords, "The sort child number " + i + " of the operation " + operation.name + " is null.")); continue; }
if (operation == null) Console.WriteLine("operation is null ");
if (children[i].sort != operation.sorts[i])
throw new KontextException(coords,"Error while building the tree " + operation.name + ": The the child (" + type + ") " + children[i].name
+" with the Sort " + children[i].sort.name + " is not " + operation.sorts[i].name + "!");
errors.Add(new SemanticAnalysisError(coords, "Error while building the tree " + operation.name + ": The the child (" + type + ") " + children[i].name
+ " with the Sort " + children[i].sort.name + " is not " + operation.sorts[i].name + "!"));
}
}
/// <summary>
......@@ -338,8 +374,11 @@ namespace Eingabeverwaltung.Parser
private void Test_Tree_Variables_were_defined_in_ADT() {/* Nothing here need to be. */}
private void Test_Equation_both_sides_have_same_Sort(Tree leftTree, Tree rightTree, Coords coords)
{
if (leftTree.sort.name != rightTree.sort.name)
throw new KontextException(coords,"The Equation has not the same Sort on its 2 sides! Sort of leftTree: " + leftTree.sort.name + " Sort of rightTree: " + rightTree.sort.name);
try
{
if (leftTree.sort.name != rightTree.sort.name)
errors.Add(new SemanticAnalysisError(coords, "The Equation has not the same Sort on its 2 sides! Sort of leftTree: " + leftTree.sort.name + " Sort of rightTree: " + rightTree.sort.name));
}catch(NullReferenceException) { errors.Add(new SemanticAnalysisError(coords, "One or more sides of one Equation are null!")); }
}
/// <summary>
......@@ -349,7 +388,7 @@ namespace Eingabeverwaltung.Parser
/// <param name="sortName"></param>
private void Test_Variable_Sort_was_defined_in_ADT(string sortName, Coords coords)
{
if (findSortInADT_Sorts(sortName) == null) throw new KontextException(coords,"Found a Sort " + sortName + " in Variable that was not defined in Sorts!");
if (findSortInADT_Sorts(sortName) == null) errors.Add(new SemanticAnalysisError(coords,"Found a Sort " + sortName + " in Variable that was not defined in Sorts!"));
}
/// <summary>
......@@ -361,7 +400,7 @@ namespace Eingabeverwaltung.Parser
{
if (findVariableInADT_Vars(variableName) != null
|| findVariableInAllQVarsOrFixedVars(variableName) != null
) throw new KontextException(coords,"The Variable " + variableName + " was defined more than 1 times.!");
) errors.Add(new SemanticAnalysisError(coords,"The Variable " + variableName + " was defined more than 1 times.!"));
}
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Antlr.cs
View file @ 11691f38
......@@ -24,12 +24,14 @@ namespace Eingabeverwaltung.Parser
ProofParser.ProofContext tree = parser.proof();
// create Proof without TransformationSteps
IProofListener PL = new Proof_Listener(container);
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);
IProofListener TL = new TransformationStep_Listener(container,LH);
ParseTreeWalker.Default.Walk(TL, tree);
LH.close();
}
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
View file @ 11691f38
......@@ -34,10 +34,10 @@ namespace Eingabeverwaltung.Parser
// Transformation parts
private Tree startTree;
public Proof_Listener(Container container)
public Proof_Listener(Container container, Listener_Helper LH)
{
this.container = container;
LH = new Listener_Helper(container.ADT.sorts, container.ADT.operations, null, container.ADT.axioms, null, null);
this.LH = LH;
mainProof = null;
lemmata = null;
......@@ -55,7 +55,7 @@ namespace Eingabeverwaltung.Parser
public void EnterProof([NotNull] ProofParser.ProofContext context) => lemmata = new List<Lemma>();
public void ExitProof([NotNull] ProofParser.ProofContext context)
{
if (mainProof == null) throw new KontextException(new Coords(context),"No main proof found in ExitProof!");
if (mainProof == null) throw new SemanticAnalysisDeadlyError(new Coords(context),"No main proof found in ExitProof!");
container.Proof = new Proof(mainProof, lemmata);
}
public void EnterMainProof([NotNull] ProofParser.MainProofContext context)
......@@ -96,7 +96,7 @@ namespace Eingabeverwaltung.Parser
public void EnterSingleProof([NotNull] ProofParser.SingleProofContext context) => SP = null;
public void ExitSingleProof([NotNull] ProofParser.SingleProofContext context)
{
if (SP == null) throw new KontextException(new Coords(context),"No SingleProof found in ExitSingleProof!");
if (SP == null) throw new SemanticAnalysisDeadlyError(new Coords(context),"No SingleProof found in ExitSingleProof!");
}
public void EnterProof_end([NotNull] ProofParser.Proof_endContext context) { }
public void ExitProof_end([NotNull] ProofParser.Proof_endContext context) { }
......@@ -111,7 +111,7 @@ namespace Eingabeverwaltung.Parser
public void EnterStart_tree([NotNull] ProofParser.Start_treeContext context) => LH.trees = new List<Tree>();
public void ExitStart_tree([NotNull] ProofParser.Start_treeContext context)
{
if (LH.trees.Count != 1) throw new KontextException(new Coords(context),"Trees was Expected to have 1 Tree for Start_tree, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
if (LH.trees.Count != 1) throw new SemanticAnalysisDeadlyError(new Coords(context), "Trees was Expected to have 1 Tree for Start_tree, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
startTree = LH.trees[0];
}
......@@ -153,10 +153,9 @@ namespace Eingabeverwaltung.Parser
foreach (SingleTask lemmaTask in container.Task.lemmaTasks)
if (lemmaTask.name == proofName) { indVar = lemmaTask.indVariable; lemmaIndVarTask = lemmaTask; break; }
}
else throw new KontextException(coords,"ExitInduction with Context = " + context.GetText() + " was not able to find the sense of its life.");
else throw new SemanticAnalysisDeadlyError(coords,"ExitInduction with Context = " + context.GetText() + " was not able to find the sense of its life.");
}
if (indVar == null) throw new KontextException(coords,"Induction variable of proof "+ proofName + " is neither definied in proof nor in task!");
Equation eq = null; List<Variable> fixedVars = null;
if (lemmaDef != null)
{// this SP is in lemma lemmaDef
......@@ -165,11 +164,12 @@ namespace Eingabeverwaltung.Parser
{// this SP is in Mainproof
eq = container.Task.task.eq; fixedVars = container.Task.task.fixedVars;
}
if (lemmaIndVarTask != null)
if (indVar == null) LH.errors.Add(new SemanticAnalysisError(coords, "Induction variable of proof " + proofName + " is neither definied in proof nor in task!"));
else if (lemmaIndVarTask != null)
{ // inVar must be of context of its lemma: find substitution to get correct variable.
Ueberpruefung.CheckHelper.getSubsAndRenamings(eq, lemmaIndVarTask.eq, out List<Substitution> subs, out List<Substitution> renamings);
bool changed = false;
if (subs != null) // then lemma is not proving the task (error 22), do nothing then
if (subs != null) // else lemma is not proving the task (error 22), do nothing then
foreach(Substitution renaming in renamings)
if (renaming.tree is TreeVariable tv)
if (tv.variable == indVar) { indVar = renaming.variable; changed = true; break; }
......@@ -181,7 +181,7 @@ namespace Eingabeverwaltung.Parser
{
string variableName = context.BEZ().GetText();
Variable variable = LH.findVariableInADT_Vars(variableName);
if (variable == null) throw new KontextException(new Coords(context),"Could not find Induction variable " + variableName + " in current context of variables.");
if (variable == null) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"Could not find Induction variable " + variableName + " in current context of variables."));
indVar = variable;
}
public void ExitInd_var([NotNull] ProofParser.Ind_varContext context) { }
......@@ -191,7 +191,7 @@ namespace Eingabeverwaltung.Parser
Coords coords = new Coords(context);
if (SP is Transformation tr)
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!");
else throw new SemanticAnalysisDeadlyError(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)
......@@ -199,7 +199,7 @@ namespace Eingabeverwaltung.Parser
Coords coords = new Coords(context);
if (SP is Transformation tr)
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!");
else throw new SemanticAnalysisDeadlyError(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)
......@@ -210,10 +210,9 @@ namespace Eingabeverwaltung.Parser
name = context.BEZ().GetText();
else name = "IH";
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(coords,name,LH.equation, LH.fixedVars));
if (ih.name == name) LH.errors.Add(new SemanticAnalysisError(coords,"There are more then 1 inductionhypothesis with name "+name+"!"));
Test_Lemmata_all_Unique(name, "InductionHypothesis", coords);
indHyps.Add(new InductionHypothesis(coords, name, LH.equation, LH.fixedVars));
}
public void EnterInd_case([NotNull] ProofParser.Ind_caseContext context) { }
public void ExitInd_case([NotNull] ProofParser.Ind_caseContext context)
......@@ -290,11 +289,11 @@ namespace Eingabeverwaltung.Parser
private void Test_Lemmata_all_Unique(string name, string type, Coords coords)
{
foreach (Rule axiom in LH.adt_axioms)
if (axiom.name == name) throw new KontextException(coords,"The " + type + " "+ name + " has same name like 1 Axiom of ADT!");
foreach (Rule lemma in lemmata)
if (lemma.name == name) throw new KontextException(coords,"The " + type + " "+ name + " has same name like 1 Lemma of Proof!");
if (axiom.name == name) LH.errors.Add(new SemanticAnalysisError(coords,"The " + type + " "+ name + " has same name like 1 Axiom of ADT!"));
foreach (Rule lemma in lemmata)
if (lemma.name == name) LH.errors.Add(new SemanticAnalysisError(coords, "The " + type + " " + name + " has same name like 1 Lemma of Proof!"));
foreach (Rule lemma in container.Task.lemmata)
if (lemma.name == name) throw new KontextException(coords,"The " + type + " "+ name + " has same name like 1 Lemma of Task!");
if (lemma.name == name) LH.errors.Add(new SemanticAnalysisError(coords, "The " + type + " " + name + " has same name like 1 Lemma of Task!"));
}
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/SemanticAnalysisDeadlyError.cs 0 → 100644
View file @ 11691f38
namespace Eingabeverwaltung.Parser
{
public class SemanticAnalysisDeadlyError : KontextException
{
public SemanticAnalysisDeadlyError(Coords coords, string message) : base(coords,message) { }
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/SemanticAnalysisError.cs 0 → 100644
View file @ 11691f38
namespace Eingabeverwaltung.Parser
{
public class SemanticAnalysisError
{
public readonly string message;
public SemanticAnalysisError(Coords coords, string message)
{
this.message = "Error in " + coords.line + ":" + coords.column + ": " + message;
}
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/SemanticAnalysisWarning.cs 0 → 100644
View file @ 11691f38
namespace Eingabeverwaltung.Parser
{
public class SemanticAnalysisWarning
{
public readonly string message;
public SemanticAnalysisWarning(Coords coords, string message)
{
this.message = "Warning in " + coords.line + ":" + coords.column + ": " + message;
}
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Antlr.cs
View file @ 11691f38
......@@ -22,9 +22,11 @@ namespace Eingabeverwaltung.Parser
parser.BuildParseTree = true;
TaskParser.TaskContext tree = parser.task();
ITaskListener adt_Listener = new Task_Listener(container);
Listener_Helper LH = new Listener_Helper(container.ADT.sorts, container.ADT.operations, container.ADT.axioms);
TaskParser.TaskContext tree = parser.task();
ITaskListener adt_Listener = new Task_Listener(container,LH);
ParseTreeWalker.Default.Walk(adt_Listener, tree);
}
LH.close();
}
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Task_Listener.cs
View file @ 11691f38
......@@ -34,11 +34,11 @@ namespace Eingabeverwaltung.Parser
/// Requires a Container with filled ADT
/// </summary>
/// <param name="container"></param>
public Task_Listener(Container container)
public Task_Listener(Container container, Listener_Helper LH)
{
this.container = container;
LH = new Listener_Helper(container.ADT.sorts,container.ADT.operations, null, container.ADT.axioms, null, null);
this.LH = LH;
lemmata = new List<TaskLemma>();
mainTask = null;
......@@ -62,7 +62,7 @@ namespace Eingabeverwaltung.Parser
public void EnterTask_eq([NotNull] TaskParser.Task_eqContext context) { }
public void ExitTask_eq([NotNull] TaskParser.Task_eqContext context)
{
if (mainConfig == null) throw new KontextException(new Coords(context),"No Config found for main task!");
if (mainConfig == null) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"No Config found for main task!"));
mainTask = new SingleTask("main task", LH.equation, LH.fixedVars, mainConfig, indVar);
indVar = null;
}
......@@ -75,7 +75,7 @@ namespace Eingabeverwaltung.Parser
Coords coords = new Coords(context);
string lemmaName = context.BEZ().GetText();
Test_Lemmata_all_Unique(lemmaName,coords);
if (mainConfig == null) throw new KontextException(coords,"No Config found for lemma " + lemmaName);
if (mainConfig == null) LH.errors.Add(new SemanticAnalysisError(coords,"No Config found for lemma " + lemmaName));
lemmaTasks.Add(new SingleTask(lemmaName,LH.equation, LH.fixedVars, mainConfig, indVar));
indVar = null;
}
......@@ -96,10 +96,11 @@ namespace Eingabeverwaltung.Parser
string variableName = context.BEZ().GetText();
Variable variable = LH.findVariableInADT_Vars(variableName);
Coords coords = new Coords(context);
if (!LH.allQVars.Contains(variable))
throw new KontextException(coords,"Induction variable for task "+ context.Parent.GetChild(0).GetText()+" was not definied as allquantified before.");
if (variable.sort.GetConstructors().Count == 0)
throw new KontextException(coords,"Induction variable for task " + context.Parent.GetChild(0).GetText()+" has no constructors!");
if (!LH.allQVars.Contains(variable))
LH.errors.Add(new SemanticAnalysisError(coords,"Induction variable for task "+ context.Parent.GetChild(0).GetText()+" was not definied as allquantified before."));
else
if (variable.sort.GetConstructors().Count == 0)
LH.errors.Add(new SemanticAnalysisError(coords,"Induction variable for task " + context.Parent.GetChild(0).GetText()+" has no constructors!"));
indVar = variable;
}
public void ExitInd_var([NotNull] TaskParser.Ind_varContext context) { }
......@@ -120,11 +121,12 @@ namespace Eingabeverwaltung.Parser
{
Coords coords = new Coords(context);
string taskName = context.Parent.Parent.GetChild(0).GetText();
if (indVar == null) throw new KontextException(coords,"Config for induction can't find its relation to induction variable!");
if (indCaseConfigs.Count < indVar.sort.GetConstructors().Count)
throw new KontextException(coords,"There are " + (indVar.sort.GetConstructors().Count - indCaseConfigs.Count)
+ " missing cases for Config of induction for task " + taskName);
if (indHypConfig == null) throw new KontextException(coords,"No Config for Inductionhypotheses found for task " + taskName);
if (indVar == null)
LH.errors.Add(new SemanticAnalysisError(coords,"Config for induction can't find its relation to induction variable!"));
else if (indCaseConfigs.Count < indVar.sort.GetConstructors().Count)
LH.errors.Add(new SemanticAnalysisError(coords,"There are " + (indVar.sort.GetConstructors().Count - indCaseConfigs.Count)
+ " missing cases for Config of induction for task " + taskName));
if (indHypConfig == null) LH.errors.Add(new SemanticAnalysisError(coords,"No Config for Inductionhypotheses found for task " + taskName));
mainConfig = new InductionConfig(indCaseConfigs, indHypConfig);
}
public void EnterCase_pt([NotNull] TaskParser.Case_ptContext context) { singleConfig = null; }
......@@ -133,9 +135,9 @@ namespace Eingabeverwaltung.Parser
Coords coords = new Coords(context);
string constructorName = context.BEZ().GetText();
Operation constructor = LH.findOperationInADT_Ops(constructorName, 0, false,coords);
if (constructor as Constructor == null) throw new KontextException(coords,"The induction case config refers not to a constructor: " + constructorName + "!");
if (singleConfig == null) throw new KontextException(coords,"No config found for induction case " + constructorName + "!");
indCaseConfigs.Add(new InductionCaseConfig((Constructor)constructor, singleConfig));
if (constructor as Constructor == null) LH.errors.Add(new SemanticAnalysisError(coords,"The induction case config refers not to a constructor: " + constructorName + "!"));
if (singleConfig == null) LH.errors.Add(new SemanticAnalysisError(coords,"No config found for induction case " + constructorName + "!"));
indCaseConfigs.Add(new InductionCaseConfig(constructor as Constructor, singleConfig));
}
public void EnterIh_pt([NotNull] TaskParser.Ih_ptContext context) { maxPt = -1; minSteps = -1; maxSteps = -1; }
public void ExitIh_pt([NotNull] TaskParser.Ih_ptContext context) { indHypConfig = new SingleConfig(maxPt, minSteps, maxSteps); }
......@@ -144,9 +146,9 @@ namespace Eingabeverwaltung.Parser
public void ExitTask_pt([NotNull] TaskParser.Task_ptContext context)
{
Coords coords = new Coords(context);
if (maxPt < 0) throw new KontextException(coords,"No maxPt found!");
if (minSteps < 0) throw new KontextException(coords,"No minsteps found!");
if (maxSteps < 0) throw new KontextException(coords,"No maxsteps found!");
if (maxPt < 0) LH.errors.Add(new SemanticAnalysisError(coords,"No maxPt found!"));
if (minSteps < 0) LH.errors.Add(new SemanticAnalysisError(coords,"No minsteps found!"));
if (maxSteps < 0) LH.errors.Add(new SemanticAnalysisError(coords,"No maxsteps found!"));
singleConfig = new SingleConfig(maxPt, minSteps, maxSteps);
}
public void EnterMaxpt([NotNull] TaskParser.MaxptContext context) { }
......@@ -221,11 +223,11 @@ namespace Eingabeverwaltung.Parser
private void Test_Lemmata_all_Unique(string lemmaName,Coords coords)
{
foreach (Rule axiom in LH.adt_axioms)
if (axiom.name == lemmaName) throw new KontextException(coords,"The Lemma " + lemmaName + " has same name like 1 Axiom of ADT!");
if (axiom.name == lemmaName) LH.errors.Add(new SemanticAnalysisError(coords,"The Lemma " + lemmaName + " has same name like 1 Axiom of ADT!"));
foreach (Rule lemma in lemmata)
if (lemma.name == lemmaName) throw new KontextException(coords,"The Lemma " + lemmaName + " is defined multiple times in Task!");
if (lemma.name == lemmaName) LH.errors.Add(new SemanticAnalysisError(coords,"The Lemma " + lemmaName + " is defined multiple times in Task!"));
foreach (Rule lemma in lemmaTasks)
if (lemma.name == lemmaName) throw new KontextException(coords,"The Lemma " + lemmaName + " is defined multiple times in Task!");
if (lemma.name == lemmaName) LH.errors.Add(new SemanticAnalysisError(coords,"The Lemma " + lemmaName + " is defined multiple times in Task!"));
}
}
}
BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
View file @ 11691f38
......@@ -38,7 +38,7 @@ namespace Eingabeverwaltung.Parser
private Transformation_Step TS;
private List<Transformation_Step> TSs;
public TransformationStep_Listener(Container container)
public TransformationStep_Listener(Container container, Listener_Helper LH)
{
this.container = container;
currentTR = null;
......@@ -46,7 +46,7 @@ namespace Eingabeverwaltung.Parser
currentIndCase = null;
currentIndCaseIndex = -1;
currentLemma = null;
LH = new Listener_Helper(container.ADT.sorts, container.ADT.operations, null, container.ADT.axioms, null, null);
this.LH = LH;
TS = null;
TSs = null;
......@@ -58,7 +58,7 @@ namespace Eingabeverwaltung.Parser
{
if (container.Proof.proof is Transformation tr) currentTR = tr;
else if (container.Proof.proof is Induction ind) currentInd = ind; // will find tr by ind rules
else throw new KontextException(new Coords(context),"Error: The proof of MainProof is wether Transformation nor Induction!");
else throw new SemanticAnalysisDeadlyError(new Coords(context),"Error: The proof of MainProof is neither Transformation nor Induction!");
// Variablen der Aufgabenstellung gelten im Hauptbeweis als erstes
List<List<Variable>> variableDefinitionContext;
variableDefinitionContext = new List<List<Variable>>() { container.Task.task.eq.variables };
......@@ -76,10 +76,10 @@ namespace Eingabeverwaltung.Parser
currentLemma = null;
foreach(Lemma lemma in container.Proof.lemmata)
if (lemma.name == lemmaName) currentLemma = lemma;
if (currentLemma == null) throw new KontextException(coords,"Cannot find current Lemma: "+lemmaName+" in Container!");
if (currentLemma == null) throw new SemanticAnalysisDeadlyError(coords,"Cannot find current Lemma: "+lemmaName+" in Container!");
if (currentLemma.proof is Transformation tr) currentTR = tr;
else if (currentLemma.proof is Induction ind) currentInd = ind; // will find tr by ind rules
else throw new KontextException(coords,"Error: The proof of Lemma "+lemmaName+" is wether Transformation nor Induction!");
else throw new SemanticAnalysisDeadlyError(coords,"Error: The proof of Lemma "+lemmaName+" is neither Transformation nor Induction!");
}
public void ExitLemma([NotNull] ProofParser.LemmaContext context) => currentLemma = null;
......@@ -103,7 +103,7 @@ namespace Eingabeverwaltung.Parser
public void EnterTransformation([NotNull] ProofParser.TransformationContext context) => TSs = new List<Transformation_Step>();
public void ExitTransformation([NotNull] ProofParser.TransformationContext context)
{
if (TSs.Count < 1) throw new KontextException(new Coords(context),"No TransformationSteps found in Transformation at ExitTransformation!");
if (TSs.Count < 1) throw new SemanticAnalysisDeadlyError(new Coords(context),"No TransformationSteps found in Transformation at ExitTransformation!");
Tree startT = currentTR.startTree;
for (int i = 0; i < TSs.Count; i++)
{
......@@ -128,6 +128,10 @@ namespace Eingabeverwaltung.Parser
{
Coords coords = new Coords(context);
Rule rule = null;
// begin preparation for exception case (this is for exception case to avoid NullReferenceException on reading TS.rule.eq)
Tree exceptionTree = new TreeVariable(new Variable("", new Sort("")));
Equation exeptionEquation = new Equation(exceptionTree, exceptionTree, new List<Variable>());
// end preparation for exception case
if (context.BEZ() != null)
{
string ruleName = context.BEZ().GetText();
......@@ -151,9 +155,9 @@ namespace Eingabeverwaltung.Parser
{
rule = findRuleIn(ruleName, currentInd.indHyps.Cast<Rule>().ToList());
if (rule != null) TS.rule = rule;
else throw new KontextException(coords,"The rule " + ruleName + " is not defined!");
else { LH.errors.Add(new SemanticAnalysisError(coords, "The rule " + ruleName + " is not defined!")); TS.rule = new InductionHypothesis(coords, ruleName, exeptionEquation, new List<Variable>()); }
}
else throw new KontextException(coords,"The rule " + ruleName + " is not defined!");
else { LH.errors.Add(new SemanticAnalysisError(coords, "The rule " + ruleName + " is not defined!")); TS.rule = new InductionHypothesis(coords, ruleName, exeptionEquation, new List<Variable>()); }
}
}
}
......@@ -161,18 +165,9 @@ namespace Eingabeverwaltung.Parser
}
else if (context.GetChild(0).GetText() == "IH")
{
if (currentInd != null) rule = findRuleIn("IH", currentInd.indHyps.Cast<Rule>().ToList()); ;
if (currentInd != null) rule = findRuleIn("IH", currentInd.indHyps.Cast<Rule>().ToList());
if (rule != null) TS.rule = rule;
else
{
string position = "";
if (currentLemma == null) position += "main proof > ";
else position += "lemma: " + currentLemma.name + " > ";
if (currentInd != null) position += "induction ";
if (currentIndCase != null) position += " of case " + currentIndCase.type + " > ";
position += " TransformationStep No " + (TSs.Count+1);
throw new KontextException(coords,"The Inductionhypothesis is not defined for the current TransformationStep (" + position + ")!");
}
else { LH.errors.Add(new SemanticAnalysisError(coords,"The Inductionhypothesis is not defined for the current TransformationStep!")); TS.rule = new InductionHypothesis(coords,"IH", exeptionEquation, new List<Variable>()); }
}
}
......@@ -184,14 +179,15 @@ namespace Eingabeverwaltung.Parser
{
case "rl": TS.direction = '<'; break;
case "lr": TS.direction = '>'; break;
default: throw new KontextException(new Coords(context),"The Direction of the TransformationStep is undefined! Expected \'rl\' or \'lr' but found \"" + direction + "\".");
default: LH.errors.Add(new SemanticAnalysisError(new Coords(context),"The Direction of the TransformationStep is undefined! Expected \'rl\' or \'lr\' but found \"" + direction + "\"."));
TS.direction = '>'; break;
}
}
public void EnterTermpart([NotNull] ProofParser.TermpartContext context) => LH.trees = new List<Tree>();
public void ExitTermpart([NotNull] ProofParser.TermpartContext context)
{
if (LH.trees.Count != 1) throw new KontextException(new Coords(context),"Trees was Expected to have 1 Tree for Termpart, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
if (LH.trees.Count != 1) throw new SemanticAnalysisDeadlyError(new Coords(context), "Trees was Expected to have 1 Tree for Termpart, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
TS.termpart = LH.trees[0];
LH.trees = null;
}
......@@ -217,17 +213,17 @@ namespace Eingabeverwaltung.Parser
public void ExitSub([NotNull] ProofParser.SubContext context)
{
Coords coords = new Coords(context);
if (LH.trees.Count != 1) throw new KontextException(coords,"Trees was Expected to have 1 Tree for Termpart, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
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(coords,variableName, variable, LH.trees[0]));
if (LH.trees.Count != 1) throw new SemanticAnalysisDeadlyError(coords, "Trees was Expected to have 1 Tree for Termpart, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
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>();
public void ExitResult_tree([NotNull] ProofParser.Result_treeContext context)
{
if (LH.trees.Count != 1) throw new KontextException(new Coords(context),"Trees was Expected to have 1 Tree for ResultTree, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
if (LH.trees.Count != 1) throw (new SemanticAnalysisDeadlyError(new Coords(context), "Trees was Expected to have 1 Tree for ResultTree, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees)));
TS.resultTree = LH.trees[0];
}
......@@ -239,10 +235,10 @@ namespace Eingabeverwaltung.Parser
public void EnterInd_basis([NotNull] ProofParser.Ind_basisContext context)
{
Coords coords = new Coords(context);
if (currentInd.GetIndBasises().Count < 1) throw new KontextException(coords,"Error: Found no Inductionbasis in the current Induction!");
if (currentInd.GetIndBasises().Count < 1) throw new SemanticAnalysisDeadlyError(coords,"Error: Found no Inductionbasis in the current Induction!");
else try { currentIndCase = currentInd.indCases[++currentIndCaseIndex]; }
catch(ArgumentOutOfRangeException)
{ throw new KontextException(coords,"Error: Found more Inductionbasises: "
{ throw new SemanticAnalysisDeadlyError(coords,"Error: Found more Inductionbasises: "
+currentIndCaseIndex+" than Inductioncases in the current Induction!");
}
}
......@@ -250,11 +246,11 @@ namespace Eingabeverwaltung.Parser
public void EnterInd_step([NotNull] ProofParser.Ind_stepContext context)
{
Coords coords = new Coords(context);
if (currentInd.GetIndSteps().Count < 1) throw new KontextException(coords,"Error: Found no Inductionstep in the current Induction while entering Inductionstep!");
if (currentInd.GetIndSteps().Count < 1) throw new SemanticAnalysisDeadlyError(coords,"Error: Found no Inductionstep in the current Induction while entering Inductionstep!");
else try { currentIndCase = currentInd.indCases[++currentIndCaseIndex]; }
catch (ArgumentOutOfRangeException)
{
throw new KontextException(coords,"Error: Found more Inductionbasises and Inductionsteps: "
throw new SemanticAnalysisDeadlyError(coords,"Error: Found more Inductionbasises and Inductionsteps: "
+ currentIndCaseIndex + " than Inductioncases in the current Induction!");
}
}
......@@ -350,7 +346,7 @@ namespace Eingabeverwaltung.Parser
private void Test_Substitution_Variable_isCorrect(string variableName, Variable variable, Coords coords)
{
if (variable != null && variableName != variable.name)
throw new KontextException(coords,"The found Variable " + variable.ToString() + " has a different name than the inputed variableName " + variableName);
LH.errors.Add(new SemanticAnalysisError(coords,"The found Variable " + variable.ToString() + " has a different name than the inputed variableName " + variableName));
}
}
}
......
BewerterStrukturellerInduktion/Eingabeverwaltung/SimpleEingabeverwalter.cs
View file @ 11691f38
......@@ -7,7 +7,7 @@ using System.Text;
namespace Eingabeverwaltung
{
public class SimpleEingabeverwalter : AbstactEingabeverwalter
public class SimpleEingabeverwalter : AbstractEingabeverwalter
{
private string adtPath;
private string taskPath;
......
BewerterStrukturellerInduktion/Eingabeverwaltung/TestEingabeverwalter.cs 0 → 100644
View file @ 11691f38

using Eingabeverwaltung.Metamodell;
using Eingabeverwaltung.Parser;
using System.Collections.Generic;
using System.Collections.Immutable;
using System;
using System.IO;
namespace Eingabeverwaltung
{
/// <summary>
/// TestEingabeverwalter lets you managing the input and the exceptions thrown while parsing.
/// </summary>
public class TestEingabeverwalter : AbstractEingabeverwalter
{
public TestEingabeverwalter() :base() { }
/// <summary>
/// All Tests are managing its input on their own, they need to call each input file on their own
/// </summary>
/// <exception cref="InvalidOperationException"></exception>
public override void verwalteEingabe()
{
throw new InvalidOperationException();
}
/// <summary>
/// This is only for Testing. All Exceptions
/// </summary>
/// <param name="action"></param>
/// <param name="path"></param>
public void Eingabe_Interface(string action, string path)
{
ImmutableDictionary<string, Action<string>> eingabe = new Dictionary<string, Action<string>>
{
["ADT"] = ADT_Eingabe,
["Task"] = Task_Eingabe,
["Proof"] = Proof_Eingabe,
}.ToImmutableDictionary();
string input = File.ReadAllText(path);
eingabe[action](input);
void ADT_Eingabe(string input)
{
ADT adt = ADT_Antlr.parse(input);
inputContainer = new Container();
inputContainer.ADT = adt;
}
void Task_Eingabe(string input)
{
Task_Antlr.parse(input, inputContainer);
inputContainer.Proof = null;
}
void Proof_Eingabe(string input)
{
Proof_Antlr.parse(input,inputContainer);
}
}
}
}
BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs
View file @ 11691f38
using Ueberpruefung;
using Eingabeverwaltung.Metamodell;
using System;
using System.Collections.Generic;
using Ueberpruefung;
namespace Testverwaltung
{
......@@ -7,15 +10,16 @@ namespace Testverwaltung
private int currentTestNumber;
public ExtraTest() : base()
{
numTests = 2;
currentTestNumber = 0;
}
public override bool run()
{
resultString = "Testing Extras (Function Tree, Comments)\r\n\r\n";
resultString = "Testing Extras (Function Tree, Comments, NonDeadSemanticErrors)\r\n\r\n";
string pathPrefix = "Tests\\extra\\";
singleTest(pathPrefix+"FTree\\");
singleTest(pathPrefix+"Comment\\");
NonDeadSemErrsTest(pathPrefix + "NonDeadSemErrs\\");
numTests = currentTestNumber;
return passed;
}
......@@ -27,5 +31,70 @@ namespace Testverwaltung
Ueberpruefer.ueberpruefe(ein.GetContainer());
resultString += assert(currentTestNumber++, aus.NoErrors(), aus.printAllErrors(ein.GetContainer()));
}
/// <summary>
/// Tests Exceptions of non dead semantic errors
/// </summary>
/// <param name="path"></param>
private void NonDeadSemErrsTest(string path)
{
// Test ADT
List<string> adtFileNames = new List<string>() { "tree1","tree2","tree3","tree4","tree5","sort","op","ax","chaos" };
List<string> adtShallValues = new List<string>()
{
"Errors:\r\nError in 9:11: The Operation_Tree plus was inputted with 1 children, expected 2 children!\r\nError in 10:11: The Operation_Tree plus was inputted with 3 children, expected 2 children!\r\n",
"Error in 10:18: The Tree ink could not be found in Operations of the ADT!",
"Errors:\r\nError in 9:18: The Tree zero could not be found in Vars or Operations of the ADT!\r\nError in 9:26: The Tree k could not be found in Vars or Operations of the ADT!\r\nError in 9:7: One or more sides of one Equation are null!\r\nError in 10:22: The Tree k could not be found in Vars or Operations of the ADT!\r\n",
"Errors:\r\nError in 9:11: Error while building the tree plus: The the child (Variable) k with the Sort Nat2 is not Nat!\r\nError in 9:7: The Equation has not the same Sort on its 2 sides! Sort of leftTree: Nat Sort of rightTree: Nat2\r\nError in 11:7: The Equation has not the same Sort on its 2 sides! Sort of leftTree: Nat2 Sort of rightTree: Nat\r\nError in 12:27: Error while building the tree plus: The the child (ComposedTree) mal with the Sort Nat2 is not Nat!\r\nError in 12:7: The Equation has not the same Sort on its 2 sides! Sort of leftTree: Nat2 Sort of rightTree: Nat\r\n",
"Errors:\r\nError in 8:23: The Variable n was defined more than 1 times.!\r\n",
"Errors:\r\nError in 4:11: The Sort Nat was defined more than 1 times in Sorts of ADT!\r\nError in 5:0: The sort Nat has building constructors, but no basic constructors.\r\n",
"Errors:\r\nError in 7:24: Found a Sort Nat2 in Operations that was not defined in Sorts!\r\nError in 7:11: The Operation null was defined more than 1 times in Operations of ADT!\r\n",
"Errors:\r\nError in 9:7: The Axiom p0 was defined more than 1 times in Axioms of ADT!\r\n",
"Errors:\r\nError in 4:11: The Sort Nat was defined more than 1 times in Sorts of ADT!\r\nError in 5:18: Found a Sort Blub in Operations that was not defined in Sorts!\r\nError in 8:17: Found a Sort Nat1 in Operations that was not defined in Sorts!\r\nError in 8:25: Found a Sort Nat2 in Operations that was not defined in Sorts!\r\nError in 8:33: Found a Sort Blub in Operations that was not defined in Sorts!\r\nError in 9:11: The Operation plus was defined more than 1 times in Operations of ADT!\r\nError in 10:17: Found a Sort Blub in Operations that was not defined in Sorts!\r\nError in 10:25: Found a Sort Nat3 in Operations that was not defined in Sorts!\r\nError in 10:33: Found a Sort Nat4 in Operations that was not defined in Sorts!\r\nError in 13:5: Found a Sort Bla in Variable that was not defined in Sorts!\r\nError in 13:14: Found a Sort Nat5 in Variable that was not defined in Sorts!\r\nError in 13:24: Found a Sort Bla2 in Variable that was not defined in Sorts!\r\nError in 13:24: The Variable n was defined more than 1 times.!\r\nError in 16:18: The Tree null could not be found in Vars or Operations of the ADT!\r\nError in 16:7: One or more sides of one Equation are null!\r\nError in 17:7: One or more sides of one Equation are null!\r\nError in 18:17: The Tree null could not be found in Vars or Operations of the ADT!\r\nError in 18:25: The Tree null could not be found in Vars or Operations of the ADT!\r\nError in 18:7: One or more sides of one Equation are null!\r\nError in 19:7: One or more sides of one Equation are null!\r\n"
};
for (int i = 0; i < adtFileNames.Count; i++)
ExceptionTesting("ADT", path + adtFileNames[i]+".adt", adtShallValues[i]);
// Test Task
List<string> taskFileNames = new List<string>() { "tree1", "tree2", "tree3", "tree4", "tree5", "var", "lemma" };
List<string> taskShallValues = new List<string>()
{
"Errors:\r\nError in 2:27: The Operation_Tree plus was inputted with 3 children, expected 2 children!\r\nError in 14:33: The Operation_Tree inc was inputted with 0 children, expected 1 children!\r\nError in 14:46: The Operation_Tree plus was inputted with 1 children, expected 2 children!\r\nError in 14:42: The Operation_Tree inc was inputted with 2 children, expected 1 children!\r\n",
"Error in 2:27: The Tree add could not be found in Operations of the ADT!",
"Errors:\r\nError in 2:27: The Tree k could not be found in Vars or Operations of the ADT!\r\nError in 2:37: The Tree m could not be found in Vars or Operations of the ADT!\r\nError in 9:26: The Tree zero could not be found in Vars or Operations of the ADT!\r\n",
"Errors:\r\nError in 2:28: Error while building the tree plus: The the child (Variable) n with the Sort Nat2 is not Nat!\r\nError in 2:40: Error while building the tree plus: The the child (Variable) n with the Sort Nat2 is not Nat!\r\nError in 9:21: Error while building the tree plus: The the child (ComposedTree) null2 with the Sort Nat2 is not Nat!\r\nError in 14:33: Error while building the tree inc2: The the child (Variable) n with the Sort Nat is not Nat2!\r\nError in 14:28: Error while building the tree plus: The the child (ComposedTree) inc2 with the Sort Nat2 is not Nat!\r\nError in 14:46: Error while building the tree inc2: The the child (ComposedTree) plus with the Sort Nat is not Nat2!\r\nError in 14:6: The Equation has not the same Sort on its 2 sides! Sort of leftTree: Nat Sort of rightTree: Nat2\r\n",
"Errors:\r\nError in 2:26: The Variable n was defined more than 1 times.!\r\nError in 9:27: The Variable m was defined more than 1 times.!\r\nError in 10:4: Induction variable for task L1 was not definied as allquantified before.\r\n",
"Errors:\r\nError in 2:2: Induction variable for task task was not definied as allquantified before.\r\nError in 3:4: Config for induction can't find its relation to induction variable!\r\nError in 14:6: Config for induction can't find its relation to induction variable!\r\n",
"Errors:\r\nError in 8:2: The Lemma p0 has same name like 1 Axiom of ADT!\r\nError in 19:8: The Lemma L2 is defined multiple times in Task!\r\nError in 21:8: The Lemma L3 is defined multiple times in Task!\r\n"
};
ein.Eingabe_Interface("ADT", path + "1riginal.adt");
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> 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",
};
ein.Eingabe_Interface("ADT", path + "0riginal.adt");
ein.Eingabe_Interface("Task", path + "1riginal.task");
for (int i = 0; i < proofFileNames.Count; i++)
ExceptionTesting("Proof", path + proofFileNames[i] + ".proof", proofShallValues[i]);
}
private void ExceptionTesting(string inputType, string inputPath, string shallMessage)
{
string ExceptionMessage = "";
try
{
ein.Eingabe_Interface(inputType, inputPath);
}
catch (Exception e)
{
ExceptionMessage = e.Message;
}
resultString += assert(currentTestNumber++, shallMessage, ExceptionMessage);
}
}
}
BewerterStrukturellerInduktion/Testverwaltung/Test.cs
View file @ 11691f38
......@@ -8,13 +8,13 @@ namespace Testverwaltung
protected string resultString;
protected int numTests;
protected bool passed;
protected Eingabeverwalter ein;
protected TestEingabeverwalter ein;
protected Ausgabeverwalter aus;
public Test()
{
resultString = "";
ein = new Eingabeverwalter();
ein = new TestEingabeverwalter();
aus = new Ausgabeverwalter();
passed = true;
}
......
BewerterStrukturellerInduktion/Testverwaltung/TransformationTest.cs
View file @ 11691f38
using Ueberpruefung;
using System.Collections.Generic;
using Eingabeverwaltung.Metamodell;
namespace Testverwaltung
{
......