From f51e3304e29173950c67fa1bb5e9642c9ee64c0b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 28 Jan 2021 09:51:42 +0100 Subject: [PATCH 1/7] Term-Paket fertig --- package.json | 38 +--------------- pom.xml | 3 +- .../java/edu/kit/typicalc/model/Tree.java | 3 +- .../edu/kit/typicalc/model/term/AbsTerm.java | 3 +- .../edu/kit/typicalc/model/term/AppTerm.java | 21 +++++++-- .../kit/typicalc/model/term/BooleanTerm.java | 24 +++++++++- .../kit/typicalc/model/term/ConstTerm.java | 16 +++++-- .../kit/typicalc/model/term/IntegerTerm.java | 23 +++++++++- .../kit/typicalc/model/term/LambdaTerm.java | 12 +++++ .../edu/kit/typicalc/model/term/LetTerm.java | 45 +++++++++++++++++-- .../edu/kit/typicalc/model/term/VarTerm.java | 19 ++++++-- .../kit/typicalc/model/type/NamedType.java | 10 +++++ 12 files changed, 158 insertions(+), 59 deletions(-) create mode 100644 src/main/java/edu/kit/typicalc/model/type/NamedType.java diff --git a/package.json b/package.json index ea2cfad..ed8d860 100644 --- a/package.json +++ b/package.json @@ -12,14 +12,11 @@ "@vaadin/vaadin-charts": "7.0.0", "@vaadin/vaadin-combo-box": "5.4.7", "@vaadin/vaadin-confirm-dialog": "1.3.0", - "@vaadin/vaadin-core-shrinkwrap": "18.0.5", "@vaadin/vaadin-custom-field": "1.3.0", - "@vaadin/vaadin-date-picker": "4.4.1", "@vaadin/vaadin-details": "1.2.0", "@vaadin/vaadin-dialog": "2.5.2", "@vaadin/vaadin-form-layout": "2.3.0", "@vaadin/vaadin-grid": "5.7.7", - "@vaadin/vaadin-grid-pro": "2.2.2", "@vaadin/vaadin-icons": "4.3.2", "@vaadin/vaadin-item": "2.3.0", "@vaadin/vaadin-list-box": "1.4.0", @@ -30,26 +27,12 @@ "@vaadin/vaadin-ordered-layout": "1.4.0", "@vaadin/vaadin-progress-bar": "1.3.0", "@vaadin/vaadin-select": "2.4.0", - "@vaadin/vaadin-shrinkwrap": "18.0.5", "@vaadin/vaadin-split-layout": "4.3.0", "@vaadin/vaadin-text-field": "2.8.2", "lit-element": "2.3.1", "@vaadin/form": "./target/flow-frontend/form", "@vaadin/vaadin-avatar": "1.0.3", - "open": "^7.2.1", - "@vaadin/vaadin-crud": "1.3.0", - "@vaadin/vaadin-cookie-consent": "1.2.0", - "@vaadin/vaadin-upload": "4.4.1", - "@vaadin/vaadin-board": "2.2.0", - "@vaadin/vaadin-date-time-picker": "1.4.0", - "@vaadin/vaadin-login": "1.2.0", - "@vaadin/vaadin-accordion": "1.2.0", - "@vaadin/vaadin-checkbox": "2.5.0", - "@vaadin/vaadin-time-picker": "2.4.0", - "@vaadin/vaadin-context-menu": "4.5.0", - "@vaadin/vaadin-tabs": "3.2.0", - "@vaadin/vaadin-radio-button": "1.5.1", - "@vaadin/vaadin-rich-text-editor": "1.3.0" + "open": "^7.2.1" }, "devDependencies": { "webpack": "4.42.0", @@ -84,15 +67,12 @@ "@vaadin/vaadin-icons": "4.3.2", "@vaadin/vaadin-split-layout": "4.3.0", "@vaadin/vaadin-combo-box": "5.4.7", - "@vaadin/vaadin-core-shrinkwrap": "18.0.5", "@vaadin/vaadin-dialog": "2.5.2", "@vaadin/vaadin-select": "2.4.0", "@vaadin/vaadin-app-layout": "2.2.0", "@vaadin/vaadin-item": "2.3.0", "@vaadin/vaadin-notification": "1.6.0", - "@vaadin/vaadin-grid-pro": "2.2.2", "@vaadin/vaadin-progress-bar": "1.3.0", - "@vaadin/vaadin-shrinkwrap": "18.0.5", "@vaadin/vaadin-ordered-layout": "1.4.0", "@vaadin/vaadin-button": "2.4.0", "@vaadin/vaadin-text-field": "2.8.2", @@ -109,21 +89,7 @@ "@vaadin/vaadin-custom-field": "1.3.0", "lit-element": "2.3.1", "@vaadin/vaadin-avatar": "1.0.3", - "open": "^7.2.1", - "@vaadin/vaadin-crud": "1.3.0", - "@vaadin/vaadin-cookie-consent": "1.2.0", - "@vaadin/vaadin-upload": "4.4.1", - "@vaadin/vaadin-board": "2.2.0", - "@vaadin/vaadin-charts": "7.0.0", - "@vaadin/vaadin-date-time-picker": "1.4.0", - "@vaadin/vaadin-login": "1.2.0", - "@vaadin/vaadin-date-picker": "4.4.1", - "@vaadin/vaadin-accordion": "1.2.0", - "@vaadin/vaadin-checkbox": "2.5.0", - "@vaadin/vaadin-time-picker": "2.4.0", - "@vaadin/vaadin-tabs": "3.2.0", - "@vaadin/vaadin-radio-button": "1.5.1", - "@vaadin/vaadin-rich-text-editor": "1.3.0" + "open": "^7.2.1" }, "devDependencies": { "webpack-babel-multi-target-plugin": "2.3.3", diff --git a/pom.xml b/pom.xml index 5630b1d..30663be 100644 --- a/pom.xml +++ b/pom.xml @@ -75,8 +75,7 @@ com.vaadin - - vaadin + vaadin-core com.vaadin diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index 7116bb9..d12b300 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -115,8 +115,7 @@ public class Tree implements TermVisitorTree { } @Override - public InferenceStep visit(ConstTerm constTerm, Map typeAssumptions, Type conclusionType) { + public InferenceStep visit(ConstTerm constant, Map typeAssumptions, Type conclusionType) { return null; // TODO } 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 36e7da9..5edac46 100644 --- a/src/main/java/edu/kit/typicalc/model/term/AbsTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/AbsTerm.java @@ -51,8 +51,7 @@ public class AbsTerm extends LambdaTerm { @Override public InferenceStep accept(TermVisitorTree termVisitorTree, Map assumptions, Type type) { - //todo implement - return null; + return termVisitorTree.visit(this, assumptions, type); } @Override 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 dddcdd6..d502e08 100644 --- a/src/main/java/edu/kit/typicalc/model/term/AppTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/AppTerm.java @@ -7,20 +7,34 @@ import edu.kit.typicalc.model.type.TypeAbstraction; import java.util.Map; import java.util.Objects; +/** + * Representation of an application term consisting of a function and the parameter passed to it. + */ public class AppTerm extends LambdaTerm { private final LambdaTerm left; private final LambdaTerm right; + /** + * Initializes a new application term with one lambda term for the function and one lambda term for the parameter. + * @param left the function + * @param right the parameter + */ public AppTerm(LambdaTerm left, LambdaTerm right) { this.left = left; this.right = right; } - public LambdaTerm getLeft() { + /** + * @return the function used in this application + */ + public LambdaTerm getFunction() { return left; } - public LambdaTerm getRight() { + /** + * @return the parameter used in this application + */ + public LambdaTerm getParameter() { return right; } @@ -36,8 +50,7 @@ public class AppTerm extends LambdaTerm { @Override public InferenceStep accept(TermVisitorTree termVisitorTree, Map assumptions, Type type) { - // todo implement - return null; + return termVisitorTree.visit(this, assumptions, type); } @Override 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 d605975..a61ae72 100644 --- a/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java @@ -1,12 +1,34 @@ package edu.kit.typicalc.model.term; +import edu.kit.typicalc.model.type.NamedType; +import edu.kit.typicalc.model.type.Type; + +/** + * Representation of a constant boolean lambda term: either false or true. + */ public class BooleanTerm extends ConstTerm { + private final boolean value; + + /** + * Initializes a new boolean lambda term with the given value. + * @param value true or false + */ public BooleanTerm(boolean value) { - // TODO + this.value = value; + } + + @Override + public NamedType getType() { + return NamedType.BOOLEAN; } @Override public boolean hasLet() { return false; } + + @Override + public String toString() { + return Boolean.toString(value); + } } 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 68aa292..c4823d0 100644 --- a/src/main/java/edu/kit/typicalc/model/term/ConstTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/ConstTerm.java @@ -1,12 +1,21 @@ package edu.kit.typicalc.model.term; import edu.kit.typicalc.model.step.InferenceStep; +import edu.kit.typicalc.model.type.NamedType; import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeAbstraction; import java.util.Map; -public class ConstTerm extends LambdaTerm { +/** + * Abstract representation of a constant lambda term that has a predetermined type and a value of that type. + */ +public abstract class ConstTerm extends LambdaTerm { + /** + * @return the named type of the constant + */ + public abstract NamedType getType(); + @Override public boolean hasLet() { return false; @@ -18,8 +27,7 @@ public class ConstTerm extends LambdaTerm { } @Override - public InferenceStep accept(TermVisitorTree termVisitorTree, Map assumptions, Type type) { - // todo implment - return null; + public InferenceStep accept(TermVisitorTree visitor, Map assumptions, Type type) { + return visitor.visit(this, assumptions, type); } } diff --git a/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java b/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java index 5cb35f8..fabfc1d 100644 --- a/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java @@ -1,7 +1,28 @@ package edu.kit.typicalc.model.term; +import edu.kit.typicalc.model.type.NamedType; + +/** + * Representation of a constant integer lambda term: e.g. -1, 0 or 16. + */ public class IntegerTerm extends ConstTerm { + private final int value; + + /** + * Initializes a new integer lambda term with the given value. + * @param value an integer + */ public IntegerTerm(int value) { - // TODO + this.value = value; + } + + @Override + public NamedType getType() { + return NamedType.INT; + } + + @Override + public String toString() { + return Integer.toString(value); } } 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 2ef8c5c..ec7c03b 100644 --- a/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java @@ -6,6 +6,11 @@ import edu.kit.typicalc.model.type.TypeAbstraction; import java.util.Map; +/** + * Abstract representation of a lambda term. + * Depending on the subclass used, a lambda term may contain several other lambda terms + * and thus form a tree-like structure of lambda terms. + */ public abstract class LambdaTerm { /** * @return whether the lambda term contains a let expression @@ -18,6 +23,13 @@ public abstract class LambdaTerm { */ public abstract void accept(TermVisitor termVisitor); + /** + * Uses exactly one method of the visitor and provides the arguments passed. + * @param termVisitorTree the visitor + * @param assumptions type assumptions + * @param type a type + * @return the result returned by the visitor + */ public abstract InferenceStep accept(TermVisitorTree termVisitorTree, Map assumptions, Type type); 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 fb1b1a1..8cf3fd2 100644 --- a/src/main/java/edu/kit/typicalc/model/term/LetTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/LetTerm.java @@ -6,8 +6,25 @@ import edu.kit.typicalc.model.type.TypeAbstraction; import java.util.Map; +/** + * Representation of a let term with its variable, the lambda term assigned + * to this variable and the lambda term the variable is used in. + */ public class LetTerm extends LambdaTerm { - public LetTerm(VarTerm var, LambdaTerm def, LambdaTerm body) { + private final VarTerm variable; + private final LambdaTerm definition; + private final LambdaTerm body; + + /** + * Initializes a new let term with its variable and two lambda terms. + * @param variable the variable of the let term + * @param definition the lambda term assigned to the variable + * @param body the lambda term the variable may be used in + */ + public LetTerm(VarTerm variable, LambdaTerm definition, LambdaTerm body) { + this.variable = variable; + this.definition = definition; + this.body = body; } @Override @@ -21,8 +38,28 @@ public class LetTerm extends LambdaTerm { } @Override - public InferenceStep accept(TermVisitorTree termVisitorTree, Map assumptions, Type type) { - //todo implement - return null; + public InferenceStep accept(TermVisitorTree visitor, Map assumptions, Type type) { + return visitor.visit(this, assumptions, type); + } + + /** + * @return the variable defined in this let expression + */ + public VarTerm getVariable() { + return variable; + } + + /** + * @return definition of the variable + */ + public LambdaTerm getVariableDefinition() { + return definition; + } + + /** + * @return the inner lambda term (where the variable is used) + */ + public LambdaTerm getInner() { + return body; } } 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 75ab5ca..635ce99 100644 --- a/src/main/java/edu/kit/typicalc/model/term/VarTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/VarTerm.java @@ -7,14 +7,28 @@ import edu.kit.typicalc.model.type.TypeAbstraction; import java.util.Map; import java.util.Objects; +/** + * Representation of a variable term with its name. + */ public class VarTerm extends LambdaTerm { private final String name; + /** + * Initializes a new variable term with its name. + * @param name the name of the variable + */ public VarTerm(String name) { super(); this.name = name; } + /** + * @return the name of this variable + */ + public String getName() { + return name; + } + @Override public boolean hasLet() { return false; @@ -26,9 +40,8 @@ public class VarTerm extends LambdaTerm { } @Override - public InferenceStep accept(TermVisitorTree termVisitorTree, Map assumptions, Type type) { - //todo implement - return null; + public InferenceStep accept(TermVisitorTree visitor, Map assumptions, Type type) { + return visitor.visit(this, assumptions, type); } @Override diff --git a/src/main/java/edu/kit/typicalc/model/type/NamedType.java b/src/main/java/edu/kit/typicalc/model/type/NamedType.java new file mode 100644 index 0000000..66f4099 --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/type/NamedType.java @@ -0,0 +1,10 @@ +package edu.kit.typicalc.model.type; + +public class NamedType extends Type { + public static final NamedType BOOLEAN = new NamedType("boolean"); + public static final NamedType INT = new NamedType("int"); + + public NamedType(String name) { + // TODO + } +} From 52693f28e41c9f69ad15452cd5a08c4f85cd97e8 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 28 Jan 2021 09:53:21 +0100 Subject: [PATCH 2/7] Checkstyle-Fehler behoben --- src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java | 1 - 1 file changed, 1 deletion(-) 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 a61ae72..a4c2f52 100644 --- a/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java @@ -1,7 +1,6 @@ package edu.kit.typicalc.model.term; import edu.kit.typicalc.model.type.NamedType; -import edu.kit.typicalc.model.type.Type; /** * Representation of a constant boolean lambda term: either false or true. From 451c99bb2d403491620fc57b4a678bfcfbe06b44 Mon Sep 17 00:00:00 2001 From: Johanna Stuber Date: Thu, 28 Jan 2021 10:12:22 +0100 Subject: [PATCH 3/7] Tree visit(appTerm) --- src/main/java/edu/kit/typicalc/model/Tree.java | 14 +++++++++++++- .../edu/kit/typicalc/model/parser/ParseError.java | 9 +++++++++ .../edu/kit/typicalc/model/type/FunctionType.java | 2 ++ 3 files changed, 24 insertions(+), 1 deletion(-) diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index 7116bb9..d0521ea 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -11,6 +11,7 @@ import edu.kit.typicalc.model.term.LambdaTerm; 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.FunctionType; import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeAbstraction; import edu.kit.typicalc.model.type.TypeVariable; @@ -101,7 +102,18 @@ public class Tree implements TermVisitorTree { @Override public InferenceStep visit(AppTerm appTerm, Map typeAssumptions, Type conclusionType) { - return null; // TODO + Type leftType = typeVarFactory.nextTypeVariable(); + InferenceStep leftPremise = appTerm.getLeft().accept(this, typeAssumptions, leftType); + + Type rightType = typeVarFactory.nextTypeVariable(); + InferenceStep rightPremise = appTerm.getRight().accept(this, typeAssumptions, rightType); + + FunctionType function = new FunctionType(rightType, conclusionType); + Constraint newConstraint = new Constraint(leftType, function); + constraints.add(newConstraint); + + Conclusion conclusion = new Conclusion(typeAssumptions, appTerm, conclusionType); + return stepFactory.createAppStep(leftPremise, rightPremise, conclusion, newConstraint); } @Override diff --git a/src/main/java/edu/kit/typicalc/model/parser/ParseError.java b/src/main/java/edu/kit/typicalc/model/parser/ParseError.java index bd75ef0..4bb340b 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/ParseError.java +++ b/src/main/java/edu/kit/typicalc/model/parser/ParseError.java @@ -1,7 +1,16 @@ package edu.kit.typicalc.model.parser; public enum ParseError { + + /** + * the lambda term didn't meet the specified syntax + */ UNEXPECTED_TOKEN, + TOO_MANY_TOKENS, + + /** + * the String contained a character not allowed in that place + */ UNEXPECTED_CHARACTER } diff --git a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java index 3276623..55bf2d7 100644 --- a/src/main/java/edu/kit/typicalc/model/type/FunctionType.java +++ b/src/main/java/edu/kit/typicalc/model/type/FunctionType.java @@ -1,5 +1,7 @@ package edu.kit.typicalc.model.type; public class FunctionType extends Type { + public FunctionType(Type parameter, Type output) { + } } From 2092bf380e41cf55bb6412a33655c8d6e4a07fca Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 28 Jan 2021 10:14:52 +0100 Subject: [PATCH 4/7] Test let parsing --- .../typicalc/model/parser/LambdaLexer.java | 41 ++++++++++++++++++- .../kit/typicalc/model/term/IntegerTerm.java | 19 +++++++++ .../edu/kit/typicalc/model/term/LetTerm.java | 20 +++++++++ .../model/parser/LambdaParserTest.java | 20 +++++++++ 4 files changed, 98 insertions(+), 2 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java b/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java index b2a6401..09847f1 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java +++ b/src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java @@ -3,9 +3,13 @@ package edu.kit.typicalc.model.parser; import edu.kit.typicalc.model.parser.Token.TokenType; import edu.kit.typicalc.util.Result; +import java.util.ArrayDeque; +import java.util.Deque; + /** * This class lexes a term given as String into tokens. - * Tokens are lexed one by one as requested by the parser. + * Tokens are lexed all at once (to catch errors early), + * and passed to the parser on demand. */ public class LambdaLexer { /** @@ -16,6 +20,7 @@ public class LambdaLexer { * current position in the term */ private int pos = 0; + private Result, ParseError> result; /** * Constructs a lexer that lexes the given term @@ -23,6 +28,24 @@ public class LambdaLexer { */ public LambdaLexer(String term) { this.term = term; + tokenize(); + } + + private void tokenize() { + Deque tokens = new ArrayDeque<>(); + while (true) { + Result token = parseNextToken(); + if (token.isError()) { + result = new Result<>(null, token.unwrapError()); + return; + } + Token value = token.unwrap(); + tokens.add(value); + if (value.getType() == TokenType.EOF) { + break; + } + } + result = new Result<>(tokens); } /** @@ -33,10 +56,24 @@ public class LambdaLexer { } /** - * Lexes and returns the next token. + * Returns the next token and advances the lexer position. * @return the next token */ public Result nextToken() { + if (result.isError()) { + return new Result<>(null, result.unwrapError()); + } + Deque tokens = result.unwrap(); + if (!tokens.isEmpty()) { + Token token = tokens.removeFirst(); + return new Result<>(token); + } else { + return new Result<>(new Token(TokenType.EOF, "", 0)); + } + + } + + public Result parseNextToken() { while (pos < term.length() && Character.isWhitespace(term.charAt(pos))) { advance(); } diff --git a/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java b/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java index fabfc1d..8694f4e 100644 --- a/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java @@ -2,6 +2,8 @@ package edu.kit.typicalc.model.term; import edu.kit.typicalc.model.type.NamedType; +import java.util.Objects; + /** * Representation of a constant integer lambda term: e.g. -1, 0 or 16. */ @@ -25,4 +27,21 @@ public class IntegerTerm extends ConstTerm { public String toString() { return Integer.toString(value); } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + IntegerTerm that = (IntegerTerm) o; + return value == that.value; + } + + @Override + public int hashCode() { + return Objects.hash(value); + } } 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 8cf3fd2..cc635ba 100644 --- a/src/main/java/edu/kit/typicalc/model/term/LetTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/LetTerm.java @@ -5,6 +5,7 @@ import edu.kit.typicalc.model.type.Type; import edu.kit.typicalc.model.type.TypeAbstraction; import java.util.Map; +import java.util.Objects; /** * Representation of a let term with its variable, the lambda term assigned @@ -62,4 +63,23 @@ public class LetTerm extends LambdaTerm { public LambdaTerm getInner() { return body; } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + LetTerm letTerm = (LetTerm) o; + return Objects.equals(variable, letTerm.variable) + && Objects.equals(definition, letTerm.definition) + && Objects.equals(body, letTerm.body); + } + + @Override + public int hashCode() { + return Objects.hash(variable, definition, body); + } } 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 c27709b..eecba8c 100644 --- a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java +++ b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java @@ -4,8 +4,12 @@ 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.ConstTerm; +import edu.kit.typicalc.model.term.IntegerTerm; import edu.kit.typicalc.model.term.LambdaTerm; +import edu.kit.typicalc.model.term.LetTerm; import edu.kit.typicalc.model.term.VarTerm; +import edu.kit.typicalc.model.type.NamedType; import edu.kit.typicalc.util.Result; import org.junit.jupiter.api.Test; @@ -29,4 +33,20 @@ class LambdaParserTest { new AppTerm(new AbsTerm(new VarTerm("x"), new VarTerm("x")), new AbsTerm(new VarTerm("x"), new VarTerm("x")))); } + @Test + void letTerm() { + LambdaParser parser = new LambdaParser("let id = λx.x in id 1"); + assertEquals(parser.parse().unwrap(), + new LetTerm( + new VarTerm("id"), + new AbsTerm( + new VarTerm("x"), + new VarTerm("x") + ), + new AppTerm( + new VarTerm("id"), + new IntegerTerm(1) + ) + )); + } } From c329a4e7d67965e995edcb0fe62f9b7b0d71a97f Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 28 Jan 2021 10:15:59 +0100 Subject: [PATCH 5/7] Use renamed AppTerms method in Tree --- src/main/java/edu/kit/typicalc/model/Tree.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index cb089f0..f1acede 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -103,10 +103,10 @@ public class Tree implements TermVisitorTree { @Override public InferenceStep visit(AppTerm appTerm, Map typeAssumptions, Type conclusionType) { Type leftType = typeVarFactory.nextTypeVariable(); - InferenceStep leftPremise = appTerm.getLeft().accept(this, typeAssumptions, leftType); + InferenceStep leftPremise = appTerm.getFunction().accept(this, typeAssumptions, leftType); Type rightType = typeVarFactory.nextTypeVariable(); - InferenceStep rightPremise = appTerm.getRight().accept(this, typeAssumptions, rightType); + InferenceStep rightPremise = appTerm.getParameter().accept(this, typeAssumptions, rightType); FunctionType function = new FunctionType(rightType, conclusionType); Constraint newConstraint = new Constraint(leftType, function); From 7a4ef77e7f6bcc3fd2217d9ed23ab410ead703ed Mon Sep 17 00:00:00 2001 From: Johanna Stuber Date: Thu, 28 Jan 2021 10:16:49 +0100 Subject: [PATCH 6/7] falschen Methodenaufruf korrigieren --- src/main/java/edu/kit/typicalc/model/Tree.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index cb089f0..f1acede 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/src/main/java/edu/kit/typicalc/model/Tree.java @@ -103,10 +103,10 @@ public class Tree implements TermVisitorTree { @Override public InferenceStep visit(AppTerm appTerm, Map typeAssumptions, Type conclusionType) { Type leftType = typeVarFactory.nextTypeVariable(); - InferenceStep leftPremise = appTerm.getLeft().accept(this, typeAssumptions, leftType); + InferenceStep leftPremise = appTerm.getFunction().accept(this, typeAssumptions, leftType); Type rightType = typeVarFactory.nextTypeVariable(); - InferenceStep rightPremise = appTerm.getRight().accept(this, typeAssumptions, rightType); + InferenceStep rightPremise = appTerm.getParameter().accept(this, typeAssumptions, rightType); FunctionType function = new FunctionType(rightType, conclusionType); Constraint newConstraint = new Constraint(leftType, function); From c5a3cce7bf87ed2dafd18f6f7858cf04dd20f061 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 28 Jan 2021 10:31:58 +0100 Subject: [PATCH 7/7] CI: test coverage And a complicated parser test --- .gitlab-ci.yml | 4 +++ pom.xml | 27 ++++++++++++++++++ .../kit/typicalc/model/parser/ParseError.java | 7 +++-- .../kit/typicalc/model/term/BooleanTerm.java | 19 +++++++++++++ .../model/parser/LambdaParserTest.java | 28 +++++++++++++++++++ 5 files changed, 83 insertions(+), 2 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1f58140..6b6a807 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -2,3 +2,7 @@ build: script: - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp checkstyle:check - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp test + - mvn -Dmaven.repo.local=/tmp/m2/repository -Duser.home=/tmp cobertura:cobertura + artifacts: + reports: + cobertura: target/site/cobertura/coverage.xml diff --git a/pom.xml b/pom.xml index 30663be..fc13d67 100644 --- a/pom.xml +++ b/pom.xml @@ -154,6 +154,17 @@ maven-surefire-plugin 2.22.2 + + org.codehaus.mojo + cobertura-maven-plugin + 2.7 + + + + xml + + + maven-checkstyle-plugin @@ -255,4 +266,20 @@ + + + + + org.codehaus.mojo + cobertura-maven-plugin + 2.7 + + + + xml + + + + + \ No newline at end of file diff --git a/src/main/java/edu/kit/typicalc/model/parser/ParseError.java b/src/main/java/edu/kit/typicalc/model/parser/ParseError.java index 4bb340b..4b11451 100644 --- a/src/main/java/edu/kit/typicalc/model/parser/ParseError.java +++ b/src/main/java/edu/kit/typicalc/model/parser/ParseError.java @@ -6,11 +6,14 @@ public enum ParseError { * the lambda term didn't meet the specified syntax */ UNEXPECTED_TOKEN, - + + /** + * some tokens were remaining after parsing a full lambda term + */ TOO_MANY_TOKENS, /** - * the String contained a character not allowed in that place + * the string contained a character not allowed in that context */ UNEXPECTED_CHARACTER } 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 a4c2f52..06626f7 100644 --- a/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java +++ b/src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java @@ -2,6 +2,8 @@ package edu.kit.typicalc.model.term; import edu.kit.typicalc.model.type.NamedType; +import java.util.Objects; + /** * Representation of a constant boolean lambda term: either false or true. */ @@ -30,4 +32,21 @@ public class BooleanTerm extends ConstTerm { public String toString() { return Boolean.toString(value); } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + BooleanTerm that = (BooleanTerm) o; + return value == that.value; + } + + @Override + public int hashCode() { + return Objects.hash(value); + } } 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 eecba8c..ec5409d 100644 --- a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java +++ b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java @@ -4,6 +4,7 @@ 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.BooleanTerm; import edu.kit.typicalc.model.term.ConstTerm; import edu.kit.typicalc.model.term.IntegerTerm; import edu.kit.typicalc.model.term.LambdaTerm; @@ -49,4 +50,31 @@ class LambdaParserTest { ) )); } + @Test + void complicatedTerm() { + LambdaParser parser = new LambdaParser("(λx.λy.x y 5)(λz.z)(true)"); + assertEquals(parser.parse().unwrap(), + new AppTerm( + new AppTerm( + new AbsTerm( + new VarTerm("x"), + new AbsTerm( + new VarTerm("y"), + new AppTerm( + new AppTerm( + new VarTerm("x"), + new VarTerm("y") + ), + new IntegerTerm(5) + ) + ) + ), + new AbsTerm( + new VarTerm("z"), + new VarTerm("z") + ) + ), + new BooleanTerm(true) + )); + } }