diff --git a/src/ast/transform/TypeChecker.cpp b/src/ast/transform/TypeChecker.cpp index 8785248090e..d594b76d359 100644 --- a/src/ast/transform/TypeChecker.cpp +++ b/src/ast/transform/TypeChecker.cpp @@ -38,6 +38,7 @@ #include #include #include +#include #include #include namespace souffle::ast::transform { @@ -82,8 +83,15 @@ class TypeCheckerImpl : Visitor { const FunctorAnalysis& functorAnalysis = *tu.getAnalysis(); const Program& program = tu.getProgram(); + std::unordered_set 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(type)) return true; return isA(type) && !isA(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 diff --git a/tests/semantic.at b/tests/semantic.at index d51bbdb232d..55fa0ea28c7 100644 --- a/tests/semantic.at +++ b/tests/semantic.at @@ -239,6 +239,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]) diff --git a/tests/semantic/rule_typecompat/rule_typecompat.err b/tests/semantic/rule_typecompat/rule_typecompat.err index a6f0c015ecd..acf0def19c2 100644 --- a/tests/semantic/rule_typecompat/rule_typecompat.err +++ b/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 diff --git a/tests/semantic/type_system12/type_system12.err b/tests/semantic/type_system12/type_system12.err index 576f195e5ad..c30268be383 100644 --- a/tests/semantic/type_system12/type_system12.err +++ b/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 diff --git a/tests/semantic/type_system_negation/type_system_negation.dl b/tests/semantic/type_system_negation/type_system_negation.dl new file mode 100644 index 00000000000..16e590b43ee --- /dev/null +++ b/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 +// - /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. diff --git a/tests/semantic/type_system_negation/type_system_negation.err b/tests/semantic/type_system_negation/type_system_negation.err new file mode 100644 index 00000000000..ba61f7de03b --- /dev/null +++ b/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) +------^--------------- diff --git a/tests/semantic/type_system_negation/type_system_negation.out b/tests/semantic/type_system_negation/type_system_negation.out new file mode 100644 index 00000000000..e69de29bb2d diff --git a/tests/semantic/union_types/union_types.dl b/tests/semantic/union_types/union_types.dl index 1b0f76e051f..e0d62ea6054 100644 --- a/tests/semantic/union_types/union_types.dl +++ b/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 diff --git a/tests/semantic/union_types/union_types.err b/tests/semantic/union_types/union_types.err index 528dda8ea14..2927484d170 100644 --- a/tests/semantic/union_types/union_types.err +++ b/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