From f51e3304e29173950c67fa1bb5e9642c9ee64c0b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 28 Jan 2021 09:51:42 +0100 Subject: [PATCH] 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 + } +}