mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-09 10:50:42 +00:00
Term javadocs, TermVisitor, Result javadocs, mehr Parser-Tests
This commit is contained in:
parent
f3fd6d0696
commit
143999d6e9
@ -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<TypeAssumption> typeAssumptions, Type conclusionType) {
|
||||
return null; // TODO
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep visit(AbsTerm absTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
|
||||
return null; // TODO
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep visit(LetTerm letTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
|
||||
return null; // TODO
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep visit(ConstTerm constTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
|
||||
return null; // TODO
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep visit(VarTerm varTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
|
||||
return null; // TODO
|
||||
}
|
||||
}
|
||||
|
@ -84,10 +84,10 @@ public class LambdaParser {
|
||||
switch (token.getType()) {
|
||||
case LAMBDA:
|
||||
Result<AbsTerm, ParseError> abs = parseAbstraction();
|
||||
return new Result<>(abs.unwrap(), abs.unwrapError());
|
||||
return new Result<>(abs.unwrap(), abs.getError());
|
||||
case LET:
|
||||
Result<LetTerm, ParseError> 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<VarTerm, ParseError> var = parseVar();
|
||||
return new Result<>(var.unwrap(), var.unwrapError());
|
||||
return new Result<>(var.unwrap(), var.getError());
|
||||
case NUMBER:
|
||||
String number = token.getText();
|
||||
int n;
|
||||
|
@ -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) {
|
||||
|
@ -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) {
|
||||
|
@ -4,4 +4,9 @@ public class BooleanTerm extends ConstTerm {
|
||||
public BooleanTerm(boolean value) {
|
||||
// TODO
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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) {
|
||||
|
@ -0,0 +1,5 @@
|
||||
package edu.kit.typicalc.model.type;
|
||||
|
||||
public class FunctionType extends Type {
|
||||
|
||||
}
|
@ -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);
|
||||
}
|
||||
|
@ -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 <T> value type
|
||||
* @param <E> error type
|
||||
*/
|
||||
public class Result<T, E> {
|
||||
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;
|
||||
}
|
||||
}
|
||||
|
@ -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) {
|
||||
|
||||
}
|
||||
}
|
||||
|
@ -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<LambdaTerm, ParseError> term = parser.parse();
|
||||
System.out.println(term);
|
||||
assertEquals(term.unwrap(), new VarTerm("x"));
|
||||
}
|
||||
@Test
|
||||
void absTerm() {
|
||||
|
Loading…
Reference in New Issue
Block a user