mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-09 10:50:42 +00:00
Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc
This commit is contained in:
commit
8b08d2d3ab
38
package.json
38
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",
|
||||
|
3
pom.xml
3
pom.xml
@ -75,8 +75,7 @@
|
||||
<dependencies>
|
||||
<dependency>
|
||||
<groupId>com.vaadin</groupId>
|
||||
<!-- Replace artifactId with vaadin-core to use only free components -->
|
||||
<artifactId>vaadin</artifactId>
|
||||
<artifactId>vaadin-core</artifactId>
|
||||
</dependency>
|
||||
<dependency>
|
||||
<groupId>com.vaadin</groupId>
|
||||
|
@ -127,8 +127,7 @@ public class Tree implements TermVisitorTree {
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep visit(ConstTerm constTerm, Map<VarTerm,
|
||||
TypeAbstraction> typeAssumptions, Type conclusionType) {
|
||||
public InferenceStep visit(ConstTerm constant, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
|
||||
return null; // TODO
|
||||
}
|
||||
|
||||
|
@ -51,8 +51,7 @@ public class AbsTerm extends LambdaTerm {
|
||||
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
//todo implement
|
||||
return null;
|
||||
return termVisitorTree.visit(this, assumptions, type);
|
||||
}
|
||||
|
||||
@Override
|
||||
|
@ -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<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
// todo implement
|
||||
return null;
|
||||
return termVisitorTree.visit(this, assumptions, type);
|
||||
}
|
||||
|
||||
@Override
|
||||
|
@ -1,12 +1,33 @@
|
||||
package edu.kit.typicalc.model.term;
|
||||
|
||||
import edu.kit.typicalc.model.type.NamedType;
|
||||
|
||||
/**
|
||||
* 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);
|
||||
}
|
||||
}
|
||||
|
@ -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<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
// todo implment
|
||||
return null;
|
||||
public InferenceStep accept(TermVisitorTree visitor, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return visitor.visit(this, assumptions, type);
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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<VarTerm, TypeAbstraction> assumptions, Type type);
|
||||
|
||||
|
@ -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<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
//todo implement
|
||||
return null;
|
||||
public InferenceStep accept(TermVisitorTree visitor, Map<VarTerm, TypeAbstraction> 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;
|
||||
}
|
||||
}
|
||||
|
@ -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<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
//todo implement
|
||||
return null;
|
||||
public InferenceStep accept(TermVisitorTree visitor, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return visitor.visit(this, assumptions, type);
|
||||
}
|
||||
|
||||
@Override
|
||||
|
10
src/main/java/edu/kit/typicalc/model/type/NamedType.java
Normal file
10
src/main/java/edu/kit/typicalc/model/type/NamedType.java
Normal file
@ -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
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue
Block a user