arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 10:20:41 +00:00
Code Issues Packages Projects Releases Wiki Activity

merge

Browse Source
This commit is contained in:
ucrhh 2021-01-28 10:43:57 +01:00
commit 164c04eeb3
17 changed files with 366 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
.gitlab-ci.yml
View File

@ -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

16
package.json
View File

@ -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,7 +27,6 @@
"@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",
"@vaadin/form": "./target/flow-frontend/form",
@ -49,7 +45,11 @@
"@vaadin/vaadin-tabs": "3.2.0",
"@vaadin/vaadin-radio-button": "1.5.1",
"@vaadin/vaadin-rich-text-editor": "1.3.0",
"lit-element": "2.3.1"
"lit-element": "2.3.1",
"@vaadin/vaadin-core-shrinkwrap": "18.0.5",
"@vaadin/vaadin-grid-pro": "2.2.2",
"@vaadin/vaadin-shrinkwrap": "18.0.5",
"@vaadin/vaadin-date-picker": "4.4.1"
},
"devDependencies": {
"@types/validator": "13.1.0",
@ -84,15 +84,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",
@ -112,9 +109,12 @@
"open": "^7.2.1",
"@vaadin/vaadin-crud": "1.3.0",
"@vaadin/vaadin-cookie-consent": "1.2.0",
"@vaadin/vaadin-core-shrinkwrap": "18.0.5",
"@vaadin/vaadin-upload": "4.4.1",
"@vaadin/vaadin-board": "2.2.0",
"@vaadin/vaadin-charts": "7.0.0",
"@vaadin/vaadin-grid-pro": "2.2.2",
"@vaadin/vaadin-shrinkwrap": "18.0.5",
"@vaadin/vaadin-date-time-picker": "1.4.0",
"@vaadin/vaadin-login": "1.2.0",
"@vaadin/vaadin-date-picker": "4.4.1",

30
pom.xml
View File

@ -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>
@ -155,6 +154,17 @@
<artifactId>maven-surefire-plugin</artifactId>
<version>2.22.2</version>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>cobertura-maven-plugin</artifactId>
<version>2.7</version>
<configuration>
<check/>
<formats>
<format>xml</format>
</formats>
</configuration>
</plugin>
<plugin>
<artifactId>maven-checkstyle-plugin</artifactId>
@ -256,4 +266,20 @@
</profile>
</profiles>
<reporting>
<plugins>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>cobertura-maven-plugin</artifactId>
<version>2.7</version>
<configuration>
<check/>
<formats>
<format>xml</format>
</formats>
</configuration>
</plugin>
</plugins>
</reporting>
</project>

17
src/main/java/edu/kit/typicalc/model/Tree.java
View File

@ -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<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
Type leftType = typeVarFactory.nextTypeVariable();
InferenceStep leftPremise = appTerm.getFunction().accept(this, typeAssumptions, leftType);
Type rightType = typeVarFactory.nextTypeVariable();
InferenceStep rightPremise = appTerm.getParameter().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
@ -115,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
}

41
src/main/java/edu/kit/typicalc/model/parser/LambdaLexer.java
View File

@ -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<Deque<Token>, 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<Token> tokens = new ArrayDeque<>();
while (true) {
Result<Token, ParseError> 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<Token, ParseError> nextToken() {
if (result.isError()) {
return new Result<>(null, result.unwrapError());
}
Deque<Token> 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<Token, ParseError> parseNextToken() {
while (pos < term.length() && Character.isWhitespace(term.charAt(pos))) {
advance();
}

12
src/main/java/edu/kit/typicalc/model/parser/ParseError.java
View File

@ -1,7 +1,19 @@
package edu.kit.typicalc.model.parser;
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 context
*/
UNEXPECTED_CHARACTER
}

3
src/main/java/edu/kit/typicalc/model/term/AbsTerm.java
View File

@ -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

21
src/main/java/edu/kit/typicalc/model/term/AppTerm.java
View File

@ -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

42
src/main/java/edu/kit/typicalc/model/term/BooleanTerm.java
View File

@ -1,12 +1,52 @@
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.
*/
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);
}
@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);
}
}

16
src/main/java/edu/kit/typicalc/model/term/ConstTerm.java
View File

@ -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);
}
}

42
src/main/java/edu/kit/typicalc/model/term/IntegerTerm.java
View File

@ -1,7 +1,47 @@
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.
*/
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);
}
@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);
}
}

12
src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java
View File

@ -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);

65
src/main/java/edu/kit/typicalc/model/term/LetTerm.java
View File

@ -5,9 +5,27 @@ 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
* 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 +39,47 @@ 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;
}
@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);
}
}

19
src/main/java/edu/kit/typicalc/model/term/VarTerm.java
View File

@ -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

2
src/main/java/edu/kit/typicalc/model/type/FunctionType.java
View File

@ -1,5 +1,7 @@
package edu.kit.typicalc.model.type;
public class FunctionType extends Type {
public FunctionType(Type parameter, Type output) {
}
}

10
src/main/java/edu/kit/typicalc/model/type/NamedType.java Normal file
View 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
}
}

48
src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java
View File

@ -4,8 +4,13 @@ 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;
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 +34,47 @@ 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)
)
));
}
@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)
));
}
}