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

various small changes

Browse Source
This commit is contained in:
Robin 2021-10-12 03:57:46 +02:00
parent 376933a4f5
commit b80e170006
3 changed files with 31 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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/Tree.java
View File

@ -100,7 +100,7 @@ public class Tree implements TermVisitorTree {
}
/**
* Indicates whether the tree contains a sub-inference of a let step that failed
* Indicates whether the tree contains a sub-inference of a let step that failed.
*
* @return true, if the tree contains a failed sub-inference, false otherwise
*/
@ -165,7 +165,7 @@ public class Tree implements TermVisitorTree {
Type premiseType = typeVarFactory.nextTypeVariable();
Constraint newConstraint = new Constraint(conclusionType, premiseType);
newConstraint.setStepIndex(stepNr); // TODO: also set on other let constraints?
newConstraint.setStepIndex(stepNr);
InferenceStep premise;
if (typeInfererLet.getType().isPresent()) {

40
src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
View File

@ -52,6 +52,11 @@ public class TypeAssumptionParser {
}
}
/**
* Starts the process of parsing the given type assumptions.
* @param assumptions type assumptions as a string
* @return if successful, a map of the type assumptions, otherwise an error
*/
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parse(String assumptions) {
lexer = new LambdaLexer(
cleanAssumptionText(assumptions), ParseError.ErrorSource.TYPE_ASSUMPTION_ERROR);
@ -59,10 +64,10 @@ public class TypeAssumptionParser {
}
/**
* parses Type Environment
* Parses a TypeEnvironment.
* @return if successful, a map of the type assumptions, otherwise an error
*/
public Result<Map<VarTerm, TypeAbstraction>, ParseError> parseTE() {
private Result<Map<VarTerm, TypeAbstraction>, ParseError> parseTE() {
HashMap<VarTerm, TypeAbstraction> map = new HashMap<>();
while (true) {
Result<Token, ParseError> nextLexerToken = lexer.nextToken();
@ -93,10 +98,11 @@ public class TypeAssumptionParser {
}
/**
* Parses single Type Assumption
* @return if successful, a type assumption, otherwise an error
* Parses a TypeAbstraction.
* @return if successful, a map entry consisting of a VarTerm and its corresponding TypeAbstraction,
* otherwise an error
*/
public Result<MapEntry<VarTerm, TypeAbstraction>, ParseError> parseTA() {
private Result<MapEntry<VarTerm, TypeAbstraction>, ParseError> parseTA() {
VarTerm term;
if (currentToken.getType() == Token.TokenType.VARIABLE) {
term = new VarTerm(currentToken.getText());
@ -125,10 +131,10 @@ public class TypeAssumptionParser {
/**
* Parses a Type
* @return if successful a type abstraction, otherwise an error.
* Parses a Type.
* @return if successful a TypeAbstraction, otherwise an error
*/
public Result<TypeAbstraction, ParseError> parseType() {
private Result<TypeAbstraction, ParseError> parseType() {
Result<Token, ParseError> nextLexerToken = lexer.nextToken();
if (nextLexerToken.isError()) {
return nextLexerToken.castError();
@ -206,10 +212,10 @@ public class TypeAssumptionParser {
}
/**
* parses a single Type
* @return if successful a type, otherwise an error
* Parses a SingleType.
* @return if successful a Type, otherwise an error
*/
public Result<Type, ParseError> parseSingleType() {
private Result<Type, ParseError> parseSingleType() {
Result<Type, ParseError> result = parseSimpleType();
if (result.isError()) {
@ -236,10 +242,10 @@ public class TypeAssumptionParser {
}
/**
* parses a simple type
* @return if successful a type, otherwise an error
* Parses a SimpleType.
* @return if successful a Type, otherwise an error
*/
public Result<Type, ParseError> parseSimpleType() {
private Result<Type, ParseError> parseSimpleType() {
if (currentToken.getType() == Token.TokenType.VARIABLE) {
Type type = parseLiteral(currentToken.getText());
return new Result<>(type);
@ -268,10 +274,10 @@ public class TypeAssumptionParser {
}
/**
* parses the rest of a single type
* @return if successful a type or an empty optional, otherwise an error
* Parses a Rest.
* @return if successful a Type or an empty Optional, otherwise an error
*/
public Result<Optional<Type>, ParseError> parseRest() {
private Result<Optional<Type>, ParseError> parseRest() {
switch (currentToken.getType()) {
case ARROW:
Result<Token, ParseError> nextLexerToken = lexer.nextToken();