| 0 | 0 |
# TODO: these should probably come from a "eqthy.hints" module
|
| 1 | |
from eqthy.parser import Reflexivity, Substitution, Congruence
|
|
1 |
from eqthy.parser import Reflexivity, Substitution, Congruence, Reference
|
| 2 | 2 |
from eqthy.terms import Eqn, all_matches, expand, subterm_at_index, update_at_index, render, RewriteRule, replace
|
| 3 | 3 |
|
| 4 | 4 |
|
|
| 59 | 59 |
raise DerivationError("No step in proof showed {}".format(render(theorem.eqn)))
|
| 60 | 60 |
|
| 61 | 61 |
def obtain_rewritten_step(self, step, prev):
|
|
62 |
rules_to_try = self.rules
|
| 62 | 63 |
if step.hint is not None:
|
| 63 | 64 |
self.log("==> step has hint {}", step.hint)
|
| 64 | |
result = self.resolve_step_hint(step, prev)
|
|
65 |
result = self.resolve_step_hint(step, prev, rules_to_try)
|
| 65 | 66 |
if result:
|
| 66 | 67 |
return result
|
| 67 | 68 |
|
| 68 | 69 |
# if no hint or hint resolution punted, search for rule to apply
|
| 69 | 70 |
|
| 70 | |
for rule in self.rules:
|
|
71 |
for rule in rules_to_try:
|
| 71 | 72 |
self.log(" Trying to rewrite lhs {} with {}", render(prev.eqn.lhs), render(rule))
|
| 72 | 73 |
for rewritten_lhs in self.all_rewrites(rule, prev.eqn.lhs):
|
| 73 | 74 |
self.log(" Using {}, rewrote {} to {}", render(rule), render(prev.eqn.lhs), render(rewritten_lhs))
|
|
| 84 | 85 |
self.log(" Can rewrite rhs to obtain: {}", render(rewritten_eqn))
|
| 85 | 86 |
return rewritten_eqn
|
| 86 | 87 |
|
| 87 | |
def resolve_step_hint(self, step, prev):
|
|
88 |
def resolve_step_hint(self, step, prev, rules_to_try):
|
|
89 |
"""`rules_to_try` is passed by reference, expected to perhaps be modified"""
|
| 88 | 90 |
if isinstance(step.hint, Substitution):
|
| 89 | 91 |
# replace all occurrences of variable in step with term
|
| 90 | 92 |
rewritten_eqn = Eqn(
|
|
| 110 | 112 |
return step.eqn
|
| 111 | 113 |
else:
|
| 112 | 114 |
raise DerivationError("Could not derive {} from Reflexivity".format(render(step.eqn)))
|
|
115 |
elif isinstance(step.hint, Reference):
|
|
116 |
# TODO: narrow down rules_to_try
|
|
117 |
return None
|
| 113 | 118 |
else:
|
| 114 | |
# TODO do other checking on this hint instead of ignoring it
|
| 115 | |
self.log("==> step has unacted-upon hint {}", step.hint)
|
|
119 |
raise NotImplementedError(str(step.hint))
|
| 116 | 120 |
|
| 117 | 121 |
def all_rewrites(self, rule, term):
|
| 118 | 122 |
"""Given a term, and a rule, return a list of the terms that would result
|