From 7fb99f0225911a8962aaf3493b89f41e791df359 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 19 Sep 2022 21:33:55 +0200 Subject: feat(language): problem desugaring --- .../ProblemCrossrefProposalProvider.java | 2 +- .../ProblemSemanticHighlightingCalculator.java | 8 +- subprojects/language-model/problem.aird | 67 +++-- .../src/main/resources/model/problem.ecore | 1 + .../src/main/resources/model/problem.genmodel | 1 + .../java/tools/refinery/language/ProblemUtil.java | 151 ----------- .../resource/ProblemDerivedStateComputer.java | 41 ++- .../resource/ProblemLocationInFileProvider.java | 2 +- .../ProblemResourceDescriptionStrategy.java | 2 +- .../language/resource/ReferenceCounter.java | 5 +- .../scoping/ProblemGlobalScopeProvider.java | 2 +- .../scoping/ProblemLocalScopeProvider.java | 2 +- .../language/scoping/ProblemScopeProvider.java | 10 +- .../refinery/language/utils/BuiltinSymbols.java | 14 + .../refinery/language/utils/CollectedSymbols.java | 10 + .../tools/refinery/language/utils/NodeInfo.java | 12 + .../refinery/language/utils/ProblemDesugarer.java | 142 +++++++++++ .../tools/refinery/language/utils/ProblemUtil.java | 82 ++++++ .../refinery/language/utils/RelationInfo.java | 27 ++ .../refinery/language/utils/SymbolCollector.java | 284 +++++++++++++++++++++ .../language/validation/ProblemValidator.java | 2 +- .../tools/refinery/language/builtin.problem | 4 +- .../language/tests/utils/SymbolCollectorTest.java | 276 ++++++++++++++++++++ .../model/tests/utils/WrappedArgument.java | 8 +- .../tests/utils/WrappedAssertionArgument.java | 7 +- .../language/model/tests/utils/WrappedProblem.java | 13 +- 26 files changed, 974 insertions(+), 201 deletions(-) delete mode 100644 subprojects/language/src/main/java/tools/refinery/language/ProblemUtil.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/utils/CollectedSymbols.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/utils/NodeInfo.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java create mode 100644 subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java create mode 100644 subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java (limited to 'subprojects') diff --git a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java index 3650561a..8f04ed00 100644 --- a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java +++ b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java @@ -14,9 +14,9 @@ import org.eclipse.xtext.resource.IEObjectDescription; import com.google.inject.Inject; -import tools.refinery.language.ProblemUtil; import tools.refinery.language.model.problem.Problem; import tools.refinery.language.resource.ReferenceCounter; +import tools.refinery.language.utils.ProblemUtil; public class ProblemCrossrefProposalProvider extends IdeCrossrefProposalProvider { @Inject diff --git a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/syntaxcoloring/ProblemSemanticHighlightingCalculator.java b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/syntaxcoloring/ProblemSemanticHighlightingCalculator.java index 477940aa..6a05005d 100644 --- a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/syntaxcoloring/ProblemSemanticHighlightingCalculator.java +++ b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/syntaxcoloring/ProblemSemanticHighlightingCalculator.java @@ -15,7 +15,6 @@ import org.eclipse.xtext.util.CancelIndicator; import com.google.common.collect.ImmutableList; import com.google.inject.Inject; -import tools.refinery.language.ProblemUtil; import tools.refinery.language.model.problem.ClassDeclaration; import tools.refinery.language.model.problem.NamedElement; import tools.refinery.language.model.problem.Node; @@ -23,6 +22,8 @@ import tools.refinery.language.model.problem.PredicateDefinition; import tools.refinery.language.model.problem.PredicateKind; import tools.refinery.language.model.problem.ProblemPackage; import tools.refinery.language.model.problem.ReferenceDeclaration; +import tools.refinery.language.utils.ProblemDesugarer; +import tools.refinery.language.utils.ProblemUtil; public class ProblemSemanticHighlightingCalculator extends DefaultSemanticHighlightingCalculator { private static final String BUILTIN_CLASS = "builtin"; @@ -36,6 +37,9 @@ public class ProblemSemanticHighlightingCalculator extends DefaultSemanticHighli @Inject private OperationCanceledManager operationCanceledManager; + @Inject + private ProblemDesugarer desugarer; + @Override protected boolean highlightElement(EObject object, IHighlightedPositionAcceptor acceptor, CancelIndicator cancelIndicator) { @@ -101,7 +105,7 @@ public class ProblemSemanticHighlightingCalculator extends DefaultSemanticHighli classesBuilder.add(ABSTRACT_CLASS); } if (eObject instanceof ReferenceDeclaration referenceDeclaration - && ProblemUtil.isContainmentReference(referenceDeclaration)) { + && desugarer.isContainmentReference(referenceDeclaration)) { classesBuilder.add(CONTAINMENT_CLASS); } if (eObject instanceof PredicateDefinition predicateDefinition diff --git a/subprojects/language-model/problem.aird b/subprojects/language-model/problem.aird index 60d52cc4..a02adf78 100644 --- a/subprojects/language-model/problem.aird +++ b/subprojects/language-model/problem.aird @@ -7,7 +7,7 @@ build/resources/main/model/problem.genmodel - + @@ -788,7 +788,7 @@ - + @@ -1060,17 +1060,17 @@ - + - + - + @@ -1283,17 +1283,17 @@ - + - + - + - + @@ -1528,11 +1528,11 @@ - + - + @@ -1676,8 +1676,8 @@ - - + + @@ -1842,17 +1842,17 @@ - + - + - + - + @@ -1904,6 +1904,22 @@ + + + + + + + + + + + + + + + + @@ -2431,7 +2447,7 @@ - + KEEP_LOCATION @@ -3140,7 +3156,7 @@ - + KEEP_LOCATION @@ -3825,6 +3841,19 @@ + + + + + + labelSize + + + labelSize + + + + diff --git a/subprojects/language-model/src/main/resources/model/problem.ecore b/subprojects/language-model/src/main/resources/model/problem.ecore index 58f26eae..0106dd61 100644 --- a/subprojects/language-model/src/main/resources/model/problem.ecore +++ b/subprojects/language-model/src/main/resources/model/problem.ecore @@ -129,6 +129,7 @@ + diff --git a/subprojects/language-model/src/main/resources/model/problem.genmodel b/subprojects/language-model/src/main/resources/model/problem.genmodel index 5442d29d..da70f922 100644 --- a/subprojects/language-model/src/main/resources/model/problem.genmodel +++ b/subprojects/language-model/src/main/resources/model/problem.genmodel @@ -140,6 +140,7 @@ + diff --git a/subprojects/language/src/main/java/tools/refinery/language/ProblemUtil.java b/subprojects/language/src/main/java/tools/refinery/language/ProblemUtil.java deleted file mode 100644 index 0be296fd..00000000 --- a/subprojects/language/src/main/java/tools/refinery/language/ProblemUtil.java +++ /dev/null @@ -1,151 +0,0 @@ -package tools.refinery.language; - -import java.util.ArrayDeque; -import java.util.Collection; -import java.util.Deque; -import java.util.HashSet; -import java.util.Optional; -import java.util.Set; - -import org.eclipse.emf.common.util.URI; -import org.eclipse.emf.ecore.EObject; -import org.eclipse.emf.ecore.resource.Resource; - -import tools.refinery.language.model.problem.ClassDeclaration; -import tools.refinery.language.model.problem.ImplicitVariable; -import tools.refinery.language.model.problem.Node; -import tools.refinery.language.model.problem.Problem; -import tools.refinery.language.model.problem.ProblemPackage; -import tools.refinery.language.model.problem.ReferenceDeclaration; -import tools.refinery.language.model.problem.Relation; -import tools.refinery.language.model.problem.Variable; - -public final class ProblemUtil { - public static final String BUILTIN_LIBRARY_NAME = "builtin"; - - public static final URI BUILTIN_LIBRARY_URI = getLibraryUri(BUILTIN_LIBRARY_NAME); - - public static final String NODE_CLASS_NAME = "node"; - - public static final String DOMAIN_CLASS_NAME = "domain"; - - public static final String DATA_CLASS_NAME = "data"; - - private ProblemUtil() { - throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); - } - - public static boolean isSingletonVariable(Variable variable) { - return variable.eContainingFeature() == ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__SINGLETON_VARIABLE; - } - - public static boolean isImplicitVariable(Variable variable) { - return variable instanceof ImplicitVariable; - } - - public static boolean isImplicitNode(Node node) { - return node.eContainingFeature() == ProblemPackage.Literals.PROBLEM__NODES; - } - - public static boolean isImplicit(EObject eObject) { - if (eObject instanceof Node node) { - return isImplicitNode(node); - } else if (eObject instanceof Variable variable) { - return isImplicitVariable(variable); - } else { - return false; - } - } - - public static boolean isIndividualNode(Node node) { - var containingFeature = node.eContainingFeature(); - return containingFeature == ProblemPackage.Literals.INDIVIDUAL_DECLARATION__NODES - || containingFeature == ProblemPackage.Literals.ENUM_DECLARATION__LITERALS; - } - - public static boolean isNewNode(Node node) { - return node.eContainingFeature() == ProblemPackage.Literals.CLASS_DECLARATION__NEW_NODE; - } - - public static Optional getBuiltInLibrary(EObject context) { - return Optional.ofNullable(context.eResource()).map(Resource::getResourceSet) - .map(resourceSet -> resourceSet.getResource(BUILTIN_LIBRARY_URI, true)).map(Resource::getContents) - .filter(contents -> !contents.isEmpty()).map(contents -> contents.get(0)) - .filter(Problem.class::isInstance).map(Problem.class::cast); - } - - public static boolean isBuiltIn(EObject eObject) { - if (eObject != null) { - var eResource = eObject.eResource(); - if (eResource != null) { - return BUILTIN_LIBRARY_URI.equals(eResource.getURI()); - } - } - return false; - } - - public static Optional getBuiltinClassDeclaration(EObject context, String name) { - return getBuiltInLibrary(context).flatMap(problem -> problem.getStatements().stream() - .filter(ClassDeclaration.class::isInstance).map(ClassDeclaration.class::cast) - .filter(declaration -> name.equals(declaration.getName())).findFirst()); - } - - public static Collection getSuperclassesAndSelf(ClassDeclaration classDeclaration) { - Set found = new HashSet<>(); - getBuiltinClassDeclaration(classDeclaration, NODE_CLASS_NAME).ifPresent(found::add); - 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); - } - } - } - } - getBuiltinClassDeclaration(classDeclaration, DATA_CLASS_NAME).ifPresent((dataClassDelcaration) -> { - if (!found.contains(dataClassDelcaration)) { - getBuiltinClassDeclaration(classDeclaration, DOMAIN_CLASS_NAME).ifPresent(found::add); - } - }); - return found; - } - - public static Collection getAllReferenceDeclarations(ClassDeclaration classDeclaration) { - Set referenceDeclarations = new HashSet<>(); - for (ClassDeclaration superclass : getSuperclassesAndSelf(classDeclaration)) { - referenceDeclarations.addAll(superclass.getReferenceDeclarations()); - } - return referenceDeclarations; - } - - public static boolean isDataClass(Relation relation) { - if (relation instanceof ClassDeclaration classDeclaration) { - var supertypes = getSuperclassesAndSelf(classDeclaration); - return getBuiltinClassDeclaration(classDeclaration, DATA_CLASS_NAME).map(supertypes::contains) - .orElse(false); - } - return false; - } - - public static boolean isContainmentReference(ReferenceDeclaration referenceDeclaration) { - switch (referenceDeclaration.getKind()) { - case REFERENCE, CONTAINER: - return false; - case CONTAINMENT: - return true; - case DEFAULT: - return isDataClass(referenceDeclaration.getReferenceType()); - default: - throw new IllegalArgumentException("Unknown reference kind " + referenceDeclaration.getKind()); - } - } - - private static URI getLibraryUri(String libraryName) { - return URI.createURI(ProblemUtil.class.getClassLoader() - .getResource("tools/refinery/language/%s.problem".formatted(libraryName)).toString()); - } -} diff --git a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemDerivedStateComputer.java b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemDerivedStateComputer.java index 275feca3..f28e1791 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemDerivedStateComputer.java +++ b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemDerivedStateComputer.java @@ -24,7 +24,9 @@ import com.google.inject.Provider; import com.google.inject.Singleton; import com.google.inject.name.Named; +import tools.refinery.language.model.problem.Assertion; import tools.refinery.language.model.problem.ClassDeclaration; +import tools.refinery.language.model.problem.ConstantAssertionArgument; import tools.refinery.language.model.problem.Node; import tools.refinery.language.model.problem.Problem; import tools.refinery.language.model.problem.ProblemFactory; @@ -34,6 +36,8 @@ import tools.refinery.language.model.problem.Statement; public class ProblemDerivedStateComputer implements IDerivedStateComputer { public static final String NEW_NODE = "new"; + public static final String CONSTANT_NODE = "constant"; + @Inject @Named(Constants.LANGUAGE_NAME) private String languageName; @@ -82,8 +86,17 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer { for (Statement statement : problem.getStatements()) { if (statement instanceof ClassDeclaration declaration && !declaration.isAbstract() && declaration.getNewNode() == null) { - var newNode = adapter.createNodeIfAbsent(declaration, key -> createNode(NEW_NODE)); + var newNode = adapter.createNewNodeIfAbsent(declaration, key -> createNode(NEW_NODE)); declaration.setNewNode(newNode); + } else if (statement instanceof Assertion assertion) { + for (var argument : assertion.getArguments()) { + if (argument instanceof ConstantAssertionArgument constantAssertionArgument + && constantAssertionArgument.getNode() == null) { + var constantNode = adapter.createConstantNodeIfAbsent(constantAssertionArgument, + key -> createNode(CONSTANT_NODE)); + constantAssertionArgument.setNode(constantNode); + } + } } } } @@ -117,14 +130,22 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer { protected void discardDerivedProblemState(Problem problem, Adapter adapter) { Set classDeclarations = new HashSet<>(); + Set constantAssertionArguments = new HashSet<>(); problem.getNodes().clear(); - for (Statement statement : problem.getStatements()) { + for (var statement : problem.getStatements()) { if (statement instanceof ClassDeclaration classDeclaration) { classDeclaration.setNewNode(null); classDeclarations.add(classDeclaration); + } else if (statement instanceof Assertion assertion) { + for (var argument : assertion.getArguments()) { + if (argument instanceof ConstantAssertionArgument constantAssertionArgument) { + constantAssertionArgument.setNode(null); + constantAssertionArguments.add(constantAssertionArgument); + } + } } } - adapter.retainAll(classDeclarations); + adapter.retainAll(classDeclarations, constantAssertionArguments); derivedVariableComputer.discardDerivedVariables(problem); } @@ -147,12 +168,22 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer { protected static class Adapter extends AdapterImpl { private Map newNodes = new HashMap<>(); - public Node createNodeIfAbsent(ClassDeclaration classDeclaration, Function createNode) { + private Map constantNodes = new HashMap<>(); + + public Node createNewNodeIfAbsent(ClassDeclaration classDeclaration, + Function createNode) { return newNodes.computeIfAbsent(classDeclaration, createNode); } - public void retainAll(Collection classDeclarations) { + public Node createConstantNodeIfAbsent(ConstantAssertionArgument constantAssertionArgument, + Function createNode) { + return constantNodes.computeIfAbsent(constantAssertionArgument, createNode); + } + + public void retainAll(Collection classDeclarations, + Collection constantAssertionArguments) { newNodes.keySet().retainAll(classDeclarations); + constantNodes.keySet().retainAll(constantAssertionArguments); } @Override diff --git a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemLocationInFileProvider.java b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemLocationInFileProvider.java index f6ae4f1e..df822987 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemLocationInFileProvider.java +++ b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemLocationInFileProvider.java @@ -4,9 +4,9 @@ import org.eclipse.emf.ecore.EObject; import org.eclipse.xtext.resource.DefaultLocationInFileProvider; import org.eclipse.xtext.util.ITextRegion; -import tools.refinery.language.ProblemUtil; import tools.refinery.language.model.problem.ImplicitVariable; import tools.refinery.language.model.problem.Node; +import tools.refinery.language.utils.ProblemUtil; public class ProblemLocationInFileProvider extends DefaultLocationInFileProvider { @Override 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 24d00f07..1a0b73a8 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 @@ -12,12 +12,12 @@ import org.eclipse.xtext.util.IAcceptor; import com.google.inject.Inject; import com.google.inject.Singleton; -import tools.refinery.language.ProblemUtil; import tools.refinery.language.model.problem.NamedElement; import tools.refinery.language.model.problem.Node; import tools.refinery.language.model.problem.Problem; import tools.refinery.language.model.problem.Variable; import tools.refinery.language.naming.NamingUtil; +import tools.refinery.language.utils.ProblemUtil; @Singleton public class ProblemResourceDescriptionStrategy extends DefaultResourceDescriptionStrategy { diff --git a/subprojects/language/src/main/java/tools/refinery/language/resource/ReferenceCounter.java b/subprojects/language/src/main/java/tools/refinery/language/resource/ReferenceCounter.java index 7525dfc6..ca20325e 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/resource/ReferenceCounter.java +++ b/subprojects/language/src/main/java/tools/refinery/language/resource/ReferenceCounter.java @@ -5,6 +5,7 @@ import java.util.Map; import org.eclipse.emf.ecore.EObject; import org.eclipse.xtext.util.IResourceScopeCache; +import org.eclipse.xtext.util.Tuples; import com.google.inject.Inject; import com.google.inject.Singleton; @@ -14,7 +15,7 @@ import tools.refinery.language.model.problem.Problem; @Singleton public class ReferenceCounter { @Inject - private IResourceScopeCache cache; + private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE; public int countReferences(Problem problem, EObject eObject) { var count = getReferenceCounts(problem).get(eObject); @@ -29,7 +30,7 @@ public class ReferenceCounter { if (resource == null) { return doGetReferenceCounts(problem); } - return cache.get(problem, resource, () -> doGetReferenceCounts(problem)); + return cache.get(Tuples.create(problem, "referenceCounts"), resource, () -> doGetReferenceCounts(problem)); } protected Map doGetReferenceCounts(Problem problem) { diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemGlobalScopeProvider.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemGlobalScopeProvider.java index ea4682f9..b749154c 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemGlobalScopeProvider.java +++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemGlobalScopeProvider.java @@ -6,7 +6,7 @@ import org.eclipse.emf.common.util.URI; import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.xtext.scoping.impl.ImportUriGlobalScopeProvider; -import tools.refinery.language.ProblemUtil; +import tools.refinery.language.utils.ProblemUtil; public class ProblemGlobalScopeProvider extends ImportUriGlobalScopeProvider { @Override 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 53815e37..61883f0e 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 @@ -13,7 +13,7 @@ import org.eclipse.xtext.scoping.impl.ImportedNamespaceAwareLocalScopeProvider; import com.google.inject.Inject; -import tools.refinery.language.ProblemUtil; +import tools.refinery.language.utils.ProblemUtil; public class ProblemLocalScopeProvider extends ImportedNamespaceAwareLocalScopeProvider { private static final QualifiedName BUILTIN_LIBRARY_QUALIFIED_NAME = QualifiedName 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 925ac3a5..567c3c26 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 @@ -12,7 +12,8 @@ import org.eclipse.xtext.EcoreUtil2; import org.eclipse.xtext.scoping.IScope; import org.eclipse.xtext.scoping.Scopes; -import tools.refinery.language.ProblemUtil; +import com.google.inject.Inject; + import tools.refinery.language.model.problem.ClassDeclaration; import tools.refinery.language.model.problem.Consequent; import tools.refinery.language.model.problem.ExistentialQuantifier; @@ -23,15 +24,18 @@ import tools.refinery.language.model.problem.ProblemPackage; import tools.refinery.language.model.problem.ReferenceDeclaration; import tools.refinery.language.model.problem.Variable; import tools.refinery.language.model.problem.VariableOrNodeArgument; +import tools.refinery.language.utils.ProblemDesugarer; /** * This class contains custom scoping description. - * + * * See * https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#scoping * on how and when to use it. */ public class ProblemScopeProvider extends AbstractProblemScopeProvider { + @Inject + private ProblemDesugarer desugarer; @Override public IScope getScope(EObject context, EReference reference) { @@ -106,7 +110,7 @@ public class ProblemScopeProvider extends AbstractProblemScopeProvider { return delegateScope; } var classDeclaration = (ClassDeclaration) relation; - var referenceDeclarations = ProblemUtil.getAllReferenceDeclarations(classDeclaration); + var referenceDeclarations = desugarer.getAllReferenceDeclarations(classDeclaration); return Scopes.scopeFor(referenceDeclarations, delegateScope); } } 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 new file mode 100644 index 00000000..7e43cecf --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java @@ -0,0 +1,14 @@ +package tools.refinery.language.utils; + +import tools.refinery.language.model.problem.ClassDeclaration; +import tools.refinery.language.model.problem.EnumDeclaration; +import tools.refinery.language.model.problem.Node; +import tools.refinery.language.model.problem.PredicateDefinition; +import tools.refinery.language.model.problem.Problem; +import tools.refinery.language.model.problem.ReferenceDeclaration; + +public record BuiltinSymbols(Problem problem, ClassDeclaration node, ReferenceDeclaration equals, + PredicateDefinition exists, ClassDeclaration domain, ClassDeclaration data, EnumDeclaration bool, Node boolTrue, + Node boolFalse, ClassDeclaration intClass, ClassDeclaration real, ClassDeclaration string, + PredicateDefinition contained, PredicateDefinition contains, PredicateDefinition root) { +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/CollectedSymbols.java b/subprojects/language/src/main/java/tools/refinery/language/utils/CollectedSymbols.java new file mode 100644 index 00000000..b5682f32 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/CollectedSymbols.java @@ -0,0 +1,10 @@ +package tools.refinery.language.utils; + +import java.util.Map; + +import tools.refinery.language.model.problem.Node; +import tools.refinery.language.model.problem.Relation; + +public record CollectedSymbols(Map nodes, Map relations) { + +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/NodeInfo.java b/subprojects/language/src/main/java/tools/refinery/language/utils/NodeInfo.java new file mode 100644 index 00000000..38db0e29 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/NodeInfo.java @@ -0,0 +1,12 @@ +package tools.refinery.language.utils; + +import java.util.ArrayList; +import java.util.Collection; + +import tools.refinery.language.model.problem.NodeValueAssertion; + +public record NodeInfo(String name, boolean individual, Collection valueAssertions) { + public NodeInfo(String name, boolean individual) { + this(name, individual, new ArrayList<>()); + } +} 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 new file mode 100644 index 00000000..23fd8982 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java @@ -0,0 +1,142 @@ +package tools.refinery.language.utils; + +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.xtext.util.IResourceScopeCache; +import org.eclipse.xtext.util.Tuples; +import tools.refinery.language.model.problem.*; + +import java.util.*; + +@Singleton +public class ProblemDesugarer { + @Inject + private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE; + + @Inject + private Provider symbolCollectorProvider; + + 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(ProblemUtil.BUILTIN_LIBRARY_URI, true)) + .map(Resource::getContents).filter(contents -> !contents.isEmpty()).map(contents -> contents.get(0)) + .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 = doGetEqualsReference(node); + var exists = doGetDeclaration(builtin, PredicateDefinition.class, "exists"); + var domain = doGetDeclaration(builtin, ClassDeclaration.class, "domain"); + var data = doGetDeclaration(builtin, ClassDeclaration.class, "data"); + var bool = doGetDeclaration(builtin, EnumDeclaration.class, "bool"); + var boolTrue = doGetLiteral(bool, "true"); + var boolFalse = doGetLiteral(bool, "false"); + var intClass = doGetDeclaration(builtin, ClassDeclaration.class, "int"); + var real = doGetDeclaration(builtin, ClassDeclaration.class, "real"); + var string = doGetDeclaration(builtin, ClassDeclaration.class, "string"); + var contained = doGetDeclaration(builtin, PredicateDefinition.class, "contained"); + var contains = doGetDeclaration(builtin, PredicateDefinition.class, "contains"); + var root = doGetDeclaration(builtin, PredicateDefinition.class, "root"); + return new BuiltinSymbols(builtin, node, equals, exists, domain, data, bool, boolTrue, boolFalse, intClass, + real, string, contained, contains, root); + } + + 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")); + } + + private ReferenceDeclaration doGetEqualsReference(ClassDeclaration nodeClassDeclaration) { + return nodeClassDeclaration.getReferenceDeclarations().stream() + .filter(reference -> "equals".equals(reference.getName())).findFirst() + .orElseThrow(() -> new IllegalArgumentException("Reference " + "equals" + " not found")); + } + + private Node doGetLiteral(EnumDeclaration enumDeclaration, String name) { + return enumDeclaration.getLiterals().stream().filter(literal -> name.equals(literal.getName())).findFirst() + .orElseThrow(() -> new IllegalArgumentException("Enum literal " + name + " 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); + } + } + } + } + if (builtinSymbols.isPresent() && !found.contains(builtinSymbols.get().data())) { + found.add(builtinSymbols.get().domain()); + } + 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.getReferenceDeclarations()); + } + return referenceDeclarations; + } + + public boolean isContainmentReference(ReferenceDeclaration referenceDeclaration) { + switch (referenceDeclaration.getKind()) { + case REFERENCE, CONTAINER: + return false; + case CONTAINMENT: + return true; + case DEFAULT: + return isDataClass(referenceDeclaration.getReferenceType()); + default: + throw new IllegalArgumentException("Unknown reference kind " + referenceDeclaration.getKind()); + } + } + + public boolean isDataClass(Relation relation) { + if (relation instanceof ClassDeclaration classDeclaration) { + var supertypes = getSuperclassesAndSelf(classDeclaration); + var builtinSymbols = getBuiltinSymbols(relation); + return builtinSymbols.isPresent() && supertypes.contains(builtinSymbols.get().data()); + } + return false; + } + + public CollectedSymbols collectSymbols(Problem problem) { + return cache.get(Tuples.create(problem, "collectedSymbols"), problem.eResource(), + () -> symbolCollectorProvider.get().collectSymbols(problem)); + } +} 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 new file mode 100644 index 00000000..a7acd747 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java @@ -0,0 +1,82 @@ +package tools.refinery.language.utils; + +import org.eclipse.emf.common.util.URI; +import org.eclipse.emf.ecore.EObject; + +import tools.refinery.language.model.problem.ImplicitVariable; +import tools.refinery.language.model.problem.Node; +import tools.refinery.language.model.problem.ProblemPackage; +import tools.refinery.language.model.problem.Variable; + +public final class ProblemUtil { + public static final String BUILTIN_LIBRARY_NAME = "builtin"; + + public static final URI BUILTIN_LIBRARY_URI = getLibraryUri(BUILTIN_LIBRARY_NAME); + + public static final String NODE_CLASS_NAME = "node"; + + public static final String DOMAIN_CLASS_NAME = "domain"; + + public static final String DATA_CLASS_NAME = "data"; + + public static final String INT_CLASS_NAME = "int"; + + public static final String REAL_CLASS_NAME = "real"; + + public static final String STRING_CLASS_NAME = "string"; + + public static final String EQUALS_RELATION_NAME = "equals"; + + public static final String EXISTS_PREDICATE_NAME = "exists"; + + private ProblemUtil() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static boolean isBuiltIn(EObject eObject) { + if (eObject != null) { + var eResource = eObject.eResource(); + if (eResource != null) { + return ProblemUtil.BUILTIN_LIBRARY_URI.equals(eResource.getURI()); + } + } + return false; + } + + public static boolean isSingletonVariable(Variable variable) { + return variable.eContainingFeature() == ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__SINGLETON_VARIABLE; + } + + public static boolean isImplicitVariable(Variable variable) { + return variable instanceof ImplicitVariable; + } + + public static boolean isImplicitNode(Node node) { + return node.eContainingFeature() == ProblemPackage.Literals.PROBLEM__NODES; + } + + public static boolean isImplicit(EObject eObject) { + if (eObject instanceof Node node) { + return isImplicitNode(node); + } else if (eObject instanceof Variable variable) { + return isImplicitVariable(variable); + } else { + return false; + } + } + + public static boolean isIndividualNode(Node node) { + var containingFeature = node.eContainingFeature(); + return containingFeature == ProblemPackage.Literals.INDIVIDUAL_DECLARATION__NODES + || containingFeature == ProblemPackage.Literals.ENUM_DECLARATION__LITERALS; + } + + public static boolean isNewNode(Node node) { + return node.eContainingFeature() == ProblemPackage.Literals.CLASS_DECLARATION__NEW_NODE; + } + + private static URI getLibraryUri(String libraryName) { + return URI.createURI(ProblemUtil.class.getClassLoader() + .getResource("tools/refinery/language/%s.problem".formatted(libraryName)).toString()); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java b/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java new file mode 100644 index 00000000..ae56e3a5 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java @@ -0,0 +1,27 @@ +package tools.refinery.language.utils; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; + +import tools.refinery.language.model.problem.Assertion; +import tools.refinery.language.model.problem.Conjunction; +import tools.refinery.language.model.problem.Multiplicity; +import tools.refinery.language.model.problem.Parameter; +import tools.refinery.language.model.problem.PredicateKind; +import tools.refinery.language.model.problem.Relation; +import tools.refinery.language.model.problem.TypeScope; + +public record RelationInfo(String name, PredicateKind kind, List parameters, Multiplicity multiplicity, + Relation opposite, Collection bodies, Collection defaultAssertions, + Collection assertions, Collection typeScopes) { + public RelationInfo(String name, PredicateKind kind, List parameters, Multiplicity multiplicity, + Relation opposite, Collection bodies) { + this(name, kind, parameters, multiplicity, opposite, bodies, new ArrayList<>(), new ArrayList<>(), + new ArrayList<>()); + } + + public boolean hasDefinition() { + return bodies != null && !bodies.isEmpty(); + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java b/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java new file mode 100644 index 00000000..87cce1f3 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java @@ -0,0 +1,284 @@ +package tools.refinery.language.utils; + +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; + +import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.util.EcoreUtil; +import org.eclipse.xtext.naming.IQualifiedNameConverter; +import org.eclipse.xtext.naming.IQualifiedNameProvider; + +import com.google.inject.Inject; + +import tools.refinery.language.model.problem.Assertion; +import tools.refinery.language.model.problem.ClassDeclaration; +import tools.refinery.language.model.problem.ConstantAssertionArgument; +import tools.refinery.language.model.problem.EnumDeclaration; +import tools.refinery.language.model.problem.IndividualDeclaration; +import tools.refinery.language.model.problem.IntConstant; +import tools.refinery.language.model.problem.LogicValue; +import tools.refinery.language.model.problem.Node; +import tools.refinery.language.model.problem.NodeValueAssertion; +import tools.refinery.language.model.problem.PredicateDefinition; +import tools.refinery.language.model.problem.PredicateKind; +import tools.refinery.language.model.problem.Problem; +import tools.refinery.language.model.problem.ProblemFactory; +import tools.refinery.language.model.problem.RealConstant; +import tools.refinery.language.model.problem.Relation; +import tools.refinery.language.model.problem.StringConstant; + +class SymbolCollector { + @Inject + private IQualifiedNameProvider qualifiedNameProvider; + + @Inject + private IQualifiedNameConverter qualifiedNameConverter; + + @Inject + ProblemDesugarer desugarer; + + private BuiltinSymbols builtinSymbols; + private final Map nodes = new LinkedHashMap<>(); + private final Map relations = new LinkedHashMap<>(); + + public CollectedSymbols collectSymbols(Problem problem) { + builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( + "Problem has no associated built-in library")); + collectOwnSymbols(builtinSymbols.problem()); + collectOwnSymbols(problem); + return new CollectedSymbols(nodes, relations); + } + + public void collectOwnSymbols(Problem problem) { + collectOwnRelations(problem); + collectOwnNodes(problem); + collectOwnAssertions(problem); + } + + private void collectOwnRelations(Problem problem) { + for (var statement : problem.getStatements()) { + if (statement instanceof PredicateDefinition predicateDefinition) { + collectPredicate(predicateDefinition); + } else if (statement instanceof ClassDeclaration classDeclaration) { + collectClass(classDeclaration); + } else if (statement instanceof EnumDeclaration enumDeclaration) { + collectEnum(enumDeclaration); + } + } + } + + private void collectPredicate(PredicateDefinition predicateDefinition) { + var info = new RelationInfo(getQualifiedNameString(predicateDefinition), + predicateDefinition.getKind(), + predicateDefinition.getParameters(), null, null, predicateDefinition.getBodies()); + relations.put(predicateDefinition, info); + } + + private void collectClass(ClassDeclaration classDeclaration) { + // node and domain classes are not contained by default, but every other type is + // contained, including data types. + var contained = + classDeclaration != builtinSymbols.node() && classDeclaration != builtinSymbols.domain(); + var classKind = contained ? PredicateKind.CONTAINED : PredicateKind.DEFAULT; + var instanceParameter = ProblemFactory.eINSTANCE.createParameter(); + instanceParameter.setName("instance"); + var classInfo = new RelationInfo(getQualifiedNameString(classDeclaration), classKind, + List.of(instanceParameter), null, null, List.of()); + relations.put(classDeclaration, classInfo); + collectReferences(classDeclaration); + } + + private void collectReferences(ClassDeclaration classDeclaration) { + for (var referenceDeclaration : classDeclaration.getReferenceDeclarations()) { + var referenceKind = desugarer.isContainmentReference(referenceDeclaration) ? + PredicateKind.CONTAINMENT : + PredicateKind.DEFAULT; + var sourceParameter = ProblemFactory.eINSTANCE.createParameter(); + sourceParameter.setName("source"); + sourceParameter.setParameterType(classDeclaration); + var targetParameter = ProblemFactory.eINSTANCE.createParameter(); + targetParameter.setName("target"); + var multiplicity = referenceDeclaration.getMultiplicity(); + if (multiplicity == null) { + var exactMultiplicity = ProblemFactory.eINSTANCE.createExactMultiplicity(); + exactMultiplicity.setExactValue(1); + multiplicity = exactMultiplicity; + } + targetParameter.setParameterType(referenceDeclaration.getReferenceType()); + var referenceInfo = new RelationInfo(getQualifiedNameString(referenceDeclaration), referenceKind, + List.of(sourceParameter, targetParameter), multiplicity, referenceDeclaration.getOpposite(), + List.of()); + this.relations.put(referenceDeclaration, referenceInfo); + } + } + + private void collectEnum(EnumDeclaration enumDeclaration) { + var instanceParameter = ProblemFactory.eINSTANCE.createParameter(); + instanceParameter.setName("instance"); + var info = new RelationInfo(getQualifiedNameString(enumDeclaration), PredicateKind.DEFAULT, + List.of(instanceParameter), null, null, List.of()); + this.relations.put(enumDeclaration, info); + } + + private void collectOwnNodes(Problem problem) { + for (var statement : problem.getStatements()) { + if (statement instanceof IndividualDeclaration individualDeclaration) { + collectIndividuals(individualDeclaration); + } else if (statement instanceof ClassDeclaration classDeclaration) { + collectNewNode(classDeclaration); + } else if (statement instanceof EnumDeclaration enumDeclaration) { + collectEnumLiterals(enumDeclaration); + } else if (statement instanceof Assertion assertion) { + collectConstantNodes(assertion); + } + } + for (var node : problem.getNodes()) { + addNode(node, false); + } + } + + private void collectIndividuals(IndividualDeclaration individualDeclaration) { + for (var individual : individualDeclaration.getNodes()) { + addNode(individual, true); + } + } + + private void collectNewNode(ClassDeclaration classDeclaration) { + var newNode = classDeclaration.getNewNode(); + if (newNode != null) { + addNode(newNode, false); + } + } + + private void collectEnumLiterals(EnumDeclaration enumDeclaration) { + for (var literal : enumDeclaration.getLiterals()) { + addNode(literal, true); + } + } + + private void collectConstantNodes(Assertion assertion) { + for (var argument : assertion.getArguments()) { + if (argument instanceof ConstantAssertionArgument constantAssertionArgument) { + var constantNode = constantAssertionArgument.getNode(); + if (constantNode != null) { + addNode(constantNode, false); + } + } + } + } + + private void addNode(Node node, boolean individual) { + var info = new NodeInfo(getQualifiedNameString(node), individual); + this.nodes.put(node, info); + } + + private String getQualifiedNameString(EObject eObject) { + var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject); + if (qualifiedName == null) { + return null; + } + return qualifiedNameConverter.toString(qualifiedName); + } + + private void collectOwnAssertions(Problem problem) { + for (var statement : problem.getStatements()) { + if (statement instanceof Assertion assertion) { + collectAssertion(assertion); + } else if (statement instanceof NodeValueAssertion nodeValueAssertion) { + collectNodeValueAssertion(nodeValueAssertion); + } else if (statement instanceof ClassDeclaration classDeclaration) { + collectClassAssertion(classDeclaration); + } else if (statement instanceof EnumDeclaration enumDeclaration) { + collectEnumAssertions(enumDeclaration); + } + } + } + + private void collectAssertion(Assertion assertion) { + var relationInfo = this.relations.get(assertion.getRelation()); + if (relationInfo == null) { + throw new IllegalStateException("Assertion refers to unknown relation"); + } + if (assertion.getArguments().size() != relationInfo.parameters().size()) { + // Silently ignoring assertions of invalid arity helps when SymbolCollector is called on an invalid + // Problem during editing. The errors can still be detected by the Problem validator. + return; + } + if (assertion.isDefault()) { + relationInfo.defaultAssertions().add(assertion); + } else { + relationInfo.assertions().add(assertion); + } + for (var argument : assertion.getArguments()) { + if (argument instanceof ConstantAssertionArgument constantAssertionArgument) { + var constantNode = constantAssertionArgument.getNode(); + if (constantNode != null) { + var valueAssertion = ProblemFactory.eINSTANCE.createNodeValueAssertion(); + valueAssertion.setNode(constantNode); + valueAssertion.setValue(EcoreUtil.copy(constantAssertionArgument.getConstant())); + collectNodeValueAssertion(valueAssertion); + var logicValue = assertion.getValue(); + if (logicValue != LogicValue.TRUE) { + addAssertion(builtinSymbols.exists(), logicValue, constantNode); + } + } + } + } + } + + private void collectNodeValueAssertion(NodeValueAssertion nodeValueAssertion) { + var node = nodeValueAssertion.getNode(); + if (node == null) { + return; + } + var nodeInfo = this.nodes.get(node); + if (nodeInfo == null) { + throw new IllegalStateException("Node value assertion refers to unknown node"); + } + nodeInfo.valueAssertions().add(nodeValueAssertion); + var constant = nodeValueAssertion.getValue(); + if (constant == null) { + return; + } + Relation dataType; + if (constant instanceof IntConstant) { + dataType = builtinSymbols.intClass(); + } else if (constant instanceof RealConstant) { + dataType = builtinSymbols.real(); + } else if (constant instanceof StringConstant) { + dataType = builtinSymbols.string(); + } else { + throw new IllegalArgumentException("Unknown constant type"); + } + addAssertion(dataType, LogicValue.TRUE, node); + } + + private void collectClassAssertion(ClassDeclaration classDeclaration) { + var node = classDeclaration.getNewNode(); + if (node == null) { + return; + } + addAssertion(classDeclaration, LogicValue.TRUE, node); + addAssertion(builtinSymbols.exists(), LogicValue.UNKNOWN, node); + addAssertion(builtinSymbols.equals(), LogicValue.UNKNOWN, node, node); + } + + private void collectEnumAssertions(EnumDeclaration enumDeclaration) { + for (var literal : enumDeclaration.getLiterals()) { + addAssertion(enumDeclaration, LogicValue.TRUE, literal); + } + } + + private void addAssertion(Relation relation, LogicValue logicValue, Node... nodes) { + var assertion = ProblemFactory.eINSTANCE.createAssertion(); + assertion.setRelation(relation); + for (var node : nodes) { + var argument = ProblemFactory.eINSTANCE.createNodeAssertionArgument(); + argument.setNode(node); + assertion.getArguments().add(argument); + } + assertion.setValue(logicValue); + collectAssertion(assertion); + } +} 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 6b0982eb..a0e78e1d 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 @@ -8,13 +8,13 @@ import org.eclipse.xtext.validation.Check; import com.google.inject.Inject; -import tools.refinery.language.ProblemUtil; import tools.refinery.language.model.problem.Node; import tools.refinery.language.model.problem.Problem; import tools.refinery.language.model.problem.ProblemPackage; import tools.refinery.language.model.problem.Variable; import tools.refinery.language.model.problem.VariableOrNodeArgument; import tools.refinery.language.resource.ReferenceCounter; +import tools.refinery.language.utils.ProblemUtil; /** * This class contains custom validation rules. diff --git a/subprojects/language/src/main/resources/tools/refinery/language/builtin.problem b/subprojects/language/src/main/resources/tools/refinery/language/builtin.problem index e39ff1a3..2f7c667a 100644 --- a/subprojects/language/src/main/resources/tools/refinery/language/builtin.problem +++ b/subprojects/language/src/main/resources/tools/refinery/language/builtin.problem @@ -14,10 +14,10 @@ enum bool { true, false } -class real extends data. - class int extends data. +class real extends data. + class string extends data. pred contained(node node). diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java new file mode 100644 index 00000000..e2e3218c --- /dev/null +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java @@ -0,0 +1,276 @@ +package tools.refinery.language.tests.utils; + +import com.google.inject.Inject; +import org.eclipse.xtext.testing.InjectWith; +import org.eclipse.xtext.testing.extensions.InjectionExtension; +import org.hamcrest.Matcher; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.extension.ExtendWith; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.Arguments; +import org.junit.jupiter.params.provider.MethodSource; +import tools.refinery.language.model.problem.*; +import tools.refinery.language.model.tests.utils.ProblemParseHelper; +import tools.refinery.language.tests.ProblemInjectorProvider; +import tools.refinery.language.utils.ProblemDesugarer; + +import java.util.stream.Stream; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.*; +import static org.junit.jupiter.api.Assertions.assertDoesNotThrow; + +@ExtendWith(InjectionExtension.class) +@InjectWith(ProblemInjectorProvider.class) +class SymbolCollectorTest { + @Inject + private ProblemParseHelper parseHelper; + + @Inject + private ProblemDesugarer desugarer; + + @Test + void implicitNodeTest() { + var problem = parseHelper.parse(""" + exists(a). + """); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + var node = problem.node("a"); + assertThat(collectedSymbols.nodes(), hasKey(node)); + assertThat(collectedSymbols.nodes().get(node).individual(), is(false)); + } + + @Test + void individualNodeTest() { + var problem = parseHelper.parse(""" + indiv a. + """); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + var node = problem.individualNode("a"); + assertThat(collectedSymbols.nodes(), hasKey(node)); + assertThat(collectedSymbols.nodes().get(node).individual(), is(true)); + } + + @Test + void classTest() { + var problem = parseHelper.parse(""" + class Foo. + """); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + var classDeclaration = problem.findClass("Foo").get(); + assertThat(collectedSymbols.relations(), hasKey(classDeclaration)); + var classInfo = collectedSymbols.relations().get(classDeclaration); + assertThat(classInfo.parameters(), hasSize(1)); + assertThat(classInfo.kind(), is(PredicateKind.CONTAINED)); + assertThat(classInfo.hasDefinition(), is(false)); + var newNode = classDeclaration.getNewNode(); + assertThat(collectedSymbols.nodes(), hasKey(newNode)); + assertThat(collectedSymbols.nodes().get(newNode).individual(), is(false)); + assertThat(classInfo.assertions(), assertsNode(newNode, LogicValue.TRUE)); + assertThat(collectedSymbols.relations().get(problem.builtinSymbols().exists()).assertions(), + assertsNode(newNode, LogicValue.UNKNOWN)); + assertThat(collectedSymbols.relations().get(problem.builtinSymbols().equals()).assertions(), + assertsNode(newNode, LogicValue.UNKNOWN)); + } + + @Test + void abstractClassTest() { + var problem = parseHelper.parse(""" + abstract class Foo. + """); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + assertThat(collectedSymbols.relations().get(problem.findClass("Foo").get()).assertions(), hasSize(0)); + } + + @Test + void referenceTest() { + var problem = parseHelper.parse(""" + class Foo { + Foo[] bar opposite quux + Foo quux opposite bar + } + """); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + var fooClass = problem.findClass("Foo"); + var barReference = fooClass.reference("bar"); + var barInfo = collectedSymbols.relations().get(barReference); + var quuxReference = fooClass.reference("quux"); + var quuxInfo = collectedSymbols.relations().get(quuxReference); + assertThat(barInfo.kind(), is(PredicateKind.DEFAULT)); + assertThat(barInfo.opposite(), is(quuxReference)); + assertThat(barInfo.multiplicity(), is(instanceOf(UnboundedMultiplicity.class))); + assertThat(barInfo.hasDefinition(), is(false)); + assertThat(quuxInfo.kind(), is(PredicateKind.DEFAULT)); + assertThat(quuxInfo.opposite(), is(barReference)); + assertThat(quuxInfo.multiplicity(), is(instanceOf(ExactMultiplicity.class))); + assertThat(quuxInfo.multiplicity(), hasProperty("exactValue", is(1))); + assertThat(quuxInfo.hasDefinition(), is(false)); + } + + @Test + void containmentReferenceTest() { + var problem = parseHelper.parse(""" + class Foo { + contains Foo[] bar + } + """); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + assertThat(collectedSymbols.relations().get(problem.findClass("Foo").reference("bar")).kind(), + is(PredicateKind.CONTAINMENT)); + } + + @Test + void dataReferenceTest() { + var problem = parseHelper.parse(""" + class Foo { + int bar + } + """); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + assertThat(collectedSymbols.relations().get(problem.findClass("Foo").reference("bar")).kind(), + is(PredicateKind.CONTAINMENT)); + } + + @Test + void enumTest() { + var problem = parseHelper.parse(""" + enum Foo { + bar, quux + } + """); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + var enumDeclaration = problem.findEnum("Foo"); + var enumInfo = collectedSymbols.relations().get(enumDeclaration.get()); + assertThat(enumInfo.kind(), is(PredicateKind.DEFAULT)); + assertThat(enumInfo.assertions(), assertsNode(enumDeclaration.literal("bar"), LogicValue.TRUE)); + assertThat(enumInfo.assertions(), assertsNode(enumDeclaration.literal("quux"), LogicValue.TRUE)); + } + + @ParameterizedTest + @MethodSource + void predicateTest(String keyword, PredicateKind kind) { + var problem = parseHelper.parse(keyword + " foo(node x) <-> domain(x); data(x)."); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + var predicateInfo = collectedSymbols.relations().get(problem.pred("foo").get()); + assertThat(predicateInfo.kind(), is(kind)); + assertThat(predicateInfo.parameters(), hasSize(1)); + assertThat(predicateInfo.bodies(), hasSize(2)); + assertThat(predicateInfo.hasDefinition(), is(true)); + } + + static Stream predicateTest() { + return Stream.of(Arguments.of("pred", PredicateKind.DEFAULT), Arguments.of("error", PredicateKind.ERROR), + Arguments.of("contained", PredicateKind.CONTAINED), Arguments.of("containment", + PredicateKind.CONTAINMENT)); + } + + @ParameterizedTest + @MethodSource("logicValues") + void assertionTest(String keyword, LogicValue value) { + var problem = parseHelper.parse(""" + pred foo(node x). + foo(a): %s. + """.formatted(keyword)); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).assertions(), + assertsNode(problem.node("a"), value)); + } + + @ParameterizedTest + @MethodSource("logicValues") + void defaultAssertionTest(String keyword, LogicValue value) { + var problem = parseHelper.parse(""" + pred foo(node x). + default foo(a): %s. + """.formatted(keyword)); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).defaultAssertions(), + assertsNode(problem.node("a"), value)); + } + + static Stream logicValues() { + return Stream.of(Arguments.of("true", LogicValue.TRUE), Arguments.of("false", LogicValue.FALSE), + Arguments.of("unknown", LogicValue.UNKNOWN), Arguments.of("error", LogicValue.ERROR)); + } + + @Test + void invalidAssertionArityTest() { + var problem = parseHelper.parse(""" + pred foo(node x). + foo(a, b). + """); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).assertions(), hasSize(0)); + } + + @ParameterizedTest + @MethodSource("valueTypes") + void nodeValueAssertionTest(String value, String typeName) { + var problem = parseHelper.parse("a: %s.".formatted(value)); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + var node = problem.node("a"); + var nodeInfo = collectedSymbols.nodes().get(node); + assertThat(nodeInfo.individual(), is(false)); + assertThat(nodeInfo.valueAssertions(), hasSize(1)); + assertThat(collectedSymbols.relations().get(problem.builtin().findClass(typeName).get()).assertions(), + assertsNode(node, LogicValue.TRUE)); + } + + @ParameterizedTest + @MethodSource("valueTypes") + void constantInAssertionTest(String value, String typeName) { + var problem = parseHelper.parse(""" + containment pred foo(node x, data y). + foo(a, %s). + """.formatted(value)); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + var node = problem.assertion(0).arg(1).constantNode(); + var nodeInfo = collectedSymbols.nodes().get(node); + assertThat(nodeInfo.individual(), is(false)); + assertThat(nodeInfo.valueAssertions(), hasSize(1)); + assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).assertions(), assertsNode(node, + LogicValue.TRUE)); + assertThat(collectedSymbols.relations().get(problem.builtin().findClass(typeName).get()).assertions(), + assertsNode(node, LogicValue.TRUE)); + } + + @ParameterizedTest + @MethodSource("valueTypes") + void constantInUnknownAssertionTest(String value, String typeName) { + var problem = parseHelper.parse(""" + containment pred foo(node x, data y). + foo(a, %s): unknown. + """.formatted(value)); + var collectedSymbols = desugarer.collectSymbols(problem.get()); + var node = problem.assertion(0).arg(1).constantNode(); + var nodeInfo = collectedSymbols.nodes().get(node); + assertThat(nodeInfo.individual(), is(false)); + assertThat(nodeInfo.valueAssertions(), hasSize(1)); + assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).assertions(), assertsNode(node, + LogicValue.UNKNOWN)); + assertThat(collectedSymbols.relations().get(problem.builtin().findClass(typeName).get()).assertions(), + assertsNode(node, LogicValue.TRUE)); + assertThat(collectedSymbols.relations().get(problem.builtinSymbols().exists()).assertions(), assertsNode(node, + LogicValue.UNKNOWN)); + } + + @Test + void invalidProblemTest() { + var problem = parseHelper.parse(""" + class Foo { + bar[] opposite quux + Foo quux opposite bar + } + """).get(); + assertDoesNotThrow(() -> desugarer.collectSymbols(problem)); + } + + static Stream valueTypes() { + return Stream.of(Arguments.of("3", "int"), Arguments.of("3.14", "real"), Arguments.of("\"foo\"", "string")); + } + + private static Matcher> assertsNode(Node node, LogicValue value) { + return hasItem(allOf(hasProperty("arguments", hasItem(hasProperty("node", is(node)))), hasProperty("value", + is(value)))); + } +} diff --git a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedArgument.java b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedArgument.java index 61492184..ad57a438 100644 --- a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedArgument.java +++ b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedArgument.java @@ -1,10 +1,6 @@ package tools.refinery.language.model.tests.utils; -import tools.refinery.language.model.problem.Argument; -import tools.refinery.language.model.problem.Node; -import tools.refinery.language.model.problem.Variable; -import tools.refinery.language.model.problem.VariableOrNode; -import tools.refinery.language.model.problem.VariableOrNodeArgument; +import tools.refinery.language.model.problem.*; public record WrappedArgument(Argument argument) { public Argument get() { @@ -18,7 +14,7 @@ public record WrappedArgument(Argument argument) { public Variable variable() { return (Variable) variableOrNode(); } - + public Node node() { return (Node) variableOrNode(); } diff --git a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAssertionArgument.java b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAssertionArgument.java index 77ad3746..b8b3a7de 100644 --- a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAssertionArgument.java +++ b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAssertionArgument.java @@ -1,6 +1,7 @@ package tools.refinery.language.model.tests.utils; import tools.refinery.language.model.problem.AssertionArgument; +import tools.refinery.language.model.problem.ConstantAssertionArgument; import tools.refinery.language.model.problem.Node; import tools.refinery.language.model.problem.NodeAssertionArgument; @@ -8,8 +9,12 @@ public record WrappedAssertionArgument(AssertionArgument assertionArgument) { public AssertionArgument get() { return assertionArgument; } - + public Node node() { return ((NodeAssertionArgument) assertionArgument).getNode(); } + + public Node constantNode() { + return ((ConstantAssertionArgument) assertionArgument).getNode(); + } } diff --git a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedProblem.java b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedProblem.java index 2bedb4a6..aef96b5b 100644 --- a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedProblem.java +++ b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedProblem.java @@ -6,7 +6,6 @@ import java.util.stream.Stream; import org.eclipse.emf.ecore.resource.Resource.Diagnostic; import org.eclipse.emf.ecore.util.EcoreUtil; -import tools.refinery.language.ProblemUtil; import tools.refinery.language.model.problem.Assertion; import tools.refinery.language.model.problem.ClassDeclaration; import tools.refinery.language.model.problem.EnumDeclaration; @@ -18,6 +17,8 @@ import tools.refinery.language.model.problem.PredicateDefinition; import tools.refinery.language.model.problem.Problem; import tools.refinery.language.model.problem.RuleDefinition; import tools.refinery.language.model.problem.Statement; +import tools.refinery.language.utils.BuiltinSymbols; +import tools.refinery.language.utils.ProblemDesugarer; public record WrappedProblem(Problem problem) { public Problem get() { @@ -30,11 +31,15 @@ public record WrappedProblem(Problem problem) { } public WrappedProblem builtin() { - return new WrappedProblem(ProblemUtil.getBuiltInLibrary(problem).get()); + return new WrappedProblem(new ProblemDesugarer().getBuiltinProblem(problem).orElseThrow()); + } + + public BuiltinSymbols builtinSymbols() { + return new ProblemDesugarer().getBuiltinSymbols(problem).orElseThrow(); } public List nodeNames() { - return problem.getNodes().stream().map(node -> node.getName()).toList(); + return problem.getNodes().stream().map(Node::getName).toList(); } public WrappedPredicateDefinition pred(String name) { @@ -80,6 +85,6 @@ public record WrappedProblem(Problem problem) { } private T nthStatementOfType(Class type, int n) { - return statementsOfType(type).skip(n).findFirst().get(); + return statementsOfType(type).skip(n).findFirst().orElseThrow(); } } -- cgit v1.2.3-54-g00ecf