F: Improve typechecking API for CstTypes expectations

This commit is contained in:
Ivan 2024-09-22 18:47:07 +03:00
parent 71a5b32de7
commit c8578447f3
36 changed files with 902 additions and 561 deletions

View File

@ -18,6 +18,7 @@
"cSpell.words": [
"BIGPR",
"conanfile",
"constituenta",
"coredll",
"DCMAKE",
"debool",
@ -36,6 +37,7 @@
"NOTEQUAL",
"NOTIN",
"notsubset",
"pbdoc",
"PUNC",
"pybind",
"pyconcept",

View File

@ -198,6 +198,7 @@
<ClCompile Include="src\semantic\rsmodel\rsValuesFacet.cpp" />
<ClCompile Include="src\semantic\schema\RSConcept.cpp" />
<ClCompile Include="src\semantic\schema\Schema.cpp" />
<ClCompile Include="src\semantic\schema\SchemaAuditor.cpp" />
<ClCompile Include="src\semantic\thesaurus\TextConcept.cpp" />
<ClCompile Include="src\semantic\thesaurus\Thesaurus.cpp" />
<ClCompile Include="src\tools\CstNameGenerator.cpp" />
@ -235,6 +236,7 @@
<ClInclude Include="include\ccl\semantic\rsOperationFacet.h" />
<ClInclude Include="include\ccl\semantic\rsValuesFacet.h" />
<ClInclude Include="include\ccl\semantic\Schema.h" />
<ClInclude Include="include\ccl\semantic\SchemaAuditor.h" />
<ClInclude Include="include\ccl\semantic\TextConcept.h" />
<ClInclude Include="include\ccl\semantic\TextData.hpp" />
<ClInclude Include="include\ccl\semantic\Thesaurus.h" />

View File

@ -129,6 +129,9 @@
<ClCompile Include="src\api\RSFormJA.cpp">
<Filter>06 API</Filter>
</ClCompile>
<ClCompile Include="src\semantic\schema\SchemaAuditor.cpp">
<Filter>03 semantic\01 Schema</Filter>
</ClCompile>
</ItemGroup>
<ItemGroup>
<ClInclude Include="include\ccl\env\SourceManager.hpp">
@ -248,5 +251,8 @@
<ClInclude Include="include\ccl\api\RSFormJA.h">
<Filter>06 API</Filter>
</ClInclude>
<ClInclude Include="include\ccl\semantic\SchemaAuditor.h">
<Filter>03 semantic\01 Schema</Filter>
</ClInclude>
</ItemGroup>
</Project>

View File

@ -25,6 +25,8 @@ public:
[[nodiscard]] std::string ToMinimalJSON() const;
[[nodiscard]] std::string CheckExpression(const std::string& text, rslang::Syntax syntaxHint = rslang::Syntax::UNDEF) const;
[[nodiscard]] std::string CheckConstituenta(const std::string& alias, const std::string& definition, semantic::CstType targetType) const;
};
} // namespace ccl::api

View File

@ -89,7 +89,7 @@ public:
private:
Pict* Access(PictID pid);
void InsertInternal(const Pict& pict, GridPosition pos,
void InsertInternal(Pict&& pict, GridPosition pos,
const src::Handle& srcHandle,
std::unique_ptr<OperationHandle> opHandle);

View File

@ -97,4 +97,14 @@ constexpr bool IsStatement(const CstType type) noexcept {
}
}
constexpr bool IsLogical(const CstType type) noexcept {
switch (type) {
default: return false;
case CstType::axiom:
case CstType::theorem:
case CstType::predicate:
return true;
}
}
} // namespace ccl::semantic

View File

@ -1,7 +1,7 @@
#pragma once
#include "ccl/rslang/Auditor.h"
#include "ccl/rslang/SyntaxTree.h"
#include "ccl/semantic/SchemaAuditor.h"
#include "ccl/semantic/RSConcept.h"
#include "ccl/graph/CGraph.h"
@ -50,8 +50,8 @@ class Schema final : public rslang::TypeContext {
mutable graph::UpdatableGraph graph;
// Note: Auditor should be created last because it needs context references
using RSAuditor = std::unique_ptr<rslang::Auditor>;
mutable RSAuditor auditor{ std::make_unique<rslang::Auditor>(*this, VCContext(), ASTContext()) };
using RSAuditor = std::unique_ptr<SchemaAuditor>;
mutable RSAuditor auditor{ std::make_unique<SchemaAuditor>(*this, VCContext(), ASTContext()) };
public:
~Schema() noexcept final = default;
@ -85,8 +85,13 @@ public:
[[nodiscard]] rslang::SyntaxTreeContext ASTContext() const;
[[nodiscard]] rslang::ValueClassContext VCContext() const;
bool Emplace(EntityUID newID, std::string newAlias, CstType type,
std::string definition = {}, std::string convention = {});
bool Emplace(
EntityUID newID,
std::string newAlias,
CstType type,
std::string definition = {},
std::string convention = {}
);
bool InsertCopy(const RSConcept& cst);
bool Insert(RSConcept&& cst);
void Load(RSConcept&& cst);
@ -101,11 +106,9 @@ public:
void Translate(EntityUID target, const StrTranslator& old2New);
void TranslateAll(const StrTranslator& old2New);
[[nodiscard]] static bool CheckTypeConstistency(const rslang::ExpressionType& type, CstType cstType) noexcept;
[[nodiscard]] std::unique_ptr<SchemaAuditor> MakeAuditor() const;
[[nodiscard]] std::optional<rslang::ExpressionType> Evaluate(const std::string& input) const;
[[nodiscard]] std::unique_ptr<rslang::Auditor> MakeAuditor() const;
void UpdateState();
private:

View File

@ -0,0 +1,56 @@
#pragma once
#include "ccl/semantic/CstType.hpp"
#include "ccl/rslang/Auditor.h"
#include <optional>
namespace ccl::semantic {
//! CstType semantic errors enumeration
enum class CstTypeEID : uint32_t {
cstNonemptyBase = 0x8860, // Áàçèñíîå èëè êîíñòàíòíîå ìíîæåñòâî íå ïóñòî
cstEmptyDerived = 0x8861, // Îïðåäåëåíèå ïîíÿòèÿ ïóñòî
cstCallableNoArgs = 0x8862, // Ïàðàìåòðèçîâàííîå âûðàæåíèå áåç àðãóìåíòîâ
cstNonCallableHasArgs = 0x8863, // Íåïàðàìåòðèçîâàííîå âûðàæåíèå ñ àðãóìåíòàìè
cstExpectedLogical = 0x8864, // Îæèäàëîñü ëîãè÷åñêîå âûðàæåíèå
cstExpectedTyped = 0x8865, // Îæèäàëîñü òåîðåòèêî-ìíîæåñòâåííîå âûðàæåíèå
};
//! Auditor for Schema - wrapper around rsLang::Auditor
class SchemaAuditor {
public:
StrPos prefixLen;
private:
rslang::Auditor auditor;
public:
explicit SchemaAuditor(
const rslang::TypeContext& types,
rslang::ValueClassContext globalClass,
rslang::SyntaxTreeContext globalAST
);
public:
bool CheckConstituenta(const std::string& alias, const std::string& definition, CstType targetType);
bool CheckExpression(const std::string& expr, rslang::Syntax syntax = rslang::Syntax::MATH);
bool CheckValue();
[[nodiscard]] bool IsParsed() const noexcept;
[[nodiscard]] bool IsTypeCorrect() const noexcept;
[[nodiscard]] bool IsValueCorrect() const noexcept;
[[nodiscard]] const rslang::Syntax& GetSyntax() const noexcept;
[[nodiscard]] const rslang::SyntaxTree& AST() const noexcept;
[[nodiscard]] const rslang::ErrorLogger& Errors() const noexcept;
[[nodiscard]] const rslang::FunctionArguments& GetDeclarationArgs() const noexcept;
[[nodiscard]] const rslang::ExpressionType& GetType() const noexcept;
[[nodiscard]] rslang::ValueClass GetValueClass() const noexcept;
[[nodiscard]] meta::UniqueCPPtr<rslang::SyntaxTree> ExtractAST() noexcept;
private:
void OnError(CstTypeEID errorID);
};
} // namespace ccl::semantic

View File

@ -46,7 +46,7 @@ void LoadPicts(const JSON& data, ccl::oss::OSSchema& oss) {
}
if (it->contains("attachedOperation")) {
opHandle = std::make_unique<OperationHandle>();
it->at("attachedOperation").get_to(*opHandle.get());
it->at("attachedOperation").get_to(*opHandle);
}
oss.LoadPict(std::move(pict), position, srcHandle, std::move(opHandle));
}
@ -220,7 +220,6 @@ void to_json(JSON& object, const RSCore& core) {
for (const auto uid : core.List()) {
const auto& parse = core.GetParse(uid);
const auto* typification = parse.Typification();
const auto typeStr = typification != nullptr ? typification->ToString() : std::string{};
const auto* exprTree = core.RSLang().ASTContext()(core.GetRS(uid).alias);
JSON cstJSON(core.AsRecord(uid));
cstJSON["parse"] = {
@ -309,7 +308,7 @@ void from_json(const JSON& object, TrackingFlags& mods) {
object.at("editConvention").get_to(mods.convention);
}
} // namespace ccl::semantic
} // namespace semantic
namespace rslang {
@ -379,7 +378,7 @@ void to_json(JSON& object, const Error& error) {
};
}
} // namespace ccl::rslang
} // namespace rslang
namespace lang {
@ -422,7 +421,7 @@ void from_json(const JSON& object, ManagedText& text) {
};
}
} // namespace ccl::lang
} // namespace lang
namespace src {
@ -532,12 +531,12 @@ void from_json(const JSON& object, OperationHandle& operation) {
object.at("isOutdated").get_to(operation.outdated);
if (object.contains("options")) {
auto opts = std::make_unique<ops::EquationOptions>();
object.at("options").at("data").get_to(*opts.get());
object.at("options").at("data").get_to(*opts);
operation.options = meta::UniqueCPPtr<ops::Options>{ std::move(opts) };
}
if (object.contains("translations")) {
operation.translations = std::make_unique<ops::TranslationData>();
object.at("translations").get_to(*operation.translations.get());
object.at("translations").get_to(*operation.translations);
}
}
@ -568,7 +567,7 @@ void from_json(const JSON& object, GridPosition& position) {
object.at("column").get_to(position.column);
}
} // namespace ccl::oss
} // namespace oss
namespace ops {
@ -614,7 +613,7 @@ void from_json(const JSON& object, Equation& equation) {
object.at("newTerm").get_to(equation.arg);
}
} // namespace ccl::ops
} // namespace ops
void to_json(JSON& object, const EntityTranslation& translation) {
object = JSON::array();

View File

@ -31,11 +31,11 @@ std::string ParseExpression(const std::string& expression, const rslang::Syntax
}
const semantic::RSForm& RSFormJA::data() const noexcept {
return *schema.get();
return *schema;
}
semantic::RSForm& RSFormJA::data() noexcept {
return *schema.get();
return *schema;
}
RSFormJA RSFormJA::FromData(semantic::RSForm&& data) {
@ -74,11 +74,12 @@ std::string RSFormJA::CheckExpression(const std::string& text, const rslang::Syn
JSON result{};
auto analyser = schema->Core().RSLang().MakeAuditor();
const auto typeOK = analyser->CheckType(text, syntaxHint);
const auto typeOK = analyser->CheckExpression(text, syntaxHint);
const auto valueOK = typeOK && analyser->CheckValue();
result["parseResult"] = typeOK;
result["syntax"] = analyser->parser.syntax;
result["syntax"] = analyser->GetSyntax();
result["prefixLen"] = 0;
if (typeOK) {
result["typification"] = analyser->GetType();
} else {
@ -96,9 +97,9 @@ std::string RSFormJA::CheckExpression(const std::string& text, const rslang::Syn
result["errors"] += error;
}
if (analyser->isParsed) {
result["astText"] = rslang::AST2String::Apply(analyser->parser.AST());
result["ast"] = analyser->parser.AST();
if (analyser->IsParsed()) {
result["astText"] = rslang::AST2String::Apply(analyser->AST());
result["ast"] = analyser->AST();
} else {
result["astText"] = "";
result["ast"] = JSON::array();
@ -107,4 +108,49 @@ std::string RSFormJA::CheckExpression(const std::string& text, const rslang::Syn
return result.dump(JSON_IDENT);
}
std::string RSFormJA::CheckConstituenta(
const std::string& alias,
const std::string& definition,
semantic::CstType targetType
) const {
JSON result{};
auto analyser = schema->Core().RSLang().MakeAuditor();
const auto typeOK = analyser->CheckConstituenta(alias, definition, targetType);
const auto valueOK = typeOK && analyser->CheckValue();
result["parseResult"] = typeOK;
result["syntax"] = analyser->GetSyntax();
result["prefixLen"] = analyser->prefixLen;
if (typeOK) {
result["typification"] = analyser->GetType();
}
else {
result["typification"] = "N/A";
}
if (valueOK) {
result["valueClass"] = analyser->GetValueClass();
}
else {
result["valueClass"] = ccl::rslang::ValueClass::invalid;
}
result["args"] = analyser->GetDeclarationArgs();
result["errors"] = JSON::array();
for (const auto& error : analyser->Errors().All()) {
result["errors"] += error;
}
if (typeOK) {
result["astText"] = rslang::AST2String::Apply(analyser->AST());
result["ast"] = analyser->AST();
}
else {
result["astText"] = "";
result["ast"] = JSON::array();
}
return result.dump(JSON_IDENT);
}
} // namespace ccl::api

View File

@ -139,7 +139,7 @@ const Pict& OSSchema::LoadPict(
pict.uid = idGen.NewUID();
}
const auto pid = pict.uid;
InsertInternal(pict, pos, handle, std::move(params));
InsertInternal(std::move(pict), pos, handle, std::move(params));
return storage.at(pid);
}
@ -175,15 +175,14 @@ PictPtr OSSchema::InsertBase() {
}
void OSSchema::InsertInternal(
const Pict& pict,
Pict&& pict,
GridPosition pos,
const src::Handle& srcHandle,
std::unique_ptr<OperationHandle> opHandle
) {
const auto pid = pict.uid;
idGen.AddUID(pid);
storage.emplace(pid, pict);
storage.emplace(pid, std::move(pict));
Grid().SetPosFor(pid, pos);
Src().sources.emplace(pid, srcHandle);
if (opHandle != nullptr) {

View File

@ -1,7 +1,6 @@
#include "ccl/semantic/Schema.h"
#include "ccl/semantic/RSCore.h"
#include "ccl/rslang/RSGenerator.h"
namespace ccl::semantic {
@ -243,8 +242,13 @@ void Schema::TranslateAll(const StrTranslator& old2New) {
UpdateState();
}
bool Schema::Emplace(const EntityUID newID, std::string newAlias, const CstType type,
std::string definition, std::string convention) {
bool Schema::Emplace(
const EntityUID newID,
std::string newAlias,
const CstType type,
std::string definition,
std::string convention
) {
if (info.emplace(std::pair{ newID, ParsingInfo{} }).second) {
storage.emplace(std::pair{ newID,
RSConcept{ newID, std::move(newAlias), type, std::move(definition), std::move(convention) } });
@ -357,16 +361,15 @@ rslang::ValueClassContext Schema::VCContext() const {
std::optional<rslang::ExpressionType>
Schema::Evaluate(const std::string& input) const {
if (!auditor->CheckType(input, rslang::Syntax::MATH)) {
if (!auditor->CheckExpression(input)) {
return std::nullopt;
} else {
return auditor->GetType();
}
}
[[nodiscard]] std::unique_ptr<rslang::Auditor>
Schema::MakeAuditor() const {
return std::make_unique<rslang::Auditor>(*this, VCContext(), ASTContext());
[[nodiscard]] std::unique_ptr<SchemaAuditor> Schema::MakeAuditor() const {
return std::make_unique<SchemaAuditor>(*this, VCContext(), ASTContext());
}
void Schema::TriggerParse(const EntityUID target) {
@ -381,14 +384,8 @@ void Schema::TriggerParse(const EntityUID target) {
}
void Schema::ParseCst(const EntityUID target) {
using rslang::Generator;
const auto& cst = At(target);
const auto expr = Generator::GlobalDefinition(cst.alias, cst.definition, cst.type == CstType::structured);
const auto isValid =
auditor->CheckType(expr, rslang::Syntax::MATH)
&& CheckTypeConstistency(auditor->GetType(), cst.type)
&& (IsBaseSet(cst.type) == std::empty(cst.definition));
const auto isValid = auditor->CheckConstituenta(cst.alias, cst.definition, cst.type);
info.at(target).Reset();
info.at(target).status = isValid ? ParsingStatus::VERIFIED : ParsingStatus::INCORRECT;
if (isValid) {
@ -396,24 +393,6 @@ void Schema::ParseCst(const EntityUID target) {
}
}
bool Schema::CheckTypeConstistency(const rslang::ExpressionType& type, const CstType cstType) noexcept {
switch (cstType) {
default: return false;
case CstType::base:
case CstType::constant:
case CstType::structured:
case CstType::function:
case CstType::term: {
return std::holds_alternative<rslang::Typification>(type);
}
case CstType::predicate:
case CstType::axiom:
case CstType::theorem: {
return std::holds_alternative<rslang::LogicT>(type);
}
}
}
void Schema::SaveInfoTo(ParsingInfo& out) {
out.exprType = auditor->GetType();
if (const auto& funcArgs = auditor->GetDeclarationArgs(); !std::empty(funcArgs)) {
@ -422,8 +401,8 @@ void Schema::SaveInfoTo(ParsingInfo& out) {
if (auditor->CheckValue()) {
out.valueClass = auditor->GetValueClass();
}
if (auditor->isParsed) {
out.ast = auditor->parser.ExtractAST();
if (out.status == ParsingStatus::VERIFIED) {
out.ast = auditor->ExtractAST();
}
}

View File

@ -0,0 +1,99 @@
#include "ccl/semantic/SchemaAuditor.h"
#include "ccl/rslang/RSGenerator.h"
namespace ccl::semantic {
SchemaAuditor::SchemaAuditor(
const rslang::TypeContext& types,
rslang::ValueClassContext globalClass,
rslang::SyntaxTreeContext globalAST
) : prefixLen{ 0 }, auditor { types, globalClass, globalAST } {}
bool SchemaAuditor::CheckConstituenta(const std::string& alias, const std::string& definition, const CstType targetType) {
auditor.parser.log.Clear();
const auto expr = rslang::Generator::GlobalDefinition(alias, definition, targetType == CstType::structured);
prefixLen = static_cast<StrPos>(std::ssize(expr) - std::ssize(definition));
const auto isBaseSet = IsBaseSet(targetType);
if (isBaseSet != empty(definition)) {
OnError(isBaseSet ? CstTypeEID::cstNonemptyBase : CstTypeEID::cstEmptyDerived);
return false;
}
if (!auditor.CheckType(expr, rslang::Syntax::MATH)) {
return false;
}
const auto isCallable = IsCallable(targetType);
if (isCallable == std::empty(auditor.GetDeclarationArgs())) {
auditor.isTypeCorrect = false;
OnError(isCallable ? CstTypeEID::cstCallableNoArgs : CstTypeEID::cstNonCallableHasArgs);
return false;
}
const auto& resultType = auditor.GetType();
const auto isLogical = IsLogical(targetType);
if (isLogical == std::holds_alternative<rslang::Typification>(resultType)) {
auditor.isTypeCorrect = false;
OnError(isLogical ? CstTypeEID::cstExpectedLogical : CstTypeEID::cstExpectedTyped);
return false;
}
return true;
}
bool SchemaAuditor::CheckExpression(const std::string& expr, const rslang::Syntax syntax) {
auditor.parser.log.Clear();
return auditor.CheckType(expr, syntax);
}
bool SchemaAuditor::CheckValue() {
return auditor.CheckValue();
}
bool SchemaAuditor::IsParsed() const noexcept {
return auditor.isParsed;
}
bool SchemaAuditor::IsTypeCorrect() const noexcept {
return auditor.isTypeCorrect;
}
bool SchemaAuditor::IsValueCorrect() const noexcept {
return auditor.isValueCorrect;
}
const rslang::Syntax& SchemaAuditor::GetSyntax() const noexcept {
return auditor.parser.syntax;
}
const rslang::SyntaxTree& SchemaAuditor::AST() const noexcept {
return auditor.parser.AST();
}
const rslang::ErrorLogger& SchemaAuditor::Errors() const noexcept {
return auditor.Errors();
}
const rslang::FunctionArguments& SchemaAuditor::GetDeclarationArgs() const noexcept {
return auditor.GetDeclarationArgs();
}
const rslang::ExpressionType& SchemaAuditor::GetType() const noexcept {
return auditor.GetType();
}
rslang::ValueClass SchemaAuditor::GetValueClass() const noexcept {
return auditor.GetValueClass();
}
meta::UniqueCPPtr<rslang::SyntaxTree> SchemaAuditor::ExtractAST() noexcept {
return auditor.parser.ExtractAST();
}
void SchemaAuditor::OnError(const CstTypeEID errorID) {
auditor.parser.log.LogError(rslang::Error{ static_cast<uint32_t>(errorID), 0 });
}
} // namespace ccl::semantic

View File

@ -214,6 +214,7 @@
<ClCompile Include="src\testRelativation.cpp" />
<ClCompile Include="src\testRSCalculationFacet.cpp" />
<ClCompile Include="src\testSchema.cpp" />
<ClCompile Include="src\testSchemaAuditor.cpp" />
<ClCompile Include="src\testSourceManager.cpp" />
<ClCompile Include="src\testSynthes.cpp" />
<ClCompile Include="src\testCstNameGenerator.cpp" />

View File

@ -118,6 +118,9 @@
<ClCompile Include="src\testOperation.cpp">
<Filter>s_Concept\06 OPS</Filter>
</ClCompile>
<ClCompile Include="src\testSchemaAuditor.cpp">
<Filter>s_Concept\01 Schema</Filter>
</ClCompile>
</ItemGroup>
<ItemGroup>
<Filter Include="s_OSS">

View File

@ -84,4 +84,15 @@ TEST_F(UTCstType, IsStatement) {
EXPECT_FALSE(ccl::semantic::IsStatement(CstType::function));
EXPECT_TRUE(ccl::semantic::IsStatement(CstType::theorem));
EXPECT_FALSE(ccl::semantic::IsStatement(CstType::predicate));
}
TEST_F(UTCstType, IsLogical) {
EXPECT_FALSE(ccl::semantic::IsLogical(CstType::base));
EXPECT_FALSE(ccl::semantic::IsLogical(CstType::constant));
EXPECT_FALSE(ccl::semantic::IsLogical(CstType::structured));
EXPECT_TRUE(ccl::semantic::IsLogical(CstType::axiom));
EXPECT_FALSE(ccl::semantic::IsLogical(CstType::term));
EXPECT_FALSE(ccl::semantic::IsLogical(CstType::function));
EXPECT_TRUE(ccl::semantic::IsLogical(CstType::theorem));
EXPECT_TRUE(ccl::semantic::IsLogical(CstType::predicate));
}

View File

@ -131,4 +131,15 @@ TEST_F(UTRSFormJA, CheckExpression) {
EXPECT_EQ(reponse.at("args")[0].at("alias"), "a");
EXPECT_EQ(reponse.at("args")[0].at("typification"), "X1");
}
}
TEST_F(UTRSFormJA, CheckConstituenta) {
auto wrapper = RSFormJA::FromData(SetupSchema());
auto reponse = JSON::parse(wrapper.CheckConstituenta("A100", "X1=X1", CstType::axiom));
EXPECT_EQ(reponse.at("parseResult").get<bool>(), true);
EXPECT_EQ(reponse.at("prefixLen"), 7);
EXPECT_EQ(reponse.at("syntax"), "math");
EXPECT_EQ(reponse.at("typification"), "LOGIC");
EXPECT_EQ(reponse.at("errors").size(), 0U);
}

View File

@ -22,6 +22,7 @@ protected:
using FunctionArguments = ccl::rslang::FunctionArguments;
using ValueClass = ccl::rslang::ValueClass;
using Syntax = ccl::rslang::Syntax;
using TypeID = ccl::rslang::TypedID;
protected:
Schema core{};
@ -722,28 +723,6 @@ TEST_F(UTSchema, Translations) {
}
}
TEST_F(UTSchema, TypeConsistency) {
const Typification rsType{"X1"};
EXPECT_TRUE(Schema::CheckTypeConstistency(rsType, CstType::base));
EXPECT_TRUE(Schema::CheckTypeConstistency(rsType, CstType::constant));
EXPECT_TRUE(Schema::CheckTypeConstistency(rsType, CstType::structured));
EXPECT_TRUE(Schema::CheckTypeConstistency(rsType, CstType::term));
EXPECT_FALSE(Schema::CheckTypeConstistency(rsType, CstType::axiom));
EXPECT_FALSE(Schema::CheckTypeConstistency(rsType, CstType::theorem));
EXPECT_TRUE(Schema::CheckTypeConstistency(rsType, CstType::function));
EXPECT_FALSE(Schema::CheckTypeConstistency(rsType, CstType::predicate));
const LogicT logicType{};
EXPECT_FALSE(Schema::CheckTypeConstistency(logicType, CstType::base));
EXPECT_FALSE(Schema::CheckTypeConstistency(logicType, CstType::constant));
EXPECT_FALSE(Schema::CheckTypeConstistency(logicType, CstType::structured));
EXPECT_FALSE(Schema::CheckTypeConstistency(logicType, CstType::term));
EXPECT_TRUE(Schema::CheckTypeConstistency(logicType, CstType::axiom));
EXPECT_TRUE(Schema::CheckTypeConstistency(logicType, CstType::theorem));
EXPECT_FALSE(Schema::CheckTypeConstistency(logicType, CstType::function));
EXPECT_TRUE(Schema::CheckTypeConstistency(logicType, CstType::predicate));
}
TEST_F(UTSchema, Evaluate) {
{
EXPECT_FALSE(core.Evaluate("X1=X1").has_value());
@ -766,13 +745,13 @@ TEST_F(UTSchema, MakeAuditor) {
{
auto auditor = core.MakeAuditor();
ASSERT_NE(auditor, nullptr);
EXPECT_TRUE(auditor->CheckType(R"(X1 \in B(X1))"_rs, Syntax::MATH));
EXPECT_FALSE(auditor->CheckType(R"(X1 \in B(X1))", Syntax::MATH));
EXPECT_TRUE(auditor->CheckExpression(R"(X1 \in B(X1))"_rs, Syntax::MATH));
EXPECT_FALSE(auditor->CheckExpression(R"(X1 \in B(X1))", Syntax::MATH));
}
{
auto auditor = core.MakeAuditor();
ASSERT_NE(auditor, nullptr);
EXPECT_FALSE(auditor->CheckType(R"(X1 \in B(X1))"_rs, Syntax::ASCII));
EXPECT_TRUE(auditor->CheckType(R"(X1 \in B(X1))", Syntax::ASCII));
EXPECT_FALSE(auditor->CheckExpression(R"(X1 \in B(X1))"_rs, Syntax::ASCII));
EXPECT_TRUE(auditor->CheckExpression(R"(X1 \in B(X1))", Syntax::ASCII));
}
}

View File

@ -0,0 +1,90 @@
#define GTEST_LANG_CXX11 1
#include "gtest/gtest.h"
#include "ccl/semantic/SchemaAuditor.h"
#include "ccl/semantic/Schema.h"
#include "RSLHelper.hpp"
class UTSchemaAuditor : public ::testing::Test {
protected:
UTSchemaAuditor();
protected:
using EntityUID = ccl::EntityUID;
using Schema = ccl::semantic::Schema;
using CstType = ccl::semantic::CstType;
using SchemaAuditor = ccl::semantic::SchemaAuditor;
using Syntax = ccl::rslang::Syntax;
using ValueClass = ccl::rslang::ValueClass;
using Typification = ccl::rslang::Typification;
using LogicT = ccl::rslang::LogicT;
using ExpressionType = ccl::rslang::ExpressionType;
using CstTypeEID = ccl::semantic::CstTypeEID;
using ParsingStatus = ccl::semantic::ParsingStatus;
using ParsingInfo = ccl::semantic::ParsingInfo;
using FunctionArguments = ccl::rslang::FunctionArguments;
using TypeID = ccl::rslang::TypedID;
protected:
Schema core{};
std::unique_ptr<SchemaAuditor> auditor;
static constexpr EntityUID x1{ 42 };
static constexpr EntityUID s1{ 44 };
static constexpr EntityUID d1{ 45 };
static constexpr EntityUID a1{ 46 };
static constexpr EntityUID f1{ 47 };
static constexpr EntityUID p1{ 48 };
void ExpectError(const std::string& alias, const std::string& input, CstType type, CstTypeEID errorCode);
};
UTSchemaAuditor::UTSchemaAuditor() : auditor{core.MakeAuditor()} {
core.Emplace(x1, "X1", CstType::base);
core.Emplace(s1, "S1", CstType::structured, "B(X1*X1)"_rs);
core.UpdateState();
}
void UTSchemaAuditor::ExpectError(
const std::string& alias,
const std::string& input,
const CstType type,
const CstTypeEID errorCode
) {
ASSERT_FALSE(auditor->CheckConstituenta(alias, input, type)) << input;
EXPECT_EQ(begin(auditor->Errors().All())->eid, static_cast<uint32_t>(errorCode)) << input;
}
TEST_F(UTSchemaAuditor, CheckExression) {
EXPECT_TRUE(auditor->CheckExpression(R"(X1=X1)", Syntax::MATH));
EXPECT_TRUE(auditor->CheckExpression(R"(X1 \eq X1)", Syntax::ASCII));
EXPECT_FALSE(auditor->CheckExpression(R"(X2=X2)", Syntax::MATH));
EXPECT_FALSE(auditor->CheckExpression(R"(X1=X1)", Syntax::ASCII));
}
TEST_F(UTSchemaAuditor, CheckConstituentaCorrect) {
EXPECT_TRUE(auditor->CheckConstituenta("X2", "", CstType::base));
EXPECT_TRUE(auditor->CheckConstituenta("C2", "", CstType::constant));
EXPECT_TRUE(auditor->CheckConstituenta("S2", R"(X1)", CstType::structured));
EXPECT_TRUE(auditor->CheckConstituenta("D2", R"(Pr1(S1))", CstType::term));
EXPECT_TRUE(auditor->CheckConstituenta("A2", R"(X1=X1)", CstType::axiom));
EXPECT_TRUE(auditor->CheckConstituenta("T2", R"(X1=X1)", CstType::theorem));
EXPECT_TRUE(auditor->CheckConstituenta("F2", R"([a \in X1] a)"_rs, CstType::function));
EXPECT_TRUE(auditor->CheckConstituenta("P2", R"([a \in X1] a \eq a)"_rs, CstType::predicate));
}
TEST_F(UTSchemaAuditor, CheckConstituentaErrors) {
ExpectError("X2", "1", CstType::base, CstTypeEID::cstNonemptyBase);
ExpectError("D2", "", CstType::term, CstTypeEID::cstEmptyDerived);
ExpectError("F2", "1=1", CstType::function, CstTypeEID::cstCallableNoArgs);
ExpectError("P2", "1=1", CstType::predicate, CstTypeEID::cstCallableNoArgs);
ExpectError("D2", R"([a \in X1] a \eq a)"_rs, CstType::term, CstTypeEID::cstNonCallableHasArgs);
ExpectError("A2", R"([a \in X1] a \eq a)"_rs, CstType::axiom, CstTypeEID::cstNonCallableHasArgs);
ExpectError("A2", R"(X1 \union X1)"_rs, CstType::axiom, CstTypeEID::cstExpectedLogical);
ExpectError("T2", R"(X1 \union X1)"_rs, CstType::theorem, CstTypeEID::cstExpectedLogical);
ExpectError("P2", R"([a \in X1] a)"_rs, CstType::predicate, CstTypeEID::cstExpectedLogical);
ExpectError("D2", R"(1 \eq 1)"_rs, CstType::term, CstTypeEID::cstExpectedTyped);
ExpectError("F2", R"([a \in X1] a \eq a)"_rs, CstType::function, CstTypeEID::cstExpectedTyped);
}

View File

@ -7,6 +7,7 @@
#include "../src/testTextData.cpp"
#include "../src/testRSConcept.cpp"
#include "../src/testSchema.cpp"
#include "../src/testSchemaAuditor.cpp"
#include "../src/testTextConcept.cpp"
#include "../src/testThesaurus.cpp"
#include "../src/testConceptRecord.cpp"

View File

@ -1,6 +1,7 @@
//! Unity build for Concept Core Library
#include "../src/JSON.cpp"
#include "../src/semantic/schema/SchemaAuditor.cpp"
#include "../src/semantic/schema/Schema.cpp"
#include "../src/semantic/schema/RSConcept.cpp"
#include "../src/semantic/thesaurus/Thesaurus.cpp"

View File

@ -207,6 +207,8 @@
<None Include="src\MathLexerImpl.l">
<Filter>11 parse\lexer</Filter>
</None>
<None Include="src\RSParserImpl.y" />
<None Include="src\RSParserImpl.y">
<Filter>11 parse</Filter>
</None>
</ItemGroup>
</Project>

View File

@ -450,40 +450,42 @@ namespace ccl { namespace rslang { namespace detail {
S_SEMICOLON = 60, // SEMICOLON
S_YYACCEPT = 61, // $accept
S_expression = 62, // expression
S_global_declaration = 63, // global_declaration
S_logic_or_setexpr = 64, // logic_or_setexpr
S_function_definition = 65, // function_definition
S_arguments = 66, // arguments
S_declaration = 67, // declaration
S_variable = 68, // variable
S_variable_pack = 69, // variable_pack
S_logic = 70, // logic
S_logic_no_binary = 71, // logic_no_binary
S_logic_all = 72, // logic_all
S_logic_par = 73, // logic_par
S_logic_predicates = 74, // logic_predicates
S_binary_predicate = 75, // binary_predicate
S_logic_unary = 76, // logic_unary
S_quantifier = 77, // quantifier
S_logic_binary = 78, // logic_binary
S_setexpr = 79, // setexpr
S_text_function = 80, // text_function
S_setexpr_enum = 81, // setexpr_enum
S_setexpr_enum_min2 = 82, // setexpr_enum_min2
S_literal = 83, // literal
S_identifier = 84, // identifier
S_setexpr_binary = 85, // setexpr_binary
S_setexpr_generators = 86, // setexpr_generators
S_enumeration = 87, // enumeration
S_tuple = 88, // tuple
S_boolean = 89, // boolean
S_filter_expression = 90, // filter_expression
S_declarative = 91, // declarative
S_recursion = 92, // recursion
S_imperative = 93, // imperative
S_imp_blocks = 94, // imp_blocks
S_RPE = 95, // RPE
S_RCE = 96 // RCE
S_no_declaration = 63, // no_declaration
S_global_declaration = 64, // global_declaration
S_logic_or_setexpr = 65, // logic_or_setexpr
S_function_definition = 66, // function_definition
S_arguments = 67, // arguments
S_declaration = 68, // declaration
S_variable = 69, // variable
S_variable_pack = 70, // variable_pack
S_logic = 71, // logic
S_logic_no_binary = 72, // logic_no_binary
S_logic_all = 73, // logic_all
S_logic_par = 74, // logic_par
S_logic_predicates = 75, // logic_predicates
S_binary_predicate = 76, // binary_predicate
S_logic_unary = 77, // logic_unary
S_quantifier = 78, // quantifier
S_logic_binary = 79, // logic_binary
S_setexpr = 80, // setexpr
S_text_function = 81, // text_function
S_setexpr_enum = 82, // setexpr_enum
S_setexpr_enum_min2 = 83, // setexpr_enum_min2
S_global_name = 84, // global_name
S_literal = 85, // literal
S_identifier = 86, // identifier
S_setexpr_binary = 87, // setexpr_binary
S_setexpr_generators = 88, // setexpr_generators
S_enumeration = 89, // enumeration
S_tuple = 90, // tuple
S_boolean = 91, // boolean
S_filter_expression = 92, // filter_expression
S_declarative = 93, // declarative
S_recursion = 94, // recursion
S_imperative = 95, // imperative
S_imp_blocks = 96, // imp_blocks
S_RPE = 97, // RPE
S_RCE = 98 // RCE
};
};
@ -981,9 +983,9 @@ namespace ccl { namespace rslang { namespace detail {
/// Constants.
enum
{
yylast_ = 620, ///< Last index in yytable_.
yynnts_ = 36, ///< Number of nonterminal symbols.
yyfinal_ = 89 ///< Termination state number.
yylast_ = 567, ///< Last index in yytable_.
yynnts_ = 38, ///< Number of nonterminal symbols.
yyfinal_ = 85 ///< Termination state number.
};
@ -995,7 +997,7 @@ namespace ccl { namespace rslang { namespace detail {
#line 15 "RSParserImpl.y"
} } } // ccl::rslang::detail
#line 999 "../header/RSParserImpl.h"
#line 1001 "../header/RSParserImpl.h"

View File

@ -20,9 +20,11 @@ private:
ValueAuditor valueAuditor;
public:
explicit Auditor(const TypeContext& types,
ValueClassContext globalClass,
SyntaxTreeContext globalAST);
explicit Auditor(
const TypeContext& types,
ValueClassContext globalClass,
SyntaxTreeContext globalAST
);
public:
bool CheckType(const std::string& expr, Syntax syntaxHint = Syntax::UNDEF);

View File

@ -50,9 +50,6 @@ enum class SemanticEID : uint32_t {
invalidArgumentType = 0x8819, // Типизация аргумента не совпадает с объявленной
globalStructure = 0x881C, // Родовая структура должна быть ступенью
// TODO: следующий идентификатор сейчас не используется. Нужно подобрать место для проверки
globalExpectedFunction = 0x881F, // Ожидалось выражение объявления функции
radicalUsage = 0x8821, // Радикалы запрещены вне деклараций терм-функций
invalidFilterArgumentType = 0x8822, // Типизация аргумента фильтра не корректна
invalidFilterArity = 0x8823, // Количество параметров фильра не соответствует количеству индексов

File diff suppressed because it is too large Load Diff

View File

@ -268,16 +268,18 @@ RawNode Imperative(
// ------------------------- Language Expression ------------------------------
expression
: global_declaration
| logic_or_setexpr { if(!state->FinalizeExpression($1)) YYABORT; }
| function_definition { if(!state->FinalizeExpression($1)) YYABORT; }
| no_declaration { if(!state->FinalizeExpression($1)) YYABORT; }
;
no_declaration
: logic_or_setexpr
| function_definition
;
global_declaration
: GLOBAL DEFINE { if(!state->FinalizeCstEmpty($1, $2)) YYABORT; }
| GLOBAL STRUCT setexpr { if(!state->FinalizeCstExpression($1, $2, $3)) YYABORT; }
| GLOBAL DEFINE logic_or_setexpr { if(!state->FinalizeCstExpression($1, $2, $3)) YYABORT; }
| FUNCTION DEFINE function_definition { if(!state->FinalizeCstExpression($1, $2, $3)) YYABORT; }
| PREDICATE DEFINE function_definition { if(!state->FinalizeCstExpression($1, $2, $3)) YYABORT; }
: global_name DEFINE { if(!state->FinalizeCstEmpty($1, $2)) YYABORT; }
| global_name DEFINE no_declaration { if(!state->FinalizeCstExpression($1, $2, $3)) YYABORT; }
| global_name STRUCT no_declaration { if(!state->FinalizeCstExpression($1, $2, $3)) YYABORT; }
;
logic_or_setexpr
@ -394,6 +396,12 @@ setexpr_enum_min2
: setexpr_enum COMMA setexpr { $$ = Enumeration(TokenID::INTERRUPT, $1, $3); }
;
global_name
: GLOBAL
| FUNCTION
| PREDICATE
;
literal
: INTEGER
| EMPTYSET
@ -401,9 +409,7 @@ literal
;
identifier
: GLOBAL
| FUNCTION
| PREDICATE
: global_name
| LOCAL
| RADICAL
;

View File

@ -333,6 +333,7 @@ bool TypeAuditor::ViGlobalDeclaration(Cursor iter) {
}
bool TypeAuditor::ViFunctionDefinition(Cursor iter) {
StartScope();
{
const auto guard = isFuncDeclaration.CreateGuard();
if (!VisitChild(iter, 0)) {
@ -348,6 +349,7 @@ bool TypeAuditor::ViFunctionDefinition(Cursor iter) {
if (!type.has_value()) {
return false;
}
EndScope(iter->pos.start);
return SetCurrent(type.value());
}

View File

@ -85,14 +85,26 @@ TEST_F(UTRSParser, GlobalDeclCorrect) {
ExpectNoWarnings(R"(S1 \defexpr B(C1))");
ExpectNoWarnings(R"(S1 \defexpr B(D1))");
ExpectNoWarnings(R"(S1 \defexpr B(X1*(X1*X1)))");
ExpectNoWarnings(R"(F1 \defexpr B(X1*(X1*X1)))");
ExpectNoWarnings(R"(D1 \defexpr B(X1*(X1*X1)))");
ExpectNoWarnings(R"(P1 \defexpr B(X1*(X1*X1)))");
ExpectNoWarnings(R"(D1 \defexpr X1 \setminus X1)");
ExpectNoWarnings(R"(A1 \defexpr X1 \setminus X1)");
ExpectNoWarnings(R"(F1 \defexpr X1 \setminus X1)");
ExpectNoWarnings(R"(P1 \defexpr X1 \setminus X1)");
ExpectNoWarnings(R"(A1 \defexpr 1 \eq 1)");
ExpectNoWarnings(R"(T1 \defexpr 1 \eq 1)");
ExpectNoWarnings(R"(F1 \defexpr 1 \eq 1)");
ExpectNoWarnings(R"(D1 \defexpr 1 \eq 1)");
ExpectNoWarnings(R"(S1 \defexpr [a \in X1] X1 \setminus a)");
ExpectNoWarnings(R"(D1 \defexpr [a \in X1] X1 \setminus a)");
ExpectNoWarnings(R"(F1 \defexpr [a \in X1] X1 \setminus a)");
ExpectNoWarnings(R"(F1 \defexpr [a \in R1] {a})");
ExpectNoWarnings(R"(F1 \defexpr [a \in B(D1)] X1 \setminus a)");
ExpectNoWarnings(R"(F1 \defexpr [a \in D1 \setminus D1] X1 \setminus a)");
ExpectNoWarnings(R"(P1 \defexpr [a \in D1 \setminus D1] 1 \eq 1)");
ExpectNoWarnings(R"(D1 \defexpr [a \in D1 \setminus D1] 1 \eq 1)");
ExpectNoWarnings(R"(S1 \defexpr [a \in D1 \setminus D1] 1 \eq 1)");
ExpectNoWarnings(R"(F1 \defexpr [a \in B(X1)] card(a))");
}
@ -123,10 +135,6 @@ TEST_F(UTRSParser, GlobalDeclErrors) {
ExpectError(R"(F1 \defexpr [] X1 \setminus X1)", ParseEID::expectedDeclaration, 13);
ExpectError(R"(F1 \defexpr [a] X1 \setminus a)", ParseEID::expectedDeclaration, 14);
ExpectError(R"(F1 \defexpr [a \subseteq X1] X1 \setminus a)", ParseEID::expectedDeclaration, 15);
ExpectError(R"(S1 \deftype 1 \eq 1)", ParseEID::syntax);
ExpectError(R"(F1 \defexpr )", ParseEID::syntax);
ExpectError(R"(F1 \defexpr 1 \eq 1)", ParseEID::syntax);
ExpectError(R"(F1 \defexpr X1)", ParseEID::syntax);
}
TEST_F(UTRSParser, LogicPredicatesCorrect) {

View File

@ -86,7 +86,8 @@ TEST_F(UTRSToken, TokenDefault) {
}
TEST_F(UTRSToken, TokenCompare) {
Token t1{}, t2{};
Token t1{};
Token t2{};
EXPECT_EQ(t1, t2);
t2.id = TokenID::PUNC_DEFINE;

View File

@ -127,6 +127,8 @@ TEST_F(UTTypeAuditor, DefinitionsCorrect) {
TEST_F(UTTypeAuditor, DefinitionsErrors) {
ExpectError(R"(S1 \deftype R1)", SemanticEID::globalStructure);
ExpectError(R"(S1 \deftype 1)", SemanticEID::globalStructure);
ExpectError(R"(S1 \deftype 1 \eq 1)", SemanticEID::globalStructure);
ExpectError(R"(S1 \deftype [a \in X1] a \eq a)", SemanticEID::globalStructure);
ExpectError(R"(S1 \deftype X1 \union X1)", SemanticEID::globalStructure);
ExpectError(R"(S1 \deftype B(X1 \union X1))", SemanticEID::globalStructure);
ExpectError(R"(S1 \deftype X1*(X1 \union X1))", SemanticEID::globalStructure);
@ -519,6 +521,14 @@ TEST_F(UTTypeAuditor, WarningLocalNotUsed) {
EXPECT_EQ(begin(parser.log.All())->eid, static_cast<uint32_t>(SemanticEID::localNotUsed));
}
TEST_F(UTTypeAuditor, WarningParameterNotUsed) {
const auto input = R"([a \in X1] 1 \eq 1)";
ASSERT_TRUE(parser.Parse(input, Syntax::ASCII));
ASSERT_TRUE(analyse.CheckType(parser.AST()));
EXPECT_EQ(parser.log.Count(ErrorStatus::WARNING), 1);
EXPECT_EQ(begin(parser.log.All())->eid, static_cast<uint32_t>(SemanticEID::localNotUsed));
}
TEST_F(UTTypeAuditor, NoWarningAfterError) {
const auto input = R"(D{t \in X1 | \A a \in X1 \A b \in red(X1) {a,b} \eq t})";
ASSERT_TRUE(parser.Parse(input, Syntax::ASCII));

View File

@ -19,6 +19,13 @@ Here we write upgrading notes. Make them as straightforward as possible.
### Fixed
## [0.1.7] - 2024-09-22
### Fixed
- Improve error messages for invalid types
- Add API for checking constituenta expressions
## [0.1.6] - 2024-06-14
### Fixed

View File

@ -1 +1 @@
0.1.6
0.1.7

View File

@ -15,6 +15,12 @@ std::string ConvertToMath(const std::string& expression);
// ======= Expression parse =========
std::string ParseExpression(const std::string& expression);
std::string CheckExpression(const std::string& jSchema, const std::string& expression);
std::string CheckConstituenta(
const std::string& jSchema,
const std::string& alias,
const std::string& expression,
int cstType
);
PYBIND11_MODULE(pyconcept, m) {
m.def("check_schema", &CheckSchema, R"pbdoc(Check schema definition.)pbdoc");
@ -24,5 +30,14 @@ PYBIND11_MODULE(pyconcept, m) {
m.def("convert_to_math", &ConvertToMath, R"pbdoc(Convert expression syntax to Math.)pbdoc");
m.def("parse_expression", &ParseExpression, R"pbdoc(Parse expression and create syntax tree.)pbdoc");
m.def("check_expression", &CheckExpression, R"pbdoc(Validate expression against given schema and calculate typification.)pbdoc");
m.def(
"check_expression",
&CheckExpression,
R"pbdoc(Validate expression against given schema and calculate typification.)pbdoc"
);
m.def(
"check_constituenta",
&CheckConstituenta,
R"pbdoc(Validate constituenta expression against given schema and calculate typification.)pbdoc"
);
}

View File

@ -7,7 +7,6 @@
using ccl::api::RSFormJA;
std::string CheckSchema(const std::string& jSchema) {
// TODO: consider try-catch if need to process invalid input gracefully
ccl::lang::TextEnvironment::Instance().skipResolving = true;
auto schema = RSFormJA::FromJSON(jSchema);
return schema.ToJSON();
@ -35,4 +34,14 @@ std::string ParseExpression(const std::string& expression) {
std::string CheckExpression(const std::string& jSchema, const std::string& expression) {
auto schema = RSFormJA::FromJSON(jSchema);
return schema.CheckExpression(expression);
}
std::string CheckConstituenta(
const std::string& jSchema,
const std::string& alias,
const std::string& expression,
int cstType
) {
auto schema = RSFormJA::FromJSON(jSchema);
return schema.CheckConstituenta(alias, expression, static_cast<ccl::semantic::CstType>(cstType));
}

View File

@ -55,6 +55,15 @@ class TestBinding(unittest.TestCase):
out2 = json.loads(pc.check_expression(schema, 'X1=X2'))
self.assertEqual(out2['parseResult'], False)
def test_check_constituenta(self):
''' Test checking expression against given schema '''
schema = self._get_default_schema()
out1 = json.loads(pc.check_constituenta(schema, 'A100', 'X1=X1', 5))
self.assertEqual(out1['parseResult'], True)
out2 = json.loads(pc.check_constituenta(schema, 'A100', 'X1=X2', 5))
self.assertEqual(out2['parseResult'], False)
def test_reset_aliases(self):
''' Test reset aliases in schema '''