From c04a9c84e180c1ccc900045883cceb305b6aa358 Mon Sep 17 00:00:00 2001 From: IRBorisov <8611739+IRBorisov@users.noreply.github.com> Date: Wed, 8 May 2024 02:14:17 +0300 Subject: [PATCH] Allow EmptySet as standalone typed expression --- .../include/ccl/rslang/RSErrorCodes.hpp | 2 - ccl/rslang/include/ccl/rslang/TypeAuditor.h | 4 +- ccl/rslang/include/ccl/rslang/Typification.h | 2 + ccl/rslang/src/Literals.cpp | 7 +-- ccl/rslang/src/TypeAuditor.cpp | 47 ++++++++++++++----- ccl/rslang/src/Typification.cpp | 5 ++ ccl/rslang/test/src/testTypeAuditor.cpp | 31 +++++++----- pyconcept/VERSION | 2 +- 8 files changed, 67 insertions(+), 33 deletions(-) diff --git a/ccl/rslang/include/ccl/rslang/RSErrorCodes.hpp b/ccl/rslang/include/ccl/rslang/RSErrorCodes.hpp index fa01bd7..78c1a66 100644 --- a/ccl/rslang/include/ccl/rslang/RSErrorCodes.hpp +++ b/ccl/rslang/include/ccl/rslang/RSErrorCodes.hpp @@ -47,13 +47,11 @@ enum class SemanticEID : uint32_t { invalidElementPredicate = 0x8816, // Несоответствие типов для проверки принадлежности invalidArgsArity = 0x8818, // Некорректное количество аргументов терм-функции invalidArgumentType = 0x8819, // Типизация аргумента не совпадает с объявленной - invalidEqualsEmpty = 0x881A, // Сравнение с пустым множеством не множества globalStructure = 0x881C, // Родовая структура должна быть ступенью // TODO: следующий идентификатор сейчас не используется. Нужно подобрать место для проверки globalExpectedFunction = 0x881F, // Ожидалось выражение объявления функции - emptySetUsage = 0x8820, // Некорректное использование пустого множества как типизированного выражения radicalUsage = 0x8821, // Радикалы запрещены вне деклараций терм-функций invalidFilterArgumentType = 0x8822, // Типизация аргумента фильтра не корректна invalidFilterArity = 0x8823, // Количество параметров фильра не соответствует количеству индексов diff --git a/ccl/rslang/include/ccl/rslang/TypeAuditor.h b/ccl/rslang/include/ccl/rslang/TypeAuditor.h index a48e0df..dd147f6 100644 --- a/ccl/rslang/include/ccl/rslang/TypeAuditor.h +++ b/ccl/rslang/include/ccl/rslang/TypeAuditor.h @@ -54,6 +54,7 @@ class TypeAuditor final : public ASTVisitor { std::vector functionArgsID{}; FunctionArguments functionArgs{}; + bool isTypification{ false }; types::GuardableBool isArgDeclaration{ false }; types::GuardableBool isLocalDeclaration{ false }; types::GuardableBool isFuncDeclaration{ false }; @@ -68,6 +69,7 @@ public: [[nodiscard]] bool CheckType(const SyntaxTree& tree); [[nodiscard]] const FunctionArguments& GetDeclarationArgs() const noexcept { return functionArgs; } [[nodiscard]] const ExpressionType& GetType() const noexcept; + void SetExepectTypification(const bool value = true) noexcept; protected: bool ViGlobalDefinition(Cursor iter); @@ -79,7 +81,7 @@ protected: bool ViLocal(Cursor iter); bool ViInteger(Cursor /*iter*/) { return VisitAndReturn(Typification::Integer()); } bool ViIntegerSet(Cursor /*iter*/) { return VisitAndReturn(Typification::Integer().Bool()); } - bool ViEmptySet(Cursor iter); + bool ViEmptySet(Cursor /*iter*/); bool ViLocalBind(Cursor iter); bool ViLocalEnum(Cursor iter) { return VisitAllAndReturn(iter, LogicT{}); } diff --git a/ccl/rslang/include/ccl/rslang/Typification.h b/ccl/rslang/include/ccl/rslang/Typification.h index 3318e6e..03e90da 100644 --- a/ccl/rslang/include/ccl/rslang/Typification.h +++ b/ccl/rslang/include/ccl/rslang/Typification.h @@ -74,6 +74,7 @@ class Typification : public Structured { public: static constexpr Index PR_START = 1; static constexpr std::string_view integerTypeName = "Z"; + static constexpr std::string_view anyTypificationName = "R0"; private: using Structured::Structured; @@ -87,6 +88,7 @@ public: [[nodiscard]] static Typification Tuple(std::vector factors); [[nodiscard]] static const Typification& Integer(); + [[nodiscard]] static const Typification& EmptySet(); public: using Substitutes = std::unordered_map; diff --git a/ccl/rslang/src/Literals.cpp b/ccl/rslang/src/Literals.cpp index 93b0018..5643ccb 100644 --- a/ccl/rslang/src/Literals.cpp +++ b/ccl/rslang/src/Literals.cpp @@ -41,19 +41,20 @@ Typification operator""_t(const char* input, const size_t /*size*/) { static detail::AsciiLexer lexer{}; static detail::RSParser parser{}; static EchoTypeEnvironment env{}; - static TypeAuditor analyse{ env }; + static TypeAuditor analyser{ env }; + analyser.SetExepectTypification(); env.Clear(); if (!parser.Parse(lexer(input).Stream())) { assert(false); return Typification::Integer(); } - if (!analyse.CheckType(parser.AST())) { + if (!analyser.CheckType(parser.AST())) { assert(false); return Typification::Integer(); } - const auto& result = analyse.GetType(); + const auto& result = analyser.GetType(); if (!std::holds_alternative(result)) { assert(false); return Typification::Integer(); diff --git a/ccl/rslang/src/TypeAuditor.cpp b/ccl/rslang/src/TypeAuditor.cpp index 978472a..aa279ae 100644 --- a/ccl/rslang/src/TypeAuditor.cpp +++ b/ccl/rslang/src/TypeAuditor.cpp @@ -119,13 +119,25 @@ bool TypeEnv::AreCompatible(const ExpressionType& type1, const ExpressionType& t bool TypeEnv::AreCompatible(const Typification& type1, const Typification& type2) const { if (type1 == type2) { return true; - } else if (type1.Structure() != type2.Structure()) { + } + + const auto struct1 = type1.Structure(); + const auto struct2 = type2.Structure(); + + if (struct1 == rslang::StructureType::basic && type1.E().baseID == Typification::anyTypificationName) { + return true; + } + if (struct2 == rslang::StructureType::basic && type2.E().baseID == Typification::anyTypificationName) { + return true; + } + if (struct1 != struct2) { return false; } - switch (type1.Structure()) { + + switch (struct1) { default: case rslang::StructureType::basic: return CommonType(type1, type2) != nullptr; - case rslang::StructureType::collection: return AreCompatible(type1.B().Base(), type2.B().Base()); + case rslang::StructureType::collection: return AreCompatible(type1.B().Base(), type2.B().Base()); case rslang::StructureType::tuple: { if (type1.T().Arity() != type2.T().Arity()) { return false; @@ -148,7 +160,18 @@ std::optional TypeEnv::Merge(const Typification& type1, const Typi if (type1.Structure() != type2.Structure()) { return std::nullopt; } - switch (type1.Structure()) { + + const auto struct1 = type1.Structure(); + const auto struct2 = type2.Structure(); + + if (struct1 == rslang::StructureType::basic && type1.E().baseID == Typification::anyTypificationName) { + return type2; + } + if (struct2 == rslang::StructureType::basic && type2.E().baseID == Typification::anyTypificationName) { + return type1; + } + + switch (struct1) { default: case rslang::StructureType::basic: { const auto* type = CommonType(type1, type2); @@ -239,6 +262,10 @@ const ExpressionType& TypeAuditor::GetType() const noexcept { return currentType; } +void TypeAuditor::SetExepectTypification(const bool value) noexcept { + isTypification = value; +} + void TypeAuditor::OnError(const SemanticEID eid, const StrPos position) { if (reporter.has_value()) { reporter.value()(Error{ static_cast(eid), position }); @@ -391,7 +418,7 @@ std::optional TypeAuditor::CheckFuncArguments(Cursor bool TypeAuditor::ViGlobal(Cursor iter) { const auto& globalName = iter->data.ToText(); if (iter->id == TokenID::ID_RADICAL) { - if (!isFuncDeclaration) { + if (!isFuncDeclaration && !isTypification) { OnError( SemanticEID::radicalUsage, iter->pos.start, @@ -435,9 +462,8 @@ bool TypeAuditor::ViLocal(Cursor iter) { } } -bool TypeAuditor::ViEmptySet(Cursor iter) { - OnError(SemanticEID::emptySetUsage, iter->pos.start); - return false; +bool TypeAuditor::ViEmptySet(Cursor /*iter*/) { + return VisitAndReturn(Typification::EmptySet()); } bool TypeAuditor::ViLocalBind(Cursor iter) { @@ -575,11 +601,6 @@ bool TypeAuditor::ViQuantifier(Cursor iter) { } bool TypeAuditor::ViEquals(Cursor iter) { - if (iter(1).id == TokenID::LIT_EMPTYSET) { - const auto type = ChildTypeDebool(iter, 0, SemanticEID::invalidEqualsEmpty); - return type.has_value() && VisitAndReturn(LogicT{}); - } - const auto test1 = ChildType(iter, 0); if (!test1.has_value()) { return false; diff --git a/ccl/rslang/src/Typification.cpp b/ccl/rslang/src/Typification.cpp index 0858e24..bb3c709 100644 --- a/ccl/rslang/src/Typification.cpp +++ b/ccl/rslang/src/Typification.cpp @@ -31,6 +31,11 @@ const Typification& Typification::Integer() { return integers; } +const Typification& Typification::EmptySet() { + static const auto empty = Typification{ std::string{anyTypificationName} }.Bool(); + return empty; +} + std::string Typification::ToString() const noexcept(false) { std::string result{}; std::visit(meta::Overloads{ [&](const auto& val) { result = val.ToString(); }}, diff --git a/ccl/rslang/test/src/testTypeAuditor.cpp b/ccl/rslang/test/src/testTypeAuditor.cpp index 14cb578..30896a9 100644 --- a/ccl/rslang/test/src/testTypeAuditor.cpp +++ b/ccl/rslang/test/src/testTypeAuditor.cpp @@ -99,6 +99,7 @@ TEST_F(UTTypeAuditor, DefinitionsCorrect) { ExpectTypification(R"(X1 \defexpr )", "B(X1)"_t); ExpectTypification(R"(D1 \defexpr X1 \union X1)", "B(X1)"_t); ExpectLogic(R"(A1 \defexpr 1 \eq 1)"); + ExpectTypification(R"(D1 \defexpr {})", "B(R0)"_t); ExpectTypification(R"(S1 \deftype X1)", "X1"_t); ExpectTypification(R"(S1 \deftype Z)", "Z"_t); @@ -110,11 +111,11 @@ TEST_F(UTTypeAuditor, DefinitionsCorrect) { EXPECT_EQ(args[0].name, "a"); EXPECT_EQ(args[0].type, "X1"_t); - ExpectTypification(R"(F42 \defexpr [a \in R1] {a})", Typification("R1").Bool()); + ExpectTypification(R"(F42 \defexpr [a \in R1] {a})", "B(R1)"_t); const auto& args2 = analyse.GetDeclarationArgs(); ASSERT_EQ(size(args2), 1U); EXPECT_EQ(args2[0].name, "a"); - EXPECT_EQ(args2[0].type, Typification("R1")); + EXPECT_EQ(args2[0].type, "R1"_t); ExpectTypification(R"(F42 \defexpr [a \in D{ b \in X1 | b \eq b}] {a})", "B(X1)"_t); const auto& args3 = analyse.GetDeclarationArgs(); @@ -211,8 +212,8 @@ TEST_F(UTTypeAuditor, LogicCorrect) { } TEST_F(UTTypeAuditor, LogicErrors) { - ExpectError(R"(\A a \in X1 a \eq {})", SemanticEID::invalidEqualsEmpty, 12); - ExpectError(R"(\A a \in X1*X1 a \eq {})", SemanticEID::invalidEqualsEmpty, 15); + ExpectError(R"(\A a \in X1 a \eq {})", SemanticEID::typesNotCompatible, 18); + ExpectError(R"(\A a \in X1*X1 a \eq {})", SemanticEID::typesNotCompatible, 21); ExpectError(R"(\A (a,a) \in S1 pr2(a) \in X1)", SemanticEID::localShadowing, 6); ExpectError(R"(\A (a,b) \in X1 1 \eq 1)", SemanticEID::invalidBinding, 4); @@ -243,6 +244,7 @@ TEST_F(UTTypeAuditor, ConstructorsCorrect) { ExpectTypification(R"(R{a \assign S1 | a \union a})", "B(X1*X1)"_t); ExpectTypification(R"(R{a \assign 1 | a \ls 10 | a \plus 1})", "Z"_t); ExpectTypification(R"(R{a \assign 1 | a \ls S4 | a \plus S4})", "C1"_t); + ExpectTypification(R"(R{a \assign {} | a \union {S4}})", "B(C1)"_t); ExpectTypification(R"(I{(a, b) | a \from X1; b \assign a})", "B(X1*X1)"_t); ExpectTypification(R"(I{(a, b) | a \from X1; b \assign a; 1 \eq 1})", "B(X1*X1)"_t); @@ -261,6 +263,7 @@ TEST_F(UTTypeAuditor, ConstructorsErrors) { ExpectError(R"({S6, 1})", SemanticEID::invalidEnumeration, 5); ExpectError(R"(R{a \assign S1 | {a}})", SemanticEID::typesNotEqual, 17); + ExpectError(R"(R{a \assign {} | a \union S4})", SemanticEID::invalidTypeOperation, 26); ExpectError(R"(\A a \in S1 R{(a1, a2) \assign a | a1} \eq a)", SemanticEID::typesNotEqual, 35); ExpectError(R"(I{(a, b) | a \from X1; b \assign {a}; a \noteq b})", SemanticEID::typesNotCompatible, 47); @@ -308,6 +311,9 @@ TEST_F(UTTypeAuditor, TypedOperationsCorrect) { SetupConstants(); 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 \intersect X1)", "B(X1)"_t); ExpectTypification(R"(X1 \symmdiff X1)", "B(X1)"_t); @@ -333,7 +339,6 @@ TEST_F(UTTypeAuditor, TypedOperationsCorrect) { TEST_F(UTTypeAuditor, TypedOperationsErrors) { SetupConstants(); - ExpectError(R"(X1 \union {})", SemanticEID::emptySetUsage, 10); ExpectError(R"(X1 \union S2)", SemanticEID::typesNotEqual, 10); ExpectError(R"(S2 \union X1)", SemanticEID::typesNotEqual, 10); @@ -410,10 +415,10 @@ TEST_F(UTTypeAuditor, TemplatedFunctions) { ExpectTypification(R"(F2[{S4}, 1])", "B(C1)"_t); ExpectError(R"(F2[X1, B(X1)])", SemanticEID::invalidArgumentType, 7); - env.Insert("F3", Typification::Tuple({ Typification("R1"), Typification("R2") })); + env.Insert("F3", "R1*R2"_t); FunctionArguments f3Args{}; - f3Args.emplace_back("a", Typification("R1").Bool()); - f3Args.emplace_back("b", Typification::Tuple({ Typification("R1"), Typification("R2") }).Bool()); + f3Args.emplace_back("a", "B(R1)"_t); + f3Args.emplace_back("b", "B(R1*R2)"_t); env.data["F3"].arguments = f3Args; ExpectTypification(R"(F3[X1, X1*B(X1)])", "X1*B(X1)"_t); @@ -423,14 +428,14 @@ TEST_F(UTTypeAuditor, TemplatedFunctions) { } TEST_F(UTTypeAuditor, TemplatedFunctionsNesting) { - env.Insert("F2", Typification("R1").Bool()); + env.Insert("F2", "B(R1)"_t); FunctionArguments f2Args{}; - f2Args.emplace_back(TypedID{ "a", Typification("R1") }); - f2Args.emplace_back(TypedID{ "b", Typification::Tuple({ Typification("R1"), Typification("R2") }) }); + f2Args.emplace_back(TypedID{ "a", "R1"_t }); + f2Args.emplace_back(TypedID{ "b", "R1*R2"_t }); env.data["F2"].arguments = f2Args; - ExpectTypification(R"(F3 \defexpr [a \in R2, b \in R2*R1] F2[a, b])", Typification("R2").Bool()); - ExpectTypification(R"(F3 \defexpr [a \in R3, b \in R3*R4] F2[a, b])", Typification("R3").Bool()); + ExpectTypification(R"(F3 \defexpr [a \in R2, b \in R2*R1] F2[a, b])", "B(R2)"_t); + ExpectTypification(R"(F3 \defexpr [a \in R3, b \in R3*R4] F2[a, b])", "B(R3)"_t); ExpectError(R"(F3 \defexpr [a \in R2, b \in R1*R2] F2[a, b])", SemanticEID::invalidArgumentType, 42); ExpectError(R"(F3 \defexpr [a \in R3, b \in R1*R2] F2[a, b])", SemanticEID::invalidArgumentType, 42); } diff --git a/pyconcept/VERSION b/pyconcept/VERSION index 8294c18..7693c96 100644 --- a/pyconcept/VERSION +++ b/pyconcept/VERSION @@ -1 +1 @@ -0.1.2 \ No newline at end of file +0.1.3 \ No newline at end of file