mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
UnificationStep + code style fixes
This commit is contained in:
parent
0d3d806e9c
commit
cd1cb29889
@ -3,6 +3,7 @@ package edu.kit.typicalc.model;
|
|||||||
import edu.kit.typicalc.model.type.Type;
|
import edu.kit.typicalc.model.type.Type;
|
||||||
import edu.kit.typicalc.model.type.TypeVariable;
|
import edu.kit.typicalc.model.type.TypeVariable;
|
||||||
|
|
||||||
|
import java.util.Collections;
|
||||||
import java.util.List;
|
import java.util.List;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@ -31,7 +32,7 @@ public class TypeInferenceResult {
|
|||||||
* @return the most general unifier, null if there is no valid mgu
|
* @return the most general unifier, null if there is no valid mgu
|
||||||
*/
|
*/
|
||||||
protected List<Substitution> getMGU() {
|
protected List<Substitution> getMGU() {
|
||||||
return null;
|
return Collections.emptyList();
|
||||||
// TODO
|
// TODO
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,4 +1,45 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.util.Result;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Models one step of the unification algorithm with a list of constraints and a list of substitutions.
|
||||||
|
* These lists contain all the constraints or substitutions that are present in the unification after this step.
|
||||||
|
* When detected that this unification step leads to a contradiction or an infinite type,
|
||||||
|
* it contains a {@link UnificationError} instead of a list of substitutions.
|
||||||
|
*/
|
||||||
public class UnificationStep {
|
public class UnificationStep {
|
||||||
|
private final Result<List<Substitution>, UnificationError> substitutions;
|
||||||
|
private final List<Constraint> constraints;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Initializes a new {@link UnificationStep} with the given lists of constraints and substitutions.
|
||||||
|
* When detected that this unification step leads to a contradiction or an infinite type,
|
||||||
|
* it should be passed a {@link UnificationError} instead of a list of substitutions.
|
||||||
|
* @param substitutions list of substitutions, or an error
|
||||||
|
* @param constraints the list of all constraints of the unification (in the state resulting from this step)
|
||||||
|
*/
|
||||||
|
protected UnificationStep(Result<List<Substitution>, UnificationError> substitutions,
|
||||||
|
List<Constraint> constraints) {
|
||||||
|
this.substitutions = substitutions;
|
||||||
|
this.constraints = constraints;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Returns as a {@link Result} either the list of all substitutions
|
||||||
|
* of the unification (in the state resulting from this step).
|
||||||
|
* Or, in case of a detected contradiction or infinite type, a {@link UnificationError}.
|
||||||
|
*/
|
||||||
|
public Result<List<Substitution>, UnificationError> getSubstitutions() {
|
||||||
|
return substitutions;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* @return a list of all resulting constraints
|
||||||
|
*/
|
||||||
|
public List<Constraint> getConstraints() {
|
||||||
|
return constraints;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -28,10 +28,6 @@ public class LambdaLexer {
|
|||||||
*/
|
*/
|
||||||
public LambdaLexer(String term) {
|
public LambdaLexer(String term) {
|
||||||
this.term = term;
|
this.term = term;
|
||||||
tokenize();
|
|
||||||
}
|
|
||||||
|
|
||||||
private void tokenize() {
|
|
||||||
Deque<Token> tokens = new ArrayDeque<>();
|
Deque<Token> tokens = new ArrayDeque<>();
|
||||||
while (true) {
|
while (true) {
|
||||||
Result<Token, ParseError> token = parseNextToken();
|
Result<Token, ParseError> token = parseNextToken();
|
||||||
|
@ -17,7 +17,7 @@ public enum ParseError {
|
|||||||
*/
|
*/
|
||||||
UNEXPECTED_CHARACTER;
|
UNEXPECTED_CHARACTER;
|
||||||
|
|
||||||
private Token cause;
|
private Token cause = new Token(Token.TokenType.EOF, "", -1);
|
||||||
|
|
||||||
public ParseError withToken(Token cause) {
|
public ParseError withToken(Token cause) {
|
||||||
this.cause = cause;
|
this.cause = cause;
|
||||||
|
@ -15,8 +15,8 @@ import java.util.Objects;
|
|||||||
* The subclasses vary in the premise(s) they contain.
|
* The subclasses vary in the premise(s) they contain.
|
||||||
*/
|
*/
|
||||||
public abstract class InferenceStep {
|
public abstract class InferenceStep {
|
||||||
private Conclusion conclusion;
|
private final Conclusion conclusion;
|
||||||
private Constraint constraint;
|
private final Constraint constraint;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Initializes a new InferenceStep with the given values.
|
* Initializes a new InferenceStep with the given values.
|
||||||
|
@ -4,6 +4,8 @@ import edu.kit.typicalc.model.Conclusion;
|
|||||||
import edu.kit.typicalc.model.Constraint;
|
import edu.kit.typicalc.model.Constraint;
|
||||||
import edu.kit.typicalc.model.TypeInfererLet;
|
import edu.kit.typicalc.model.TypeInfererLet;
|
||||||
|
|
||||||
|
import java.util.Objects;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Models one step of the inference tree where the let rule is applied. A let step contains an
|
* Models one step of the inference tree where the let rule is applied. A let step contains an
|
||||||
* additional instance of a type inferer that is responisble for the „sub-inference“ that takes
|
* additional instance of a type inferer that is responisble for the „sub-inference“ that takes
|
||||||
@ -46,4 +48,24 @@ public abstract class LetStep extends InferenceStep {
|
|||||||
public TypeInfererLet getTypeInferer() {
|
public TypeInfererLet getTypeInferer() {
|
||||||
return typeInferer;
|
return typeInferer;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public boolean equals(Object o) {
|
||||||
|
if (this == o) {
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
if (o == null || getClass() != o.getClass()) {
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
if (!super.equals(o)) {
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
LetStep letStep = (LetStep) o;
|
||||||
|
return premise.equals(letStep.premise) && typeInferer.equals(letStep.typeInferer);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public int hashCode() {
|
||||||
|
return Objects.hash(super.hashCode(), premise, typeInferer);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -13,10 +13,7 @@ import java.util.Optional;
|
|||||||
* Utility class to avoid unification logic duplication in type methods.
|
* Utility class to avoid unification logic duplication in type methods.
|
||||||
*/
|
*/
|
||||||
final class UnificationUtil {
|
final class UnificationUtil {
|
||||||
// TODO: document class? implementation detail?
|
private UnificationUtil() { }
|
||||||
private UnificationUtil() {
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
static Result<UnificationActions, UnificationError> functionFunction(FunctionType a, FunctionType b) {
|
static Result<UnificationActions, UnificationError> functionFunction(FunctionType a, FunctionType b) {
|
||||||
return new Result<>(new UnificationActions(List.of(
|
return new Result<>(new UnificationActions(List.of(
|
||||||
|
Loading…
Reference in New Issue
Block a user