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

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
Moritz Dieing 2021-02-20 00:33:58 +01:00
commit 3283d566f3
86 changed files with 459 additions and 250 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/main/java/edu/kit/typicalc/Application.java
View File

@ -14,9 +14,8 @@ import java.util.regex.Pattern;
/**
* The entry point of the Spring Boot application.
*
* <p>
* Use the * and some desktop browsers.
*
*/
@SpringBootApplication
public class Application extends SpringBootServletInitializer

10
src/main/java/edu/kit/typicalc/model/Conclusion.java
View File

@ -22,8 +22,8 @@ public class Conclusion {
* Initializes a new Conclusion with the given type assumptions, lambda term and type.
*
* @param typeAssumptions the type assumptions used in the conclusion
* @param lambdaTerm the lambda term in the conclusion
* @param type the type assigned to the lambda term in the conclusion
* @param lambdaTerm the lambda term in the conclusion
* @param type the type assigned to the lambda term in the conclusion
*/
public Conclusion(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm, Type type) {
this.typeAssumptions = typeAssumptions;
@ -32,6 +32,8 @@ public class Conclusion {
}
/**
* Returns the type assumptions used in the conclusion
*
* @return the type assumptions used in the conclusion
*/
public Map<VarTerm, TypeAbstraction> getTypeAssumptions() {
@ -39,6 +41,8 @@ public class Conclusion {
}
/**
* Returns the lambda term in the conclusion
*
* @return the lambda term in the conclusion
*/
public LambdaTerm getLambdaTerm() {
@ -46,6 +50,8 @@ public class Conclusion {
}
/**
* Returns the type assigned to the lambda term in the conclusion
*
* @return the type assigned to the lambda term in the conclusion
*/
public Type getType() {

4
src/main/java/edu/kit/typicalc/model/Constraint.java
View File

@ -24,6 +24,8 @@ public class Constraint {
}
/**
* Returns the first type
*
* @return the first type
*/
public Type getFirstType() {
@ -31,6 +33,8 @@ public class Constraint {
}
/**
* Returns the second type
*
* @return the second type
*/
public Type getSecondType() {

11
src/main/java/edu/kit/typicalc/model/Model.java
View File

@ -1,10 +1,10 @@
package edu.kit.typicalc.model;
import java.util.Map;
import edu.kit.typicalc.model.parser.ParseError;
import edu.kit.typicalc.util.Result;
import java.util.Map;
/**
* This interface accepts user input and returns a type inference result.
*/
@ -12,10 +12,11 @@ public interface Model {
/**
* Given the user input, an implementation of this method should compute the type
* inference results.
* @param lambdaTerm the lambda term to type-infer
* @param typeAssumptions the type assumptions to use
*
* @param lambdaTerm the lambda term to type-infer
* @param typeAssumptions the type assumptions to use
* @return either an error or a TypeInfererInterface on success
*/
Result<TypeInfererInterface, ParseError> getTypeInferer(String lambdaTerm,
Map<String, String> typeAssumptions);
Map<String, String> typeAssumptions);
}

6
src/main/java/edu/kit/typicalc/model/ModelImpl.java
View File

@ -16,13 +16,13 @@ import java.util.Map;
public class ModelImpl implements Model {
/**
*Parses the user input given as the lambdaTerm and typeAssumptions and creates
* Parses the user input given as the lambdaTerm and typeAssumptions and creates
* a TypeInferer object.
* @param lambdaTerm the lambda term to type-infer
*
* @param lambdaTerm the lambda term to type-infer
* @param typeAssumptions the type assumptions to use
* @return A TypeInferer object that has calculated the type Inference for the given Lambda Term
* and type Assumptions
*
*/
@Override
public Result<TypeInfererInterface, ParseError> getTypeInferer(String lambdaTerm,

4
src/main/java/edu/kit/typicalc/model/Substitution.java
View File

@ -26,6 +26,8 @@ public class Substitution {
}
/**
* Returns the type variable
*
* @return the type variable
*/
public TypeVariable getVariable() {
@ -33,6 +35,8 @@ public class Substitution {
}
/**
* Returns the replacement type
*
* @return the replacement type
*/
public Type getType() {

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

@ -28,8 +28,8 @@ public class Tree implements TermVisitorTree {
* lambda term considering the given type assumptions. The inference step structure
* and constraint list are generated here.
*
* @param typeAssumptions the type assumptions to consider when generating the tree
* @param lambdaTerm the lambda term to generate the tree for
* @param typeAssumptions the type assumptions to consider when generating the tree
* @param lambdaTerm the lambda term to generate the tree for
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm) {
this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVariableKind.TREE), false);
@ -42,10 +42,10 @@ public class Tree implements TermVisitorTree {
* variable names, a type variable factory is provided as a parameter. The inference
* step structure and constraint list are generated here.
*
* @param typeAssumptions the type assumptions to consider when generating the tree
* @param lambdaTerm the lambda term to generate the tree for
* @param typeAssumptions the type assumptions to consider when generating the tree
* @param lambdaTerm the lambda term to generate the tree for
* @param typeVariableFactory the type variable factory to use
* @param partOfLetTerm indicates whether the tree is generated for a sub-inference that is part of a let term
* @param partOfLetTerm indicates whether the tree is generated for a sub-inference that is part of a let term
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm,
TypeVariableFactory typeVariableFactory, boolean partOfLetTerm) {

5
src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java
View File

@ -25,9 +25,10 @@ public class TypeInferenceResult {
* to this given type variable. The mgu and the final type are generated here.
*
* @param substitutions the substitutions to generate the mgu and the final type
* @param typeVar the type variable belonging to the original lambda term
* @param typeVar the type variable belonging to the original lambda term
* @throws IllegalStateException if the given list of substitutions contains two substitutions for the same
* type variable; or if the calculated mgu contains no substitution for the given type variable
* type variable; or if the calculated mgu contains no substitution for the given
* type variable
*/
protected TypeInferenceResult(List<Substitution> substitutions, TypeVariable typeVar) {
mgu = new ArrayList<>(substitutions);

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

@ -28,7 +28,7 @@ public class TypeInferer implements TypeInfererInterface {
* The inference step structure, unification steps, the most general unifier and the
* final type are generated and calculated here.
*
* @param lambdaTerm the lambda term to generate the tree for
* @param lambdaTerm the lambda term to generate the tree for
* @param typeAssumptions the type assumptions to consider when generating the tree
*/
protected TypeInferer(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions) {

4
src/main/java/edu/kit/typicalc/model/TypeInfererLet.java
View File

@ -23,8 +23,8 @@ public class TypeInfererLet implements TypeInfererInterface {
*
* @param lambdaTerm the lambda term to generate the tree for
* @param typeAssumptions the type assumptions to consider when generating the tree
* @param typeVarFactory the type variable factory that should be used in this inference to guarantee consistency
* with the outer inference
* @param typeVarFactory the type variable factory that should be used in this inference to guarantee consistency
* with the outer inference
*/
protected TypeInfererLet(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions,
TypeVariableFactory typeVarFactory) {

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

@ -17,6 +17,7 @@ public class Unification {
/**
* Initializes a new {@link Unification} for the given constraints.
* The list of unification steps and the resulting substitutions are generated here.
*
* @param constraints constraints to execute the unification for
*/
protected Unification(Deque<Constraint> constraints) { // TODO: document List->Deque
@ -62,6 +63,8 @@ public class Unification {
}
/**
* Returns list of the unification steps the unification performs.
*
* @return list of the unification steps the unification performs.
*/
protected List<UnificationStep> getUnificationSteps() {

9
src/main/java/edu/kit/typicalc/model/UnificationStep.java
View File

@ -18,10 +18,11 @@ public class UnificationStep {
/**
* 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.
* 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)
* @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) {
@ -41,6 +42,8 @@ public class UnificationStep {
}
/**
* Returns a list of all resulting constraints
*
* @return a list of all resulting constraints
*/
public List<Constraint> getConstraints() {

16
src/main/java/edu/kit/typicalc/model/package-info.java
View File

@ -1,12 +1,12 @@
/**
* The model package contains all classes needed to model the typed lambda calculus and the type inference algorithm.
* To do so, it contains the sub-packages term, type, step and parser.
* The model package itself contains the ModelInterface, functioning as an interface for the presenter
* and the classes executing the type inference algorithm.
* The class TypeInferer combines the three separated parts of the algorithm:
* the building of the tree, execution of the unification and calculation of the most general unifier and final type.
* An instance of TypeInferer, fitting the lambda term from the user input, is passed to the view to obtain the data
* needed for the visualization of the computed steps of the algorithm.
* The model package contains all classes needed to model the typed lambda calculus and the type inference algorithm.
* To do so, it contains the sub-packages term, type, step and parser.
* The model package itself contains the ModelInterface, functioning as an interface for the presenter
* and the classes executing the type inference algorithm.
* The class TypeInferer combines the three separated parts of the algorithm:
* the building of the tree, execution of the unification and calculation of the most general unifier and final type.
* An instance of TypeInferer, fitting the lambda term from the user input, is passed to the view to obtain the data
* needed for the visualization of the computed steps of the algorithm.
*/
@NonNullFields
@NonNullApi

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

@ -13,7 +13,7 @@ import java.util.Deque;
*/
public class LambdaLexer {
/**
* The given term as a String
* the given term as a String
*/
private final String term;
/**
@ -24,6 +24,7 @@ public class LambdaLexer {
/**
* Constructs a lexer that lexes the given term
*
* @param term the term to lex
*/
public LambdaLexer(String term) {
@ -53,6 +54,7 @@ public class LambdaLexer {
/**
* Returns the next token and advances the lexer position.
*
* @return the next token
*/
public Result<Token, ParseError> nextToken() {
@ -88,7 +90,7 @@ public class LambdaLexer {
} else {
return new Result<>(null, ParseError.UNEXPECTED_CHARACTER);
}
// bunch of single-character tokens
// bunch of single-character tokens
case '.':
t = new Token(TokenType.DOT, ".", pos);
advance();

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

@ -9,7 +9,7 @@ package edu.kit.typicalc.model.parser;
public enum ParseError {
/**
* the lambda term didn't meet the specified syntax
* the lambda term didn't meet the specified syntax
*/
UNEXPECTED_TOKEN,

6
src/main/java/edu/kit/typicalc/model/parser/Token.java
View File

@ -40,9 +40,10 @@ public class Token {
/**
* Constructs a token.
*
* @param type the token type
* @param text text of this token in the source code
* @param pos position this token begins
* @param pos position this token begins
*/
public Token(TokenType type, String text, int pos) {
this.type = type;
@ -52,6 +53,7 @@ public class Token {
/**
* Returns the token type
*
* @return token type
*/
public TokenType getType() {
@ -60,6 +62,7 @@ public class Token {
/**
* Returns the text of this token in the source code
*
* @return text of this token in the source code
*/
public String getText() {
@ -68,6 +71,7 @@ public class Token {
/**
* Returns the position this token is in
*
* @return position this token is in
*/
public int getPos() {

4
src/main/java/edu/kit/typicalc/model/parser/package-info.java
View File

@ -1,6 +1,6 @@
/**
* The parser package contains all classes needed to parse the input strings from the user to an abstract form
* consisting of classes provided by the the model, term and type package.
* The parser package contains all classes needed to parse the input strings from the user to an abstract form
* consisting of classes provided by the the model, term and type package.
*/
@NonNullApi
@NonNullFields

4
src/main/java/edu/kit/typicalc/model/step/AbsStep.java
View File

@ -14,7 +14,8 @@ public abstract class AbsStep extends InferenceStep {
/**
* Initializes a new AbsStep with the given values.
* @param premise the premise of this step
*
* @param premise the premise of this step
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
*/
@ -25,6 +26,7 @@ public abstract class AbsStep extends InferenceStep {
/**
* Getter for the premise of this step.
*
* @return premise the premise of this step
*/
public InferenceStep getPremise() {

4
src/main/java/edu/kit/typicalc/model/step/AbsStepDefault.java
View File

@ -10,7 +10,8 @@ import edu.kit.typicalc.model.Constraint;
public class AbsStepDefault extends AbsStep {
/**
* Initializes a new AbsStepDefault with the given values.
* @param premise the premise of this step
*
* @param premise the premise of this step
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
*/
@ -20,6 +21,7 @@ public class AbsStepDefault extends AbsStep {
/**
* Accepts a visitor.
*
* @param stepVisitor – the visitor that wants to visit this object
*/
@Override

4
src/main/java/edu/kit/typicalc/model/step/AbsStepWithLet.java
View File

@ -10,7 +10,8 @@ import edu.kit.typicalc.model.Constraint;
public class AbsStepWithLet extends AbsStep {
/**
* Initializes a new AbsStepWithLet with the given values.
* @param premise the premise of this step
*
* @param premise the premise of this step
* @param conclusion the conclusion of this step
* @param constraint constraint that can be derived from this step
*/
@ -20,6 +21,7 @@ public class AbsStepWithLet extends AbsStep {
/**
* Accepts a visitor.
*
* @param stepVisitor the visitor that wants to visit this object
*/
@Override

10
src/main/java/edu/kit/typicalc/model/step/AppStep.java
View File

@ -16,9 +16,10 @@ public abstract class AppStep extends InferenceStep {
private final InferenceStep premise2;
/**
Initializes a new AbsStepWithLet with the given values.
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
* Initializes a new AbsStepWithLet with the given values.
*
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
* @param conclusion the conclusion of this step
* @param constraint constraint that can be derived from this step
*/
@ -30,13 +31,16 @@ public abstract class AppStep extends InferenceStep {
/**
* Getter for the first premise of this Step.
*
* @return premise1 the first premise of this Step.
*/
public InferenceStep getPremise1() {
return premise1;
}
/**
* Getter for the second premise of this Step.
*
* @return premise2 the second premise of this Step.
*/
public InferenceStep getPremise2() {

8
src/main/java/edu/kit/typicalc/model/step/AppStepDefault.java
View File

@ -9,9 +9,10 @@ import edu.kit.typicalc.model.Constraint;
*/
public class AppStepDefault extends AppStep {
/**
*Initializes a new AbsStepWithLet with the given values.
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
* Initializes a new AbsStepWithLet with the given values.
*
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
* @param conclusion the conclusion of this step
* @param constraint constraint that can be derived from this step
*/
@ -22,6 +23,7 @@ public class AppStepDefault extends AppStep {
/**
* Accepts a visitor.
*
* @param stepVisitor – the visitor that wants to visit this object
*/
@Override

1
src/main/java/edu/kit/typicalc/model/step/ConstStep.java
View File

@ -9,6 +9,7 @@ import edu.kit.typicalc.model.Constraint;
public abstract class ConstStep extends InferenceStep {
/**
* Initializes a new ConstStep with the given values.
*
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
*/

2
src/main/java/edu/kit/typicalc/model/step/ConstStepDefault.java
View File

@ -11,6 +11,7 @@ import edu.kit.typicalc.model.Constraint;
public class ConstStepDefault extends ConstStep {
/**
* Initializes a new ConstStep with the given values.
*
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
*/
@ -20,6 +21,7 @@ public class ConstStepDefault extends ConstStep {
/**
* Accepts a visitor.
*
* @param stepVisitor the visitor that wants to visit this object
*/
@Override

14
src/main/java/edu/kit/typicalc/model/step/LetStep.java
View File

@ -8,7 +8,7 @@ import java.util.Objects;
/**
* 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 responsible for the „sub-inference“ that takes
* place when applying the let rule. This type inferer grants access to all the information
* needed to visualize this sub-inference.
* If the sub-inference fails due to a contradiction or an infinite type forming in its unification,
@ -21,9 +21,10 @@ public abstract class LetStep extends InferenceStep {
/**
* Initializes a new LetStep with the given values.
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
* @param premise the right premise of this step
*
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
* @param premise the right premise of this step
* @param typeInferer the typeInferer that performs the Type Inference for the premise
* that needs its own type Inference.
*/
@ -32,9 +33,11 @@ public abstract class LetStep extends InferenceStep {
this.premise = premise;
this.typeInferer = typeInferer;
}
/**
* Returns the premise of the let step that doesn’t have its own sub-inference (the
* Returns the premise of the let step that doesn't have its own sub-inference (the
* one usually placed right in the proof tree).
*
* @return premise the right premise of this step
*/
public InferenceStep getPremise() {
@ -43,6 +46,7 @@ public abstract class LetStep extends InferenceStep {
/**
* Returns the TypeInferer for the premise which needs its own type Inference.
*
* @return typeInferer the type inferer of the sub-inference
*/
public TypeInfererLet getTypeInferer() {

8
src/main/java/edu/kit/typicalc/model/step/LetStepDefault.java
View File

@ -10,9 +10,10 @@ import edu.kit.typicalc.model.TypeInfererLet;
public class LetStepDefault extends LetStep {
/**
* Initializes a new LetStep with the given values.
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
* @param premise the right premise of this step
*
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
* @param premise the right premise of this step
* @param typeInferer the typeInferer that performs the Type Inference for the premise
* that needs its own type Inference.
*/
@ -23,6 +24,7 @@ public class LetStepDefault extends LetStep {
/**
* Accepts a visitor.
*
* @param stepVisitor the visitor that wants to visit this object
*/
@Override

27
src/main/java/edu/kit/typicalc/model/step/StepFactory.java
View File

@ -12,7 +12,8 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
public interface StepFactory {
/**
* Creates an AbsStep.
* @param premise the premise of this step
*
* @param premise the premise of this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AbsStep
@ -21,16 +22,19 @@ public interface StepFactory {
/**
* Creates an AppStep.
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
*
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AppStep
*/
AppStep createAppStep(InferenceStep premise1, InferenceStep premise2,
Conclusion conclusion, Constraint constraint);
Conclusion conclusion, Constraint constraint);
/**
* Creates an ConstStep.
*
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created ConstStep
@ -39,19 +43,22 @@ public interface StepFactory {
/**
* Creates a VarStep.
* @param typeAbstraction the type abstraction of this step
*
* @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AbsStep
*/
VarStep createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
Conclusion conclusion, Constraint constraint);
/**
* Creates a LetStep.
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param premise the premise that doesn't need its own type inference
*
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param premise the premise that doesn't need its own type inference
* @param typeInferer the typeInferer for the premise that needs its own type inference
* @return the created AppStep
*/

25
src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java
View File

@ -13,7 +13,8 @@ public class StepFactoryDefault implements StepFactory {
/**
* Creates an AbsStepDefault.
* @param premise the premise of this step
*
* @param premise the premise of this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AbsStepDefault
@ -25,20 +26,22 @@ public class StepFactoryDefault implements StepFactory {
/**
* Creates an AppStepDefault.
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
*
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AppStepDefault
*/
@Override
public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2,
Conclusion conclusion, Constraint constraint) {
Conclusion conclusion, Constraint constraint) {
return new AppStepDefault(premise1, premise2, conclusion, constraint);
}
/**
* Creates an ConstStepDefault.
*
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created ConstStepDefault
@ -50,10 +53,11 @@ public class StepFactoryDefault implements StepFactory {
/**
* Creates a VarStepDefault.
* @param typeAbstraction the type abstraction of this step
*
* @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AbsStepDefault
*/
@Override
@ -67,9 +71,10 @@ public class StepFactoryDefault implements StepFactory {
* This method should never be called, as a StepFactoryDefault should only be used
* for lambda terms without any let polymorphism and therefore should never have
* to create a step where the let rule is applied.
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param premise the premise that doesn't need its own type inference
*
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param premise the premise that doesn't need its own type inference
* @param typeInferer the typeInferer for the premise that needs its own type inference
* @return nothing
*/

23
src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java
View File

@ -13,7 +13,8 @@ public class StepFactoryWithLet implements StepFactory {
/**
* Creates an AbsStepWithLet.
* @param premise the premise of this step
*
* @param premise the premise of this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AbsStepWithLet
@ -25,8 +26,9 @@ public class StepFactoryWithLet implements StepFactory {
/**
* Creates an AppStepDefault.
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
*
* @param premise1 the first premise of this step
* @param premise2 the second premise of this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created AppStepDefault
@ -39,6 +41,7 @@ public class StepFactoryWithLet implements StepFactory {
/**
* Creates an ConstStepDefault.
*
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created ConstStepDefault
@ -50,10 +53,11 @@ public class StepFactoryWithLet implements StepFactory {
/**
* Creates a VarStepWithLet.
* @param typeAbstraction the type abstraction of this step
*
* @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @return the created VarStepWithLet
*/
@Override
@ -64,9 +68,10 @@ public class StepFactoryWithLet implements StepFactory {
/**
* Creates a LetStepDefault.
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param premise the premise that doesn't need its own type inference
*
* @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step
* @param premise the premise that doesn't need its own type inference
* @param typeInferer the typeInferer for the premise that needs its own type inference
* @return the created LetStepDefault
*/

8
src/main/java/edu/kit/typicalc/model/step/StepVisitor.java
View File

@ -7,48 +7,56 @@ public interface StepVisitor {
/**
* Visits an AbsStepDefault.
*
* @param absD the AbsStepDefault to visit
*/
void visit(AbsStepDefault absD);
/**
* Visits an AbsStepWithLet.
*
* @param absL the AbsStepWithLet to visit
*/
void visit(AbsStepWithLet absL);
/**
* Visits an AppStepDefault.
*
* @param appD the AppStepDefault to visit
*/
void visit(AppStepDefault appD);
/**
* ConstStepDefault.
*
* @param constD the ConstStepDefault to visit
*/
void visit(ConstStepDefault constD);
/**
* Visits a VarStepDefault.
*
* @param varD the VarStepDefault to visit
*/
void visit(VarStepDefault varD);
/**
* Visits a VarStepWithLet.
*
* @param varL the VarStepWithLet to visit
*/
void visit(VarStepWithLet varL);
/**
* Visits a LetStepDefault.
*
* @param letD the LetStepDefault to visit
*/
void visit(LetStepDefault letD);
/**
* Visits an empty step
*
* @param empty the empty step to visit
*/
void visit(EmptyStep empty);

7
src/main/java/edu/kit/typicalc/model/step/VarStep.java
View File

@ -20,9 +20,9 @@ public abstract class VarStep extends InferenceStep {
* Initializes a new VarStep with the given values.
*
* @param typeAbstractionInPremise the type abstraction in the premise of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
*/
protected VarStep(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
Constraint constraint) {
@ -30,6 +30,7 @@ public abstract class VarStep extends InferenceStep {
this.typeAbstractionInPremise = typeAbstractionInPremise;
this.instantiatedTypeAbs = instantiatedTypeAbs;
}
/**
* Returns the type abstraction in the premise of the step, that is identified as the
* variable’s type.

11
src/main/java/edu/kit/typicalc/model/step/VarStepDefault.java
View File

@ -5,14 +5,18 @@ import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
/**
* Models one step of the inference tree where the variable rule is applied and
* let polymorphism is not used in the entire tree.
*/
public class VarStepDefault extends VarStep {
/**
* Initializes a new VarStep with the given values.
*
* @param typeAbstractionInPremise the type abstraction in the premise of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
*/
public VarStepDefault(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
Constraint constraint) {
@ -21,6 +25,7 @@ public class VarStepDefault extends VarStep {
/**
* Accepts a visitor.
*
* @param stepVisitor the visitor that wants to visit this object
*/
@Override

12
src/main/java/edu/kit/typicalc/model/step/VarStepWithLet.java
View File

@ -5,14 +5,19 @@ import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
/**
* Models one step of the inference tree where the variable rule is applied and at least one
* let rule is applied in the entire tree. It additionally constrains a type that is obtained when
* instantiating the type abstraction in the premise of the step.
*/
public class VarStepWithLet extends VarStep {
/**
* Initializes a new VarStep with the given values.
*
* @param typeAbstractionInPremise the type abstraction in the premise of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step
* @param constraint the constraint added in this step
*/
public VarStepWithLet(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
Constraint constraint) {
@ -21,6 +26,7 @@ public class VarStepWithLet extends VarStep {
/**
* Accepts a visitor.
*
* @param stepVisitor the visitor that wants to visit this object
*/
@Override

6
src/main/java/edu/kit/typicalc/model/step/package-info.java
View File

@ -1,7 +1,7 @@
/**
* The step package models the inference steps that are executed while generating the prof tree.
* To represent the different kinds of typing rules that can be applied, InferenceStep has various subclasses.
* These subclasses can be produced by factories, appropriate to the desired context.
* The step package models the inference steps that are executed while generating the prof tree.
* To represent the different kinds of typing rules that can be applied, InferenceStep has various subclasses.
* These subclasses can be produced by factories, appropriate to the desired context.
*/
@NonNullFields
@NonNullApi

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

@ -19,7 +19,8 @@ public class AbsTerm extends LambdaTerm {
/**
* 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 var the variable bound by the abstraction
* @param body the lambda term of the abstraction
*/
public AbsTerm(VarTerm var, LambdaTerm body) {
@ -28,6 +29,8 @@ public class AbsTerm extends LambdaTerm {
}
/**
* Returns the variable of this abstraction
*
* @return the variable of this abstraction
*/
public VarTerm getVariable() {
@ -35,6 +38,8 @@ public class AbsTerm extends LambdaTerm {
}
/**
* Returns the function body of this abstraction
*
* @return the function body of this abstraction
*/
public LambdaTerm getInner() {

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

@ -15,7 +15,8 @@ public class AppTerm extends LambdaTerm {
/**
* Initializes a new application term with one lambda term for the function and one lambda term for the parameter.
* @param left the function
*
* @param left the function
* @param right the parameter
*/
public AppTerm(LambdaTerm left, LambdaTerm right) {
@ -24,6 +25,8 @@ public class AppTerm extends LambdaTerm {
}
/**
* Returns the function used in this application
*
* @return the function used in this application
*/
public LambdaTerm getFunction() {
@ -31,6 +34,8 @@ public class AppTerm extends LambdaTerm {
}
/**
* Returns the parameter used in this application
*
* @return the parameter used in this application
*/
public LambdaTerm getParameter() {

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

@ -12,6 +12,7 @@ public class BooleanTerm extends ConstTerm {
/**
* Initializes a new boolean lambda term with the given value.
*
* @param value true or false
*/
public BooleanTerm(boolean value) {
@ -20,6 +21,7 @@ public class BooleanTerm extends ConstTerm {
/**
* Returns the value of the boolean constant term.
*
* @return the value of the term
*/
public boolean getValue() {

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

@ -13,7 +13,10 @@ import java.util.Set;
* Abstract representation of a constant lambda term that has a predetermined type and a value of that type.
*/
public abstract class ConstTerm extends LambdaTerm {
/**
* Returns the named type of the constant
*
* @return the named type of the constant
*/
public abstract NamedType getType();

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

@ -12,6 +12,7 @@ public class IntegerTerm extends ConstTerm {
/**
* Initializes a new integer lambda term with the given value.
*
* @param value an integer
*/
public IntegerTerm(int value) {
@ -20,6 +21,7 @@ public class IntegerTerm extends ConstTerm {
/**
* Returns the value of the integer constant term.
*
* @return the value of the term
*/
public int getValue() {

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

@ -14,27 +14,32 @@ import java.util.Set;
*/
public abstract class LambdaTerm {
/**
* Returns whether the lambda term contains a let expression
*
* @return whether the lambda term contains a let expression
*/
public abstract boolean hasLet();
/**
* Returns a set of all free variables occurring in the lambda term.
*
* @return all free variables
*/
public abstract Set<VarTerm> getFreeVariables();
/**
* 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
* @param assumptions type assumptions
* @param type a type
* @return the result returned by the visitor
*/
public abstract InferenceStep accept(TermVisitorTree termVisitorTree,

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

@ -20,9 +20,10 @@ public class LetTerm extends LambdaTerm {
/**
* Initializes a new let term with its variable and two lambda terms.
* @param variable the variable of the let term
*
* @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
* @param body the lambda term the variable may be used in
*/
public LetTerm(VarTerm variable, LambdaTerm definition, LambdaTerm body) {
this.variable = variable;

9
src/main/java/edu/kit/typicalc/model/term/TermVisitor.java
View File

@ -1,38 +1,47 @@
package edu.kit.typicalc.model.term;
/**
* Represents the visitor in the visitor pattern.
*/
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 an integer constant.
*
* @param intTerm the integer constant
*/
void visit(IntegerTerm intTerm);
/**
* Visit a boolean constant.
*
* @param boolTerm the boolean constant
*/
void visit(BooleanTerm boolTerm);

53
src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java
View File

@ -6,18 +6,21 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
/**
* Represents the visitor in the visitor pattern.
*/
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 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
* 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);
@ -27,12 +30,12 @@ public interface TermVisitorTree {
* 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 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
* 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);
@ -42,12 +45,12 @@ public interface TermVisitorTree {
* 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 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
* 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);
@ -57,12 +60,12 @@ public interface TermVisitorTree {
* 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 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
* 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);
@ -72,12 +75,12 @@ public interface TermVisitorTree {
* 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 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
* 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);

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

@ -14,6 +14,7 @@ public class VarTerm extends LambdaTerm {
/**
* Initializes a new variable term with its name.
*
* @param name the name of the variable
*/
public VarTerm(String name) {
@ -22,6 +23,8 @@ public class VarTerm extends LambdaTerm {
}
/**
* Returns the name of this variable
*
* @return the name of this variable
*/
public String getName() {

4
src/main/java/edu/kit/typicalc/model/term/package-info.java
View File

@ -1,6 +1,6 @@
/**
* The term package models the different kinds of lambda terms:
* application, abstraction, variable constant and let-polymorphism.
* The term package models the different kinds of lambda terms:
* application, abstraction, variable constant and let-polymorphism.
*/
@NonNullFields
@NonNullApi

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

@ -14,10 +14,12 @@ public class FunctionType extends Type {
private final Type parameter;
private final Type output;
/**
* Initializes a new FunctionType with the given parameter and output types.
*
* @param parameter the type of this function’s parameter
* @param output the type of this function’s output
* @param output the type of this function’s output
*/
public FunctionType(Type parameter, Type output) {
this.parameter = parameter;
@ -26,6 +28,7 @@ public class FunctionType extends Type {
/**
* Checks whether some type occurs in the parameter or output of this function.
*
* @param x the type to look for
* @return whether the specified type occurs in this type
*/
@ -43,7 +46,8 @@ public class FunctionType extends Type {
/**
* Substitutes a type variable for a different type.
* @param a the type variable to replace
*
* @param a the type variable to replace
* @param b the type to insert
* @return a new FunctionType that is created by substituting a and b in the parameter
* and output type
@ -55,6 +59,7 @@ public class FunctionType extends Type {
/**
* Accepts a visitor.
*
* @param typeVisitor the visitor that wants to visit this
*/
@Override
@ -66,7 +71,8 @@ public class FunctionType extends Type {
* Computes the necessary constraints (and substitution) to unify this type with
* another. This method uses the constrainEqualToFunction method on the other
* type.
* @param type the other type
*
* @param type the other type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
@ -77,6 +83,7 @@ public class FunctionType extends Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
*
* @param type the function type
* @return unification steps necessary, or an error if that is impossible
*/
@ -88,6 +95,7 @@ public class FunctionType extends Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
*
* @param type the named type
* @return unification steps necessary, or an error if that is impossible
*/
@ -99,6 +107,7 @@ public class FunctionType extends Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
*
* @param type the type variable
* @return the unification steps necessary, or an error if that is impossible
*/
@ -109,6 +118,7 @@ public class FunctionType extends Type {
/**
* Getter for output
*
* @return output
*/
public Type getOutput() {
@ -117,6 +127,7 @@ public class FunctionType extends Type {
/**
* Getter for parameter
*
* @return parameter
*/
public Type getParameter() {

11
src/main/java/edu/kit/typicalc/model/type/NamedType.java
View File

@ -24,6 +24,7 @@ public class NamedType extends Type {
/**
* Initializes a new NamedType with the given name.
*
* @param name the name of this type
*/
public NamedType(String name) {
@ -32,6 +33,7 @@ public class NamedType extends Type {
/**
* Returns the name of the named type.
*
* @return the name of this type
*/
public String getName() {
@ -40,6 +42,7 @@ public class NamedType extends Type {
/**
* Checks whether some type occurs in this type.
*
* @param x the type to look for
* @return whether the specified type is equal to this type
*/
@ -54,6 +57,7 @@ public class NamedType extends Type {
/**
* Substitutes a type variable for a different type.
*
* @param a the type to replace
* @param b the type to insert
* @return itself, or b if a is equal to this object
@ -65,6 +69,7 @@ public class NamedType extends Type {
/**
* Accepts a visitor.
*
* @param typeVisitor the visitor that wants to visit this
*/
@Override
@ -76,7 +81,8 @@ public class NamedType extends Type {
* Computes the necessary constraints (and substitution) to unify this type with
* another. This method uses the constrainEqualToNamedType method on the other
* type.
* @param type the other type
*
* @param type the other type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
@ -87,6 +93,7 @@ public class NamedType extends Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
*
* @param type the function type
* @return unification steps necessary, or an error if that is impossible
*/
@ -98,6 +105,7 @@ public class NamedType extends Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
*
* @param type the named type
* @return unification steps necessary, or an error if that is impossible
*/
@ -109,6 +117,7 @@ public class NamedType extends Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
*
* @param type the type variable
* @return the unification steps necessary, or an error if that is impossible
*/

11
src/main/java/edu/kit/typicalc/model/type/Type.java
View File

@ -12,6 +12,7 @@ import java.util.Set;
public abstract class Type {
/**
* Checks whether some type occurs in this type.
*
* @param x the type to look for
* @return whether the specified type occurs in this type
*/
@ -19,12 +20,14 @@ public abstract class Type {
/**
* Returns a set of all free type variables occurring in the type.
*
* @return all free type variables
*/
public abstract Set<TypeVariable> getFreeTypeVariables();
/**
* Substitutes a type Variable for a different type.
*
* @param a the type to replace
* @param b the type to insert
* @return a Type that is created by replacing a with b
@ -33,6 +36,7 @@ public abstract class Type {
/**
* Applies the given substitution to the type.
*
* @param substitution the substitution to apply to the type
* @return the substituted type
*/
@ -42,6 +46,7 @@ public abstract class Type {
/**
* Accepts a visitor
*
* @param typeVisitor the visitor that wants to visit this
*/
public abstract void accept(TypeVisitor typeVisitor);
@ -49,7 +54,8 @@ public abstract class Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with
* another type.
* @param type the other type
*
* @param type the other type
* @return unification steps necessary, or an error if that is impossible
*/
public abstract Result<UnificationActions, UnificationError> constrainEqualTo(Type type);
@ -57,6 +63,7 @@ public abstract class Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
*
* @param type the function type
* @return unification steps necessary, or an error if that is impossible
*/
@ -65,6 +72,7 @@ public abstract class Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
*
* @param type the named type
* @return unification steps necessary, or an error if that is impossible
*/
@ -73,6 +81,7 @@ public abstract class Type {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
*
* @param type the type variable
* @return the unification steps necessary, or an error if that is impossible
*/

13
src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java
View File

@ -13,10 +13,12 @@ public class TypeAbstraction {
private final Type type;
private final SortedSet<TypeVariable> quantifiedVariables;
/**
* Initializes a new type abstraction with its type and the type variables bound by
* the for-all quantifier.
* @param type the type of the type abstraction
*
* @param type the type of the type abstraction
* @param quantifiedVariables the type variables bound by the for-all quantifier
*/
public TypeAbstraction(Type type, Set<TypeVariable> quantifiedVariables) {
@ -27,6 +29,7 @@ public class TypeAbstraction {
/**
* Initializes a new type abstraction with its type and no type variables bound by the
* for-all quantifier.
*
* @param type the type of the type abstraction
*/
public TypeAbstraction(Type type) {
@ -38,7 +41,7 @@ public class TypeAbstraction {
* Initializes a new type abstraction with its type and all type variables quantified
* that occur free in the given type, but not free in the given type assumptions
*
* @param type the type of the type abstraction
* @param type the type of the type abstraction
* @param typeAssumptions the type assumptions to consider when quantifying the type variables
*/
public TypeAbstraction(Type type, Map<VarTerm, TypeAbstraction> typeAssumptions) {
@ -52,7 +55,7 @@ public class TypeAbstraction {
* Instantiates the type abstraction with a new type and returns it. The new type
* contains new type variables generated by the given type variable factory.
*
* @param typeVarFactory the type variable factory used to generate the new type variables
* @param typeVarFactory the type variable factory used to generate the new type variables
* @return the new type resulting from the instantiation of the type abstraction
*/
public Type instantiate(TypeVariableFactory typeVarFactory) {
@ -66,6 +69,7 @@ public class TypeAbstraction {
/**
* Indicates whether any type variables are quantified in the type abstraction.
*
* @return true if one or more type variables are quantified, false otherwise
*/
public boolean hasQuantifiedVariables() {
@ -75,6 +79,7 @@ public class TypeAbstraction {
/**
* Returns a list of all type variables that are bound by an for-all quantifier in the
* type abstraction.
*
* @return a list of all quantified type variables
*/
public Set<TypeVariable> getQuantifiedVariables() {
@ -83,6 +88,7 @@ public class TypeAbstraction {
/**
* Returns a set of all free type variables occurring in the type abstraction.
*
* @return all free type variables
*/
public Set<TypeVariable> getFreeTypeVariables() {
@ -93,6 +99,7 @@ public class TypeAbstraction {
/**
* Getter for the inner type of the type abstraction
*
* @return the inner type of the type abstraction
*/
public Type getInnerType() {

15
src/main/java/edu/kit/typicalc/model/type/TypeVariable.java
View File

@ -16,7 +16,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
/**
* Initializes a new TypeVariable with the given index.
*
* @param kind the kind of type variable
* @param kind the kind of type variable
* @param index the index of this variable
*/
public TypeVariable(TypeVariableKind kind, int index) {
@ -26,6 +26,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
/**
* Returns the kind of the type variable.
*
* @return the variable's kind
*/
public TypeVariableKind getKind() {
@ -34,6 +35,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
/**
* Returns the index of the type variable as an integer
*
* @return the variable's index
*/
public int getIndex() {
@ -42,6 +44,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
/**
* Checks whether some type occurs in this type.
*
* @param x the type to look for
* @return whether the specified type is equal to this type
*/
@ -57,6 +60,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
/**
* Substitutes a type variable for a different type.
*
* @param a the type to replace
* @param b the type to insert
* @return itself, or b if a is equal to this object
@ -64,7 +68,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
@Override
public Type substitute(TypeVariable a, Type b) {
if (this.equals(a)) {
return b;
return b;
} else {
return this;
}
@ -72,6 +76,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
/**
* Accepts a visitor.
*
* @param typeVisitor the visitor that wants to visit this
*/
public void accept(TypeVisitor typeVisitor) {
@ -82,7 +87,8 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
* Computes the necessary constraints (and substitution) to unify this type with
* another. This method uses the constrainEqualToVariable method on the other
* type.
* @param type the other type
*
* @param type the other type
* @return unification steps necessary, or an error if that is impossible
*/
@Override
@ -93,6 +99,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
*
* @param type the function type
* @return unification steps necessary, or an error if that is impossible
*/
@ -104,6 +111,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
*
* @param type the named type
* @return unification steps necessary, or an error if that is impossible
*/
@ -115,6 +123,7 @@ public class TypeVariable extends Type implements Comparable<TypeVariable> {
/**
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
*
* @param type the type variable
* @return the unification steps necessary, or an error if that is impossible
*/

3
src/main/java/edu/kit/typicalc/model/type/TypeVisitor.java
View File

@ -6,18 +6,21 @@ package edu.kit.typicalc.model.type;
public interface TypeVisitor {
/**
* Visit a named type.
*
* @param named the type to be visited
*/
void visit(NamedType named);
/**
* Visit a type variable
*
* @param variable the variable to be visited
*/
void visit(TypeVariable variable);
/**
* Visit a function.
*
* @param function the function to be visited
*/
void visit(FunctionType function);

6
src/main/java/edu/kit/typicalc/model/type/UnificationActions.java
View File

@ -16,7 +16,8 @@ public class UnificationActions {
/**
* Initializes this object using the provided constraints and substitution.
* @param constraints added constraints, if any
*
* @param constraints added constraints, if any
* @param substitution necessary substitution, if any
*/
protected UnificationActions(Collection<Constraint> constraints, Optional<Substitution> substitution) {
@ -34,13 +35,16 @@ public class UnificationActions {
/**
* Getter for constraints
*
* @return the constraints stored in this object
*/
public Collection<Constraint> getConstraints() {
return constraints;
}
/**
* Getter for substitution
*
* @return the substitution stored in this object
*/
public Optional<Substitution> getSubstitution() {

3
src/main/java/edu/kit/typicalc/model/type/UnificationUtil.java
View File

@ -15,7 +15,8 @@ import java.util.Optional;
* @see Type
*/
final class UnificationUtil {
private UnificationUtil() { }
private UnificationUtil() {
}
static Result<UnificationActions, UnificationError> functionFunction(FunctionType a, FunctionType b) {
return new Result<>(new UnificationActions(List.of(

2
src/main/java/edu/kit/typicalc/model/type/package-info.java
View File

@ -1,5 +1,5 @@
/**
* The type package models all types that can be assigned to lambda terms.
* The type package models all types that can be assigned to lambda terms.
*/
@NonNullApi
@NonNullFields

4
src/main/java/edu/kit/typicalc/presenter/Presenter.java
View File

@ -1,6 +1,7 @@
package edu.kit.typicalc.presenter;
import java.util.Map;
import edu.kit.typicalc.model.Model;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.parser.ParseError;
@ -18,8 +19,9 @@ public class Presenter implements MainViewListener {
/**
* Initializes a new presenter object with the provided model and view.
*
* @param model the implementation of the Model
* @param view the implementation of the MainView
* @param view the implementation of the MainView
*/
public Presenter(Model model, MainView view) {
this.model = model;

1
src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java
View File

@ -4,6 +4,7 @@ import java.util.List;
import java.util.Locale;
import java.util.MissingResourceException;
import java.util.ResourceBundle;
import org.springframework.stereotype.Component;
import com.vaadin.flow.i18n.I18NProvider;

2
src/main/java/edu/kit/typicalc/view/content/ControlPanel.java
View File

@ -22,7 +22,7 @@ public class ControlPanel extends HorizontalLayout {
/**
* Sets up buttons with click-listeners that call the corresponding method in the view.
*
* @param view the view that reacts to the button clicks
* @param view the view that reacts to the button clicks
* @param focusArea the component key shortcuts should work in
*/
public ControlPanel(ControlPanelView view, Component focusArea) {

8
src/main/java/edu/kit/typicalc/view/content/ControlPanelView.java
View File

@ -1,10 +1,16 @@
package edu.kit.typicalc.view.content;
/**
* Provides an interface for the ControlPanel to interact with its views. If a view doesn't
* support a certain operation(s), it may provide a dummy implementation and/or disable
* the corresponding button(s).
*/
public interface ControlPanelView {
/**
* Provides user with a way to share contents shown in the view (the URL and LaTeX code).
*/
default void shareButton() { }
default void shareButton() {
}
/**
* Go to the first step.

10
src/main/java/edu/kit/typicalc/view/content/infocontent/ImageSlide.java
View File

@ -17,16 +17,16 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
public class ImageSlide extends Slide implements LocaleChangeObserver {
private static final long serialVersionUID = 232255503611054445L;
private static final String SLIDE_LAYOUT_ID = "slideLayout";
private static final String EXPLANATION_ID = "explanation";
private final Span explanation;
private final String explanationKey;
/**
* Create a new ImageSlide with the path of the image and a key for the text.
*
*
* @param imgPath the path of the image
* @param textKey key for the text
*/
@ -40,7 +40,7 @@ public class ImageSlide extends Slide implements LocaleChangeObserver {
slideLayout.setId(SLIDE_LAYOUT_ID);
add(slideLayout);
}
@Override
public void localeChange(LocaleChangeEvent event) {
explanation.setText(getTranslation(explanationKey));

24
src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java
View File

@ -29,7 +29,7 @@ import edu.kit.typicalc.view.main.MainViewImpl;
public class StartPageView extends VerticalLayout implements ControlPanelView, LocaleChangeObserver {
private static final long serialVersionUID = 2502750919087936406L;
private static final String HEADING_ID = "startPage-Heading";
private static final String H_LINE_ID = "horizontalLine";
private static final String INTRODUCTION_ID = "introduction";
@ -40,14 +40,14 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
private static final String SLIDE_SHOW_ID = "slideShow";
private static final String DOT = ".";
private final ControlPanel controlPanel;
private final Span introduction;
private final Carousel slideShow;
private final ProgressBar slideProgress;
private final Text linkText;
private final Anchor link;
/**
* Fills the view with content.
*/
@ -55,10 +55,10 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
controlPanel = new ControlPanel(this, this);
controlPanel.setId(CONTROL_PANEL_ID);
controlPanel.setEnabledShareButton(false);
slideShow = createSzenarioCarousel();
slideShow.setId(SLIDE_SHOW_ID);
H1 heading = new H1(getTranslation("root.typicalc"));
heading.setId(HEADING_ID);
Hr line1 = new Hr();
@ -67,16 +67,16 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
line2.setId(H_LINE_ID);
introduction = new Span(getTranslation("root.slideExp"));
introduction.setId(INTRODUCTION_ID);
linkText = new Text(getTranslation("root.linkText"));
link = new Anchor(getTranslation("root.link"), getTranslation("root.here"));
link.setTarget("_blank"); // opens new tab
Span linkContainer = new Span(linkText, link, new Text(DOT));
linkContainer.setId(LINK_CONTAINER_ID);
slideProgress = new ProgressBar(slideShow.getStartPosition(), slideShow.getSlides().length - 1);
slideProgress.setId(SLIDE_PROGRESS_ID);
add(heading, line1, introduction, linkContainer, slideProgress, slideShow, line2, controlPanel);
setId(START_PAGE_ID);
}
@ -90,11 +90,11 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
Slide slide6 = new ImageSlide(getTranslation("root.image6"), "root.text6");
Slide slide7 = new ImageSlide(getTranslation("root.image7"), "root.text7");
Slide slide8 = new ImageSlide(getTranslation("root.image8"), "root.text8");
return new Carousel(slide1, slide2, slide3, slide4, slide5, slide6, slide7, slide8).withoutNavigation()
.withoutSwipe();
}
@Override
public void firstStepButton() {
slideShow.movePos(0);
@ -116,10 +116,10 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
@Override
public void previousStepButton() {
slideShow.movePrev();
slideProgress.setValue((slideProgress.getValue() - 1 + slideShow.getSlides().length)
slideProgress.setValue((slideProgress.getValue() - 1 + slideShow.getSlides().length)
% slideShow.getSlides().length);
}
@Override
public void localeChange(LocaleChangeEvent event) {
introduction.setText(getTranslation("root.slideExp"));

1
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/MathjaxUnification.java
View File

@ -26,6 +26,7 @@ public class MathjaxUnification extends LitTemplate implements MathjaxAdapter {
/**
* Creates a new HTML element that renders the constraints and unification and
* calculates the steps.
*
* @param latex the LaTeX-String[] to render with MathJax
*/
public MathjaxUnification(String[] latex) {

7
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/ShareDialog.java
View File

@ -24,10 +24,11 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
/**
* Sets up three GUI elements, one for each parameter. The content of each element is equal
* to the String that is passed as corresponding parameter.
* @param url a permalink to share with other users
*
* @param url a permalink to share with other users
* @param latexPackages the needed LaTeX-packages to use the displayed mathematics
* in other LaTeX documents. Should be in the form „\\usepackage<package>“
* @param latexCode LaTeX code for users to copy into their own LaTeX document(s)
* in other LaTeX documents. Should be in the form „\\usepackage&ltpackage&gt“
* @param latexCode LaTeX code for users to copy into their own LaTeX document(s)
*/
public ShareDialog(String url, String latexPackages, String latexCode) {
VerticalLayout layout = new VerticalLayout();

15
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/TypeInferenceView.java
View File

@ -15,6 +15,13 @@ import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCrea
import java.util.List;
import java.util.Locale;
/**
* The main user interface. It provides a way to show the proof tree, the constrains, the
* unification, the most general unifier and the final type of the lambda term to the user.
* Also provides a way for the user to interact with it, e.g. looking at everything step-by-step.
* In order to do this, this class uses {@link LatexCreator} tp create LaTeX-code from the
* {@link TypeInfererInterface} and MathJax to render the LaTeX to the user.
*/
@CssImport("./styles/view/type-inference.css")
public class TypeInferenceView extends VerticalLayout
implements ControlPanelView, ComponentEventListener<AttachEvent> {
@ -36,6 +43,12 @@ public class TypeInferenceView extends VerticalLayout
private final transient LatexCreator lc;
private final Div content;
/**
* Initializes the component. When initialization is complete, the first step of the type
* inference algorithm is shown to the user.
*
* @param typeInferer used to create LaTeX code from
*/
public TypeInferenceView(TypeInfererInterface typeInferer) {
setId(ID);
addAttachListener(this);
@ -64,7 +77,7 @@ public class TypeInferenceView extends VerticalLayout
@Override
public void shareButton() {
UI.getCurrent().getPage().executeJs("return decodeURI(window.location.href)").then(url ->
new ShareDialog(url.asString(), lc.getLatexPackages(), lc.getTree()).open()
new ShareDialog(url.asString(), lc.getLatexPackages(), lc.getTree()).open()
);
}

7
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/AssumptionGeneratorUtil.java
View File

@ -8,8 +8,13 @@ import java.util.Map;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.*;
import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants.DOT_SIGN;
/**
* Util class for {@link LatexCreator} and {@link LatexCreatorConstraints} to generate LaTeX code from
* a Map representing type assumptions.
*/
public final class AssumptionGeneratorUtil {
private AssumptionGeneratorUtil() { }
private AssumptionGeneratorUtil() {
}
protected static String typeAssumptionsToLatex(Map<VarTerm, TypeAbstraction> typeAssumptions) {
if (typeAssumptions.isEmpty()) {

8
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/ConstraintSetIndexFactory.java
View File

@ -29,10 +29,10 @@ public class ConstraintSetIndexFactory {
protected String nextConstraintSetIndex() {
String index = nextConstraintSetIndex == FIRST_CONSTRAINT_SET_INDEX
? ""
: nextConstraintSetIndex == FIRST_CONSTRAINT_SET_INDEX + 1
? "" + UNDERSCORE + CURLY_LEFT + LET + CURLY_RIGHT
: "" + UNDERSCORE + CURLY_LEFT + LET + UNDERSCORE
+ CURLY_LEFT + nextConstraintSetIndex + CURLY_RIGHT + CURLY_RIGHT;
: nextConstraintSetIndex == FIRST_CONSTRAINT_SET_INDEX + 1
? "" + UNDERSCORE + CURLY_LEFT + LET + CURLY_RIGHT
: "" + UNDERSCORE + CURLY_LEFT + LET + UNDERSCORE
+ CURLY_LEFT + nextConstraintSetIndex + CURLY_RIGHT + CURLY_RIGHT;
nextConstraintSetIndex++;
return index;

10
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreator.java
View File

@ -28,7 +28,7 @@ public class LatexCreator implements StepVisitor {
/**
* Generate the pieces of LaTeX-code from the type inferer.
*
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
* @param typeInferer theTypeInfererInterface to create the LaTeX-code from
* @param translationProvider translation text provider for {@link UnificationError}
*/
public LatexCreator(TypeInfererInterface typeInferer, Function<UnificationError, String> translationProvider) {
@ -38,8 +38,8 @@ public class LatexCreator implements StepVisitor {
/**
* Generate the pieces of LaTeX-code from the type inferer.
*
* @param typeInferer theTypeInfererInterface to create the LaTeX code from
* @param stepLabels turns step labels on or off
* @param typeInferer theTypeInfererInterface to create the LaTeX code from
* @param stepLabels turns step labels on or off
* @param translationProvider translation text provider for {@link UnificationError}
*/
public LatexCreator(TypeInfererInterface typeInferer, boolean stepLabels,
@ -51,7 +51,7 @@ public class LatexCreator implements StepVisitor {
}
/**
* Returns the proof tree
* Returns the proof tree.
*
* @return the LaTeX-code for the proof tree
*/
@ -60,7 +60,7 @@ public class LatexCreator implements StepVisitor {
}
/**
* Returns the LaTeX-code for constraints, unification, MGU and final type
* Returns the LaTeX-code for constraints, unification, MGU and final type.
*
* @return the LaTeX-code for constraints and unification
*/

14
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstraints.java
View File

@ -40,7 +40,7 @@ public class LatexCreatorConstraints implements StepVisitor {
* Initializes the LatexCreatorConstraints with the right values calculates the strings
* that will be returned in getEverything().
*
* @param typeInferer the source for the generation of the LaTeX code
* @param typeInferer the source for the generation of the LaTeX code
* @param translationProvider translation text provider for {@link UnificationError}
*/
protected LatexCreatorConstraints(TypeInfererInterface typeInferer,
@ -51,12 +51,12 @@ public class LatexCreatorConstraints implements StepVisitor {
}
private LatexCreatorConstraints(TypeInfererInterface typeInferer,
ConstraintSetIndexFactory constraintSetIndexFactory,
TreeNumberGenerator numberGenerator,
String prefix,
Optional<VarTerm> letVariable,
Optional<Map<VarTerm, TypeAbstraction>> newTypeAssumption,
Function<UnificationError, String> translationProvider) {
ConstraintSetIndexFactory constraintSetIndexFactory,
TreeNumberGenerator numberGenerator,
String prefix,
Optional<VarTerm> letVariable,
Optional<Map<VarTerm, TypeAbstraction>> newTypeAssumption,
Function<UnificationError, String> translationProvider) {
this.prefix = prefix;
this.letVariable = letVariable;
this.newTypeAssumption = newTypeAssumption;

10
src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorTerm.java
View File

@ -13,6 +13,7 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La
public class LatexCreatorTerm implements TermVisitor {
private final StringBuilder latex = new StringBuilder();
private enum ParenthesesNeeded {
NEVER,
SOMETIMES,
@ -31,16 +32,11 @@ public class LatexCreatorTerm implements TermVisitor {
}
/**
* Returns the generated LaTeX code
*
* @return the generated LaTeX code
*/
public String getLatex() {
// long count = latex.chars().filter(ch -> ch == PAREN_LEFT).count();
// if (latex.indexOf(String.valueOf(PAREN_LEFT)) == 0
// && latex.indexOf(String.valueOf(PAREN_RIGHT)) == latex.length() - 1
// && count == 1) {
// latex.deleteCharAt(latex.length() - 1);
// latex.deleteCharAt(0);
// }
return latex.toString();
}

6
src/main/java/edu/kit/typicalc/view/main/ErrorNotification.java
View File

@ -41,21 +41,21 @@ public class ErrorNotification extends Notification {
setPosition(Position.MIDDLE);
setId(NOTIFICATION_ID);
}
private Details buildErrorMessage(ParseError error) {
VerticalLayout additionalInformation = new VerticalLayout();
additionalInformation.setId(ADDITIONAL_INFO_ID);
Paragraph summary = new Paragraph(getTranslation("root." + error.toString()));
summary.setId(ERROR_SUMMARY_ID);
Details errorMessage = new Details(summary, additionalInformation);
if (error == ParseError.TOO_FEW_TOKENS) {
additionalInformation.add(new Span(getTranslation("root.tooFewTokensHelp")));
} else {
additionalInformation.add(new Span(getTranslation("root.wrongCharacter") + error.getCause().getText()));
additionalInformation.add(new Span(getTranslation("root.position") + error.getCause().getPos()));
}
return errorMessage;
}
}

5
src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
View File

@ -12,7 +12,6 @@ import java.util.function.Consumer;
/**
* Contains all predefined examples as buttons.
* Clicking on a button inserts the example string into the input field.
*
*/
public class ExampleDialog extends Dialog implements LocaleChangeObserver {
@ -35,8 +34,8 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
for (String term : examples) {
Button button = new Button(term);
button.addClickListener(click -> {
callback.accept(term);
this.close();
callback.accept(term);
this.close();
});
button.setId(term); // needed for integration test
layout.add(button);

6
src/main/java/edu/kit/typicalc/view/main/HelpContentField.java
View File

@ -23,7 +23,7 @@ public class HelpContentField extends AccordionPanel implements LocaleChangeObse
/**
* Create a HelpContentField with keys for the strings of the summary and the content of this AccordionPanel.
*
*
* @param summaryKey the key for the string of the summary
* @param contentKey the key for the string of the content
*/
@ -39,9 +39,9 @@ public class HelpContentField extends AccordionPanel implements LocaleChangeObse
/**
* Create a HelpContentField with a button and keys for the string of the summary and the content of this
* AccordionPanel.
*
*
* @param summaryKey the key for the string of the summary
* @param button the button
* @param button the button
* @param contentKey the key for the string of the content
*/
protected HelpContentField(String summaryKey, Button button, String contentKey) {

2
src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java
View File

@ -39,7 +39,7 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb
* Initializes an InferenceRuleField with a key to get the name of the inference rule and the LaTeX-code
* for its visual representation.
*
* @param latex the LaTeX-code
* @param latex the LaTeX-code
* @param nameKey the key to get the name of the inference rule
*/
protected InferenceRuleField(String latex, String nameKey) {

18
src/main/java/edu/kit/typicalc/view/main/InputBar.java
View File

@ -58,19 +58,19 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
inputField.setId(INPUT_FIELD_ID);
inputField.setClearButtonVisible(true);
inputField.setMaxLength(MAX_INPUT_LENGTH);
// attach a listener that replaces \ with λ
// JavaScript is used because Vaadin does not have APIs for selectionStart/selectionEnd
UI.getCurrent().getPage().executeJs(
"document.getElementById('" + INPUT_FIELD_ID + "').addEventListener('keyup', e => {"
+ "var area = e.target.shadowRoot.querySelector('input');"
+ "if (area.value.indexOf('\\\\') >= 0) {"
+ " var start = area.selectionStart;"
+ " var end = area.selectionEnd;"
+ " area.value = area.value.replace('\\\\', 'λ');"
+ " area.selectionStart = start;"
+ " area.selectionEnd = end;"
+ "}});");
+ "var area = e.target.shadowRoot.querySelector('input');"
+ "if (area.value.indexOf('\\\\') >= 0) {"
+ " var start = area.selectionStart;"
+ " var end = area.selectionEnd;"
+ " area.value = area.value.replace('\\\\', 'λ');"
+ " area.selectionStart = start;"
+ " area.selectionEnd = end;"
+ "}});");
Button lambdaButton = new Button(getTranslation("root.lambda"));
lambdaButton.setId(LAMBDA_BUTTON_ID);
UI.getCurrent().getPage().executeJs("window.lambdaButtonListener($0, $1);", LAMBDA_BUTTON_ID, INPUT_FIELD_ID);

19
src/main/java/edu/kit/typicalc/view/main/MainView.java
View File

@ -1,9 +1,10 @@
package edu.kit.typicalc.view.main;
import java.util.Map;
import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.parser.ParseError;
import java.util.Map;
/**
* Provides an interface for the presenter to interact with the view. The interaction consists of
* either passing a TypeInfererInterface or a ParseError to the view.
@ -13,27 +14,27 @@ public interface MainView {
/**
* Starts the creation of the visual representation of the provided typeInferer.
* After the process is finished, the first step of the type inference tree is displayed.
*
*
* @param typeInferer the result of the computation of the type inference algorithm
*/
void setTypeInferenceView(TypeInfererInterface typeInferer);
/**
* Displays the provided error indicating syntactically invalid input.
*
*
* @param error the error which is displayed to indicate invalid input
*/
void displayError(ParseError error);
/**
* Provides an interface for the view to interact with the model.
* Provides an interface for the view to interact with the model.
*/
interface MainViewListener {
/**
* Provides the user input to the model and provide the result to the main view.
*
* @param lambdaTerm the lambda term to type-infer
*
* @param lambdaTerm the lambda term to type-infer
* @param typeAssumptions type assumptions to use during the calculation
*/
void typeInferLambdaString(String lambdaTerm, Map<String, String> typeAssumptions);

1
src/main/java/edu/kit/typicalc/view/main/MathjaxDisplay.java
View File

@ -18,6 +18,7 @@ public class MathjaxDisplay extends LitTemplate implements MathjaxAdapter {
@Id("tc-content")
private Div content;
/**
* Creates a new HTML element that renders the LaTeX code.
*

4
src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java
View File

@ -36,8 +36,8 @@ public class TypeAssumptionField extends HorizontalLayout implements LocaleChang
* type assumption from the {@link TypeAssumptionsArea}.
*
* @param deleteSelf deletes this object from the TypeAssumptionsArea
* @param variable variable of the type assumption
* @param type type of the type assumption
* @param variable variable of the type assumption
* @param type type of the type assumption
*/
protected TypeAssumptionField(Consumer<TypeAssumptionField> deleteSelf, String variable, String type) {
this(deleteSelf);

4
src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java
View File

@ -69,7 +69,7 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver
assumptionContainer = new VerticalLayout();
assumptionContainer.setId(ASS_CONTAINER_ID);
initializeWithAssumptions(types);
layout.add(heading, buttons, assumptionContainer);
add(layout);
@ -82,7 +82,7 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver
protected TypeAssumptionsArea() {
this(new HashMap<>());
}
private void initializeWithAssumptions(Map<String, String> types) {
for (Map.Entry<String, String> param : types.entrySet()) {
TypeAssumptionField assumption = new TypeAssumptionField(value -> {

6
src/main/java/edu/kit/typicalc/view/main/UpperBar.java
View File

@ -40,8 +40,8 @@ public class UpperBar extends HorizontalLayout {
/**
* Initializes a new UpperBar with the provided mainViewListener.
*
* @param presenter the listener used to communicate with the model
* @param setContent function to set the content of the application
* @param presenter the listener used to communicate with the model
* @param setContent function to set the content of the application
* @param setTermInURL function to set the term into the URL
*/
protected UpperBar(MainViewListener presenter, Consumer<Component> setContent,
@ -79,7 +79,7 @@ public class UpperBar extends HorizontalLayout {
* Calls the inferTerm method in {@link InputBar} with the provided
* string as the argument.
*
* @param term the provided string
* @param term the provided string
* @param typeAssumptions type assumptions to use
*/
protected void inferTerm(String term, Map<String, String> typeAssumptions) {

2
src/main/java/edu/kit/typicalc/view/main/package-info.java
View File

@ -1,4 +1,4 @@
/**
/**
* This package contains classes for building the constantly displayed parts of the UI. This includes classes
* which provide methods to pass the user input to the {@link edu.kit.typicalc.presenter.Presenter}.
*/

4
src/test/java/edu/kit/typicalc/model/ModelImplTest.java
View File

@ -58,9 +58,9 @@ class ModelImplTest {
new Conclusion(Map.of(
x, new TypeAbstraction(NamedType.INT),
y, new TypeAbstraction(a2)),
x, a3),
x, a3),
new Constraint(a3, NamedType.INT)
),
),
new Conclusion(Map.of(x, new TypeAbstraction(NamedType.INT)), term, a1),
new Constraint(a1, new FunctionType(a2, a3))
), typeInference.getFirstInferenceStep()

1
src/test/java/edu/kit/typicalc/model/step/AbsStepWithLetTest.java
View File

@ -35,6 +35,7 @@ class AbsStepWithLetTest {
constraint = new Constraint(type1, type2);
premise = new ConstStepDefault(conclusion, constraint);
}
@Test
void equalsTest() {
AbsStepWithLet step1 = new AbsStepWithLet(premise, conclusion, constraint);

3
src/test/java/edu/kit/typicalc/model/step/AppStepDefaultTest.java
View File

@ -22,6 +22,7 @@ class AppStepDefaultTest {
static Constraint constraint = null;
static NamedType namedType = null;
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
@ -37,6 +38,7 @@ class AppStepDefaultTest {
premise1 = new ConstStepDefault(conclusion, constraint);
premise2 = new ConstStepDefault(conclusion, constraint);
}
@Test
void equalsTest() {
AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint);
@ -54,6 +56,7 @@ class AppStepDefaultTest {
assertNotEquals(step1, step5);
}
@Test
void hashCodeTest() {
AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint);

3
src/test/java/edu/kit/typicalc/model/step/ConstStepDefaultTest.java
View File

@ -20,6 +20,7 @@ class ConstStepDefaultTest {
static Constraint constraint = null;
static NamedType namedType = null;
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
@ -33,6 +34,7 @@ class ConstStepDefaultTest {
NamedType type2 = new NamedType("b");
constraint = new Constraint(type1, type2);
}
@Test
void equalsTest() {
ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint);
@ -45,6 +47,7 @@ class ConstStepDefaultTest {
assertNotEquals(step1, step3);
}
@Test
void hashCodeTest() {
ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint);

3
src/test/java/edu/kit/typicalc/model/step/VarStepDefaultTest.java
View File

@ -21,6 +21,7 @@ class VarStepDefaultTest {
static Constraint constraint = null;
static NamedType namedType = null;
static TypeAbstraction typeAbstraction = null;
@BeforeAll
static void setUp() {
Map<VarTerm, TypeAbstraction> map = new LinkedHashMap<>();
@ -34,6 +35,7 @@ class VarStepDefaultTest {
NamedType type2 = new NamedType("b");
constraint = new Constraint(type1, type2);
}
@Test
void equalsTest() {
VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint);
@ -51,6 +53,7 @@ class VarStepDefaultTest {
assertNotEquals(step1, step5);
}
@Test
void hashCodeTest() {
VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint);

31
src/test/java/edu/kit/typicalc/view/ScreenshotIT.java
View File

@ -1,18 +1,16 @@
package edu.kit.typicalc.view;
import static org.junit.Assert.assertTrue;
import static org.junit.jupiter.api.Assertions.assertEquals;
import com.vaadin.testbench.Parameters;
import com.vaadin.testbench.commands.TestBenchCommandExecutor;
import edu.kit.typicalc.view.pageobjects.InputBarElement;
import org.junit.Test;
import org.openqa.selenium.HasCapabilities;
import java.io.File;
import java.io.IOException;
import org.junit.Test;
import org.openqa.selenium.HasCapabilities;
import com.vaadin.testbench.Parameters;
import com.vaadin.testbench.commands.TestBenchCommandExecutor;
import edu.kit.typicalc.view.pageobjects.InputBarElement;
import static org.junit.Assert.assertTrue;
import static org.junit.jupiter.api.Assertions.assertEquals;
/**
* This example contains usage examples of screenshot comparison feature.
@ -21,7 +19,7 @@ import edu.kit.typicalc.view.pageobjects.InputBarElement;
public class ScreenshotIT extends AbstractIT {
private static final String IDENTITY_TERM = "λx.x";
/**
* We'll want to perform some additional setup functions, so we override the
* setUp() method.
@ -56,25 +54,25 @@ public class ScreenshotIT extends AbstractIT {
+ " for error images",
testBench().compareScreen("initialView"));
}
@Test
public void basicExecution() throws Exception {
//TODO take screenshot and add to proper folder
InputBarElement inputBar = $(InputBarElement.class).first();
inputBar.setCurrentValue(IDENTITY_TERM);
assertEquals(IDENTITY_TERM, inputBar.getCurrentValue());
inputBar.typeInfer();
TestBenchCommandExecutor executer = getCommandExecutor();
executer.waitForVaadin();
assertTrue("Screenshot comparison for 'identityView' failed, see "
+ Parameters.getScreenshotErrorDirectory()
+ " for error images",
testBench().compareScreen("identityView"));
}
/**
* Generates a reference screenshot if no reference exists.
* <p>
@ -82,8 +80,7 @@ public class ScreenshotIT extends AbstractIT {
* perform this task manually after verifying that the screenshots look
* correct.
*
* @param referenceId
* the id of the reference image
* @param referenceId the id of the reference image
* @throws IOException
*/
private void generateReferenceIfNotFound(String referenceId)

6
src/test/java/edu/kit/typicalc/view/pageobjects/InputBarElement.java
View File

@ -17,7 +17,7 @@ public class InputBarElement extends HorizontalLayoutElement {
public void typeInfer() {
$(ButtonElement.class).id("inferButton").click();
}
/**
* Set the current value of the inputField.
*
@ -26,7 +26,7 @@ public class InputBarElement extends HorizontalLayoutElement {
public void setCurrentValue(String value) {
$(TextFieldElement.class).id("inputField").setValue(value);
}
/**
* Get the current value of the inputField.
*
@ -35,7 +35,7 @@ public class InputBarElement extends HorizontalLayoutElement {
public String getCurrentValue() {
return $(TextFieldElement.class).id("inputField").getValue();
}
/**
* Open the example dialog.
*/