From 143999d6e9b6501953a04cfabe3c91bfc234fae2 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 27 Jan 2021 21:44:17 +0100 Subject: [PATCH] Term javadocs, TermVisitor, Result javadocs, mehr Parser-Tests --- .../java/edu/kit/typicalc/model/Tree.java | 35 +++++++++- .../typicalc/model/parser/LambdaParser.java | 6 +- .../edu/kit/typicalc/model/term/AbsTerm.java | 25 +++++++ .../edu/kit/typicalc/model/term/AppTerm.java | 10 +++ .../kit/typicalc/model/term/BooleanTerm.java | 5 ++ .../kit/typicalc/model/term/ConstTerm.java | 9 +++ .../kit/typicalc/model/term/LambdaTerm.java | 12 +++- .../edu/kit/typicalc/model/term/LetTerm.java | 10 +++ .../kit/typicalc/model/term/TermVisitor.java | 29 +++++++++ .../edu/kit/typicalc/model/term/VarTerm.java | 10 +++ .../kit/typicalc/model/type/FunctionType.java | 5 ++ .../kit/typicalc/model/type/TypeVisitor.java | 19 ++++++ .../java/edu/kit/typicalc/util/Result.java | 65 ++++++++++++++++++- .../typeinferencecontent/LatexCreator.java | 48 ++++++++++++++ .../model/parser/LambdaParserTest.java | 6 +- 15 files changed, 285 insertions(+), 9 deletions(-) create mode 100644 src/main/java/edu/kit/typicalc/model/type/FunctionType.java diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index 6c7eb80..b7b6fe9 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -1,10 +1,16 @@ package edu.kit.typicalc.model; import edu.kit.typicalc.model.step.InferenceStep; +import edu.kit.typicalc.model.term.AbsTerm; +import edu.kit.typicalc.model.term.AppTerm; +import edu.kit.typicalc.model.term.ConstTerm; import edu.kit.typicalc.model.term.LambdaTerm; -import edu.kit.typicalc.model.term.TermVisitor; +import edu.kit.typicalc.model.term.LetTerm; +import edu.kit.typicalc.model.term.TermVisitorTree; import edu.kit.typicalc.model.term.VarTerm; +import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeAbstraction; +import edu.kit.typicalc.model.type.TypeAssumption; import java.util.List; import java.util.Map; @@ -15,7 +21,7 @@ import java.util.Map; * are part of these steps. It is guaranteed that these members can be accessed right after * instantiation (no additional initialization is required). */ -public class Tree implements TermVisitor { +public class Tree implements TermVisitorTree { /** * Initializes a new Tree representing the proof tree for the type inference of the given @@ -67,4 +73,29 @@ public class Tree implements TermVisitor { return null; // TODO } + + @Override + public InferenceStep visit(AppTerm appTerm, List typeAssumptions, Type conclusionType) { + return null; // TODO + } + + @Override + public InferenceStep visit(AbsTerm absTerm, List typeAssumptions, Type conclusionType) { + return null; // TODO + } + + @Override + public InferenceStep visit(LetTerm letTerm, List typeAssumptions, Type conclusionType) { + return null; // TODO + } + + @Override + public InferenceStep visit(ConstTerm constTerm, List typeAssumptions, Type conclusionType) { + return null; // TODO + } + + @Override + public InferenceStep visit(VarTerm varTerm, List typeAssumptions, Type conclusionType) { + return null; // TODO + } } diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java index e6a8924..8672467 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java +++ b/src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java @@ -84,10 +84,10 @@ public class LambdaParser { switch (token.getType()) { case LAMBDA: Result abs = parseAbstraction(); - return new Result<>(abs.unwrap(), abs.unwrapError()); + return new Result<>(abs.unwrap(), abs.getError()); case LET: Result let = parseLet(); - return new Result<>(let.unwrap(), let.unwrapError()); + return new Result<>(let.unwrap(), let.getError()); default: return parseApplication(); } @@ -136,7 +136,7 @@ public class LambdaParser { switch (token.getType()) { case VARIABLE: Result var = parseVar(); - return new Result<>(var.unwrap(), var.unwrapError()); + return new Result<>(var.unwrap(), var.getError()); case NUMBER: String number = token.getText(); int n; diff --git a/src/main/java/edu/kit/typicalc/model/term/AbsTerm.java b/src/main/java/edu/kit/typicalc/model/term/AbsTerm.java index 461b366..e32e57b 100644 --- a/src/main/java/edu/kit/typicalc/model/term/AbsTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/AbsTerm.java @@ -2,23 +2,48 @@ package edu.kit.typicalc.model.term; import java.util.Objects; +/** + * Representation of an abstraction term with its two sub-lambda terms. + */ public class AbsTerm extends LambdaTerm { private final VarTerm var; private final LambdaTerm body; + /** + * Initializes a new abstraction term with the variable bound + * by the abstraction and the lambda term of the abstraction. + * @param var the variable bound by the abstraction + * @param body the lambda term of the abstraction + */ public AbsTerm(VarTerm var, LambdaTerm body) { this.var = var; this.body = body; } + /** + * @return the variable of this abstraction + */ public VarTerm getVariable() { return var; } + /** + * @return the function body of this abstraction + */ public LambdaTerm getInner() { return body; } + @Override + public boolean hasLet() { + return body.hasLet(); + } + + @Override + public void accept(TermVisitor termVisitor) { + termVisitor.visit(this); + } + @Override public boolean equals(Object o) { if (this == o) { diff --git a/src/main/java/edu/kit/typicalc/model/term/AppTerm.java b/src/main/java/edu/kit/typicalc/model/term/AppTerm.java index 7415f43..d7ac3d1 100644 --- a/src/main/java/edu/kit/typicalc/model/term/AppTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/AppTerm.java @@ -19,6 +19,16 @@ public class AppTerm extends LambdaTerm { return right; } + @Override + public boolean hasLet() { + return left.hasLet() || right.hasLet(); + } + + @Override + public void accept(TermVisitor termVisitor) { + termVisitor.visit(this); + } + @Override public boolean equals(Object o) { if (this == o) { diff --git a/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java b/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java index 358a722..d605975 100644 --- a/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java @@ -4,4 +4,9 @@ public class BooleanTerm extends ConstTerm { public BooleanTerm(boolean value) { // TODO } + + @Override + public boolean hasLet() { + return false; + } } diff --git a/src/main/java/edu/kit/typicalc/model/term/ConstTerm.java b/src/main/java/edu/kit/typicalc/model/term/ConstTerm.java index 694f82f..2aa0c4a 100644 --- a/src/main/java/edu/kit/typicalc/model/term/ConstTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/ConstTerm.java @@ -1,4 +1,13 @@ package edu.kit.typicalc.model.term; public class ConstTerm extends LambdaTerm { + @Override + public boolean hasLet() { + return false; + } + + @Override + public void accept(TermVisitor termVisitor) { + termVisitor.visit(this); + } } diff --git a/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java b/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java index 6945106..dde58fe 100644 --- a/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java @@ -1,4 +1,14 @@ package edu.kit.typicalc.model.term; -public class LambdaTerm { +public abstract class LambdaTerm { + /** + * @return whether the lambda term contains a let expression + */ + public abstract boolean hasLet(); + + /** + * Calls exactly one method on the visitor depending on the lambda term type. + * @param termVisitor a visitor + */ + public abstract void accept(TermVisitor termVisitor); } diff --git a/src/main/java/edu/kit/typicalc/model/term/LetTerm.java b/src/main/java/edu/kit/typicalc/model/term/LetTerm.java index ad70177..1638f97 100644 --- a/src/main/java/edu/kit/typicalc/model/term/LetTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/LetTerm.java @@ -3,4 +3,14 @@ package edu.kit.typicalc.model.term; public class LetTerm extends LambdaTerm { public LetTerm(VarTerm var, LambdaTerm def, LambdaTerm body) { } + + @Override + public boolean hasLet() { + return true; + } + + @Override + public void accept(TermVisitor termVisitor) { + termVisitor.visit(this); + } } diff --git a/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java b/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java index c35bec0..2085ec5 100644 --- a/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java +++ b/src/main/java/edu/kit/typicalc/model/term/TermVisitor.java @@ -1,4 +1,33 @@ package edu.kit.typicalc.model.term; public interface TermVisitor { + /** + * Visit an application term. + * @param appTerm the term + */ + void visit(AppTerm appTerm); + + /** + * Visit an abstraction term. + * @param absTerm the term + */ + void visit(AbsTerm absTerm); + + /** + * Visit a let expression. + * @param letTerm the term + */ + void visit(LetTerm letTerm); + + /** + * Visit a variable. + * @param varTerm the variable + */ + void visit(VarTerm varTerm); + + /** + * Visit a constant. + * @param constTerm the constant + */ + void visit(ConstTerm constTerm); } diff --git a/src/main/java/edu/kit/typicalc/model/term/VarTerm.java b/src/main/java/edu/kit/typicalc/model/term/VarTerm.java index fa67492..3a7d98c 100644 --- a/src/main/java/edu/kit/typicalc/model/term/VarTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/VarTerm.java @@ -10,6 +10,16 @@ public class VarTerm extends LambdaTerm { this.name = name; } + @Override + public boolean hasLet() { + return false; + } + + @Override + public void accept(TermVisitor termVisitor) { + termVisitor.visit(this); + } + @Override public boolean equals(Object o) { if (this == o) { diff --git a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java new file mode 100644 index 0000000..3276623 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java @@ -0,0 +1,5 @@ +package edu.kit.typicalc.model.type; + +public class FunctionType extends Type { + +} diff --git a/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java b/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java index 74e7eb1..6755bc4 100644 --- a/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java +++ b/src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java @@ -1,4 +1,23 @@ package edu.kit.typicalc.model.type; +import com.fasterxml.jackson.databind.jsontype.NamedType; + public interface TypeVisitor { + /** + * Visit a named type. + * @param named the type + */ + void visit(NamedType named); + + /** + * Visit a type variable + * @param variable the variable + */ + void visit(TypeVariable variable); + + /** + * Visit a function. + * @param function the function + */ + void visit(FunctionType function); } diff --git a/src/main/java/edu/kit/typicalc/util/Result.java b/src/main/java/edu/kit/typicalc/util/Result.java index 8cc01c1..dc4d426 100644 --- a/src/main/java/edu/kit/typicalc/util/Result.java +++ b/src/main/java/edu/kit/typicalc/util/Result.java @@ -1,28 +1,89 @@ package edu.kit.typicalc.util; +/** + * Can be a value of type T or an error of type E (if the computation failed). + * @param value type + * @param error type + */ public class Result { private final T value; private final E error; + /** + * Creates a new result containing the given value. + * @param value the value + */ public Result(T value) { this.value = value; this.error = null; } - public Result(T value, E error) { // TODO: Java does not allow both constructors otherwise + /** + * Creates a new result containing the given value or error. + * Only one of the parameters may be non-null. + * @param value the value + * @param error the error + * @throws IllegalArgumentException if more or less than one parameter is null + */ + public Result(T value, E error) { + if ((value != null) == (error != null)) { + throw new IllegalArgumentException("value xor error must be null in constructor!"); + } this.value = value; this.error = error; } + /** + * @return whether the result contains a regular value + */ + public boolean isOk() { + return value != null; + } + + /** + * @return whether the result contains an error + */ public boolean isError() { return error != null; } - public T unwrap() { + /** + * If the result contains a regular value, returns that value. + * Otherwise an IllegalStateException is thrown. + * @return the value + * @throws IllegalStateException if this is an error + */ + public T unwrap() throws IllegalStateException { + if (value == null) { + throw new IllegalStateException("tried to unwrap an error"); + } return value; } + /** + * If the result contains an error, returns that error. + * Otherwise an IllegalStateException is thrown. + * @return the error + * @throws IllegalStateException if this is a regular value + */ public E unwrapError() { + if (error == null) { + throw new IllegalStateException("tried to unwrap a value"); + } + return error; + } + + /** + * @return the value contained, or null + */ + public T getValue() { + return value; + } + + /** + * @return the error contained, or null + */ + public E getError() { return error; } } diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java index e9b9457..1e9ab05 100644 --- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java +++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/LatexCreator.java @@ -1,10 +1,18 @@ package edu.kit.typicalc.view.content.typeinferencecontent; +import com.fasterxml.jackson.databind.jsontype.NamedType; import edu.kit.typicalc.model.Conclusion; import edu.kit.typicalc.model.TypeInfererInterface; import edu.kit.typicalc.model.step.*; +import edu.kit.typicalc.model.term.AbsTerm; +import edu.kit.typicalc.model.term.AppTerm; +import edu.kit.typicalc.model.term.ConstTerm; +import edu.kit.typicalc.model.term.LetTerm; import edu.kit.typicalc.model.term.TermVisitor; +import edu.kit.typicalc.model.term.VarTerm; +import edu.kit.typicalc.model.type.FunctionType; +import edu.kit.typicalc.model.type.TypeVariable; import edu.kit.typicalc.model.type.TypeVisitor; /** @@ -131,4 +139,44 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor { generateConclusion(letD, LABEL_LET, UIC); } + + @Override + public void visit(AppTerm appTerm) { + + } + + @Override + public void visit(AbsTerm absTerm) { + + } + + @Override + public void visit(LetTerm letTerm) { + + } + + @Override + public void visit(VarTerm varTerm) { + + } + + @Override + public void visit(ConstTerm constTerm) { + + } + + @Override + public void visit(NamedType named) { + + } + + @Override + public void visit(TypeVariable variable) { + + } + + @Override + public void visit(FunctionType function) { + + } } diff --git a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java index a3f22cf..c27709b 100644 --- a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java +++ b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java @@ -4,14 +4,18 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import edu.kit.typicalc.model.term.AbsTerm; import edu.kit.typicalc.model.term.AppTerm; +import edu.kit.typicalc.model.term.LambdaTerm; import edu.kit.typicalc.model.term.VarTerm; +import edu.kit.typicalc.util.Result; import org.junit.jupiter.api.Test; class LambdaParserTest { @Test void varTerm() { LambdaParser parser = new LambdaParser("x"); - assertEquals(parser.parse().unwrap(), new VarTerm("x")); + Result term = parser.parse(); + System.out.println(term); + assertEquals(term.unwrap(), new VarTerm("x")); } @Test void absTerm() {