mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-09 10:50:42 +00:00
Formatting
This commit is contained in:
parent
87304d23f1
commit
91099dcb9f
@ -11,63 +11,63 @@ 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;
|
||||
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;
|
||||
}
|
||||
/**
|
||||
* 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 variable of this abstraction
|
||||
*/
|
||||
public VarTerm getVariable() {
|
||||
return var;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the function body of this abstraction
|
||||
*/
|
||||
public LambdaTerm getInner() {
|
||||
return body;
|
||||
}
|
||||
/**
|
||||
* @return the function body of this abstraction
|
||||
*/
|
||||
public LambdaTerm getInner() {
|
||||
return body;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return body.hasLet();
|
||||
}
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return body.hasLet();
|
||||
}
|
||||
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return termVisitorTree.visit(this, assumptions, type);
|
||||
}
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return termVisitorTree.visit(this, assumptions, type);
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
AbsTerm absTerm = (AbsTerm) o;
|
||||
return Objects.equals(var, absTerm.var) && Objects.equals(body, absTerm.body);
|
||||
}
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
AbsTerm absTerm = (AbsTerm) o;
|
||||
return Objects.equals(var, absTerm.var) && Objects.equals(body, absTerm.body);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(var, body);
|
||||
}
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(var, body);
|
||||
}
|
||||
}
|
||||
|
@ -11,62 +11,62 @@ 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;
|
||||
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;
|
||||
}
|
||||
/**
|
||||
* 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;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the function used in this application
|
||||
*/
|
||||
public LambdaTerm getFunction() {
|
||||
return left;
|
||||
}
|
||||
/**
|
||||
* @return the function used in this application
|
||||
*/
|
||||
public LambdaTerm getFunction() {
|
||||
return left;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the parameter used in this application
|
||||
*/
|
||||
public LambdaTerm getParameter() {
|
||||
return right;
|
||||
}
|
||||
/**
|
||||
* @return the parameter used in this application
|
||||
*/
|
||||
public LambdaTerm getParameter() {
|
||||
return right;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return left.hasLet() || right.hasLet();
|
||||
}
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return left.hasLet() || right.hasLet();
|
||||
}
|
||||
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return termVisitorTree.visit(this, assumptions, type);
|
||||
}
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return termVisitorTree.visit(this, assumptions, type);
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
AppTerm appTerm = (AppTerm) o;
|
||||
return Objects.equals(left, appTerm.left) && Objects.equals(right, appTerm.right);
|
||||
}
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
AppTerm appTerm = (AppTerm) o;
|
||||
return Objects.equals(left, appTerm.left) && Objects.equals(right, appTerm.right);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(left, right);
|
||||
}
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(left, right);
|
||||
}
|
||||
}
|
||||
|
@ -8,45 +8,45 @@ import java.util.Objects;
|
||||
* Representation of a constant boolean lambda term: either false or true.
|
||||
*/
|
||||
public class BooleanTerm extends ConstTerm {
|
||||
private final boolean value;
|
||||
private final boolean value;
|
||||
|
||||
/**
|
||||
* Initializes a new boolean lambda term with the given value.
|
||||
* @param value true or false
|
||||
*/
|
||||
public BooleanTerm(boolean value) {
|
||||
this.value = value;
|
||||
}
|
||||
/**
|
||||
* Initializes a new boolean lambda term with the given value.
|
||||
* @param value true or false
|
||||
*/
|
||||
public BooleanTerm(boolean value) {
|
||||
this.value = value;
|
||||
}
|
||||
|
||||
@Override
|
||||
public NamedType getType() {
|
||||
return NamedType.BOOLEAN;
|
||||
}
|
||||
@Override
|
||||
public NamedType getType() {
|
||||
return NamedType.BOOLEAN;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return false;
|
||||
}
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return false;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return Boolean.toString(value);
|
||||
}
|
||||
@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 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);
|
||||
}
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(value);
|
||||
}
|
||||
}
|
||||
|
@ -11,23 +11,23 @@ import java.util.Map;
|
||||
* 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();
|
||||
/**
|
||||
* @return the named type of the constant
|
||||
*/
|
||||
public abstract NamedType getType();
|
||||
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return false;
|
||||
}
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return false;
|
||||
}
|
||||
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree visitor, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return visitor.visit(this, assumptions, type);
|
||||
}
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree visitor, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return visitor.visit(this, assumptions, type);
|
||||
}
|
||||
}
|
||||
|
@ -8,40 +8,40 @@ 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;
|
||||
private final int value;
|
||||
|
||||
/**
|
||||
* Initializes a new integer lambda term with the given value.
|
||||
* @param value an integer
|
||||
*/
|
||||
public IntegerTerm(int value) {
|
||||
this.value = value;
|
||||
}
|
||||
/**
|
||||
* Initializes a new integer lambda term with the given value.
|
||||
* @param value an integer
|
||||
*/
|
||||
public IntegerTerm(int value) {
|
||||
this.value = value;
|
||||
}
|
||||
|
||||
@Override
|
||||
public NamedType getType() {
|
||||
return NamedType.INT;
|
||||
}
|
||||
@Override
|
||||
public NamedType getType() {
|
||||
return NamedType.INT;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return Integer.toString(value);
|
||||
}
|
||||
@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 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);
|
||||
}
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(value);
|
||||
}
|
||||
}
|
||||
|
@ -12,24 +12,24 @@ import java.util.Map;
|
||||
* and thus form a tree-like structure of lambda terms.
|
||||
*/
|
||||
public abstract class LambdaTerm {
|
||||
/**
|
||||
* @return whether the lambda term contains a let expression
|
||||
*/
|
||||
public abstract boolean hasLet();
|
||||
/**
|
||||
* @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);
|
||||
/**
|
||||
* Calls exactly one method on the visitor depending on the lambda term type.
|
||||
* @param termVisitor a visitor
|
||||
*/
|
||||
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
|
||||
*/
|
||||
/**
|
||||
* 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);
|
||||
|
||||
|
@ -12,74 +12,74 @@ import java.util.Objects;
|
||||
* to this variable and the lambda term the variable is used in.
|
||||
*/
|
||||
public class LetTerm extends LambdaTerm {
|
||||
private final VarTerm variable;
|
||||
private final LambdaTerm definition;
|
||||
private final 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;
|
||||
}
|
||||
/**
|
||||
* 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
|
||||
public boolean hasLet() {
|
||||
return true;
|
||||
}
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return true;
|
||||
}
|
||||
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree visitor, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return visitor.visit(this, assumptions, type);
|
||||
}
|
||||
@Override
|
||||
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 the variable defined in this let expression
|
||||
*/
|
||||
public VarTerm getVariable() {
|
||||
return variable;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return definition of the variable
|
||||
*/
|
||||
public LambdaTerm getVariableDefinition() {
|
||||
return definition;
|
||||
}
|
||||
/**
|
||||
* @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;
|
||||
}
|
||||
/**
|
||||
* @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 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);
|
||||
}
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(variable, definition, body);
|
||||
}
|
||||
}
|
||||
|
@ -1,33 +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 application term.
|
||||
* @param appTerm the term
|
||||
*/
|
||||
void visit(AppTerm appTerm);
|
||||
|
||||
/**
|
||||
* Visit an abstraction term.
|
||||
* @param absTerm the term
|
||||
*/
|
||||
void visit(AbsTerm absTerm);
|
||||
/**
|
||||
* 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 let expression.
|
||||
* @param letTerm the term
|
||||
*/
|
||||
void visit(LetTerm letTerm);
|
||||
|
||||
/**
|
||||
* Visit a variable.
|
||||
* @param varTerm the variable
|
||||
*/
|
||||
void visit(VarTerm varTerm);
|
||||
/**
|
||||
* Visit a variable.
|
||||
* @param varTerm the variable
|
||||
*/
|
||||
void visit(VarTerm varTerm);
|
||||
|
||||
/**
|
||||
* Visit a constant.
|
||||
* @param constTerm the constant
|
||||
*/
|
||||
void visit(ConstTerm constTerm);
|
||||
/**
|
||||
* Visit a constant.
|
||||
* @param constTerm the constant
|
||||
*/
|
||||
void visit(ConstTerm constTerm);
|
||||
}
|
||||
|
@ -7,73 +7,73 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
|
||||
import java.util.Map;
|
||||
|
||||
public interface TermVisitorTree {
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.AppStep} suiting the given application (lambda term)
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param appTerm the application (lambda term) to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.AppStep}
|
||||
*/
|
||||
InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.AppStep} suiting the given application (lambda term)
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param appTerm the application (lambda term) to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.AppStep}
|
||||
*/
|
||||
InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term)
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param absTerm the abstraction (lambda term) to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.AbsStep}
|
||||
*/
|
||||
InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term)
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param absTerm the abstraction (lambda term) to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.AbsStep}
|
||||
*/
|
||||
InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term)
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param letTerm the let expression (lambda term) to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.LetStep}
|
||||
*/
|
||||
InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term)
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param letTerm the let expression (lambda term) to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.LetStep}
|
||||
*/
|
||||
InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param constTerm the constant to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.ConstStep}
|
||||
*/
|
||||
InferenceStep visit(ConstTerm constTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param constTerm the constant to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.ConstStep}
|
||||
*/
|
||||
InferenceStep visit(ConstTerm constTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term)
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param varTerm the variable (lambda term) to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.VarStep}
|
||||
*/
|
||||
InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
/**
|
||||
* Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term)
|
||||
* to type-infer and the type assumptions to consider.
|
||||
* Simultaneously assembles the tree's constraint list.
|
||||
* @param varTerm the variable (lambda term) to build the inference step structure for,
|
||||
* i.e. the lambda term in the conclusion of the returned inference step
|
||||
* @param typeAssumptions the type assumptions to consider,
|
||||
* i.e. the type assumptions in the conclusion of the returned inference step
|
||||
* @param conclusionType the type that the lambda term in the conclusion
|
||||
* of the returned inference step will be assigned
|
||||
* @return an {@link edu.kit.typicalc.model.step.VarStep}
|
||||
*/
|
||||
InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
|
||||
}
|
||||
|
@ -11,53 +11,53 @@ import java.util.Objects;
|
||||
* Representation of a variable term with its name.
|
||||
*/
|
||||
public class VarTerm extends LambdaTerm {
|
||||
private final String name;
|
||||
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;
|
||||
}
|
||||
/**
|
||||
* 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;
|
||||
}
|
||||
/**
|
||||
* @return the name of this variable
|
||||
*/
|
||||
public String getName() {
|
||||
return name;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return false;
|
||||
}
|
||||
@Override
|
||||
public boolean hasLet() {
|
||||
return false;
|
||||
}
|
||||
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
@Override
|
||||
public void accept(TermVisitor termVisitor) {
|
||||
termVisitor.visit(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree visitor, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return visitor.visit(this, assumptions, type);
|
||||
}
|
||||
@Override
|
||||
public InferenceStep accept(TermVisitorTree visitor, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
|
||||
return visitor.visit(this, assumptions, type);
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
VarTerm varTerm = (VarTerm) o;
|
||||
return Objects.equals(name, varTerm.name);
|
||||
}
|
||||
@Override
|
||||
public boolean equals(Object o) {
|
||||
if (this == o) {
|
||||
return true;
|
||||
}
|
||||
if (o == null || getClass() != o.getClass()) {
|
||||
return false;
|
||||
}
|
||||
VarTerm varTerm = (VarTerm) o;
|
||||
return Objects.equals(name, varTerm.name);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(name);
|
||||
}
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return Objects.hash(name);
|
||||
}
|
||||
}
|
||||
|
@ -2,88 +2,93 @@ 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;
|
||||
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;
|
||||
}
|
||||
/**
|
||||
* Creates a new result containing the given value.
|
||||
*
|
||||
* @param value the value
|
||||
*/
|
||||
public Result(T value) {
|
||||
this.value = value;
|
||||
this.error = null;
|
||||
}
|
||||
|
||||
/**
|
||||
* 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;
|
||||
}
|
||||
/**
|
||||
* 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 a regular value
|
||||
*/
|
||||
public boolean isOk() {
|
||||
return value != null;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return whether the result contains an error
|
||||
*/
|
||||
public boolean isError() {
|
||||
return error != null;
|
||||
}
|
||||
/**
|
||||
* @return whether the result contains an error
|
||||
*/
|
||||
public boolean isError() {
|
||||
return error != null;
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 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;
|
||||
}
|
||||
/**
|
||||
* 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 value contained, or null
|
||||
*/
|
||||
public T getValue() {
|
||||
return value;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the error contained, or null
|
||||
*/
|
||||
public E getError() {
|
||||
return error;
|
||||
}
|
||||
/**
|
||||
* @return the error contained, or null
|
||||
*/
|
||||
public E getError() {
|
||||
return error;
|
||||
}
|
||||
}
|
||||
|
@ -1,4 +1,4 @@
|
||||
root.close=Schlie<EFBFBD>en
|
||||
root.close=Schließen
|
||||
root.copyLatex=Kopiere Latex-Code
|
||||
|
||||
abs-rule=\\begin{prooftree}\
|
||||
@ -10,5 +10,4 @@ abs-rule=\\begin{prooftree}\
|
||||
\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\
|
||||
\\end{prooftree}
|
||||
|
||||
test=hello world
|
||||
|
||||
test=hello world
|
@ -9,4 +9,4 @@ abs-rule=\
|
||||
|
||||
test=hello world
|
||||
root.close=Close
|
||||
root.copyLatex=Copy latex code
|
||||
root.copyLatex=Copy latex code
|
Loading…
Reference in New Issue
Block a user