F: Add check for nonsensical emptyset uses

This commit is contained in:
Ivan 2024-09-25 22:43:35 +03:00
parent 6860706e7a
commit daff622090
6 changed files with 49 additions and 15 deletions

View File

@ -46,6 +46,7 @@ enum class SemanticEID : uint32_t {
invalidBinding = 0x8814, // Количество переменных в кортеже не соответствует размерности декартова произведения invalidBinding = 0x8814, // Количество переменных в кортеже не соответствует размерности декартова произведения
localOutOfScope = 0x8815, // Использование имени вне области видимости localOutOfScope = 0x8815, // Использование имени вне области видимости
invalidElementPredicate = 0x8816, // Несоответствие типов для проверки принадлежности invalidElementPredicate = 0x8816, // Несоответствие типов для проверки принадлежности
invalidEmptySetUsage = 0x8817, // Бессмысленное использование пустого множества
invalidArgsArity = 0x8818, // Некорректное количество аргументов терм-функции invalidArgsArity = 0x8818, // Некорректное количество аргументов терм-функции
invalidArgumentType = 0x8819, // Типизация аргумента не совпадает с объявленной invalidArgumentType = 0x8819, // Типизация аргумента не совпадает с объявленной
globalStructure = 0x881C, // Родовая структура должна быть ступенью globalStructure = 0x881C, // Родовая структура должна быть ступенью

View File

@ -38,6 +38,8 @@ class TypeAuditor final : public ASTVisitor<TypeAuditor> {
friend class SyntaxTree::Cursor; friend class SyntaxTree::Cursor;
friend class ASTVisitor<TypeAuditor>; friend class ASTVisitor<TypeAuditor>;
using DeboolCallback = std::function<void(const std::string&)>;
static constexpr auto typeDeductionDepth = 5; static constexpr auto typeDeductionDepth = 5;
struct LocalData { struct LocalData {
@ -85,7 +87,7 @@ protected:
bool ViLocal(Cursor iter); bool ViLocal(Cursor iter);
bool ViInteger(Cursor /*iter*/) { return SetCurrent(Typification::Integer()); } bool ViInteger(Cursor /*iter*/) { return SetCurrent(Typification::Integer()); }
bool ViIntegerSet(Cursor /*iter*/) { return SetCurrent(Typification::Integer().Bool()); } bool ViIntegerSet(Cursor /*iter*/) { return SetCurrent(Typification::Integer().Bool()); }
bool ViEmptySet(Cursor /*iter*/); bool ViEmptySet(Cursor iter);
bool ViTupleDeclaration(Cursor iter); bool ViTupleDeclaration(Cursor iter);
bool ViEnumDeclaration(Cursor iter) { return VisitAllAndSetCurrent(iter, LogicT{}); } bool ViEnumDeclaration(Cursor iter) { return VisitAllAndSetCurrent(iter, LogicT{}); }
@ -132,6 +134,7 @@ private:
[[nodiscard]] std::optional<ExpressionType> ChildType(Cursor iter, Index index); [[nodiscard]] std::optional<ExpressionType> ChildType(Cursor iter, Index index);
[[nodiscard]] std::optional<Typification> ChildTypeDebool(Cursor iter, Index index, SemanticEID eid); [[nodiscard]] std::optional<Typification> ChildTypeDebool(Cursor iter, Index index, SemanticEID eid);
[[nodiscard]] std::optional<Typification> ChildTypeDebool(Cursor iter, Index index, DeboolCallback onError);
void OnError(SemanticEID eid, StrPos position); void OnError(SemanticEID eid, StrPos position);
void OnError(SemanticEID eid, StrPos position, std::string param); void OnError(SemanticEID eid, StrPos position, std::string param);

View File

@ -469,7 +469,23 @@ bool TypeAuditor::ViLocal(Cursor iter) {
} }
} }
bool TypeAuditor::ViEmptySet(Cursor /*iter*/) { bool TypeAuditor::ViEmptySet(Cursor iter) {
static const std::vector<TokenID> invalidParents{
TokenID::CARD,
TokenID::DEBOOL,
TokenID::UNION,
TokenID::INTERSECTION,
TokenID::SET_MINUS,
TokenID::SYMMINUS,
TokenID::DECART,
TokenID::REDUCE,
TokenID::BIGPR,
TokenID::SMALLPR
};
if (std::find(invalidParents.begin(), invalidParents.end(), iter.Parent().id) != invalidParents.end()) {
OnError(SemanticEID::invalidEmptySetUsage, iter->pos.start);
return false;
}
return SetCurrent(Typification::EmptySet()); return SetCurrent(Typification::EmptySet());
} }
@ -862,7 +878,11 @@ bool TypeAuditor::ViSetexprBinary(Cursor iter) {
bool TypeAuditor::ViProjectSet(Cursor iter) { bool TypeAuditor::ViProjectSet(Cursor iter) {
// T(Pri(a)) = B(Pi(D(T(a)))) // T(Pri(a)) = B(Pi(D(T(a))))
const auto maybeArgument = ChildTypeDebool(iter, 0, SemanticEID::invalidProjectionSet); const auto maybeArgument = ChildTypeDebool(iter, 0,
[iter, this](const std::string& typeString) {
this->OnError(SemanticEID::invalidProjectionSet, iter(0).pos.start, { iter->ToString(), typeString });
}
);
if (!maybeArgument.has_value()) { if (!maybeArgument.has_value()) {
return false; return false;
} }
@ -1064,6 +1084,14 @@ std::optional<ExpressionType> TypeAuditor::ChildType(Cursor iter, const Index in
} }
std::optional<Typification> TypeAuditor::ChildTypeDebool(Cursor iter, const Index index, const SemanticEID eid) { std::optional<Typification> TypeAuditor::ChildTypeDebool(Cursor iter, const Index index, const SemanticEID eid) {
return ChildTypeDebool(iter, index,
[iter, eid, index, this](const std::string& typeString) {
this->OnError(eid, iter(index).pos.start, typeString);
}
);
}
std::optional<Typification> TypeAuditor::ChildTypeDebool(Cursor iter, const Index index, DeboolCallback onError) {
const auto maybeResult = ChildType(iter, index); const auto maybeResult = ChildType(iter, index);
if (!maybeResult.has_value() || !std::holds_alternative<Typification>(maybeResult.value())) { if (!maybeResult.has_value() || !std::holds_alternative<Typification>(maybeResult.value())) {
return std::nullopt; return std::nullopt;
@ -1073,11 +1101,7 @@ std::optional<Typification> TypeAuditor::ChildTypeDebool(Cursor iter, const Inde
return result; return result;
} }
if (!result.IsCollection()) { if (!result.IsCollection()) {
OnError( onError(ToString(maybeResult.value()));
eid,
iter(index).pos.start,
ToString(maybeResult.value())
);
return std::nullopt; return std::nullopt;
} }
return result.B().Base(); return result.B().Base();

View File

@ -181,6 +181,7 @@ TEST_F(UTTypeAuditor, NumericErrors) {
ExpectError(R"(card(debool(X1)))", SemanticEID::invalidCard, 5); ExpectError(R"(card(debool(X1)))", SemanticEID::invalidCard, 5);
ExpectError(R"(card(S4))", SemanticEID::invalidCard, 5); ExpectError(R"(card(S4))", SemanticEID::invalidCard, 5);
ExpectError(R"(card(1))", SemanticEID::invalidCard, 5); ExpectError(R"(card(1))", SemanticEID::invalidCard, 5);
ExpectError(R"(card({}))", SemanticEID::invalidEmptySetUsage, 5);
ExpectError(R"(card((1,2)))", SemanticEID::invalidCard, 5); ExpectError(R"(card((1,2)))", SemanticEID::invalidCard, 5);
ExpectError(R"(debool(X1) \plus 1)", SemanticEID::arithmeticNotSupported, 0); ExpectError(R"(debool(X1) \plus 1)", SemanticEID::arithmeticNotSupported, 0);
@ -328,9 +329,6 @@ TEST_F(UTTypeAuditor, TypedOperationsCorrect) {
SetupConstants(); SetupConstants();
ExpectTypification(R"(X1 \union X1)", "B(X1)"_t); ExpectTypification(R"(X1 \union X1)", "B(X1)"_t);
ExpectTypification(R"({} \union {})", "B(R0)"_t);
ExpectTypification(R"(X1 \union {})", "B(X1)"_t);
ExpectTypification(R"({} \union X1)", "B(X1)"_t);
ExpectTypification(R"(X1 \setminus X1)", "B(X1)"_t); ExpectTypification(R"(X1 \setminus X1)", "B(X1)"_t);
ExpectTypification(R"(X1 \intersect X1)", "B(X1)"_t); ExpectTypification(R"(X1 \intersect X1)", "B(X1)"_t);
ExpectTypification(R"(X1 \symmdiff X1)", "B(X1)"_t); ExpectTypification(R"(X1 \symmdiff X1)", "B(X1)"_t);
@ -344,14 +342,12 @@ TEST_F(UTTypeAuditor, TypedOperationsCorrect) {
ExpectTypification(R"(B(X1))", "BB(X1)"_t); ExpectTypification(R"(B(X1))", "BB(X1)"_t);
ExpectTypification(R"(X1*X1)", "B(X1*X1)"_t); ExpectTypification(R"(X1*X1)", "B(X1*X1)"_t);
ExpectTypification(R"(Pr1(S1))", "B(X1)"_t); ExpectTypification(R"(Pr1(S1))", "B(X1)"_t);
ExpectTypification(R"(Pr1({}))", "B(R0)"_t);
ExpectTypification(R"(Fi1[X1](S1))", "B(X1*X1)"_t); ExpectTypification(R"(Fi1[X1](S1))", "B(X1*X1)"_t);
ExpectTypification(R"(Fi1,2[X1, X1](S1))", "B(X1*X1)"_t); ExpectTypification(R"(Fi1,2[X1, X1](S1))", "B(X1*X1)"_t);
ExpectTypification(R"(Fi1,2[X1 * X1](S1))", "B(X1*X1)"_t); ExpectTypification(R"(Fi1,2[X1 * X1](S1))", "B(X1*X1)"_t);
ExpectTypification(R"(Fi1[{1,2,3}](Z*X1))", "B(Z*X1)"_t); ExpectTypification(R"(Fi1[{1,2,3}](Z*X1))", "B(Z*X1)"_t);
ExpectTypification(R"(Fi1[{1,2,3}](C1*X1))", "B(C1*X1)"_t); ExpectTypification(R"(Fi1[{1,2,3}](C1*X1))", "B(C1*X1)"_t);
ExpectTypification(R"(Pr1,2(S1))", "B(X1*X1)"_t); ExpectTypification(R"(Pr1,2(S1))", "B(X1*X1)"_t);
ExpectTypification(R"(Pr1,2({}))", "B(R0)"_t);
ExpectTypification(R"(bool(X1))", "BB(X1)"_t); ExpectTypification(R"(bool(X1))", "BB(X1)"_t);
ExpectTypification(R"(debool({X1}))", "B(X1)"_t); ExpectTypification(R"(debool({X1}))", "B(X1)"_t);
ExpectTypification(R"(red(S2))", "B(X1)"_t); ExpectTypification(R"(red(S2))", "B(X1)"_t);
@ -361,11 +357,14 @@ TEST_F(UTTypeAuditor, TypedOperationsErrors) {
SetupConstants(); SetupConstants();
ExpectError(R"(X1 \union S2)", SemanticEID::typesNotEqual, 10); ExpectError(R"(X1 \union S2)", SemanticEID::typesNotEqual, 10);
ExpectError(R"(X1 \union {})", SemanticEID::invalidEmptySetUsage, 10);
ExpectError(R"(S2 \union X1)", SemanticEID::typesNotEqual, 10); ExpectError(R"(S2 \union X1)", SemanticEID::typesNotEqual, 10);
ExpectError(R"(Pr1(X1))", SemanticEID::invalidProjectionSet, 4); ExpectError(R"(Pr1(X1))", SemanticEID::invalidProjectionSet, 4);
ExpectError(R"(Pr1({}))", SemanticEID::invalidEmptySetUsage, 4);
ExpectError(R"(Pr3(S1))", SemanticEID::invalidProjectionSet, 4); ExpectError(R"(Pr3(S1))", SemanticEID::invalidProjectionSet, 4);
ExpectError(R"(pr1(debool(X1)))", SemanticEID::invalidProjectionTuple, 4); ExpectError(R"(pr1(debool(X1)))", SemanticEID::invalidProjectionTuple, 4);
ExpectError(R"(pr1({}))", SemanticEID::invalidEmptySetUsage, 4);
ExpectError(R"(Fi1[X1](B(X1)))", SemanticEID::invalidFilterArgumentType, 8); ExpectError(R"(Fi1[X1](B(X1)))", SemanticEID::invalidFilterArgumentType, 8);
ExpectError(R"(Fi1[1](B(X1)))", SemanticEID::invalidFilterArgumentType, 7); ExpectError(R"(Fi1[1](B(X1)))", SemanticEID::invalidFilterArgumentType, 7);
ExpectError(R"(Fi1[S4](B(X1)))", SemanticEID::invalidFilterArgumentType, 8); ExpectError(R"(Fi1[S4](B(X1)))", SemanticEID::invalidFilterArgumentType, 8);
@ -377,6 +376,7 @@ TEST_F(UTTypeAuditor, TypedOperationsErrors) {
ExpectError(R"(\A a \in X1 Fi1[a](B(X1)*X1) \eq X1)", SemanticEID::typesNotEqual, 16); ExpectError(R"(\A a \in X1 Fi1[a](B(X1)*X1) \eq X1)", SemanticEID::typesNotEqual, 16);
ExpectError(R"(\A a \in X1*X1 Fi1[a](B(X1)*X1) \eq X1)", SemanticEID::typesNotEqual, 19); ExpectError(R"(\A a \in X1*X1 Fi1[a](B(X1)*X1) \eq X1)", SemanticEID::typesNotEqual, 19);
ExpectError(R"(red(X1))", SemanticEID::invalidReduce, 5); ExpectError(R"(red(X1))", SemanticEID::invalidReduce, 5);
ExpectError(R"(red({}))", SemanticEID::invalidEmptySetUsage, 4);
ExpectError(R"(\A a \in X1 B(a) \eq X1)", SemanticEID::invalidBoolean, 14); ExpectError(R"(\A a \in X1 B(a) \eq X1)", SemanticEID::invalidBoolean, 14);
ExpectError(R"(\A a \in S1 B(a) \eq X1)", SemanticEID::invalidBoolean, 14); ExpectError(R"(\A a \in S1 B(a) \eq X1)", SemanticEID::invalidBoolean, 14);

View File

@ -19,6 +19,12 @@ Here we write upgrading notes. Make them as straightforward as possible.
### Fixed ### Fixed
## [0.1.9] - 2024-09-25
### Added
- Add new rule to prevent unreasonable use of emptyset
## [0.1.8] - 2024-09-22 ## [0.1.8] - 2024-09-22
### Fixed ### Fixed

View File

@ -1 +1 @@
0.1.8 0.1.9