Merge pull request #1558 from darth-tytus/bugTypesComponents

Type system fix

src/ast/TypeSystem.cpp

@@ -367,4 +367,8 @@ std::optional<TypeAttribute> getTypeAttribute(const TypeSet& type) {
     return {};
 }
 
+bool areEquivalentTypes(const Type& a, const Type& b) {
+    return isSubtypeOf(a, b) && isSubtypeOf(b, a);
+}
+
 }  // end of namespace souffle

src/ast/TypeSystem.h

@@ -365,11 +365,7 @@ struct TypeSet {
  */
 class TypeEnvironment {
 public:
-    TypeEnvironment()
-            : constantTypes(initializeConstantTypes()),
-              constantNumericTypes(TypeSet(getType("__numberConstant"), getType("__unsignedConstant"),
-                      getType("__floatConstant"))),
-              primitiveTypes(initializePrimitiveTypes()){};
+    TypeEnvironment() = default;
 
     TypeEnvironment(const TypeEnvironment&) = delete;
 
@@ -446,10 +442,11 @@ class TypeEnvironment {
     /** The list of covered types. */
     std::map<AstQualifiedName, std::unique_ptr<Type>> types;
 
-    const TypeSet constantTypes;
-    const TypeSet constantNumericTypes;
+    const TypeSet constantTypes = initializeConstantTypes();
+    const TypeSet constantNumericTypes =
+            TypeSet(getType("__numberConstant"), getType("__unsignedConstant"), getType("__floatConstant"));
 
-    const TypeSet primitiveTypes;
+    const TypeSet primitiveTypes = initializePrimitiveTypes();
 };
 
 // ---------------------------------------------------------------
@@ -514,4 +511,10 @@ TypeSet getGreatestCommonSubtypes(const Types&... types) {
  */
 bool haveCommonSupertype(const Type& a, const Type& b);
 
+/**
+ * Determine if two types are equivalent.
+ * That is, check if a <: b and b <: a
+ */
+bool areEquivalentTypes(const Type& a, const Type& b);
+
 }  // end namespace souffle

src/ast/transform/SemanticChecker.cpp

@@ -1437,24 +1437,34 @@ void TypeChecker::visitBinaryConstraint(const AstBinaryConstraint& constraint) {
     auto op = constraint.getOperator();
     auto left = constraint.getLHS();
     auto right = constraint.getRHS();
-    auto opRamTypes = getBinaryConstraintTypes(op);
+    auto opTypesAttrs = getBinaryConstraintTypes(op);
+
+    auto leftTypes = typeAnalysis.getTypes(left);
+    auto rightTypes = typeAnalysis.getTypes(right);
+
     // Skip checks if either side is `Bottom` b/c it just adds noise.
     // The unable-to-deduce-type checker will point out the issue.
-    if (typeAnalysis.getTypes(left).empty() || typeAnalysis.getTypes(right).empty()) return;
+    if (leftTypes.empty() || rightTypes.empty() || leftTypes.isAll() || rightTypes.isAll()) return;
+
+    assert((leftTypes.size() == 1) && (rightTypes.size() == 1));
+
+    // Extract types from singleton sets.
+    auto& leftType = *typeAnalysis.getTypes(left).begin();
+    auto& rightType = *typeAnalysis.getTypes(right).begin();
 
     // give them a slightly nicer error
-    if (isOrderedBinaryConstraintOp(op) && typeAnalysis.getTypes(left) != typeAnalysis.getTypes(right)) {
+    if (isOrderedBinaryConstraintOp(op) && !areEquivalentTypes(leftType, rightType)) {
         report.addError("Cannot compare different types", constraint.getSrcLoc());
     } else {
         auto checkTyAttr = [&](AstArgument const& side) {
-            auto opMatchesType = any_of(opRamTypes,
-                    [&](auto& ramType) { return isOfKind(typeAnalysis.getTypes(&side), ramType); });
+            auto opMatchesType = any_of(opTypesAttrs,
+                    [&](auto& typeAttr) { return isOfKind(typeAnalysis.getTypes(&side), typeAttr); });
 
             if (!opMatchesType) {
                 std::stringstream ss;
                 ss << "Constraint requires an operand of type "
-                   << join(opRamTypes, " or ", [&](auto& out, auto& ramTy) {
-                          switch (ramTy) {
+                   << join(opTypesAttrs, " or ", [&](auto& out, auto& typeAttr) {
+                          switch (typeAttr) {
                               case TypeAttribute::Signed: out << "`number`"; break;
                               case TypeAttribute::Symbol: out << "`symbol`"; break;
                               case TypeAttribute::Unsigned: out << "`unsigned`"; break;

src/tests/type_system_test.cpp

@@ -255,4 +255,13 @@ TEST(TypeSystem, RecordSubsets) {
     EXPECT_EQ("{A}", toString(getGreatestCommonSubtypes(A, R)));
 }
 
+TEST(TypeSystem, EquivTypes) {
+    TypeEnvironment env;
+
+    auto& A = env.createType<SubsetType>("A", env.getType("number"));
+    auto& U = env.createType<UnionType>("U", toVector(dynamic_cast<const Type*>(&A)));
+
+    EXPECT_TRUE(areEquivalentTypes(A, U));
+}
+
 }  // namespace souffle::test

tests/semantic.at

@@ -231,6 +231,7 @@ NEGATIVE_TEST([type_system14],[semantic])
 POSITIVE_TEST([type_system_records],[semantic])
 NEGATIVE_TEST([type_system_records2],[semantic])
 NEGATIVE_TEST([type_udef],[semantic])
+POSITIVE_TEST([types_components], [semantic])
 POSITIVE_TEST([underscore2],[semantic])
 POSITIVE_TEST([underscore3],[semantic])
 POSITIVE_TEST([underscore4],[semantic])

tests/semantic/type_system_records2/type_system_records2.err

@@ -1,39 +1,21 @@
 Error: Ambiguous record in file type_system_records2.dl at line 14
 A(1) :- [1,2] = [1].
 --------^------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 14
-A(1) :- [1,2] = [1].
---------^------------
 Error: Ambiguous record in file type_system_records2.dl at line 14
 A(1) :- [1,2] = [1].
 ----------------^----
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 14
-A(1) :- [1,2] = [1].
-----------------^----
 Error: Ambiguous record in file type_system_records2.dl at line 15
 A(2) :- [1,2] != [1].
 --------^-------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 15
-A(2) :- [1,2] != [1].
---------^-------------
 Error: Ambiguous record in file type_system_records2.dl at line 15
 A(2) :- [1,2] != [1].
 -----------------^----
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 15
-A(2) :- [1,2] != [1].
------------------^----
 Error: Ambiguous record in file type_system_records2.dl at line 16
 A(3) :- [1,2] = [1, 2, "3"].
 --------^--------------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 16
-A(3) :- [1,2] = [1, 2, "3"].
---------^--------------------
 Error: Ambiguous record in file type_system_records2.dl at line 16
 A(3) :- [1,2] = [1, 2, "3"].
 ----------------^------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 16
-A(3) :- [1,2] = [1, 2, "3"].
-----------------^------------
 Error: Unsigned constant (type mismatch) in file type_system_records2.dl at line 17
 A(4) :- [1u,2] != [2.0, 3].
 ---------^------------------
@@ -43,28 +25,16 @@ A(4) :- [1u,2] != [2.0, 3].
 Error: Ambiguous record in file type_system_records2.dl at line 18
 A(5) :- a = [1, 2], a = [b], b = [].
 ------------^------------------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 18
-A(5) :- a = [1, 2], a = [b], b = [].
-------------^------------------------
 Error: Ambiguous record in file type_system_records2.dl at line 18
 A(5) :- a = [1, 2], a = [b], b = [].
 ------------------------^------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 18
-A(5) :- a = [1, 2], a = [b], b = [].
-------------------------^------------
 Error: Ambiguous record in file type_system_records2.dl at line 18
 A(5) :- a = [1, 2], a = [b], b = [].
 ---------------------------------^---
 Error: Ambiguous record in file type_system_records2.dl at line 19
 A(6) :- [1] != _.
 --------^---------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 19
-A(6) :- [1] != _.
---------^---------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 19
-A(6) :- [1] != _.
----------------^--
 Error: Underscore in binary relation in file type_system_records2.dl at line 19
 A(6) :- [1] != _.
 ---------------^--
-23 errors generated, evaluation aborted
+13 errors generated, evaluation aborted

tests/semantic/types_components/types_components.dl

@@ -0,0 +1,39 @@
+// Souffle - A Datalog Compiler
+// Copyright (c) 2020, The Souffle Developers. All rights reserved
+// Licensed under the Universal Permissive License v 1.0 as shown at:
+// - https://opensource.org/licenses/UPL
+// - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+//
+// Types components
+// Check if types are deduced correctly, created for #1520
+//
+
+
+// aeflores' example
+.type BasicBlock <: symbol
+
+.comp Graph<N> {
+      .type TNode = N
+      .decl edge(a:TNode,b:TNode)
+}
+
+.init cfg = Graph<BasicBlock>
+
+.decl reach(a:BasicBlock, b:BasicBlock, c:BasicBlock)
+reach(origin, mid, end) :- reach(origin, z, end),
+                           cfg.edge(z, mid),
+                           mid != end.
+
+
+// azreika's example
+.type TypeOne = symbol
+.type TypeTwo = TypeOne
+
+.decl A(X:TypeOne)
+A("hello").
+
+.decl B(X:TypeTwo)
+B(X) :- A(Y), B(X), X != Y.
+
+.output B()

tests/semantic/types_components/types_components.err

@@ -0,0 +1,3 @@
+Warning: No rules/facts defined for relation cfg.edge in file types_components.dl at line 18
+      .decl edge(a:TNode,b:TNode)
+------------^---------------------