-
Notifications
You must be signed in to change notification settings - Fork 153
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.
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
Calculate used variable names better in buildRule #2698
Conversation
pyk/src/pyk/cterm.py
Outdated
def with_constraint(self, new_constraint: KInner) -> 'CTerm': | ||
return CTerm(mlAnd([self.config, new_constraint] + list(self.constraints), Sorts.GENERATED_TOP_CELL)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd call it add_constraint
instead. To me, with_constraint
suggests "take the configuration, and couple it with the constraint provided."
def with_constraint(self, new_constraint: KInner) -> 'CTerm': | |
return CTerm(mlAnd([self.config, new_constraint] + list(self.constraints), Sorts.GENERATED_TOP_CELL)) | |
def add_constraint(self, constraint: KInner) -> 'CTerm': | |
return CTerm(mlAnd((self.config, constraint) + self.constraints, Sorts.GENERATED_TOP_CELL)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done.
pyk/src/pyk/cterm.py
Outdated
constraints = CTerm._normalize_constraints(flattenLabel('#And', constraint)) | ||
object.__setattr__(self, 'config', config) | ||
object.__setattr__(self, 'constraints', constraints) | ||
|
||
@staticmethod | ||
def _split_config_and_constraints(kast: KInner) -> Tuple[KInner, KInner]: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As a first step, I'd just move this to cterm.py
. Later, when we are ready to eliminate calls to the function, e.g. by replacing
config, constraint = split_config_and_constraints(term)
by
config, *constraints = Cterm(term)
constraint = mlAnd(constraints)
we can make it a private static method.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good.
This PR does several things:
splitConfigAndConstraint
to insideCTerm
, so now there are no dependencies ofcterm.py
onkastManip.py
.buildRule
, and renames method tobuild_rule
.build_rule
to operate overCTerm
, instead of overKInner
.build_rule
is producing variable names in the rule which cause the frontend to emit warnings.build_rule
is naming variables poorly.with_constraint
toCTerm
for easily making newCTerm
with an added constraint.build_rule
that becomes redundant with the added tests here.test_configuration.py
tests into unit tests undertest_kastManip.py
so they don't build definitions every time (they don't need to).The main change to
buildRule
is that if you have a rule:It will now realize that
K_CELL
should be anonymous, and rename it to_K_CELL
before feeding it to the frontend. This is to avoid a bunch of frontend warnings.