Checkpoint developing all_matches logic.
Chris Pressey
2 years ago
| 15 | 15 | argparser.add_argument("--dump-ast", |
| 16 | 16 | action="store_true", |
| 17 | 17 | help="Just show the AST and stop" |
| 18 | ) | |
| 19 | argparser.add_argument("--traceback", | |
| 20 | action="store_true", | |
| 21 | help="When an error occurs, display a full Python traceback." | |
| 18 | 22 | ) |
| 19 | 23 | argparser.add_argument("--verbose", |
| 20 | 24 | action="store_true", |
| 39 | 43 | verifier.verify() |
| 40 | 44 | except Exception as e: |
| 41 | 45 | print('*** {}: {}'.format(e.__class__.__name__, e)) |
| 46 | if options.traceback: | |
| 47 | raise | |
| 42 | 48 | sys.exit(1) |
| 1 | 1 | |
| 2 | 2 | from eqthy.scanner import Scanner |
| 3 | 3 | from eqthy.terms import Term, Variable, Eqn |
| 4 | ||
| 5 | ||
| 6 | # Program := {Axiom} {Theorem}. | |
| 7 | # Axiom := "axiom" Eqn. | |
| 8 | # Theorem := "theorem" Eqn "proof" {Step} "qed". | |
| 9 | # Step := Eqn. | |
| 10 | # Eqn := Term "=" Term. | |
| 11 | # Term := Var | Name ["(" [Term {"," Term} ")"]. | |
| 4 | 12 | |
| 5 | 13 | |
| 6 | 14 | Program = namedtuple('Program', ['axioms', 'theorems']) |
| 47 | 47 | else: |
| 48 | 48 | assert isinstance(pattern, Term) |
| 49 | 49 | if not isinstance(term, Term) or len(term.subterms) != len(pattern.subterms): |
| 50 | return False | |
| 50 | return unify_fail | |
| 51 | 51 | unifier = Unifier(success=True, bindings={}) |
| 52 | 52 | for (subpattern, subterm) in zip(pattern.subterms, term.subterms): |
| 53 | 53 | subunifier = match(subpattern, subterm) |
| 62 | 62 | matches = [] |
| 63 | 63 | |
| 64 | 64 | unifier = match(pattern, term) |
| 65 | matches.append((index, unifier)) | |
| 65 | if unifier.success: | |
| 66 | matches.append((index, unifier)) | |
| 66 | 67 | |
| 67 | for n, subterm in enumerate(term.subterms): | |
| 68 | matches += all_matches(pattern, subterm, index + [n]) | |
| 68 | if isinstance(term, Term): | |
| 69 | for n, subterm in enumerate(term.subterms): | |
| 70 | matches += all_matches(pattern, subterm, index + [n]) | |
| 69 | 71 | |
| 70 | 72 | return matches |
| 73 | ||
| 74 | ||
| 75 | def subst(term, unifier): | |
| 76 | if not unifier.success: | |
| 77 | return term | |
| 78 | elif isinstance(term, Variable): | |
| 79 | if term.name in unifier.bindings: | |
| 80 | return unifier.bindings[term.name] | |
| 81 | else: | |
| 82 | return term | |
| 83 | elif isinstance(term, Term): | |
| 84 | return Term(term.ctor, [subst(st, unifier) for st in term.subterms]) | |
| 85 | else: | |
| 86 | raise NotImplementedError(str(term)) | |
| 0 | from eqthy.terms import all_matches, render, RewriteRule | |
| 0 | from eqthy.terms import all_matches, subst, render, RewriteRule | |
| 1 | 1 | from collections import namedtuple |
| 2 | 2 | |
| 3 | 3 | |
| 4 | 4 | class DerivationError(Exception): |
| 5 | 5 | pass |
| 6 | ||
| 7 | ||
| 8 | def rewrite_deep(rule, term): | |
| 9 | return False | |
| 10 | 6 | |
| 11 | 7 | |
| 12 | 8 | class Verifier: |
| 50 | 46 | # TODO: if name of rule given, use that rule only |
| 51 | 47 | rewritten_lhs = None |
| 52 | 48 | for rule in self.rules: |
| 53 | self.log("Trying to rewrite {} with {}", render(prev.lhs), render(rule)) | |
| 54 | result = rewrite_deep(rule, prev.lhs) | |
| 55 | if result: | |
| 56 | rewritten_lhs = result | |
| 57 | break | |
| 49 | self.log(" Trying to rewrite {} with {}", render(prev.lhs), render(rule)) | |
| 50 | rewrites = self.all_rewrites(rule, prev.lhs) | |
| 51 | if rewrites: | |
| 52 | for rewrite in rewrites: | |
| 53 | self.log(" Can rewrite to {}", render(rewrite)) | |
| 54 | # rewritten_lhs = result | |
| 55 | # break | |
| 58 | 56 | if not rewritten_lhs: |
| 59 | 57 | raise DerivationError("Could not derive {} from {}".format(render(step), render(prev))) |
| 60 | 58 | |
| 61 | 59 | prev = step |
| 60 | ||
| 61 | def all_rewrites(self, rule, term): | |
| 62 | matches = all_matches(rule.pattern, term) | |
| 63 | self.log(" Matches: {}", matches) | |
| 64 | rewrites = [] | |
| 65 | for (index, unifier) in matches: | |
| 66 | rewrites += subst(term, unifier) | |
| 67 | return rewrites | |