Merge pull request souffle-lang#1712 from darth-tytus/negation

Relax type constraints involving negation.

src/ast/transform/TypeChecker.cpp

@@ -38,6 +38,7 @@
 #include <map>
 #include <sstream>
 #include <string>
+#include <unordered_set>
 #include <utility>
 #include <vector>
 namespace souffle::ast::transform {
@@ -82,8 +83,15 @@ class TypeCheckerImpl : Visitor<void> {
     const FunctorAnalysis& functorAnalysis = *tu.getAnalysis<FunctorAnalysis>();
     const Program& program = tu.getProgram();
 
+    std::unordered_set<const Atom*> negatedAtoms;
+
+    /** Collect negated atoms */
+    void visitNegation(const Negation& neg) override;
+
+    /* Type checks */
+    /** Check if declared types of the relation match deduced types. */
     void visitAtom(const Atom& atom) override;
-    void visitVariable(const ast::Variable& var) override;
+    void visitVariable(const Variable& var) override;
     void visitStringConstant(const StringConstant& constant) override;
     void visitNumericConstant(const NumericConstant& constant) override;
     void visitNilConstant(const NilConstant& constant) override;
@@ -284,14 +292,20 @@ void TypeCheckerImpl::visitAtom(const Atom& atom) {
 
     for (size_t i = 0; i < attributes.size(); ++i) {
         auto& typeName = attributes[i]->getTypeName();
-        if (typeEnv.isType(typeName)) {
-            auto argTypes = typeAnalysis.getTypes(arguments[i]);
-            auto& attributeType = typeEnv.getType(typeName);
+        if (!typeEnv.isType(typeName)) {
+            continue;
+        }
 
-            if (argTypes.isAll() || argTypes.empty()) {
-                continue;  // This will be reported later.
-            }
+        auto argTypes = typeAnalysis.getTypes(arguments[i]);
+        auto& attributeType = typeEnv.getType(typeName);
 
+        if (argTypes.isAll() || argTypes.empty()) {
+            continue;  // This will be reported later.
+        }
+
+        // We consider two cases: negated and not negated atoms.
+        // Negated atom have to agree in kind, non-negated atom need to follow source/sink rules.
+        if (negatedAtoms.count(&atom) == 0) {
             // Attribute and argument type agree if, argument type is a subtype of declared type
             // or is of the appropriate constant type or the (constant) record type.
             bool validAttribute = all_of(argTypes, [&attributeType](const analysis::Type& type) {
@@ -300,6 +314,7 @@ void TypeCheckerImpl::visitAtom(const Atom& atom) {
                 if (isA<ConstantType>(type)) return true;
                 return isA<analysis::RecordType>(type) && !isA<analysis::SubsetType>(type);
             });
+
             if (!validAttribute && !Global::config().has("legacy")) {
                 auto primaryDiagnostic =
                         DiagnosticMessage("Atom's argument type is not a subtype of its declared type",
@@ -312,6 +327,26 @@ void TypeCheckerImpl::visitAtom(const Atom& atom) {
                 report.addDiagnostic(Diagnostic(Diagnostic::Type::ERROR, std::move(primaryDiagnostic),
                         {std::move(declaredTypeInfo)}));
             }
+        } else {  // negation case.
+            // Declared attribute and deduced type agree if:
+            // They are the same type, or
+            // They are derived from the same constant type.
+            bool validAttribute = all_of(argTypes, [&](const analysis::Type& type) {
+                return type == attributeType || any_of(typeEnv.getConstantTypes(), [&](auto& constantType) {
+                    return isSubtypeOf(attributeType, constantType) && isSubtypeOf(type, constantType);
+                });
+            });
+
+            if (!validAttribute) {
+                auto primaryDiagnostic =
+                        DiagnosticMessage("The kind of atom's argument doesn't match the declared type kind",
+                                arguments[i]->getSrcLoc());
+                auto declaredTypeInfo =
+                        DiagnosticMessage(tfm::format("The argument's declared type is %s", typeName),
+                                attributes[i]->getSrcLoc());
+                report.addDiagnostic(Diagnostic(Diagnostic::Type::ERROR, std::move(primaryDiagnostic),
+                        {std::move(declaredTypeInfo)}));
+            }
         }
     }
 }
@@ -564,4 +599,8 @@ void TypeCheckerImpl::visitAggregator(const Aggregator& aggregator) {
     }
 }
 
+void TypeCheckerImpl::visitNegation(const Negation& neg) {
+    negatedAtoms.insert(neg.getAtom());
+}
+
 }  // namespace souffle::ast::transform

tests/semantic.at

@@ -238,6 +238,7 @@ NEGATIVE_TEST([type_system12],[semantic])
 NEGATIVE_TEST([type_system13],[semantic])
 NEGATIVE_TEST([type_system14],[semantic])
 NEGATIVE_TEST([type_system15],[semantic])
+POSITIVE_TEST([type_system_negation],[semantic])
 NEGATIVE_TEST([type_system_sum_types],[semantic])
 NEGATIVE_TEST([type_system_sum_types2],[semantic])
 POSITIVE_TEST([type_system_records],[semantic])

tests/semantic/rule_typecompat/rule_typecompat.err

@@ -121,33 +121,9 @@ F(x,y) :- F(x,v), F(w,y), A(w), D(v).
 Warning: Variable w only occurs once in file rule_typecompat.dl at line 52
 F(x,y) :- F(x,v), F(w,y), !H(v), !D(v).
 --------------------^-------------------
-Error: Atom's argument type is not a subtype of its declared type in file rule_typecompat.dl at line 52
-F(x,y) :- F(x,v), F(w,y), !H(v), !D(v).
-------------------------------------^---
-The argument's declared type is R in file rule_typecompat.dl at line 9
-.decl D (r:R)
------------^--
 Warning: Variable v only occurs once in file rule_typecompat.dl at line 53
 F(x,y) :- F(x,v), F(w,y), !H(w), !D(w).
 --------------^-------------------------
-Error: Atom's argument type is not a subtype of its declared type in file rule_typecompat.dl at line 53
-F(x,y) :- F(x,v), F(w,y), !H(w), !D(w).
------------------------------^----------
-The argument's declared type is T in file rule_typecompat.dl at line 5
-.decl H (t:T)
------------^--
-Error: Atom's argument type is not a subtype of its declared type in file rule_typecompat.dl at line 54
-F(x,y) :- F(x,v), F(w,y), !H(w), !D(v).
------------------------------^----------
-The argument's declared type is T in file rule_typecompat.dl at line 5
-.decl H (t:T)
------------^--
-Error: Atom's argument type is not a subtype of its declared type in file rule_typecompat.dl at line 54
-F(x,y) :- F(x,v), F(w,y), !H(w), !D(v).
-------------------------------------^---
-The argument's declared type is R in file rule_typecompat.dl at line 9
-.decl D (r:R)
------------^--
 Error: Unable to deduce type for variable x in file rule_typecompat.dl at line 57
 F(x,y) :- F(x,y),  x > y.
 --^-----------------------
@@ -190,4 +166,4 @@ F(x,y) :- F(x,y),  t < x.
 Warning: Variable t only occurs once in file rule_typecompat.dl at line 63
 F(x,y) :- F(x,y),  t < x.
 -------------------^------
-40 errors generated, evaluation aborted
+36 errors generated, evaluation aborted

tests/semantic/type_system12/type_system12.err

@@ -10,10 +10,4 @@ C(x) :- !A(x), B(x).               // Error
 The argument's declared type is S1 in file type_system12.dl at line 37
 .decl C(x : S1)
 ------------^---
-Error: Atom's argument type is not a subtype of its declared type in file type_system12.dl at line 39
-C(x) :- !A(x), B(x).               // Error
------------^--------------------------------
-The argument's declared type is S2 in file type_system12.dl at line 23
-.decl A(x : S2)
-------------^---
-3 errors generated, evaluation aborted
+2 errors generated, evaluation aborted

tests/semantic/type_system_negation/type_system_negation.dl

@@ -0,0 +1,69 @@
+// 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
+
+//
+// Type System Negation
+// Created for issues #1464 & #1560
+//
+
+
+
+////////////////////////////
+// #1464 by @nevillegrech //
+////////////////////////////
+
+.type Variable <: symbol
+.type StackIndex <: symbol
+.type VariableOrStackIndex = Variable | StackIndex
+
+.decl Aa(a: VariableOrStackIndex)
+.decl Bb(a: Variable)
+.decl Cc(a: VariableOrStackIndex)
+
+
+Cc(a) :- !Bb(a), Aa(a).
+
+
+////////////////////////////////
+// #1560 by @langston-barrett //
+////////////////////////////////
+.type A <: symbol
+.type B <: symbol
+.type U = A | B
+
+.decl b(x:B)
+.decl u(x:U)
+.decl r(x:U, y:U)
+.decl s(x:B, y:number)
+
+// Get rid of "no rules/facts defined" warning
+b("a").
+r("a1", "b2").
+s("b2", 1).
+
+u(x) :- b(x).
+u(x) :- s(x, _).
+u(x) :- r(x, y), s(y, _).
+u(x) :- r(x, y), !s(y, _).
+
+
+////////////////////////
+// #1560 by @b-scholz //
+////////////////////////
+
+.type even <: number  // even numbers
+.type odd <: number   // odd numbers
+
+.decl e(n:number)
+e(0).
+e(x + 2) :- e(x), x < 100.
+
+.decl o(n:number)
+o(1).
+o(x + 2) :- o(x), x < 100.
+
+.decl my_even(n:number)
+my_even(x) :- e(x), !o(x), x <= 10.

tests/semantic/type_system_negation/type_system_negation.err

@@ -0,0 +1,6 @@
+Warning: No rules/facts defined for relation Aa in file type_system_negation.dl at line 22
+.decl Aa(a: VariableOrStackIndex)
+------^---------------------------
+Warning: No rules/facts defined for relation Bb in file type_system_negation.dl at line 23
+.decl Bb(a: Variable)
+------^---------------

tests/semantic/union_types/union_types.dl

@@ -32,8 +32,7 @@ F(X) :- A(X). // no error
 F(X) :- B(X). // no error
 G(X) :- E(X). // error
 
-// F(X) is the only source, thus type(X) = all, but we have two sinks in form of negation that require a more specific subtype, thus we have error.
-E(X) :- F(X), !A(X), !B(X). // error.
+E(X) :- F(X), !A(X), !B(X). // no error
 E(X) :- F(X), A(X), B(X). // error
 
 C(X) :- D(X), !A(X). // error

tests/semantic/union_types/union_types.err

@@ -7,37 +7,25 @@ G(X) :- E(X). // error
 The argument's declared type is one in file union_types.dl at line 20
 .decl G (i:one)
 -----------^----
-Error: Atom's argument type is not a subtype of its declared type in file union_types.dl at line 36
-E(X) :- F(X), !A(X), !B(X). // error.
------------------^--------------------
-The argument's declared type is one in file union_types.dl at line 15
-.decl A (i:one)
------------^----
-Error: Atom's argument type is not a subtype of its declared type in file union_types.dl at line 36
-E(X) :- F(X), !A(X), !B(X). // error.
-------------------------^-------------
-The argument's declared type is two in file union_types.dl at line 16
-.decl B (i:two)
------------^----
-Error: Unable to deduce type for variable X in file union_types.dl at line 37
+Error: Unable to deduce type for variable X in file union_types.dl at line 36
 E(X) :- F(X), A(X), B(X). // error
 --^--------------------------------
-Error: Unable to deduce type for variable X in file union_types.dl at line 37
+Error: Unable to deduce type for variable X in file union_types.dl at line 36
 E(X) :- F(X), A(X), B(X). // error
 ----------^------------------------
-Error: Unable to deduce type for variable X in file union_types.dl at line 37
+Error: Unable to deduce type for variable X in file union_types.dl at line 36
 E(X) :- F(X), A(X), B(X). // error
 ----------------^------------------
-Error: Unable to deduce type for variable X in file union_types.dl at line 37
+Error: Unable to deduce type for variable X in file union_types.dl at line 36
 E(X) :- F(X), A(X), B(X). // error
 ----------------------^------------
-Error: Unable to deduce type for variable X in file union_types.dl at line 39
+Error: Unable to deduce type for variable X in file union_types.dl at line 38
 C(X) :- D(X), !A(X). // error
 --^---------------------------
-Error: Unable to deduce type for variable X in file union_types.dl at line 39
+Error: Unable to deduce type for variable X in file union_types.dl at line 38
 C(X) :- D(X), !A(X). // error
 ----------^-------------------
-Error: Unable to deduce type for variable X in file union_types.dl at line 39
+Error: Unable to deduce type for variable X in file union_types.dl at line 38
 C(X) :- D(X), !A(X). // error
 -----------------^------------
-10 errors generated, evaluation aborted
+8 errors generated, evaluation aborted