1 | 1 |
# This file is distributed under a 2-clause BSD license. See LICENSES directory:
|
2 | 2 |
# SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Eqthy
|
3 | 3 |
|
4 | |
from typing import Dict, Union, Any
|
|
4 |
from typing import Dict, Tuple, Union, Any
|
5 | 5 |
|
6 | 6 |
from eqthy.objects import (
|
7 | 7 |
Document, Theorem, Step,
|
|
63 | 63 |
))
|
64 | 64 |
|
65 | 65 |
if rewritten_eqn == theorem.eqn:
|
66 | |
self.log("With {} we have now shown the theorem {}".format(render(rewritten_eqn), render(theorem.eqn)))
|
|
66 |
self.log("With {} we have now shown the theorem {}", render(rewritten_eqn), render(theorem.eqn))
|
67 | 67 |
eqn_shown = True
|
68 | 68 |
prev = step
|
69 | 69 |
|
|
71 | 71 |
raise DerivationError("No step in proof of {} showed {}".format(theorem.name, render(theorem.eqn)))
|
72 | 72 |
|
73 | 73 |
def obtain_rewritten_step(self, step: Step, prev: Step) -> Union[Eqn, None]:
|
|
74 |
try_lhs = True
|
|
75 |
try_rhs = True
|
74 | 76 |
rules_to_try = self.rules
|
75 | 77 |
if step.hint is not None:
|
76 | 78 |
self.log("==> step has hint {}", step.hint)
|
77 | 79 |
result = self.resolve_step_hint(step, prev)
|
78 | 80 |
if result:
|
79 | 81 |
return result
|
80 | |
result2 = self.narrow_rule_search(step)
|
81 | |
if result2:
|
82 | |
rules_to_try = result2
|
|
82 |
if isinstance(step.hint, Reference):
|
|
83 |
rules_to_try, try_lhs, try_rhs = self.narrow_search_using_reference(step.hint)
|
83 | 84 |
|
84 | 85 |
# if no hint or hint resolution punted, search for rule to apply
|
85 | 86 |
|
86 | 87 |
for (name, rule) in rules_to_try.items():
|
87 | |
self.log(" Trying to rewrite lhs {} with:\n {}", render(prev.eqn.lhs), render(rule))
|
88 | |
for rewritten_lhs in all_rewrites(rule.pattern, rule.substitution, prev.eqn.lhs):
|
89 | |
self.log(" ! Rewrote to {}", render(rewritten_lhs))
|
90 | |
rewritten_eqn = Eqn(rewritten_lhs, prev.eqn.rhs)
|
91 | |
if step.eqn == rewritten_eqn:
|
92 | |
self.log(" !! Can rewrite lhs to obtain: {}", render(rewritten_eqn))
|
93 | |
return rewritten_eqn
|
|
88 |
if try_lhs:
|
|
89 |
self.log(" Trying to rewrite lhs {} with:\n {}", render(prev.eqn.lhs), render(rule))
|
|
90 |
for rewritten_lhs in all_rewrites(rule.pattern, rule.substitution, prev.eqn.lhs):
|
|
91 |
self.log(" ! Rewrote to {}", render(rewritten_lhs))
|
|
92 |
rewritten_eqn = Eqn(rewritten_lhs, prev.eqn.rhs)
|
|
93 |
if step.eqn == rewritten_eqn:
|
|
94 |
self.log(" !! Can rewrite lhs to obtain: {}", render(rewritten_eqn))
|
|
95 |
return rewritten_eqn
|
94 | 96 |
|
95 | |
self.log(" Trying to rewrite rhs {} with:\n {}", render(prev.eqn.rhs), render(rule))
|
96 | |
for rewritten_rhs in all_rewrites(rule.pattern, rule.substitution, prev.eqn.rhs):
|
97 | |
self.log(" ! Rewrote to {}", render(rewritten_rhs))
|
98 | |
rewritten_eqn = Eqn(prev.eqn.lhs, rewritten_rhs)
|
99 | |
if step.eqn == rewritten_eqn:
|
100 | |
self.log(" !! Can rewrite rhs to obtain: {}", render(rewritten_eqn))
|
101 | |
return rewritten_eqn
|
|
97 |
if try_rhs:
|
|
98 |
self.log(" Trying to rewrite rhs {} with:\n {}", render(prev.eqn.rhs), render(rule))
|
|
99 |
for rewritten_rhs in all_rewrites(rule.pattern, rule.substitution, prev.eqn.rhs):
|
|
100 |
self.log(" ! Rewrote to {}", render(rewritten_rhs))
|
|
101 |
rewritten_eqn = Eqn(prev.eqn.lhs, rewritten_rhs)
|
|
102 |
if step.eqn == rewritten_eqn:
|
|
103 |
self.log(" !! Can rewrite rhs to obtain: {}", render(rewritten_eqn))
|
|
104 |
return rewritten_eqn
|
102 | 105 |
|
103 | 106 |
return None
|
104 | 107 |
|
|
131 | 134 |
else:
|
132 | 135 |
return None
|
133 | 136 |
|
134 | |
def narrow_rule_search(self, step: Step) -> Union[Dict[str, RewriteRule], None]:
|
135 | |
if isinstance(step.hint, Reference):
|
136 | |
if step.hint.name + '_1' not in self.rules:
|
137 | |
raise DerivationError("Rule named {} has not been established".format(step.hint.name))
|
138 | |
rules = {}
|
139 | |
rules[step.hint.name + '_1'] = apply_substs_to_rule(self.rules[step.hint.name + '_1'], step.hint.substs)
|
140 | |
rules[step.hint.name + '_2'] = apply_substs_to_rule(self.rules[step.hint.name + '_2'], step.hint.substs)
|
141 | |
return rules
|
|
137 |
def narrow_search_using_reference(self, hint: Reference) -> Tuple[Dict[str, RewriteRule], bool, bool]:
|
|
138 |
if hint.name + '_1' not in self.rules:
|
|
139 |
raise DerivationError("Rule named {} has not been established".format(hint.name))
|
|
140 |
rules = {}
|
|
141 |
rules[hint.name + '_1'] = apply_substs_to_rule(self.rules[hint.name + '_1'], hint.substs)
|
|
142 |
rules[hint.name + '_2'] = apply_substs_to_rule(self.rules[hint.name + '_2'], hint.substs)
|
|
143 |
if hint.side == 'LHS':
|
|
144 |
return rules, True, False
|
|
145 |
elif hint.side == 'RHS':
|
|
146 |
return rules, False, True
|
142 | 147 |
else:
|
143 | |
return None
|
|
148 |
return rules, True, True
|