Skip to content

Commit

Permalink
Remove comments referring to LLVM Backend code
Browse files Browse the repository at this point in the history
  • Loading branch information
tothtamas28 committed Nov 29, 2024
1 parent c61dc47 commit c62709e
Showing 1 changed file with 0 additions and 15 deletions.
15 changes: 0 additions & 15 deletions pyk/src/pyk/kore/rule.py
Original file line number Diff line number Diff line change
@@ -1,8 +1,3 @@
"""Parse KORE axioms into rewrite rules.
Based on the [LLVM Backend's implementation](https://github.com/runtimeverification/llvm-backend/blob/d5eab4b0f0e610bc60843ebb482f79c043b92702/lib/ast/pattern_matching.cpp).
"""

from __future__ import annotations

from abc import ABC
Expand Down Expand Up @@ -118,11 +113,6 @@ def from_axiom(axiom: Axiom) -> RewriteRule:

@staticmethod
def _extract(axiom: Axiom) -> tuple[App, App, Pattern | None, Pattern | None, EVar | None]:
# Cases 0-5 of get_left_hand_side
# Cases 5-10 of get_requires
# Case 2 of get_right_hand_side:
# 2: rhs(\rewrites(_, \and(X, Y))) = get_builtin(\and(X, Y))
# Below is a special case without get_builtin
match axiom.pattern:
case Rewrites(left=And(ops=(_lhs, _req)), right=_rhs):
pass
Expand Down Expand Up @@ -172,9 +162,6 @@ def from_axiom(axiom: Axiom) -> FunctionRule:

@staticmethod
def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None]:
# Cases 7-10 of get_left_hand_side
# Cases 0-3 of get_requires
# Case 0 of get_right_hand_side
match axiom.pattern:
case Implies(
left=And(
Expand Down Expand Up @@ -224,8 +211,6 @@ def from_axiom(axiom: Axiom) -> SimpliRule:

@staticmethod
def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None]:
# Cases 11-12 of get_left_hand_side
# Case 0 of get_right_hand_side
match axiom.pattern:
case Implies(left=_req, right=Equals(left=App() as lhs, right=_rhs)):
req = _extract_condition(_req)
Expand Down

0 comments on commit c62709e

Please sign in to comment.