mirror of
https://github.com/IRBorisov/ConceptCore.git
synced 2025-06-26 01:00:36 +03:00
Fix typechecking issues and update pyconcept
This commit is contained in:
parent
a4d5aa353f
commit
093e2d23fd
|
@ -112,6 +112,17 @@ private:
|
|||
|
||||
[[nodiscard]] std::optional<object::StructuredData> ExtractDomain(Cursor iter);
|
||||
[[nodiscard]] bool TryEvaluateFromFirstArg(TokenID operation, bool firstArgValue) noexcept;
|
||||
|
||||
[[nodiscard]] bool EvaluateFilterComplex(
|
||||
Cursor iter,
|
||||
const std::vector<Index>& indicies,
|
||||
const object::StructuredData& argument
|
||||
);
|
||||
[[nodiscard]] bool EvaluateFilterTuple(
|
||||
Cursor iter,
|
||||
const std::vector<Index>& indicies,
|
||||
const object::StructuredData& argument
|
||||
);
|
||||
};
|
||||
|
||||
} // namespace ccl::rslang
|
|
@ -38,6 +38,8 @@ class TypeAuditor final : public ASTVisitor<TypeAuditor> {
|
|||
friend class SyntaxTree::Cursor;
|
||||
friend class ASTVisitor<TypeAuditor>;
|
||||
|
||||
static constexpr auto typeDeductionDepth = 5;
|
||||
|
||||
struct LocalData {
|
||||
TypedID arg;
|
||||
int32_t level{};
|
||||
|
|
|
@ -492,7 +492,7 @@ bool ASTInterpreter::ViBoolean(Cursor iter) {
|
|||
if (!childValue.has_value()) {
|
||||
return false;
|
||||
}
|
||||
const auto value = std::get<StructuredData>(childValue.value());
|
||||
const auto& value = std::get<StructuredData>(childValue.value());
|
||||
if (
|
||||
(iter.IsRoot() || (iter.Parent().id != TokenID::IN && iter.Parent().id != TokenID::NT_DECLARATIVE_EXPR)) &&
|
||||
value.B().Cardinality() >= StructuredData::BOOL_INFINITY
|
||||
|
@ -600,14 +600,56 @@ bool ASTInterpreter::ViFilter(Cursor iter) {
|
|||
}
|
||||
|
||||
const auto& indicies = iter->data.ToTuple();
|
||||
const auto tupleParam = ssize(indicies) == iter.ChildrenCount() - 1;
|
||||
if (tupleParam) {
|
||||
return EvaluateFilterTuple(iter, indicies, argument);
|
||||
} else {
|
||||
return EvaluateFilterComplex(iter, indicies, argument);
|
||||
}
|
||||
}
|
||||
|
||||
bool ASTInterpreter::EvaluateFilterComplex(
|
||||
Cursor iter,
|
||||
const std::vector<Index>& indicies,
|
||||
const object::StructuredData& argument
|
||||
) {
|
||||
const auto param = EvaluateChild(iter, 0);
|
||||
if (!param.has_value()) {
|
||||
return false;
|
||||
}
|
||||
const auto& paramValue = std::get<StructuredData>(param.value());
|
||||
if (paramValue.B().IsEmpty()) {
|
||||
return SetCurrent(Factory::EmptySet());
|
||||
}
|
||||
|
||||
auto result = Factory::EmptySet();
|
||||
for (const auto& element : argument.B()) {
|
||||
std::vector<StructuredData> components{};
|
||||
for (auto i = 0U; i < size(indicies); ++i) {
|
||||
components.emplace_back(element.T().Component(indicies[i]));
|
||||
}
|
||||
const auto tuple = Factory::Tuple(components);
|
||||
if (paramValue.B().Contains(tuple)) {
|
||||
result.ModifyB().AddElement(element);
|
||||
}
|
||||
}
|
||||
return SetCurrent(std::move(result));
|
||||
}
|
||||
|
||||
bool ASTInterpreter::EvaluateFilterTuple(
|
||||
Cursor iter,
|
||||
const std::vector<Index>& indicies,
|
||||
const object::StructuredData& argument
|
||||
) {
|
||||
std::vector<StructuredData> params{};
|
||||
params.reserve(size(indicies));
|
||||
for (Index child = 0; child < iter.ChildrenCount() - 1; ++child) {
|
||||
const auto param = EvaluateChild(iter, child);
|
||||
if (!param.has_value()) {
|
||||
return false;
|
||||
}
|
||||
if (const auto val = std::get<StructuredData>(param.value()); val.B().IsEmpty()) {
|
||||
}
|
||||
const auto& val = std::get<StructuredData>(param.value());
|
||||
if (val.B().IsEmpty()) {
|
||||
return SetCurrent(Factory::EmptySet());
|
||||
} else {
|
||||
params.emplace_back(val);
|
||||
|
|
|
@ -724,15 +724,15 @@ bool TypeAuditor::ViRecursion(Cursor iter) {
|
|||
const bool isFull = iter->id == TokenID::NT_RECURSIVE_FULL;
|
||||
const auto iterationIndex = static_cast<Index>(isFull ? 3 : 2);
|
||||
|
||||
const auto iterationType = ChildType(iter, iterationIndex);
|
||||
if (!iterationType.has_value()) {
|
||||
auto iterationValue = ChildType(iter, iterationIndex);
|
||||
if (!iterationValue.has_value()) {
|
||||
return false;
|
||||
}
|
||||
if (!env.AreCompatible(iterationType.value(), initType.value())) {
|
||||
if (!env.AreCompatible(iterationValue.value(), initType.value())) {
|
||||
OnError(
|
||||
SemanticEID::typesNotEqual,
|
||||
iter(iterationIndex).pos.start,
|
||||
iterationType.value(),
|
||||
iterationValue.value(),
|
||||
initType.value()
|
||||
);
|
||||
return false;
|
||||
|
@ -740,12 +740,19 @@ bool TypeAuditor::ViRecursion(Cursor iter) {
|
|||
|
||||
{
|
||||
const auto guard = noWarnings.CreateGuard();
|
||||
ClearLocalVariables();
|
||||
if (!VisitChildDeclaration(iter, 0, std::get<Typification>(iterationType.value()))) {
|
||||
return false;
|
||||
}
|
||||
if (!VisitChild(iter, iterationIndex)) {
|
||||
return false;
|
||||
for (auto retries = typeDeductionDepth; retries > 0; --retries) {
|
||||
ClearLocalVariables();
|
||||
if (!VisitChildDeclaration(iter, 0, std::get<Typification>(iterationValue.value()))) {
|
||||
return false;
|
||||
}
|
||||
auto newIteration = ChildType(iter, iterationIndex);
|
||||
if (!newIteration.has_value()) {
|
||||
return false;
|
||||
}
|
||||
if (std::get<Typification>(newIteration.value()) == std::get<Typification>(iterationValue.value())) {
|
||||
break;
|
||||
}
|
||||
iterationValue = newIteration;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -756,7 +763,7 @@ bool TypeAuditor::ViRecursion(Cursor iter) {
|
|||
}
|
||||
|
||||
EndScope(iter->pos.start);
|
||||
return SetCurrent(iterationType.value());
|
||||
return SetCurrent(iterationValue.value());
|
||||
}
|
||||
|
||||
bool TypeAuditor::ViDecart(Cursor iter) {
|
||||
|
@ -927,7 +934,8 @@ bool TypeAuditor::ViProjectTuple(Cursor iter) {
|
|||
|
||||
bool TypeAuditor::ViFilter(Cursor iter) {
|
||||
const auto& indicies = iter->data.ToTuple();
|
||||
if (ssize(indicies) + 1 != iter.ChildrenCount()) {
|
||||
const auto tupleParam = ssize(indicies) == iter.ChildrenCount() - 1;
|
||||
if (!tupleParam && iter.ChildrenCount() > 2) {
|
||||
OnError(SemanticEID::invalidFilterArity, iter->pos.start);
|
||||
return false;
|
||||
}
|
||||
|
@ -949,7 +957,7 @@ bool TypeAuditor::ViFilter(Cursor iter) {
|
|||
return false;
|
||||
}
|
||||
|
||||
Index child{ 0 };
|
||||
std::vector<Typification> bases{};
|
||||
for (const auto index : indicies) {
|
||||
if (!argument.B().Base().T().TestIndex(index)) {
|
||||
OnError(
|
||||
|
@ -959,21 +967,43 @@ bool TypeAuditor::ViFilter(Cursor iter) {
|
|||
);
|
||||
return false;
|
||||
}
|
||||
const auto param = ChildType(iter, child);
|
||||
if(!param.has_value()) {
|
||||
bases.push_back(argument.B().Base().T().Component(index));
|
||||
}
|
||||
|
||||
if (tupleParam) {
|
||||
for (Index child = 0; child + 1 < iter.ChildrenCount(); ++child) {
|
||||
const auto param = ChildType(iter, child);
|
||||
if (!param.has_value()) {
|
||||
return false;
|
||||
}
|
||||
const auto& paramType = std::get<Typification>(param.value());
|
||||
if (!paramType.IsCollection() ||
|
||||
!env.AreCompatible(bases.at(child), paramType.B().Base())) {
|
||||
OnError(
|
||||
SemanticEID::typesNotEqual,
|
||||
iter(child).pos.start,
|
||||
bases.at(child).Bool(), paramType
|
||||
);
|
||||
return false;
|
||||
}
|
||||
++child;
|
||||
}
|
||||
} else {
|
||||
const auto param = ChildType(iter, 0);
|
||||
if (!param.has_value()) {
|
||||
return false;
|
||||
}
|
||||
const auto& paramType = std::get<Typification>(param.value());
|
||||
if (!paramType.IsCollection() ||
|
||||
!env.AreCompatible(argument.B().Base().T().Component(index), paramType.B().Base())) {
|
||||
const auto expected = Typification::Tuple(std::move(bases)).ApplyBool();
|
||||
if (!paramType.IsCollection() ||
|
||||
!env.AreCompatible(expected, paramType)) {
|
||||
OnError(
|
||||
SemanticEID::typesNotEqual,
|
||||
iter(child).pos.start,
|
||||
argument.B().Base().T().Component(index).Bool(), paramType
|
||||
iter(0).pos.start,
|
||||
expected, paramType
|
||||
);
|
||||
return false;
|
||||
}
|
||||
++child;
|
||||
}
|
||||
return SetCurrent(maybeArgument.value());
|
||||
}
|
||||
|
|
|
@ -285,6 +285,7 @@ TEST_F(UTASTInterpreter, TypedExpressions) {
|
|||
ExpectValue(R"(Pr1,2(S3 \setminus S3))", Factory::EmptySet());
|
||||
ExpectValue(R"(Fi1[X1](S3))", data.at("S3"));
|
||||
ExpectValue(R"(Fi1,2[X1,X2](S3))", data.at("S3"));
|
||||
ExpectValue(R"(Fi1,2[X1*X2](S3))", data.at("S3"));
|
||||
ExpectValue(R"(Fi2,1[X2,X1](S3))", data.at("S3"));
|
||||
ExpectValue(R"(Fi1[X1 \setminus X1](S3))", Factory::EmptySet());
|
||||
ExpectValue(R"(Fi1[X1](S3 \setminus S3))", Factory::EmptySet());
|
||||
|
|
|
@ -251,6 +251,10 @@ TEST_F(UTTypeAuditor, ConstructorsCorrect) {
|
|||
ExpectTypification(R"(R{a \assign {} | Pr1(a) \eq Pr2(a) | a \union (X1*X1)})", "B(X1*X1)"_t);
|
||||
ExpectTypification(R"(R{a \assign {} | a \union D{x \in X1 | x \eq x}})", "B(X1)"_t);
|
||||
ExpectTypification(R"(R{a \assign {} | red(a) \eq {} | a \union {X1}})", "BB(X1)"_t);
|
||||
ExpectTypification(
|
||||
R"(R{(a, b) \assign (I{(x, {}) | x \from X1}, {}) | (X1 * B(X1*X1), b \union Fi1[X1](a))})",
|
||||
"B(X1*B(X1*X1))*B(X1*B(X1*X1))"_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);
|
||||
|
@ -340,6 +344,8 @@ TEST_F(UTTypeAuditor, TypedOperationsCorrect) {
|
|||
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,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}](C1*X1))", "B(C1*X1)"_t);
|
||||
ExpectTypification(R"(Pr1,2(S1))", "B(X1*X1)"_t);
|
||||
|
@ -364,7 +370,8 @@ TEST_F(UTTypeAuditor, TypedOperationsErrors) {
|
|||
ExpectError(R"(Fi1[Z](B(X1)))", SemanticEID::invalidFilterArgumentType, 7);
|
||||
ExpectError(R"(Fi3[X1](X1*X1))", SemanticEID::invalidFilterArgumentType, 8);
|
||||
ExpectError(R"(Fi1[X1](B(X1)*X1))", SemanticEID::typesNotEqual, 4);
|
||||
ExpectError(R"(Fi1,2[X1](X1*X1))", SemanticEID::invalidFilterArity, 0);
|
||||
ExpectError(R"(Fi1,2[X1*{X1}](B(X1)*X1))", SemanticEID::typesNotEqual, 6);
|
||||
ExpectError(R"(Fi1,2,1[X1, X1](X1*X1))", SemanticEID::invalidFilterArity, 0);
|
||||
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"(red(X1))", SemanticEID::invalidReduce, 5);
|
||||
|
|
|
@ -19,6 +19,17 @@ Here we write upgrading notes. Make them as straightforward as possible.
|
|||
|
||||
### Fixed
|
||||
|
||||
## [0.1.6] - 2024-06-14
|
||||
|
||||
### Fixed
|
||||
|
||||
- Fix emptyset type deduction in recursive structures
|
||||
|
||||
### Added
|
||||
|
||||
- Allow single argument for multi-Filter
|
||||
- Add fixed dependencies versions to build requirements
|
||||
|
||||
## [0.1.5] - 2024-05-10
|
||||
|
||||
### Added
|
||||
|
|
|
@ -1 +1 @@
|
|||
0.1.5
|
||||
0.1.6
|
Binary file not shown.
Binary file not shown.
Loading…
Reference in New Issue
Block a user