Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Pattern matching improvements #938

Closed
wants to merge 5 commits into from
Closed

Pattern matching improvements #938

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
8dfb905
Implement matchesShape
Baltoli Dec 18, 2023
5485455
Begin refactoring getLeftHandSide
Baltoli Dec 18, 2023
ff5b827
Continue to refactor getLeftHandSide
Baltoli Dec 18, 2023
767eb6a
Continue to refactor getLeftHandSide
Baltoli Dec 18, 2023
f94daff
Continue to refactor getLeftHandSide
Baltoli Dec 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions include/kllvm/ast/AST.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -428,6 +428,21 @@ class KOREPattern : public std::enable_shared_from_this<KOREPattern> {
*/
virtual sptr<KOREPattern> desugarAssociative() = 0;

/**
* Abstracts the common pattern of checking whether a composite pattern has a
* particular top-level constructor and arity. For example:
*
* c(A, B) -> matchesShape(c, 2) == true
* c() -> matchesShape(c, 2) == false
* c() -> matchesShape(b, 0) == false
*
* For instances of KORECompositePattern, return this if the constructor and
* arity and match. For all other subclasses, and when they do not match,
* return nullptr;
*/
virtual sptr<KORECompositePattern>
matchesShape(std::string const &constructor, size_t arity) = 0;

friend KORECompositePattern;

private:
Expand Down Expand Up @@ -500,6 +515,11 @@ class KOREVariablePattern : public KOREPattern {
return shared_from_this();
}

sptr<KORECompositePattern>
matchesShape(std::string const &constructor, size_t arity) override {
return nullptr;
}

virtual bool matches(
substitution &subst, SubsortMap const &, SymbolMap const &,
sptr<KOREPattern> subject) override;
Expand Down Expand Up @@ -584,6 +604,9 @@ class KORECompositePattern : public KOREPattern {
substitution &, SubsortMap const &, SymbolMap const &,
sptr<KOREPattern>) override;

sptr<KORECompositePattern>
matchesShape(std::string const &constructor, size_t arity) override;

private:
virtual sptr<KOREPattern> expandMacros(
SubsortMap const &, SymbolMap const &,
Expand Down Expand Up @@ -654,6 +677,11 @@ class KOREStringPattern : public KOREPattern {
substitution &, SubsortMap const &, SymbolMap const &,
sptr<KOREPattern> subject) override;

sptr<KORECompositePattern>
matchesShape(std::string const &constructor, size_t arity) override {
return nullptr;
}

private:
virtual sptr<KOREPattern> expandMacros(
SubsortMap const &, SymbolMap const &,
Expand Down
187 changes: 82 additions & 105 deletions lib/ast/AST.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -406,6 +406,16 @@ sptr<KOREPattern> KORECompositePattern::expandAliases(KOREDefinition *def) {
return ptr;
}

sptr<KORECompositePattern> KORECompositePattern::matchesShape(
std::string const &constructor, size_t arity) {
if (getConstructor()->getName() == constructor
&& getArguments().size() == arity) {
return std::dynamic_pointer_cast<KORECompositePattern>(shared_from_this());
}

return nullptr;
}

static int indent = 0;
static bool atNewLine = true;

Expand Down Expand Up @@ -1375,120 +1385,87 @@ getPatterns(KOREPattern *pat, std::vector<KOREPattern *> &result) {
* lhs(\implies(\equals(_, _), \equals(_(Xs), _))) = Xs
*/
std::vector<KOREPattern *> KOREAxiomDeclaration::getLeftHandSide() const {
if (auto top = dynamic_cast<KORECompositePattern *>(pattern.get())) {
if (top->getConstructor()->getName() == "\\rewrites"
&& top->getArguments().size() == 2) {
if (auto andPattern = dynamic_cast<KORECompositePattern *>(
top->getArguments()[0].get())) {
if (andPattern->getConstructor()->getName() == "\\and"
&& andPattern->getArguments().size() == 2) {
if (auto firstChild = dynamic_cast<KORECompositePattern *>(
andPattern->getArguments()[0].get())) {
if (firstChild->getConstructor()->getName() == "\\equals"
&& firstChild->getArguments().size() == 2) {
return {andPattern->getArguments()[1].get()};
} else if (
firstChild->getConstructor()->getName() == "\\top"
&& firstChild->getArguments().size() == 0) {
return {andPattern->getArguments()[1].get()};
} else {
if (auto secondChild = dynamic_cast<KORECompositePattern *>(
andPattern->getArguments()[1].get())) {
if (secondChild->getConstructor()->getName() == "\\equals"
&& secondChild->getArguments().size() == 2) {
return {firstChild};
} else if (
secondChild->getConstructor()->getName() == "\\top"
&& secondChild->getArguments().size() == 0) {
return {firstChild};
} else {
if (firstChild->getConstructor()->getName() == "\\not"
&& firstChild->getArguments().size() == 1
&& secondChild->getConstructor()->getName() == "\\and"
&& secondChild->getArguments().size() == 2) {
if (auto inner = dynamic_cast<KORECompositePattern *>(
secondChild->getArguments()[0].get())) {
if (inner->getConstructor()->getName() == "\\equals"
&& inner->getArguments().size() == 2) {
return {secondChild->getArguments()[1].get()};
} else if (
inner->getConstructor()->getName() == "\\top"
&& inner->getArguments().size() == 0) {
return {secondChild->getArguments()[1].get()};
}
}
}
}
}
}
}
if (auto top = pattern->matchesShape("\\rewrites", 2)) {
if (auto andPattern = top->getArguments()[0]->matchesShape("\\and", 2)) {
auto &firstChild = andPattern->getArguments()[0];
auto &secondChild = andPattern->getArguments()[1];

if (firstChild->matchesShape("\\equals", 2)
|| firstChild->matchesShape("\\top", 0)) {
return {secondChild.get()};
}

if (secondChild->matchesShape("\\equals", 2)
|| secondChild->matchesShape("\\top", 0)) {
return {firstChild.get()};
}

if (auto secondAnd = secondChild->matchesShape("\\and", 2);
secondAnd && firstChild->matchesShape("\\not", 1)) {
auto &inner = secondAnd->getArguments()[0];

if (inner->matchesShape("\\equals", 2)
|| inner->matchesShape("\\top", 0)) {
return {secondAnd->getArguments()[1].get()};
}
}
} else if (
top->getConstructor()->getName() == "\\equals"
&& top->getArguments().size() == 2) {
if (auto firstChild = dynamic_cast<KORECompositePattern *>(
top->getArguments()[0].get())) {
std::vector<KOREPattern *> result;
for (auto &sptr : firstChild->getArguments()) {
result.push_back(sptr.get());
}
}

if (auto top = pattern->matchesShape("\\equals", 2)) {
if (auto firstChild = std::dynamic_pointer_cast<KORECompositePattern>(
top->getArguments()[0])) {
auto result = std::vector<KOREPattern *>{};

for (auto &sptr : firstChild->getArguments()) {
result.push_back(sptr.get());
}

return result;
}
}

if (auto top = pattern->matchesShape("\\implies", 2)) {
auto &impliesLhs = top->getArguments()[0];
auto &impliesRhs = top->getArguments()[1];

if (auto firstChild = impliesLhs->matchesShape("\\and", 2)) {
auto lhsAnd = firstChild;

if (auto innerFirst
= firstChild->getArguments()[0]->matchesShape("\\not", 1)) {
if (auto innerSecond = std::dynamic_pointer_cast<KORECompositePattern>(
firstChild->getArguments()[1])) {
lhsAnd = innerSecond;
}
return result;
}
} else if (
top->getConstructor()->getName() == "\\implies"
&& top->getArguments().size() == 2) {
if (auto firstChild = dynamic_cast<KORECompositePattern *>(
top->getArguments()[0].get())) {
if (firstChild->getConstructor()->getName() == "\\and"
&& firstChild->getArguments().size() == 2) {
auto lhsAnd = firstChild;
if (auto innerFirst = dynamic_cast<KORECompositePattern *>(
firstChild->getArguments()[0].get())) {
if (innerFirst->getConstructor()->getName() == "\\not"
&& innerFirst->getArguments().size() == 1) {
if (auto innerSecond = dynamic_cast<KORECompositePattern *>(
firstChild->getArguments()[1].get())) {
lhsAnd = innerSecond;
}
}
}
if (auto sideCondition = dynamic_cast<KORECompositePattern *>(
lhsAnd->getArguments()[0].get())) {
if (sideCondition->getConstructor()->getName() == "\\equals"
&& sideCondition->getArguments().size() == 2) {
std::vector<KOREPattern *> result;
return getPatterns(lhsAnd->getArguments()[1].get(), result);
} else if (
sideCondition->getConstructor()->getName() == "\\top"
&& sideCondition->getArguments().size() == 0) {
std::vector<KOREPattern *> result;
return getPatterns(lhsAnd->getArguments()[1].get(), result);
}
}
} else if (
(firstChild->getConstructor()->getName() == "\\top"
&& firstChild->getArguments().size() == 0)
|| (firstChild->getConstructor()->getName() == "\\equals"
&& firstChild->getArguments().size() == 2)) {
if (auto secondChild = dynamic_cast<KORECompositePattern *>(
top->getArguments()[1].get())) {
if (secondChild->getConstructor()->getName() == "\\equals"
&& secondChild->getArguments().size() == 2) {
if (auto lhs = dynamic_cast<KORECompositePattern *>(
secondChild->getArguments()[0].get())) {
std::vector<KOREPattern *> result;
for (auto &sptr : lhs->getArguments()) {
result.push_back(sptr.get());
}
return result;
}
}

auto &sideCondition = lhsAnd->getArguments()[0];
if (sideCondition->matchesShape("\\equals", 2)
|| sideCondition->matchesShape("\\top", 0)) {

std::vector<KOREPattern *> result;
return getPatterns(lhsAnd->getArguments()[1].get(), result);
}
}

if (impliesLhs->matchesShape("\\top", 0)
|| impliesLhs->matchesShape("\\equals", 2)) {
if (auto secondChild = impliesRhs->matchesShape("\\equals", 2)) {
if (auto lhs = std::dynamic_pointer_cast<KORECompositePattern>(
secondChild->getArguments()[0])) {

auto result = std::vector<KOREPattern *>{};
for (auto &sptr : lhs->getArguments()) {
result.push_back(sptr.get());
}

return result;
}
}
}
}

assert(false && "could not compute left hand side of axiom");
abort();
}
Expand Down
Loading