ConceptProd/ConceptCore
1
0
Fork 0
mirror of https://github.com/IRBorisov/ConceptCore.git synced 2025-06-26 01:00:36 +03:00
Code Issues Actions Packages Projects Releases Wiki Activity

Allow EmptySet as standalone typed expression

Browse Source
This commit is contained in:
IRBorisov 2024-05-08 02:14:17 +03:00
parent 5c2ef6fbc7
commit c04a9c84e1
8 changed files with 67 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
ccl/rslang/include/ccl/rslang/RSErrorCodes.hpp
View File

@ -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, // Количество параметров фильра не соответствует количеству индексов

4
ccl/rslang/include/ccl/rslang/TypeAuditor.h
View File

@ -54,6 +54,7 @@ class TypeAuditor final : public ASTVisitor<TypeAuditor> {
std::vector<size_t> 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{}); }

2
ccl/rslang/include/ccl/rslang/Typification.h
View File

@ -74,6 +74,7 @@ class Typification : public Structured<EchelonBase, EchelonTuple, EchelonBool> {
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<Typification> factors);
[[nodiscard]] static const Typification& Integer();
[[nodiscard]] static const Typification& EmptySet();
public:
using Substitutes = std::unordered_map<std::string, Typification>;

7
ccl/rslang/src/Literals.cpp
View File

@ -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<Typification>(result)) {
assert(false);
return Typification::Integer();

47
ccl/rslang/src/TypeAuditor.cpp
View File

@ -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<Typification> 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<uint32_t>(eid), position });
@ -391,7 +418,7 @@ std::optional<Typification::Substitutes> 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;

5
ccl/rslang/src/Typification.cpp
View File

@ -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(); }},

31
ccl/rslang/test/src/testTypeAuditor.cpp
View File

@ -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);
}

2
pyconcept/VERSION
View File

@ -1 +1 @@
0.1.2
0.1.3