From c14d8efd509f834b80573bc0339bb990698b265c Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 5 Mar 2024 22:01:10 +0100 Subject: feat(language): type inference * Customizable operator overloads. * Customizable aggregation operators. * Simplify ProblemQualifiedNameProvider. --- .../java/tools/refinery/language/Problem.xtext | 56 +- .../refinery/language/ProblemRuntimeModule.java | 9 +- .../expressions/AbstractTermInterpreter.java | 131 +++++ .../expressions/BuiltinTermInterpreter.java | 54 ++ .../expressions/CompositeTermInterpreter.java | 99 ++++ .../language/expressions/TermInterpreter.java | 29 ++ .../ProblemDelegateQualifiedNameProvider.java | 44 -- .../naming/ProblemQualifiedNameProvider.java | 56 +- .../ProblemResourceDescriptionStrategy.java | 20 +- .../scoping/ProblemLocalScopeProvider.java | 7 +- .../language/scoping/ProblemScopeProvider.java | 5 - .../language/scoping/imports/ImportAdapter.java | 71 ++- .../scoping/imports/ImportAdapterProvider.java | 68 +++ .../language/scoping/imports/ImportCollector.java | 5 +- .../language/typesystem/AggregatorName.java | 19 + .../refinery/language/typesystem/DataExprType.java | 19 + .../refinery/language/typesystem/ExprType.java | 16 + .../refinery/language/typesystem/FixedType.java | 18 + .../refinery/language/typesystem/InvalidType.java | 16 + .../refinery/language/typesystem/LiteralType.java | 16 + .../refinery/language/typesystem/MutableType.java | 32 ++ .../refinery/language/typesystem/NodeType.java | 16 + .../language/typesystem/ProblemTypeAnalyzer.java | 32 ++ .../refinery/language/typesystem/Signature.java | 11 + .../language/typesystem/SignatureProvider.java | 107 ++++ .../refinery/language/typesystem/TypedModule.java | 568 +++++++++++++++++++++ .../refinery/language/utils/BuiltinSymbols.java | 57 ++- .../refinery/language/utils/ProblemDesugarer.java | 98 ---- .../tools/refinery/language/utils/ProblemUtil.java | 15 +- .../language/validation/ProblemValidator.java | 96 ++-- 30 files changed, 1508 insertions(+), 282 deletions(-) create mode 100644 subprojects/language/src/main/java/tools/refinery/language/expressions/AbstractTermInterpreter.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/expressions/BuiltinTermInterpreter.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/expressions/CompositeTermInterpreter.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/expressions/TermInterpreter.java delete mode 100644 subprojects/language/src/main/java/tools/refinery/language/naming/ProblemDelegateQualifiedNameProvider.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapterProvider.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/AggregatorName.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/DataExprType.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/InvalidType.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/LiteralType.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/MutableType.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/NodeType.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/ProblemTypeAnalyzer.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/Signature.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java delete mode 100644 subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java (limited to 'subprojects/language/src/main/java') diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext index 43351d3e..08f7a585 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext @@ -17,7 +17,8 @@ enum ModuleKind: Statement: ImportStatement | Assertion | ClassDeclaration | EnumDeclaration | - DatatypeDeclaration | PredicateDefinition | /* FunctionDefinition | RuleDefinition | */ + DatatypeDeclaration | AggregatorDeclaration | PredicateDefinition | + /* FunctionDefinition | RuleDefinition | */ ScopeDeclaration | NodeDeclaration; ImportStatement: @@ -40,6 +41,9 @@ EnumLiteral returns Node: DatatypeDeclaration: "extern" "datatype" name=Identifier "."; +AggregatorDeclaration: + "extern" "aggregator" name=Identifier "."; + enum ReferenceKind: REFERENCE="refers" | CONTAINMENT="contains" | CONTAINER="container"; @@ -71,7 +75,6 @@ Conjunction: // //Case: // Conjunction ({Match.condition=current} "->" value=Expr)?; - //RuleDefinition: // "rule" // name=Identifier @@ -106,11 +109,18 @@ Expr: AssignmentExpr; AssignmentExpr returns Expr: - ComparisonExpr ({AssignmentExpr.left=current}"is" right=ComparisonExpr)*; + BooleanExpr ({AssignmentExpr.left=current} "is" right=BooleanExpr)*; + +enum BooleanBinaryOp returns BinaryOp: + AND="&&" | OR="||" | XOR="^^"; + +BooleanExpr returns Expr: + ComparisonExpr ({ArithmeticBinaryExpr.left=current} + op=BooleanBinaryOp right=ComparisonExpr)*; enum ComparisonOp: - LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="==" | NOT_EQ="!=" | - IN="in" | SUBSUMES=":>" | SUBSUMED_BY="<:" | ABS_EQ="===" | ABS_NOT_EQ="!=="; + LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="===" | NOT_EQ="!==" | + IN="in" | NODE_EQ="==" | NODE_NOT_EQ="!="; ComparisonExpr returns Expr: LatticeExpr ({ComparisonExpr.left=current} @@ -120,12 +130,8 @@ enum LatticeBinaryOp: MEET="/\\" | JOIN="\\/"; LatticeExpr returns Expr: - RangeExpr ({LatticeBinaryExpr.left=current} - op=LatticeBinaryOp right=RangeExpr)*; - -RangeExpr returns Expr: - AdditiveExpr ({RangeExpr.left=current} ".." ("*" | right=AdditiveExpr))* | - {RangeExpr} "*" ".." ("*" | right=AdditiveExpr); + AdditiveExpr ({LatticeBinaryExpr.left=current} + op=LatticeBinaryOp right=AdditiveExpr)*; enum AdditiveOp returns BinaryOp: ADD="+" | SUB="-"; @@ -145,11 +151,14 @@ enum ExponentialOp returns BinaryOp: POW="**"; ExponentialExpr returns Expr: - UnaryExpr ({ArithmeticBinaryExpr.left=current} + RangeExpr ({ArithmeticBinaryExpr.left=current} op=ExponentialOp right=ExponentialExpr)?; +RangeExpr returns Expr: + UnaryExpr ({RangeExpr.left=current} ".." right=UnaryExpr)*; + UnaryExpr returns Expr: - ArithmeticUnaryExpr | ModalExpr | NegationExpr | + ArithmeticUnaryExpr | NegationExpr | CountExpr | AggregationExpr | CastExpr; enum UnaryOp: @@ -158,23 +167,15 @@ enum UnaryOp: ArithmeticUnaryExpr: op=UnaryOp body=UnaryExpr; -enum Modality: - MAY="may" | MUST="must" | CURRENT="current"; - -ModalExpr: - modality=Modality body=UnaryExpr; - NegationExpr: "!" body=UnaryExpr; CountExpr: "count" body=UnaryExpr; -enum AggregationOp: - SUM="sum" | PROD="prod" | MIN="min" | MAX="max"; - AggregationExpr: - op=AggregationOp "{" value=Expr "|" condition=ComparisonExpr "}"; + aggregator=[AggregatorDeclaration|QualifiedName] + "{" value=Expr "|" condition=ComparisonExpr "}"; CastExpr returns Expr: CastExprBody ({CastExpr.body=current} "as" targetType=[Relation|QualifiedName])?; @@ -191,7 +192,7 @@ VariableOrNodeExpr: variableOrNode=[VariableOrNode|QualifiedName]; Constant: - RealConstant | IntConstant | StringConstant | LogicConstant; + RealConstant | IntConstant | StringConstant | InfiniteConstant | LogicConstant; IntConstant: intValue=INT; @@ -202,6 +203,9 @@ RealConstant: StringConstant: stringValue=STRING; +InfiniteConstant: + {InfiniteConstant} "*"; + enum LogicValue: TRUE="true" | FALSE="false" | UNKNOWN="unknown" | ERROR="error"; @@ -276,8 +280,8 @@ Identifier: NonContainmentIdentifier | "contains" | "container"; NonContainmentIdentifier: - ID | "atom" | "multi" | "contained" | - "sum" | "prod" | "min" | "max" | "problem" | "module"; + ID | "atom" | "multi" | "contained" | "problem" | "module" | + "datatype" | "aggregator"; Real returns ecore::EDouble: EXPONENTIAL | INT "." (INT | EXPONENTIAL); diff --git a/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java b/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java index f7039027..955a89f9 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java +++ b/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java @@ -30,9 +30,8 @@ import org.eclipse.xtext.validation.IResourceValidator; import org.eclipse.xtext.xbase.annotations.validation.DerivedStateAwareResourceValidator; import tools.refinery.language.conversion.ProblemValueConverterService; import tools.refinery.language.linking.ProblemLinkingService; -import tools.refinery.language.naming.ProblemDelegateQualifiedNameProvider; -import tools.refinery.language.naming.ProblemQualifiedNameConverter; import tools.refinery.language.naming.ProblemQualifiedNameProvider; +import tools.refinery.language.naming.ProblemQualifiedNameConverter; import tools.refinery.language.parser.ProblemEcoreElementFactory; import tools.refinery.language.parser.antlr.TokenSourceInjectingProblemParser; import tools.refinery.language.resource.ProblemLocationInFileProvider; @@ -68,12 +67,6 @@ public class ProblemRuntimeModule extends AbstractProblemRuntimeModule { return ProblemQualifiedNameConverter.class; } - public void configureIQualifiedNameProviderDelegate(Binder binder) { - binder.bind(IQualifiedNameProvider.class) - .annotatedWith(Names.named(ProblemQualifiedNameProvider.NAMED_DELEGATE)) - .to(ProblemDelegateQualifiedNameProvider.class); - } - @Override public Class bindIQualifiedNameProvider() { return ProblemQualifiedNameProvider.class; diff --git a/subprojects/language/src/main/java/tools/refinery/language/expressions/AbstractTermInterpreter.java b/subprojects/language/src/main/java/tools/refinery/language/expressions/AbstractTermInterpreter.java new file mode 100644 index 00000000..2530b707 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/expressions/AbstractTermInterpreter.java @@ -0,0 +1,131 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.expressions; + +import tools.refinery.language.model.problem.BinaryOp; +import tools.refinery.language.model.problem.UnaryOp; +import tools.refinery.language.typesystem.AggregatorName; +import tools.refinery.language.typesystem.DataExprType; + +import java.util.*; + +// This class is used to configure term interpreters by clients with various arguments. +@SuppressWarnings("SameParameterValue") +public abstract class AbstractTermInterpreter implements TermInterpreter { + private final Map negations = new HashMap<>(); + private final Map unaryOperators = new HashMap<>(); + private final Set comparisons = new HashSet<>(); + private final Set ranges = new HashSet<>(); + private final Map binaryOperators = new HashMap<>(); + private final Set casts = new HashSet<>(); + private final Map aggregators = new HashMap<>(); + + protected AbstractTermInterpreter() { + } + + protected void addNegation(DataExprType type, DataExprType result) { + negations.put(type, result); + } + + protected void addNegation(DataExprType type) { + addNegation(type, type); + } + + protected void addUnaryOperator(UnaryOp op, DataExprType type, DataExprType result) { + unaryOperators.put(new UnaryKey(op, type), result); + } + + protected void addUnaryOperator(UnaryOp op, DataExprType type) { + addUnaryOperator(op, type, type); + } + + protected void addComparison(DataExprType type) { + comparisons.add(type); + } + + protected void addRange(DataExprType type) { + ranges.add(type); + } + + protected void addBinaryOperator(BinaryOp op, DataExprType leftType, DataExprType rightType, DataExprType result) { + binaryOperators.put(new BinaryKey(op, leftType, rightType), result); + } + + protected void addBinaryOperator(BinaryOp op, DataExprType type) { + addBinaryOperator(op, type, type, type); + } + + protected void addCast(DataExprType fromType, DataExprType toType) { + if (fromType.equals(toType)) { + throw new IllegalArgumentException("The fromType and toType of a cast operator must be different"); + } + casts.add(new CastKey(fromType, toType)); + } + + protected void addAggregator(AggregatorName aggregator, DataExprType type, DataExprType result) { + aggregators.put(new AggregatorKey(aggregator, type), result); + } + + protected void addAggregator(AggregatorName aggregator, DataExprType type) { + addAggregator(aggregator, type, type); + } + + @Override + public Optional getNegationType(DataExprType type) { + return Optional.ofNullable(negations.get(type)); + } + + @Override + public Optional getUnaryOperationType(UnaryOp op, DataExprType type) { + if (unaryOperators.isEmpty()) { + return Optional.empty(); + } + return Optional.ofNullable(unaryOperators.get(new UnaryKey(op, type))); + } + + @Override + public boolean isComparisonSupported(DataExprType type) { + return comparisons.contains(type); + } + + @Override + public boolean isRangeSupported(DataExprType type) { + return ranges.contains(type); + } + + @Override + public Optional getBinaryOperationType(BinaryOp op, DataExprType leftType, DataExprType rightType) { + if (binaryOperators.isEmpty()) { + return Optional.empty(); + } + return Optional.ofNullable(binaryOperators.get(new BinaryKey(op, leftType, rightType))); + } + + @Override + public Optional getAggregationType(AggregatorName aggregator, DataExprType type) { + if (aggregators.isEmpty()) { + return Optional.empty(); + } + return Optional.ofNullable(aggregators.get(new AggregatorKey(aggregator, type))); + } + + @Override + public boolean isCastSupported(DataExprType fromType, DataExprType toType) { + return casts.contains(new CastKey(fromType, toType)); + } + + private record UnaryKey(UnaryOp op, DataExprType type) { + } + + private record BinaryKey(BinaryOp op, DataExprType leftType, DataExprType rightType) { + } + + private record CastKey(DataExprType fromType, DataExprType toType) { + } + + private record AggregatorKey(AggregatorName aggregator, DataExprType type) { + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/expressions/BuiltinTermInterpreter.java b/subprojects/language/src/main/java/tools/refinery/language/expressions/BuiltinTermInterpreter.java new file mode 100644 index 00000000..412ed8ba --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/expressions/BuiltinTermInterpreter.java @@ -0,0 +1,54 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.expressions; + +import tools.refinery.language.library.BuiltinLibrary; +import tools.refinery.language.model.problem.BinaryOp; +import tools.refinery.language.model.problem.UnaryOp; +import tools.refinery.language.typesystem.AggregatorName; +import tools.refinery.language.typesystem.DataExprType; + +public final class BuiltinTermInterpreter extends AbstractTermInterpreter { + public static final DataExprType BOOLEAN_TYPE = new DataExprType(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "boolean"); + public static final DataExprType INT_TYPE = new DataExprType(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "int"); + public static final DataExprType REAL_TYPE = new DataExprType(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "real"); + public static final DataExprType STRING_TYPE = new DataExprType(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "string"); + public static final AggregatorName MIN_AGGREGATOR = new AggregatorName(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "min"); + public static final AggregatorName MAX_AGGREGATOR = new AggregatorName(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "max"); + public static final AggregatorName SUM_AGGREGATOR = new AggregatorName(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "sum"); + + public BuiltinTermInterpreter() { + addNegation(BOOLEAN_TYPE); + addBinaryOperator(BinaryOp.AND, BOOLEAN_TYPE); + addBinaryOperator(BinaryOp.OR, BOOLEAN_TYPE); + addBinaryOperator(BinaryOp.XOR, BOOLEAN_TYPE); + + addUnaryOperator(UnaryOp.PLUS, INT_TYPE); + addUnaryOperator(UnaryOp.MINUS, INT_TYPE); + addComparison(INT_TYPE); + addRange(INT_TYPE); + addBinaryOperator(BinaryOp.ADD, INT_TYPE); + addBinaryOperator(BinaryOp.SUB, INT_TYPE); + addBinaryOperator(BinaryOp.MUL, INT_TYPE); + addAggregator(MIN_AGGREGATOR, INT_TYPE); + addAggregator(MAX_AGGREGATOR, INT_TYPE); + addAggregator(SUM_AGGREGATOR, INT_TYPE); + + addUnaryOperator(UnaryOp.PLUS, REAL_TYPE); + addUnaryOperator(UnaryOp.MINUS, REAL_TYPE); + addCast(INT_TYPE, REAL_TYPE); + addComparison(REAL_TYPE); + addRange(REAL_TYPE); + addBinaryOperator(BinaryOp.ADD, REAL_TYPE); + addBinaryOperator(BinaryOp.SUB, REAL_TYPE); + addBinaryOperator(BinaryOp.MUL, REAL_TYPE); + addBinaryOperator(BinaryOp.DIV, REAL_TYPE); + addBinaryOperator(BinaryOp.POW, REAL_TYPE); + addAggregator(MIN_AGGREGATOR, REAL_TYPE); + addAggregator(MAX_AGGREGATOR, REAL_TYPE); + addAggregator(SUM_AGGREGATOR, REAL_TYPE); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/expressions/CompositeTermInterpreter.java b/subprojects/language/src/main/java/tools/refinery/language/expressions/CompositeTermInterpreter.java new file mode 100644 index 00000000..b337e5dd --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/expressions/CompositeTermInterpreter.java @@ -0,0 +1,99 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.expressions; + +import tools.refinery.language.model.problem.BinaryOp; +import tools.refinery.language.model.problem.UnaryOp; +import tools.refinery.language.typesystem.AggregatorName; +import tools.refinery.language.typesystem.DataExprType; + +import java.util.List; +import java.util.Optional; + +public class CompositeTermInterpreter implements TermInterpreter { + private final List interpreters; + + public CompositeTermInterpreter(List interpreters) { + this.interpreters = interpreters; + } + + @Override + public Optional getNegationType(DataExprType type) { + for (var interpreter : interpreters) { + var result = interpreter.getNegationType(type); + if (result.isPresent()) { + return result; + } + } + return Optional.empty(); + } + + @Override + public Optional getUnaryOperationType(UnaryOp op, DataExprType type) { + for (var interpreter : interpreters) { + var result = interpreter.getUnaryOperationType(op, type); + if (result.isPresent()) { + return result; + } + } + return Optional.empty(); + } + + @Override + public boolean isComparisonSupported(DataExprType type) { + for (var interpreter : interpreters) { + var result = interpreter.isComparisonSupported(type); + if (result) { + return true; + } + } + return false; + } + + @Override + public boolean isRangeSupported(DataExprType type) { + for (var interpreter : interpreters) { + var result = interpreter.isRangeSupported(type); + if (result) { + return true; + } + } + return false; + } + + @Override + public Optional getBinaryOperationType(BinaryOp op, DataExprType leftType, DataExprType rightType) { + for (var interpreter : interpreters) { + var result = interpreter.getBinaryOperationType(op, leftType, rightType); + if (result.isPresent()) { + return result; + } + } + return Optional.empty(); + } + + @Override + public boolean isCastSupported(DataExprType fromType, DataExprType toType) { + for (var interpreter : interpreters) { + var result = interpreter.isCastSupported(fromType, toType); + if (result) { + return true; + } + } + return false; + } + + @Override + public Optional getAggregationType(AggregatorName aggregator, DataExprType type) { + for (var interpreter : interpreters) { + var result = interpreter.getAggregationType(aggregator, type); + if (result.isPresent()) { + return result; + } + } + return Optional.empty(); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/expressions/TermInterpreter.java b/subprojects/language/src/main/java/tools/refinery/language/expressions/TermInterpreter.java new file mode 100644 index 00000000..122785f2 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/expressions/TermInterpreter.java @@ -0,0 +1,29 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.expressions; + +import tools.refinery.language.model.problem.BinaryOp; +import tools.refinery.language.model.problem.UnaryOp; +import tools.refinery.language.typesystem.AggregatorName; +import tools.refinery.language.typesystem.DataExprType; + +import java.util.Optional; + +public interface TermInterpreter { + Optional getNegationType(DataExprType type); + + Optional getUnaryOperationType(UnaryOp op, DataExprType type); + + boolean isComparisonSupported(DataExprType type); + + boolean isRangeSupported(DataExprType type); + + Optional getBinaryOperationType(BinaryOp op, DataExprType leftType, DataExprType rightType); + + boolean isCastSupported(DataExprType fromType, DataExprType toType); + + Optional getAggregationType(AggregatorName aggregator, DataExprType type); +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemDelegateQualifiedNameProvider.java b/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemDelegateQualifiedNameProvider.java deleted file mode 100644 index b3931401..00000000 --- a/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemDelegateQualifiedNameProvider.java +++ /dev/null @@ -1,44 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2024 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.language.naming; - -import com.google.inject.Inject; -import org.eclipse.xtext.naming.DefaultDeclarativeQualifiedNameProvider; -import org.eclipse.xtext.naming.IQualifiedNameConverter; -import org.eclipse.xtext.naming.QualifiedName; -import tools.refinery.language.model.problem.Problem; -import tools.refinery.language.scoping.imports.ImportAdapter; -import tools.refinery.language.utils.ProblemUtil; - -public class ProblemDelegateQualifiedNameProvider extends DefaultDeclarativeQualifiedNameProvider { - @Inject - private IQualifiedNameConverter qualifiedNameConverter; - - protected QualifiedName qualifiedName(Problem problem) { - var qualifiedNameString = problem.getName(); - if (qualifiedNameString != null) { - return NamingUtil.stripRootPrefix(qualifiedNameConverter.toQualifiedName(qualifiedNameString)); - } - if (!ProblemUtil.isModule(problem)) { - return null; - } - var resource = problem.eResource(); - if (resource == null) { - return null; - } - var resourceUri = resource.getURI(); - if (resourceUri == null) { - return null; - } - var resourceSet = resource.getResourceSet(); - if (resourceSet == null) { - return null; - } - var adapter = ImportAdapter.getOrInstall(resourceSet); - // If a module has no explicitly specified name, return the qualified name it was resolved under. - return adapter.getQualifiedName(resourceUri); - } -} diff --git a/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemQualifiedNameProvider.java b/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemQualifiedNameProvider.java index 5b682058..2a4df4d0 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemQualifiedNameProvider.java +++ b/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemQualifiedNameProvider.java @@ -6,36 +6,44 @@ package tools.refinery.language.naming; import com.google.inject.Inject; -import com.google.inject.name.Named; -import org.eclipse.emf.ecore.EObject; -import org.eclipse.xtext.naming.IQualifiedNameProvider; +import com.google.inject.Singleton; +import org.eclipse.xtext.naming.DefaultDeclarativeQualifiedNameProvider; +import org.eclipse.xtext.naming.IQualifiedNameConverter; import org.eclipse.xtext.naming.QualifiedName; -import org.eclipse.xtext.util.IResourceScopeCache; -import org.eclipse.xtext.util.Tuples; -import tools.refinery.language.resource.ProblemResourceDescriptionStrategy; - -public class ProblemQualifiedNameProvider extends IQualifiedNameProvider.AbstractImpl { - private static final String PREFIX = "tools.refinery.language.naming.ProblemQualifiedNameProvider."; - public static final String NAMED_DELEGATE = PREFIX + "NAMED_DELEGATE"; - public static final String CACHE_KEY = PREFIX + "CACHE_KEY"; +import tools.refinery.language.model.problem.Problem; +import tools.refinery.language.scoping.imports.ImportAdapterProvider; +import tools.refinery.language.utils.ProblemUtil; +@Singleton +public class ProblemQualifiedNameProvider extends DefaultDeclarativeQualifiedNameProvider { @Inject - @Named(NAMED_DELEGATE) - private IQualifiedNameProvider delegate; + private IQualifiedNameConverter qualifiedNameConverter; @Inject - private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE; - - @Override - public QualifiedName getFullyQualifiedName(EObject obj) { - return cache.get(Tuples.pair(obj, CACHE_KEY), obj.eResource(), () -> computeFullyQualifiedName(obj)); - } + private ImportAdapterProvider importAdapterProvider; - public QualifiedName computeFullyQualifiedName(EObject obj) { - var qualifiedName = delegate.getFullyQualifiedName(obj); - if (qualifiedName != null && ProblemResourceDescriptionStrategy.shouldExport(obj)) { - return NamingUtil.addRootPrefix(qualifiedName); + protected QualifiedName qualifiedName(Problem problem) { + var qualifiedNameString = problem.getName(); + if (qualifiedNameString != null) { + return NamingUtil.stripRootPrefix(qualifiedNameConverter.toQualifiedName(qualifiedNameString)); + } + if (!ProblemUtil.isModule(problem)) { + return null; + } + var resource = problem.eResource(); + if (resource == null) { + return null; + } + var resourceUri = resource.getURI(); + if (resourceUri == null) { + return null; + } + var resourceSet = resource.getResourceSet(); + if (resourceSet == null) { + return null; } - return qualifiedName; + var adapter = importAdapterProvider.getOrInstall(resourceSet); + // If a module has no explicitly specified name, return the qualified name it was resolved under. + return adapter.getQualifiedName(resourceUri); } } diff --git a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java index 3dcf6b1f..8fd60364 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java +++ b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java @@ -8,7 +8,6 @@ package tools.refinery.language.resource; import com.google.common.collect.ImmutableMap; import com.google.inject.Inject; import com.google.inject.Singleton; -import com.google.inject.name.Named; import org.eclipse.emf.ecore.EObject; import org.eclipse.xtext.EcoreUtil2; import org.eclipse.xtext.naming.IQualifiedNameConverter; @@ -19,10 +18,9 @@ import org.eclipse.xtext.resource.IEObjectDescription; import org.eclipse.xtext.resource.impl.DefaultResourceDescriptionStrategy; import org.eclipse.xtext.util.IAcceptor; import tools.refinery.language.documentation.DocumentationCommentParser; -import tools.refinery.language.naming.ProblemQualifiedNameProvider; -import tools.refinery.language.scoping.imports.ImportCollector; import tools.refinery.language.model.problem.*; import tools.refinery.language.naming.NamingUtil; +import tools.refinery.language.scoping.imports.ImportCollector; import tools.refinery.language.utils.ProblemUtil; import java.util.Map; @@ -32,13 +30,15 @@ import java.util.stream.Collectors; public class ProblemResourceDescriptionStrategy extends DefaultResourceDescriptionStrategy { private static final String DATA_PREFIX = "tools.refinery.language.resource.ProblemResourceDescriptionStrategy."; - public static final String ARITY = DATA_PREFIX + "ARITY"; + public static final String TYPE_LIKE = DATA_PREFIX + "ARITY"; + public static final String TYPE_LIKE_TRUE = "true"; public static final String ERROR_PREDICATE = DATA_PREFIX + "ERROR_PREDICATE"; public static final String ERROR_PREDICATE_TRUE = "true"; public static final String SHADOWING_KEY = DATA_PREFIX + "SHADOWING_KEY"; public static final String SHADOWING_KEY_PROBLEM = "problem"; public static final String SHADOWING_KEY_NODE = "node"; public static final String SHADOWING_KEY_RELATION = "relation"; + public static final String SHADOWING_KEY_AGGREGATOR = "aggregator"; public static final String PREFERRED_NAME = DATA_PREFIX + "PREFERRED_NAME"; public static final String PREFERRED_NAME_TRUE = "true"; public static final String IMPORTS = DATA_PREFIX + "IMPORTS"; @@ -51,8 +51,7 @@ public class ProblemResourceDescriptionStrategy extends DefaultResourceDescripti private IQualifiedNameConverter qualifiedNameConverter; @Inject - @Named(ProblemQualifiedNameProvider.NAMED_DELEGATE) - private IQualifiedNameProvider delegateQualifiedNameProvider; + private IQualifiedNameProvider qualifiedNameProvider; @Inject private ImportCollector importCollector; @@ -123,7 +122,7 @@ public class ProblemResourceDescriptionStrategy extends DefaultResourceDescripti if (problem == null) { return QualifiedName.EMPTY; } - var qualifiedName = delegateQualifiedNameProvider.getFullyQualifiedName(problem); + var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(problem); return qualifiedName == null ? QualifiedName.EMPTY : qualifiedName; } @@ -152,8 +151,11 @@ public class ProblemResourceDescriptionStrategy extends DefaultResourceDescripti builder.put(SHADOWING_KEY, SHADOWING_KEY_NODE); } else if (eObject instanceof Relation relation) { builder.put(SHADOWING_KEY, SHADOWING_KEY_RELATION); - int arity = ProblemUtil.getArity(relation); - builder.put(ARITY, Integer.toString(arity)); + if (ProblemUtil.isTypeLike(relation)) { + builder.put(TYPE_LIKE, TYPE_LIKE_TRUE); + } + } else if (eObject instanceof AggregatorDeclaration) { + builder.put(SHADOWING_KEY, SHADOWING_KEY_AGGREGATOR); } if (eObject instanceof PredicateDefinition predicateDefinition && predicateDefinition.isError()) { builder.put(ERROR_PREDICATE, ERROR_PREDICATE_TRUE); diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemLocalScopeProvider.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemLocalScopeProvider.java index 0067bf94..3b94423a 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemLocalScopeProvider.java +++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemLocalScopeProvider.java @@ -6,7 +6,6 @@ package tools.refinery.language.scoping; import com.google.inject.Inject; -import com.google.inject.name.Named; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.EReference; import org.eclipse.emf.ecore.resource.Resource; @@ -17,14 +16,12 @@ import org.eclipse.xtext.resource.ISelectable; import org.eclipse.xtext.scoping.IScope; import org.eclipse.xtext.scoping.impl.AbstractGlobalScopeDelegatingScopeProvider; import org.eclipse.xtext.util.IResourceScopeCache; -import tools.refinery.language.naming.ProblemQualifiedNameProvider; public class ProblemLocalScopeProvider extends AbstractGlobalScopeDelegatingScopeProvider { private static final String CACHE_KEY = "tools.refinery.language.scoping.ProblemLocalScopeProvider.CACHE_KEY"; @Inject - @Named(ProblemQualifiedNameProvider.NAMED_DELEGATE) - private IQualifiedNameProvider delegateQualifiedNameProvider; + private IQualifiedNameProvider qualifiedNameProvider; @Inject private IResourceDescriptionsProvider resourceDescriptionsProvider; @@ -59,7 +56,7 @@ public class ProblemLocalScopeProvider extends AbstractGlobalScopeDelegatingScop if (rootElement == null) { return new NoFullyQualifiedNamesSelectable(resourceDescription); } - var rootName = delegateQualifiedNameProvider.getFullyQualifiedName(rootElement); + var rootName = qualifiedNameProvider.getFullyQualifiedName(rootElement); if (rootName == null) { return new NoFullyQualifiedNamesSelectable(resourceDescription); } diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java index f83a7ebd..d94c9a13 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java +++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java @@ -9,14 +9,12 @@ */ package tools.refinery.language.scoping; -import com.google.inject.Inject; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.EReference; import org.eclipse.xtext.EcoreUtil2; import org.eclipse.xtext.scoping.IScope; import org.eclipse.xtext.scoping.Scopes; import tools.refinery.language.model.problem.*; -import tools.refinery.language.utils.ProblemDesugarer; import java.util.Collection; import java.util.LinkedHashSet; @@ -29,9 +27,6 @@ import java.util.LinkedHashSet; * on how and when to use it. */ public class ProblemScopeProvider extends AbstractProblemScopeProvider { - @Inject - private ProblemDesugarer desugarer; - @Override public IScope getScope(EObject context, EReference reference) { var scope = super.getScope(context, reference); diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java index d7a5304f..753c8565 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java +++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java @@ -16,7 +16,12 @@ import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.emf.ecore.resource.ResourceSet; import org.eclipse.emf.ecore.util.EcoreUtil; import org.eclipse.xtext.naming.QualifiedName; +import tools.refinery.language.expressions.CompositeTermInterpreter; +import tools.refinery.language.expressions.TermInterpreter; +import tools.refinery.language.library.BuiltinLibrary; import tools.refinery.language.library.RefineryLibrary; +import tools.refinery.language.model.problem.Problem; +import tools.refinery.language.utils.BuiltinSymbols; import java.io.File; import java.nio.file.Path; @@ -25,15 +30,12 @@ import java.util.*; public class ImportAdapter extends AdapterImpl { private static final Logger LOG = Logger.getLogger(ImportAdapter.class); private static final List DEFAULT_LIBRARIES; + private static final List DEFAULT_TERM_INTERPRETERS; private static final List DEFAULT_PATHS; static { - var serviceLoader = ServiceLoader.load(RefineryLibrary.class); - var defaultLibraries = new ArrayList(); - for (var service : serviceLoader) { - defaultLibraries.add(service); - } - DEFAULT_LIBRARIES = List.copyOf(defaultLibraries); + DEFAULT_LIBRARIES = loadServices(RefineryLibrary.class); + DEFAULT_TERM_INTERPRETERS = loadServices(TermInterpreter.class); var pathEnv = System.getenv("REFINERY_LIBRARY_PATH"); if (pathEnv == null) { DEFAULT_PATHS = List.of(); @@ -45,16 +47,29 @@ public class ImportAdapter extends AdapterImpl { } } - private final List libraries; - private final List libraryPaths; + private static List loadServices(Class serviceClass) { + var serviceLoader = ServiceLoader.load(serviceClass); + var services = new ArrayList(); + for (var service : serviceLoader) { + services.add(service); + } + return List.copyOf(services); + } + + private ResourceSet resourceSet; + private final List libraries = new ArrayList<>(DEFAULT_LIBRARIES); + private final List termInterpreters = new ArrayList<>(DEFAULT_TERM_INTERPRETERS); + private final TermInterpreter termInterpreter = new CompositeTermInterpreter(termInterpreters); + private final List libraryPaths = new ArrayList<>(DEFAULT_PATHS); private final Cache failedResolutions = CacheBuilder.newBuilder().maximumSize(100).build(); private final Map qualifiedNameToUriMap = new LinkedHashMap<>(); private final Map uriToQualifiedNameMap = new LinkedHashMap<>(); + private Problem builtinProblem; + private BuiltinSymbols builtinSymbols; - private ImportAdapter(ResourceSet resourceSet) { - libraries = new ArrayList<>(DEFAULT_LIBRARIES); - libraryPaths = new ArrayList<>(DEFAULT_PATHS); + void setResourceSet(ResourceSet resourceSet) { + this.resourceSet = resourceSet; for (var resource : resourceSet.getResources()) { resourceAdded(resource); } @@ -69,6 +84,14 @@ public class ImportAdapter extends AdapterImpl { return libraries; } + public List getTermInterpreters() { + return termInterpreters; + } + + public TermInterpreter getTermInterpreter() { + return termInterpreter; + } + public List getLibraryPaths() { return libraryPaths; } @@ -190,16 +213,26 @@ public class ImportAdapter extends AdapterImpl { } } - public static ImportAdapter getOrInstall(ResourceSet resourceSet) { - var adapter = getAdapter(resourceSet); - if (adapter == null) { - adapter = new ImportAdapter(resourceSet); - resourceSet.eAdapters().add(adapter); + public Problem getBuiltinProblem() { + if (builtinProblem == null) { + var builtinResource = resourceSet.getResource(BuiltinLibrary.BUILTIN_LIBRARY_URI, true); + if (builtinResource == null) { + throw new IllegalStateException("Failed to load builtin resource"); + } + var contents = builtinResource.getContents(); + if (contents.isEmpty()) { + throw new IllegalStateException("builtin resource is empty"); + } + builtinProblem = (Problem) contents.getFirst(); + EcoreUtil.resolveAll(builtinResource); } - return adapter; + return builtinProblem; } - private static ImportAdapter getAdapter(ResourceSet resourceSet) { - return (ImportAdapter) EcoreUtil.getAdapter(resourceSet.eAdapters(), ImportAdapter.class); + public BuiltinSymbols getBuiltinSymbols() { + if (builtinSymbols == null) { + builtinSymbols = new BuiltinSymbols(getBuiltinProblem()); + } + return builtinSymbols; } } diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapterProvider.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapterProvider.java new file mode 100644 index 00000000..5ab3a851 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapterProvider.java @@ -0,0 +1,68 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.scoping.imports; + +import com.google.inject.Inject; +import com.google.inject.Provider; +import com.google.inject.Singleton; +import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.resource.Resource; +import org.eclipse.emf.ecore.resource.ResourceSet; +import org.eclipse.emf.ecore.util.EcoreUtil; +import org.jetbrains.annotations.NotNull; +import tools.refinery.language.expressions.TermInterpreter; +import tools.refinery.language.utils.BuiltinSymbols; + +@Singleton +public class ImportAdapterProvider { + @Inject + private Provider delegateProvider; + + public BuiltinSymbols getBuiltinSymbols(@NotNull EObject context) { + var adapter = getOrInstall(context); + return adapter.getBuiltinSymbols(); + } + + public BuiltinSymbols getBuiltinSymbols(@NotNull Resource context) { + var adapter = getOrInstall(context); + return adapter.getBuiltinSymbols(); + } + + public TermInterpreter getTermInterpreter(@NotNull EObject context) { + var adapter = getOrInstall(context); + return adapter.getTermInterpreter(); + } + + public ImportAdapter getOrInstall(@NotNull EObject context) { + var resource = context.eResource(); + if (resource == null) { + throw new IllegalArgumentException("context is not in a resource"); + } + return getOrInstall(resource); + } + + public ImportAdapter getOrInstall(@NotNull Resource context) { + var resourceSet = context.getResourceSet(); + if (resourceSet == null) { + throw new IllegalArgumentException("context is not in a resource set"); + } + return getOrInstall(resourceSet); + } + + public ImportAdapter getOrInstall(@NotNull ResourceSet resourceSet) { + var adapter = getAdapter(resourceSet); + if (adapter == null) { + adapter = delegateProvider.get(); + adapter.setResourceSet(resourceSet); + resourceSet.eAdapters().add(adapter); + } + return adapter; + } + + public static ImportAdapter getAdapter(@NotNull ResourceSet resourceSet) { + return (ImportAdapter) EcoreUtil.getAdapter(resourceSet.eAdapters(), ImportAdapter.class); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportCollector.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportCollector.java index ac5a92ba..f3ab54ae 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportCollector.java +++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportCollector.java @@ -46,6 +46,9 @@ public class ImportCollector { @Inject private Provider loadOnDemandProvider; + @Inject + private ImportAdapterProvider importAdapterProvider; + public ImportCollection getDirectImports(Resource resource) { return cache.get(DIRECT_IMPORTS_KEY, resource, () -> this.computeDirectImports(resource)); } @@ -58,7 +61,7 @@ public class ImportCollector { if (resourceSet == null) { return ImportCollection.EMPTY; } - var adapter = ImportAdapter.getOrInstall(resourceSet); + var adapter = importAdapterProvider.getOrInstall(resourceSet); var collection = new ImportCollection(); collectAutomaticImports(collection, adapter); collectExplicitImports(problem, collection, adapter); diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/AggregatorName.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/AggregatorName.java new file mode 100644 index 00000000..5939865a --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/AggregatorName.java @@ -0,0 +1,19 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +import org.eclipse.xtext.naming.QualifiedName; + +public record AggregatorName(QualifiedName qualifiedName) { + public AggregatorName(QualifiedName prefix, String name) { + this(prefix.append(name)); + } + + @Override + public String toString() { + return qualifiedName.isEmpty() ? "" : qualifiedName.getLastSegment(); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/DataExprType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/DataExprType.java new file mode 100644 index 00000000..9bc3e6aa --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/DataExprType.java @@ -0,0 +1,19 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +import org.eclipse.xtext.naming.QualifiedName; + +public record DataExprType(QualifiedName qualifiedName) implements FixedType { + public DataExprType(QualifiedName prefix, String name) { + this(prefix.append(name)); + } + + @Override + public String toString() { + return qualifiedName.isEmpty() ? "" : qualifiedName.getLastSegment(); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java new file mode 100644 index 00000000..9e44063d --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java @@ -0,0 +1,16 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +public sealed interface ExprType permits FixedType, MutableType { + NodeType NODE = new NodeType(); + LiteralType LITERAL = new LiteralType(); + InvalidType INVALID = new InvalidType(); + + FixedType getActualType(); + + ExprType unwrapIfSet(); +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java new file mode 100644 index 00000000..1b2ded48 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java @@ -0,0 +1,18 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +public sealed interface FixedType extends ExprType permits NodeType, LiteralType, InvalidType, DataExprType { + @Override + default FixedType getActualType() { + return this; + } + + @Override + default FixedType unwrapIfSet() { + return this; + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/InvalidType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/InvalidType.java new file mode 100644 index 00000000..c18612bc --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/InvalidType.java @@ -0,0 +1,16 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +public final class InvalidType implements FixedType { + InvalidType() { + } + + @Override + public String toString() { + return "invalid"; + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/LiteralType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/LiteralType.java new file mode 100644 index 00000000..7fd33553 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/LiteralType.java @@ -0,0 +1,16 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +public final class LiteralType implements FixedType { + LiteralType() { + } + + @Override + public String toString() { + return "constraint"; + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/MutableType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/MutableType.java new file mode 100644 index 00000000..78fdf884 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/MutableType.java @@ -0,0 +1,32 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +public final class MutableType implements ExprType { + private DataExprType actualType; + + @Override + public FixedType getActualType() { + return actualType == null ? INVALID : actualType; + } + + public void setActualType(DataExprType actualType) { + if (this.actualType != null) { + throw new IllegalStateException("Actual type was already set"); + } + this.actualType = actualType; + } + + @Override + public ExprType unwrapIfSet() { + return actualType == null ? this : actualType; + } + + @Override + public String toString() { + return getActualType().toString(); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/NodeType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/NodeType.java new file mode 100644 index 00000000..1baff212 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/NodeType.java @@ -0,0 +1,16 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +public final class NodeType implements FixedType { + NodeType() { + } + + @Override + public String toString() { + return "node"; + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/ProblemTypeAnalyzer.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ProblemTypeAnalyzer.java new file mode 100644 index 00000000..fcf99ad8 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ProblemTypeAnalyzer.java @@ -0,0 +1,32 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +import com.google.inject.Inject; +import com.google.inject.Provider; +import com.google.inject.Singleton; +import org.eclipse.xtext.util.IResourceScopeCache; +import tools.refinery.language.model.problem.Problem; + +@Singleton +public class ProblemTypeAnalyzer { + private static final String CACHE_KEY = "tools.refinery.language.typesystem.ProblemTypeAnalyzer.CACHE_KEY"; + + @Inject + private IResourceScopeCache resourceScopeCache; + + @Inject + private Provider typedModuleProvider; + + public TypedModule getOrComputeTypes(Problem problem) { + var resource = problem.eResource(); + return resourceScopeCache.get(CACHE_KEY, resource, () -> { + var typedModule = typedModuleProvider.get(); + typedModule.setProblem(problem); + return typedModule; + }); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/Signature.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/Signature.java new file mode 100644 index 00000000..8e72c185 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/Signature.java @@ -0,0 +1,11 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +import java.util.List; + +public record Signature(List parameterTypes, FixedType resultType) { +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java new file mode 100644 index 00000000..3e25a0f5 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java @@ -0,0 +1,107 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +import com.google.inject.Inject; +import com.google.inject.Singleton; +import org.eclipse.xtext.naming.IQualifiedNameProvider; +import org.eclipse.xtext.util.IResourceScopeCache; +import tools.refinery.language.model.problem.*; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; + +@Singleton +public class SignatureProvider { + private static final String PREFIX = "tools.refinery.language.typesystem.SignatureProvider."; + private static final String SIGNATURE_CACHE = PREFIX + "SIGNATURE_CACHE"; + private static final String DATATYPE_CACHE = PREFIX + "DATATYPE_CACHE"; + private static final String AGGREGATOR_CACHE = PREFIX + "AGGREGATOR_CACHE"; + + @Inject + private IQualifiedNameProvider qualifiedNameProvider; + + @Inject + private IResourceScopeCache cache; + + public Signature getSignature(Relation relation) { + var signatures = cache.get(SIGNATURE_CACHE, relation.eResource(), () -> new HashMap()); + return signatures.computeIfAbsent(relation, this::computeSignature); + } + + public int getArity(Relation relation) { + return getSignature(relation).parameterTypes().size(); + } + + private Signature computeSignature(Relation relation) { + return new Signature(getParameterTypes(relation), getResultType(relation)); + } + + private List getParameterTypes(Relation relation) { + return switch (relation) { + case ClassDeclaration ignored -> List.of(ExprType.NODE); + case EnumDeclaration ignored -> List.of(ExprType.NODE); + case DatatypeDeclaration datatypeDeclaration -> List.of(getDataType(datatypeDeclaration)); + case ReferenceDeclaration referenceDeclaration -> { + if (referenceDeclaration.getReferenceType() instanceof DatatypeDeclaration) { + yield List.of(ExprType.NODE); + } + yield List.of(ExprType.NODE, ExprType.NODE); + } + case ParametricDefinition parametricDefinition -> { + var parameters = parametricDefinition.getParameters(); + var exprTypes = new ArrayList(parameters.size()); + for (var parameter : parameters) { + if (parameter.getParameterType() instanceof DatatypeDeclaration datatypeDeclaration) { + exprTypes.add(getDataType(datatypeDeclaration)); + } else { + exprTypes.add(ExprType.NODE); + } + } + yield List.copyOf(exprTypes); + } + default -> throw new IllegalArgumentException("Unknown Relation: " + relation); + }; + } + + private FixedType getResultType(Relation relation) { + if (relation instanceof ReferenceDeclaration referenceDeclaration && + referenceDeclaration.getReferenceType() instanceof DatatypeDeclaration datatypeDeclaration) { + return getDataType(datatypeDeclaration); + } + return ExprType.LITERAL; + } + + public DataExprType getDataType(DatatypeDeclaration datatypeDeclaration) { + var dataTypes = cache.get(DATATYPE_CACHE, datatypeDeclaration.eResource(), + () -> new HashMap()); + return dataTypes.computeIfAbsent(datatypeDeclaration, this::computeDataType); + } + + private DataExprType computeDataType(DatatypeDeclaration datatypeDeclaration) { + var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(datatypeDeclaration); + if (qualifiedName == null) { + throw new IllegalArgumentException("Datatype declaration has no qualified name: " + datatypeDeclaration); + } + return new DataExprType(qualifiedName); + } + + public AggregatorName getAggregatorName(AggregatorDeclaration aggregatorDeclaration) { + var dataTypes = cache.get(AGGREGATOR_CACHE, aggregatorDeclaration.eResource(), + () -> new HashMap()); + return dataTypes.computeIfAbsent(aggregatorDeclaration, this::computeAggregatorName); + } + + private AggregatorName computeAggregatorName(AggregatorDeclaration aggregatorDeclaration) { + var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(aggregatorDeclaration); + if (qualifiedName == null) { + throw new IllegalArgumentException( + "Aggregator declaration has no qualified name: " + aggregatorDeclaration); + } + return new AggregatorName(qualifiedName); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java new file mode 100644 index 00000000..de923e0d --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java @@ -0,0 +1,568 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.typesystem; + +import com.google.inject.Inject; +import org.eclipse.emf.common.util.Diagnostic; +import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.EStructuralFeature; +import org.eclipse.xtext.validation.CheckType; +import org.eclipse.xtext.validation.FeatureBasedDiagnostic; +import tools.refinery.language.expressions.BuiltinTermInterpreter; +import tools.refinery.language.expressions.TermInterpreter; +import tools.refinery.language.model.problem.*; +import tools.refinery.language.scoping.imports.ImportAdapterProvider; +import tools.refinery.language.validation.ProblemValidator; + +import java.util.*; + +public class TypedModule { + private static final String OPERAND_TYPE_ERROR_MESSAGE = "Cannot determine operand type."; + + @Inject + private SignatureProvider signatureProvider; + + @Inject + private ImportAdapterProvider importAdapterProvider; + + private TermInterpreter interpreter; + private final Map> assignments = new LinkedHashMap<>(); + private final Map variableTypes = new HashMap<>(); + private final Map expressionTypes = new HashMap<>(); + private final Set variablesToProcess = new LinkedHashSet<>(); + private final List diagnostics = new ArrayList<>(); + + void setProblem(Problem problem) { + interpreter = importAdapterProvider.getTermInterpreter(problem); + gatherAssignments(problem); + checkTypes(problem); + } + + private void gatherAssignments(Problem problem) { + var iterator = problem.eAllContents(); + while (iterator.hasNext()) { + var eObject = iterator.next(); + if (!(eObject instanceof AssignmentExpr assignmentExpr)) { + continue; + } + if (assignmentExpr.getLeft() instanceof VariableOrNodeExpr variableOrNodeExpr && + variableOrNodeExpr.getVariableOrNode() instanceof Variable variable) { + var assignmentList = assignments.computeIfAbsent(variable, ignored -> new ArrayList<>(1)); + assignmentList.add(assignmentExpr); + } + iterator.prune(); + } + } + + private void checkTypes(Problem problem) { + for (var statement : problem.getStatements()) { + switch (statement) { + case PredicateDefinition predicateDefinition -> checkTypes(predicateDefinition); + case Assertion assertion -> checkTypes(assertion); + default -> { + // Nothing to type check. + } + } + } + } + + private void checkTypes(PredicateDefinition predicateDefinition) { + for (var conjunction : predicateDefinition.getBodies()) { + for (var literal : conjunction.getLiterals()) { + coerceIntoLiteral(literal); + } + } + } + + private void checkTypes(Assertion assertion) { + var relation = assertion.getRelation(); + var value = assertion.getValue(); + if (relation == null) { + return; + } + var type = signatureProvider.getSignature(relation).resultType(); + if (type == ExprType.LITERAL) { + if (value == null) { + return; + } + expectType(value, BuiltinTermInterpreter.BOOLEAN_TYPE); + return; + } + if (value == null) { + var message = "Assertion value of type %s is required.".formatted(type); + error(message, assertion, ProblemPackage.Literals.ASSERTION__RELATION, 0, ProblemValidator.TYPE_ERROR); + } + expectType(value, type); + } + + public List getDiagnostics() { + return diagnostics; + } + + public FixedType getVariableType(Variable variable) { + // We can't use computeIfAbsent here, because translating referenced queries calls this method in a reentrant + // way, which would cause a ConcurrentModificationException with computeIfAbsent. + @SuppressWarnings("squid:S3824") + var type = variableTypes.get(variable); + //noinspection Java8MapApi + if (type == null) { + type = computeVariableType(variable); + variableTypes.put(variable, type); + } + return type; + } + + private FixedType computeVariableType(Variable variable) { + if (variable instanceof Parameter) { + return computeUnassignedVariableType(variable); + } + var assignmnentList = assignments.get(variable); + if (assignmnentList == null || assignmnentList.isEmpty()) { + return computeUnassignedVariableType(variable); + } + if (variablesToProcess.contains(variable)) { + throw new IllegalStateException("Circular reference to variable: " + variable.getName()); + } + if (assignmnentList.size() > 1) { + var message = "Multiple assignments for variable '%s'.".formatted(variable.getName()); + for (var assignment : assignmnentList) { + error(message, assignment, ProblemPackage.Literals.BINARY_EXPR__LEFT, 0, + ProblemValidator.INVALID_ASSIGNMENT_ISSUE); + } + return ExprType.INVALID; + } + var assignment = assignmnentList.getFirst(); + variablesToProcess.add(variable); + try { + var assignedType = getExpressionType(assignment.getRight()); + if (assignedType instanceof MutableType) { + var message = "Cannot determine type of variable '%s'.".formatted(variable.getName()); + error(message, assignment, ProblemPackage.Literals.BINARY_EXPR__RIGHT, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + if (assignedType instanceof DataExprType dataExprType) { + return dataExprType; + } + if (assignedType != ExprType.INVALID) { + var message = "Expected data expression for variable '%s', got %s instead." + .formatted(variable.getName(), assignedType); + error(message, assignment, ProblemPackage.Literals.BINARY_EXPR__RIGHT, 0, ProblemValidator.TYPE_ERROR); + } + return ExprType.INVALID; + } finally { + variablesToProcess.remove(variable); + } + } + + private FixedType computeUnassignedVariableType(Variable variable) { + if (variable instanceof Parameter parameter && + parameter.getParameterType() instanceof DatatypeDeclaration datatypeDeclaration) { + return signatureProvider.getDataType(datatypeDeclaration); + } + // Parameters without an explicit datatype annotation are node variables. + return ExprType.NODE; + } + + public ExprType getExpressionType(Expr expr) { + // We can't use computeIfAbsent here, because translating referenced queries calls this method in a reentrant + // way, which would cause a ConcurrentModificationException with computeIfAbsent. + @SuppressWarnings("squid:S3824") + var type = expressionTypes.get(expr); + //noinspection Java8MapApi + if (type == null) { + type = computeExpressionType(expr); + expressionTypes.put(expr, type); + } + return type.unwrapIfSet(); + } + + private ExprType computeExpressionType(Expr expr) { + return switch (expr) { + case LogicConstant logicConstant -> computeExpressionType(logicConstant); + case IntConstant ignored -> BuiltinTermInterpreter.INT_TYPE; + case RealConstant ignored -> BuiltinTermInterpreter.REAL_TYPE; + case StringConstant ignored -> BuiltinTermInterpreter.STRING_TYPE; + case InfiniteConstant ignored -> new MutableType(); + case VariableOrNodeExpr variableOrNodeExpr -> computeExpressionType(variableOrNodeExpr); + case AssignmentExpr assignmentExpr -> computeExpressionType(assignmentExpr); + case Atom atom -> computeExpressionType(atom); + case NegationExpr negationExpr -> computeExpressionType(negationExpr); + case ArithmeticUnaryExpr arithmeticUnaryExpr -> computeExpressionType(arithmeticUnaryExpr); + case CountExpr countExpr -> computeExpressionType(countExpr); + case AggregationExpr aggregationExpr -> computeExpressionType(aggregationExpr); + case ComparisonExpr comparisonExpr -> computeExpressionType(comparisonExpr); + case LatticeBinaryExpr latticeBinaryExpr -> computeExpressionType(latticeBinaryExpr); + case RangeExpr rangeExpr -> computeExpressionType(rangeExpr); + case ArithmeticBinaryExpr arithmeticBinaryExpr -> computeExpressionType(arithmeticBinaryExpr); + case CastExpr castExpr -> computeExpressionType(castExpr); + default -> { + error("Unknown expression: " + expr.getClass().getSimpleName(), expr, null, 0, + ProblemValidator.UNKNOWN_EXPRESSION_ISSUE); + yield ExprType.INVALID; + } + }; + } + + private ExprType computeExpressionType(LogicConstant expr) { + return switch (expr.getLogicValue()) { + case TRUE, FALSE -> BuiltinTermInterpreter.BOOLEAN_TYPE; + case UNKNOWN, ERROR -> new MutableType(); + case null -> ExprType.INVALID; + }; + } + + private ExprType computeExpressionType(VariableOrNodeExpr expr) { + var target = expr.getVariableOrNode(); + if (target == null || target.eIsProxy()) { + return ExprType.INVALID; + } + return switch (target) { + case Node ignored -> ExprType.NODE; + case Variable variable -> { + if (variablesToProcess.contains(variable)) { + var message = "Circular reference to variable '%s'.".formatted(variable.getName()); + error(message, expr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, 0, + ProblemValidator.INVALID_ASSIGNMENT_ISSUE); + yield ExprType.INVALID; + } + yield getVariableType(variable); + } + default -> { + error("Unknown variable: " + target.getName(), expr, + ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, 0, + ProblemValidator.UNKNOWN_EXPRESSION_ISSUE); + yield ExprType.INVALID; + } + }; + } + + private ExprType computeExpressionType(AssignmentExpr expr) { + // Force the left side to type check. Since the left side is a variable, it will force the right side to also + // type check in order to infer the variable type. + return getExpressionType(expr.getLeft()) == ExprType.INVALID ? ExprType.INVALID : ExprType.LITERAL; + } + + private ExprType computeExpressionType(Atom atom) { + var relation = atom.getRelation(); + if (relation == null || relation.eIsProxy()) { + return ExprType.INVALID; + } + if (relation instanceof DatatypeDeclaration) { + var message = "Invalid call to data type. Use 'as %s' for casting.".formatted( + relation.getName()); + error(message, atom, ProblemPackage.Literals.ATOM__RELATION, 0, ProblemValidator.TYPE_ERROR); + } + var signature = signatureProvider.getSignature(relation); + var parameterTypes = signature.parameterTypes(); + var arguments = atom.getArguments(); + int size = Math.min(parameterTypes.size(), arguments.size()); + boolean ok = parameterTypes.size() == arguments.size(); + for (int i = 0; i < size; i++) { + var parameterType = parameterTypes.get(i); + var argument = arguments.get(i); + if (!expectType(argument, parameterType)) { + // Avoid short-circuiting to let us type check all arguments. + ok = false; + } + } + return ok ? signature.resultType() : ExprType.INVALID; + } + + private ExprType computeExpressionType(NegationExpr negationExpr) { + var body = negationExpr.getBody(); + if (body == null) { + return ExprType.INVALID; + } + var actualType = getExpressionType(body); + if (actualType == ExprType.LITERAL) { + // Negation of literals yields another (non-enumerable) literal. + return ExprType.LITERAL; + } + if (actualType == DataExprType.INVALID) { + return ExprType.INVALID; + } + if (actualType instanceof MutableType) { + error(OPERAND_TYPE_ERROR_MESSAGE, body, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + if (actualType instanceof DataExprType dataExprType) { + var result = interpreter.getNegationType(dataExprType); + if (result.isPresent()) { + return result.get(); + } + } + var message = "Data type %s does not support negation.".formatted(actualType); + error(message, negationExpr, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + + private ExprType computeExpressionType(ArithmeticUnaryExpr expr) { + var op = expr.getOp(); + var body = expr.getBody(); + if (op == null || body == null) { + return ExprType.INVALID; + } + var actualType = getExpressionType(body); + if (actualType == DataExprType.INVALID) { + return ExprType.INVALID; + } + if (actualType instanceof MutableType) { + error(OPERAND_TYPE_ERROR_MESSAGE, body, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + if (actualType instanceof DataExprType dataExprType) { + var result = interpreter.getUnaryOperationType(op, dataExprType); + if (result.isPresent()) { + return result.get(); + } + } + var message = "Unsupported operator for data type %s.".formatted(actualType); + error(message, expr, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + + private ExprType computeExpressionType(CountExpr countExpr) { + return coerceIntoLiteral(countExpr.getBody()) ? BuiltinTermInterpreter.INT_TYPE : ExprType.INVALID; + } + + private ExprType computeExpressionType(AggregationExpr expr) { + var aggregator = expr.getAggregator(); + if (aggregator == null || aggregator.eIsProxy()) { + return null; + } + // Avoid short-circuiting to let us type check both the value and the condition. + boolean ok = coerceIntoLiteral(expr.getCondition()); + var value = expr.getValue(); + var actualType = getExpressionType(value); + if (actualType == ExprType.INVALID) { + return ExprType.INVALID; + } + if (actualType instanceof MutableType) { + error(OPERAND_TYPE_ERROR_MESSAGE, value, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + if (actualType instanceof DataExprType dataExprType) { + var aggregatorName = signatureProvider.getAggregatorName(aggregator); + var result = interpreter.getAggregationType(aggregatorName, dataExprType); + if (result.isPresent()) { + return ok ? result.get() : ExprType.INVALID; + } + } + var message = "Unsupported aggregator for type %s.".formatted(actualType); + error(message, expr, ProblemPackage.Literals.AGGREGATION_EXPR__AGGREGATOR, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + + private ExprType computeExpressionType(ComparisonExpr expr) { + var left = expr.getLeft(); + var right = expr.getRight(); + var op = expr.getOp(); + if (op == ComparisonOp.NODE_EQ || op == ComparisonOp.NODE_NOT_EQ) { + // Avoid short-circuiting to let us type check both arguments. + boolean leftOk = expectType(left, ExprType.NODE); + boolean rightOk = expectType(right, ExprType.NODE); + return leftOk && rightOk ? ExprType.LITERAL : ExprType.INVALID; + } + if (!(getCommonDataType(expr) instanceof DataExprType commonType)) { + return ExprType.INVALID; + } + // Data equality and inequality are always supported for data types. + if (op != ComparisonOp.EQ && op != ComparisonOp.NOT_EQ && !interpreter.isComparisonSupported(commonType)) { + var message = "Data type %s does not support comparison.".formatted(commonType); + error(message, expr, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + return BuiltinTermInterpreter.BOOLEAN_TYPE; + } + + private ExprType computeExpressionType(LatticeBinaryExpr expr) { + // Lattice operations are always supported for data types. + return getCommonDataType(expr); + } + + private ExprType computeExpressionType(RangeExpr expr) { + var left = expr.getLeft(); + var right = expr.getRight(); + if (left instanceof InfiniteConstant && right instanceof InfiniteConstant) { + // `*..*` is equivalent to `unknown` if neither subexpression have been typed yet. + var mutableType = new MutableType(); + if (expressionTypes.putIfAbsent(left, mutableType) == null && + expressionTypes.put(right, mutableType) == null) { + return mutableType; + } + } + if (!(getCommonDataType(expr) instanceof DataExprType commonType)) { + return ExprType.INVALID; + } + if (!interpreter.isRangeSupported(commonType)) { + var message = "Data type %s does not support ranges.".formatted(commonType); + error(message, expr, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + return commonType; + } + + private ExprType computeExpressionType(ArithmeticBinaryExpr expr) { + var op = expr.getOp(); + var left = expr.getLeft(); + var right = expr.getRight(); + if (op == null || left == null || right == null) { + return ExprType.INVALID; + } + // Avoid short-circuiting to let us type check both arguments. + var leftType = getExpressionType(left); + var rightType = getExpressionType(right); + if (leftType == ExprType.INVALID || rightType == ExprType.INVALID) { + return ExprType.INVALID; + } + if (rightType instanceof MutableType rightMutableType) { + if (leftType instanceof DataExprType leftExprType) { + rightMutableType.setActualType(leftExprType); + rightType = leftExprType; + } else { + error(OPERAND_TYPE_ERROR_MESSAGE, right, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + } + if (leftType instanceof MutableType leftMutableType) { + if (rightType instanceof DataExprType rightExprType) { + leftMutableType.setActualType(rightExprType); + leftType = rightExprType; + } else { + error(OPERAND_TYPE_ERROR_MESSAGE, left, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + } + if (leftType instanceof DataExprType leftExprType && rightType instanceof DataExprType rightExprType) { + var result = interpreter.getBinaryOperationType(op, leftExprType, rightExprType); + if (result.isPresent()) { + return result.get(); + } + } + var messageBuilder = new StringBuilder("Unsupported operator for "); + if (leftType.equals(rightType)) { + messageBuilder.append("data type ").append(leftType); + } else { + messageBuilder.append("data types ").append(leftType).append(" and ").append(rightType); + } + messageBuilder.append("."); + error(messageBuilder.toString(), expr, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + + private ExprType computeExpressionType(CastExpr expr) { + var body = expr.getBody(); + var targetRelation = expr.getTargetType(); + if (body == null || !(targetRelation instanceof DatatypeDeclaration targetDeclaration)) { + return null; + } + var actualType = getExpressionType(body); + if (actualType == ExprType.INVALID) { + return ExprType.INVALID; + } + var targetType = signatureProvider.getDataType(targetDeclaration); + if (actualType instanceof MutableType mutableType) { + // Type ascription for polymorphic literal (e.g., `unknown as int` for the set of all integers). + mutableType.setActualType(targetType); + return targetType; + } + if (actualType.equals(targetType)) { + return targetType; + } + if (actualType instanceof DataExprType dataExprType && interpreter.isCastSupported(dataExprType, targetType)) { + return targetType; + } + var message = "Casting from %s to %s is not supported.".formatted(actualType, targetType); + error(message, expr, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + + private FixedType getCommonDataType(BinaryExpr expr) { + var commonType = getCommonType(expr); + if (!(commonType instanceof DataExprType) && commonType != ExprType.INVALID) { + var message = "Expected data expression, got %s instead.".formatted(commonType); + error(message, expr, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + return commonType; + } + + private FixedType getCommonType(BinaryExpr expr) { + var left = expr.getLeft(); + var right = expr.getRight(); + if (left == null || right == null) { + return ExprType.INVALID; + } + var leftType = getExpressionType(left); + if (leftType instanceof FixedType fixedLeftType) { + return expectType(right, fixedLeftType) ? fixedLeftType : ExprType.INVALID; + } else { + var rightType = getExpressionType(right); + if (rightType instanceof FixedType fixedRightType) { + return expectType(left, leftType, fixedRightType) ? fixedRightType : ExprType.INVALID; + } else { + error(OPERAND_TYPE_ERROR_MESSAGE, left, null, 0, ProblemValidator.TYPE_ERROR); + error(OPERAND_TYPE_ERROR_MESSAGE, right, null, 0, ProblemValidator.TYPE_ERROR); + return ExprType.INVALID; + } + } + } + + private boolean coerceIntoLiteral(Expr expr) { + if (expr == null) { + return false; + } + var actualType = getExpressionType(expr); + if (actualType == ExprType.LITERAL) { + return true; + } + return expectType(expr, actualType, BuiltinTermInterpreter.BOOLEAN_TYPE); + } + + private boolean expectType(Expr expr, FixedType expectedType) { + if (expr == null) { + return false; + } + var actualType = getExpressionType(expr); + return expectType(expr, actualType, expectedType); + } + + private boolean expectType(Expr expr, ExprType actualType, FixedType expectedType) { + if (expectedType == ExprType.INVALID) { + // Silence any further errors is the expected type failed to compute. + return false; + } + if (actualType.equals(expectedType)) { + return true; + } + if (actualType == ExprType.INVALID) { + // We have already emitted an error previously. + return false; + } + if (actualType instanceof MutableType mutableType && expectedType instanceof DataExprType dataExprType) { + mutableType.setActualType(dataExprType); + return true; + } + var builder = new StringBuilder() + .append("Expected ") + .append(expectedType) + .append(" expression"); + if (!(actualType instanceof MutableType)) { + builder.append(", got ") + .append(actualType) + .append(" instead"); + } + builder.append("."); + error(builder.toString(), expr, null, 0, ProblemValidator.TYPE_ERROR); + return false; + } + + private void error(String message, EObject object, EStructuralFeature feature, int index, String code, + String... issueData) { + diagnostics.add(new FeatureBasedDiagnostic(Diagnostic.ERROR, message, object, feature, index, + CheckType.NORMAL, code, issueData)); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java b/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java index c87fa044..72f23e85 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java @@ -1,5 +1,5 @@ /* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -7,7 +7,56 @@ package tools.refinery.language.utils; import tools.refinery.language.model.problem.*; -public record BuiltinSymbols(Problem problem, ClassDeclaration node, PredicateDefinition equals, - PredicateDefinition exists, ClassDeclaration contained, PredicateDefinition contains, - PredicateDefinition invalidContainer) { +public final class BuiltinSymbols { + private final Problem problem; + private final ClassDeclaration node; + private final PredicateDefinition equals; + private final PredicateDefinition exists; + private final ClassDeclaration contained; + private final PredicateDefinition contains; + private final PredicateDefinition invalidContainer; + + public BuiltinSymbols(Problem problem) { + this.problem = problem; + node = getDeclaration(ClassDeclaration.class, "node"); + equals = getDeclaration(PredicateDefinition.class, "equals"); + exists = getDeclaration(PredicateDefinition.class, "exists"); + contained = getDeclaration(ClassDeclaration.class, "contained"); + contains = getDeclaration(PredicateDefinition.class, "contains"); + invalidContainer = getDeclaration(PredicateDefinition.class, "invalidContainer"); + } + + public Problem problem() { + return problem; + } + + public ClassDeclaration node() { + return node; + } + + public PredicateDefinition equals() { + return equals; + } + + public PredicateDefinition exists() { + return exists; + } + + public ClassDeclaration contained() { + return contained; + } + + public PredicateDefinition contains() { + return contains; + } + + public PredicateDefinition invalidContainer() { + return invalidContainer; + } + + private T getDeclaration(Class type, String name) { + return problem.getStatements().stream().filter(type::isInstance).map(type::cast) + .filter(declaration -> name.equals(declaration.getName())).findFirst() + .orElseThrow(() -> new IllegalArgumentException("Built-in declaration " + name + " was not found")); + } } diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java deleted file mode 100644 index d45c8083..00000000 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java +++ /dev/null @@ -1,98 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.language.utils; - -import com.google.inject.Inject; -import com.google.inject.Singleton; -import org.eclipse.emf.ecore.EObject; -import org.eclipse.emf.ecore.resource.Resource; -import org.eclipse.xtext.util.IResourceScopeCache; -import org.eclipse.xtext.util.Tuples; -import tools.refinery.language.library.BuiltinLibrary; -import tools.refinery.language.model.problem.*; - -import java.util.*; - -@Singleton -public class ProblemDesugarer { - @Inject - private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE; - - public Optional getBuiltinProblem(EObject context) { - return Optional.ofNullable(context).map(EObject::eResource).flatMap(resource -> - cache.get("builtinProblem", resource, () -> doGetBuiltinProblem(resource))); - } - - private Optional doGetBuiltinProblem(Resource resource) { - return Optional.ofNullable(resource).map(Resource::getResourceSet) - .map(resourceSet -> resourceSet.getResource(BuiltinLibrary.BUILTIN_LIBRARY_URI, true)) - .map(Resource::getContents).filter(contents -> !contents.isEmpty()).map(List::getFirst) - .filter(Problem.class::isInstance).map(Problem.class::cast); - } - - public Optional getBuiltinSymbols(EObject context) { - return getBuiltinProblem(context).map(builtin -> - cache.get("builtinSymbols", builtin.eResource(), () -> doGetBuiltinSymbols(builtin))); - } - - private BuiltinSymbols doGetBuiltinSymbols(Problem builtin) { - var node = doGetDeclaration(builtin, ClassDeclaration.class, "node"); - var equals = doGetDeclaration(builtin, PredicateDefinition.class, "equals"); - var exists = doGetDeclaration(builtin, PredicateDefinition.class, "exists"); - var contained = doGetDeclaration(builtin, ClassDeclaration.class, "contained"); - var contains = doGetDeclaration(builtin, PredicateDefinition.class, "contains"); - var invalidContainer = doGetDeclaration(builtin, PredicateDefinition.class, "invalidContainer"); - return new BuiltinSymbols(builtin, node, equals, exists, contained, contains, invalidContainer); - } - - private T doGetDeclaration(Problem builtin, Class type, String name) { - return builtin.getStatements().stream().filter(type::isInstance).map(type::cast) - .filter(declaration -> name.equals(declaration.getName())).findFirst() - .orElseThrow(() -> new IllegalArgumentException("Built-in declaration " + name + " was not found")); - } - - public Collection getSuperclassesAndSelf(ClassDeclaration classDeclaration) { - return cache.get(Tuples.create(classDeclaration, "superclassesAndSelf"), classDeclaration.eResource(), - () -> doGetSuperclassesAndSelf(classDeclaration)); - } - - private Collection doGetSuperclassesAndSelf(ClassDeclaration classDeclaration) { - var builtinSymbols = getBuiltinSymbols(classDeclaration); - Set found = new HashSet<>(); - builtinSymbols.ifPresent(symbols -> found.add(symbols.node())); - Deque queue = new ArrayDeque<>(); - queue.addLast(classDeclaration); - while (!queue.isEmpty()) { - ClassDeclaration current = queue.removeFirst(); - if (!found.contains(current)) { - found.add(current); - for (Relation superType : current.getSuperTypes()) { - if (superType instanceof ClassDeclaration superDeclaration) { - queue.addLast(superDeclaration); - } - } - } - } - return found; - } - - public Collection getAllReferenceDeclarations(ClassDeclaration classDeclaration) { - return cache.get(Tuples.create(classDeclaration, "allReferenceDeclarations"), classDeclaration.eResource(), - () -> doGetAllReferenceDeclarations(classDeclaration)); - } - - private Collection doGetAllReferenceDeclarations(ClassDeclaration classDeclaration) { - Set referenceDeclarations = new HashSet<>(); - for (ClassDeclaration superclass : getSuperclassesAndSelf(classDeclaration)) { - referenceDeclarations.addAll(superclass.getFeatureDeclarations()); - } - return referenceDeclarations; - } - - public boolean isContainmentReference(ReferenceDeclaration referenceDeclaration) { - return referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT; - } -} diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java index 6d6d65da..9daa8f61 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java @@ -98,18 +98,19 @@ public final class ProblemUtil { return true; } - public static int getArity(Relation relation) { + public static boolean isTypeLike(Relation relation) { if (relation instanceof ClassDeclaration || relation instanceof EnumDeclaration || relation instanceof DatatypeDeclaration) { - return 1; - } - if (relation instanceof ReferenceDeclaration) { - return 2; + return true; } if (relation instanceof PredicateDefinition predicateDefinition) { - return predicateDefinition.getParameters().size(); + return predicateDefinition.getParameters().size() == 1; } - throw new IllegalArgumentException("Unknown Relation: " + relation); + return false; + } + + public static boolean isContainmentReference(ReferenceDeclaration referenceDeclaration) { + return referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT; } public static boolean isContainerReference(ReferenceDeclaration referenceDeclaration) { diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java index 7f45bc20..745e2d2b 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java +++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java @@ -10,6 +10,7 @@ package tools.refinery.language.validation; import com.google.inject.Inject; +import org.eclipse.emf.common.util.Diagnostic; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.EReference; import org.eclipse.xtext.EcoreUtil2; @@ -18,11 +19,15 @@ import org.eclipse.xtext.validation.Check; import org.jetbrains.annotations.Nullable; import tools.refinery.language.model.problem.*; import tools.refinery.language.naming.NamingUtil; -import tools.refinery.language.scoping.imports.ImportAdapter; -import tools.refinery.language.utils.ProblemDesugarer; +import tools.refinery.language.scoping.imports.ImportAdapterProvider; +import tools.refinery.language.typesystem.ProblemTypeAnalyzer; +import tools.refinery.language.typesystem.SignatureProvider; import tools.refinery.language.utils.ProblemUtil; -import java.util.*; +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; +import java.util.Set; /** * This class contains custom validation rules. @@ -32,47 +37,39 @@ import java.util.*; */ public class ProblemValidator extends AbstractProblemValidator { private static final String ISSUE_PREFIX = "tools.refinery.language.validation.ProblemValidator."; - public static final String UNEXPECTED_MODULE_NAME_ISSUE = ISSUE_PREFIX + "UNEXPECTED_MODULE_NAME"; - public static final String INVALID_IMPORT_ISSUE = ISSUE_PREFIX + "INVALID_IMPORT"; - public static final String SINGLETON_VARIABLE_ISSUE = ISSUE_PREFIX + "SINGLETON_VARIABLE"; - public static final String NODE_CONSTANT_ISSUE = ISSUE_PREFIX + "NODE_CONSTANT_ISSUE"; - public static final String DUPLICATE_NAME_ISSUE = ISSUE_PREFIX + "DUPLICATE_NAME"; - public static final String INVALID_MULTIPLICITY_ISSUE = ISSUE_PREFIX + "INVALID_MULTIPLICITY"; - public static final String ZERO_MULTIPLICITY_ISSUE = ISSUE_PREFIX + "ZERO_MULTIPLICITY"; - public static final String MISSING_OPPOSITE_ISSUE = ISSUE_PREFIX + "MISSING_OPPOSITE"; - public static final String INVALID_OPPOSITE_ISSUE = ISSUE_PREFIX + "INVALID_OPPOSITE"; - public static final String INVALID_SUPERTYPE_ISSUE = ISSUE_PREFIX + "INVALID_SUPERTYPE"; - public static final String INVALID_REFERENCE_TYPE_ISSUE = ISSUE_PREFIX + "INVALID_REFERENCE_TYPE"; - public static final String INVALID_ARITY_ISSUE = ISSUE_PREFIX + "INVALID_ARITY"; - public static final String INVALID_TRANSITIVE_CLOSURE_ISSUE = ISSUE_PREFIX + "INVALID_TRANSITIVE_CLOSURE"; - public static final String INVALID_VALUE_ISSUE = ISSUE_PREFIX + "INVALID_VALUE"; - public static final String UNSUPPORTED_ASSERTION_ISSUE = ISSUE_PREFIX + "UNSUPPORTED_ASSERTION"; - + public static final String UNKNOWN_EXPRESSION_ISSUE = ISSUE_PREFIX + "UNKNOWN_EXPRESSION"; public static final String INVALID_ASSIGNMENT_ISSUE = ISSUE_PREFIX + "INVALID_ASSIGNMENT"; + public static final String TYPE_ERROR = ISSUE_PREFIX + "TYPE_ERROR"; @Inject private ReferenceCounter referenceCounter; @Inject - private ProblemDesugarer desugarer; + private IQualifiedNameConverter qualifiedNameConverter; @Inject - private IQualifiedNameConverter qualifiedNameConverter; + private ImportAdapterProvider importAdapterProvider; + + @Inject + private SignatureProvider signatureProvider; + + @Inject + private ProblemTypeAnalyzer typeAnalyzer; @Check public void checkModuleName(Problem problem) { @@ -88,7 +85,7 @@ public class ProblemValidator extends AbstractProblemValidator { if (resourceSet == null) { return; } - var adapter = ImportAdapter.getOrInstall(resourceSet); + var adapter = importAdapterProvider.getOrInstall(resourceSet); var expectedName = adapter.getQualifiedName(resource.getURI()); if (expectedName == null) { return; @@ -158,15 +155,19 @@ public class ProblemValidator extends AbstractProblemValidator { public void checkUniqueDeclarations(Problem problem) { var relations = new ArrayList(); var nodes = new ArrayList(); + var aggregators = new ArrayList(); for (var statement : problem.getStatements()) { if (statement instanceof Relation relation) { relations.add(relation); } else if (statement instanceof NodeDeclaration nodeDeclaration) { nodes.addAll(nodeDeclaration.getNodes()); + } else if (statement instanceof AggregatorDeclaration aggregatorDeclaration) { + aggregators.add(aggregatorDeclaration); } } checkUniqueSimpleNames(relations); checkUniqueSimpleNames(nodes); + checkUniqueSimpleNames(aggregators); } @Check @@ -353,11 +354,14 @@ public class ProblemValidator extends AbstractProblemValidator { @Check public void checkAssertion(Assertion assertion) { - int argumentCount = assertion.getArguments().size(); - if (!(assertion.getValue() instanceof LogicConstant)) { - var message = "Assertion value must be one of 'true', 'false', 'unknown', or 'error'."; - acceptError(message, assertion, ProblemPackage.Literals.ASSERTION__VALUE, 0, INVALID_VALUE_ISSUE); + var relation = assertion.getRelation(); + if (relation instanceof DatatypeDeclaration) { + var message = "Assertions for data types are not supported."; + acceptError(message, assertion, ProblemPackage.Literals.ASSERTION__RELATION, 0, + UNSUPPORTED_ASSERTION_ISSUE); + return; } + int argumentCount = assertion.getArguments().size(); checkArity(assertion, ProblemPackage.Literals.ASSERTION__RELATION, argumentCount); } @@ -376,7 +380,7 @@ public class ProblemValidator extends AbstractProblemValidator { // Feature does not point to a {@link Relation}, we are probably already emitting another error. return; } - int arity = ProblemUtil.getArity(relation); + int arity = signatureProvider.getArity(relation); if (arity == expectedArity) { return; } @@ -387,11 +391,7 @@ public class ProblemValidator extends AbstractProblemValidator { @Check public void checkMultiObjectAssertion(Assertion assertion) { - var builtinSymbolsOption = desugarer.getBuiltinSymbols(assertion); - if (builtinSymbolsOption.isEmpty()) { - return; - } - var builtinSymbols = builtinSymbolsOption.get(); + var builtinSymbols = importAdapterProvider.getBuiltinSymbols(assertion); var relation = assertion.getRelation(); boolean isExists = builtinSymbols.exists().equals(relation); boolean isEquals = builtinSymbols.equals().equals(relation); @@ -524,5 +524,37 @@ public class ProblemValidator extends AbstractProblemValidator { acceptError(message, variableOrNodeExpr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, 0, INVALID_ASSIGNMENT_ISSUE); } + if (!(assignmentExpr.eContainer() instanceof Conjunction)) { + var message = "Assignments may only appear as top-level expressions."; + acceptError(message, assignmentExpr, null, 0, INVALID_ASSIGNMENT_ISSUE); + } + } + + @Check + private void checkInfiniteConstant(InfiniteConstant infiniteConstant) { + if (!(infiniteConstant.eContainer() instanceof RangeExpr)) { + var message = "Negative and positive infinity literals may only appear in '..' range expressions."; + acceptError(message, infiniteConstant, null, 0, TYPE_ERROR); + } + } + + @Check + private void checkTypes(Problem problem) { + var diagnostics = typeAnalyzer.getOrComputeTypes(problem).getDiagnostics(); + for (var diagnostic : diagnostics) { + switch (diagnostic.getSeverity()) { + case Diagnostic.INFO -> info(diagnostic.getMessage(), diagnostic.getSourceEObject(), + diagnostic.getFeature(), diagnostic.getIndex(), diagnostic.getIssueCode(), + diagnostic.getIssueData()); + case Diagnostic.WARNING -> warning(diagnostic.getMessage(), diagnostic.getSourceEObject(), + diagnostic.getFeature(), diagnostic.getIndex(), diagnostic.getIssueCode(), + diagnostic.getIssueData()); + case Diagnostic.ERROR -> error(diagnostic.getMessage(), diagnostic.getSourceEObject(), + diagnostic.getFeature(), diagnostic.getIndex(), diagnostic.getIssueCode(), + diagnostic.getIssueData()); + default -> throw new IllegalStateException("Unknown severity %s of %s" + .formatted(diagnostic.getSeverity(), diagnostic)); + } + } } } -- cgit v1.2.3-54-g00ecf