Improve error subsystem.
Chris Pressey
8 years ago
| 0 | 0 | from maxixe.ast import Block |
| 1 | ||
| 2 | ||
| 3 | class ProofStructureError(ValueError): | |
| 4 | pass | |
| 5 | ||
| 6 | ||
| 7 | class ReasoningError(ValueError): | |
| 8 | pass | |
| 1 | 9 | |
| 2 | 10 | |
| 3 | 11 | class Checker(object): |
| 6 | 14 | self.current_block = None |
| 7 | 15 | self.local_atoms = set() |
| 8 | 16 | self.used_atoms = set() |
| 9 | self.last_step = None | |
| 17 | self.current_step = None | |
| 10 | 18 | |
| 11 | 19 | def check(self): |
| 12 | assert self.proof.goal.is_ground(), "goal is not ground" | |
| 20 | if not self.proof.goal.is_ground(): | |
| 21 | raise ProofStructureError("goal is not ground") | |
| 22 | ||
| 13 | 23 | for step in self.proof.steps: |
| 14 | 24 | if isinstance(step, Block): |
| 15 | 25 | self.check_block(step) |
| 16 | 26 | else: |
| 17 | 27 | self.check_step(step) |
| 18 | 28 | |
| 19 | if self.last_step.term != self.proof.goal: | |
| 20 | raise ValueError("proof does not reach goal") | |
| 29 | if self.current_step.term != self.proof.goal: | |
| 30 | raise ProofStructureError("proof does not reach goal") | |
| 21 | 31 | |
| 22 | 32 | def check_block(self, block): |
| 23 | 33 | prev_block, prev_local_atoms = self.current_block, self.local_atoms |
| 25 | 35 | |
| 26 | 36 | block_rule = self.proof.get_block_rule(self.current_block.name.name) |
| 27 | 37 | if len(block_rule.cases) != len(block.cases): |
| 28 | raise ValueError("block must have same number of cases as block rule") | |
| 38 | raise ProofStructureError("block must have same number of cases as block rule") | |
| 29 | 39 | last_term = None |
| 30 | 40 | for (case_num, (block_rule_case, case)) in enumerate(zip(block_rule.cases, block.cases)): |
| 31 | 41 | self.check_case(case_num + 1, block_rule_case, case) |
| 32 | 42 | if last_term is None: |
| 33 | 43 | last_term = case.steps[-1].term |
| 34 | 44 | elif last_term != case.steps[-1].term: |
| 35 | raise ValueError("cases do not finish with same term") | |
| 45 | raise ProofStructureError("cases do not finish with same term") | |
| 36 | 46 | |
| 37 | 47 | self.current_block, self.local_atoms = prev_block, prev_local_atoms |
| 38 | 48 | |
| 39 | 49 | def check_case(self, case_num, block_rule_case, case): |
| 40 | 50 | if case.steps[0].by.name != block_rule_case.initial.var.name: |
| 41 | raise ValueError("initial step of case %s of %s must use rule %s" % | |
| 51 | raise ProofStructureError("initial step of case %s of %s must use rule %s" % | |
| 42 | 52 | (case_num, self.current_block.name, block_rule_case.initial.var.name) |
| 43 | 53 | ) |
| 44 | 54 | if block_rule_case.final is not None and case.steps[-1].by.name != block_rule_case.final.var.name: |
| 45 | raise ValueError("final step of case %s of %s must use rule %s" % | |
| 55 | raise ProofStructureError("final step of case %s of %s must use rule %s" % | |
| 46 | 56 | (case_num, self.current_block.name, block_rule_case.final.var.name) |
| 47 | 57 | ) |
| 48 | 58 | |
| 56 | 66 | case.steps[-1].term.collect_atoms(final_atoms) |
| 57 | 67 | for atom in self.local_atoms: |
| 58 | 68 | if atom in final_atoms: |
| 59 | raise ValueError("Local atom '%s' cannot be used in final step of case" % atom) | |
| 69 | raise ProofStructureError("Local atom '%s' cannot be used in final step of case" % atom) | |
| 60 | 70 | |
| 61 | 71 | def check_step(self, step): |
| 62 | 72 | block = self.current_block |
| 63 | self.last_step = step | |
| 73 | self.current_step = step | |
| 64 | 74 | rule = self.proof.get_rule(step.by.name) |
| 65 | 75 | |
| 66 | 76 | if len(rule.hypotheses) != len(step.with_): |
| 67 | raise ValueError("In %s, Number of arguments provided (%s) does not match number of hypotheses (%s)" % | |
| 68 | (step.var.name, len(step.with_), len(rule.hypotheses)) | |
| 77 | self.step_error("Number of arguments provided (%s) does not match number of hypotheses (%s)" % | |
| 78 | (len(step.with_), len(rule.hypotheses)) | |
| 69 | 79 | ) |
| 70 | 80 | unifier = {} |
| 71 | 81 | with_terms = [] |
| 72 | 82 | for (hypothesis, with_) in zip(rule.hypotheses, step.with_): |
| 73 | 83 | if hypothesis.has_attribute('atom'): |
| 74 | assert with_.is_atom(), "argument '%s' to hypothesis '%s' is not an atom" % (with_, hypothesis) | |
| 84 | if not with_.is_atom(): | |
| 85 | self.step_error("argument '%s' to hypothesis '%s' is not an atom" % (with_, hypothesis)) | |
| 75 | 86 | hypothesis.term.match(with_, unifier) |
| 76 | 87 | with_term = with_ |
| 77 | 88 | if hypothesis.has_attribute('local'): |
| 85 | 96 | from_level = 0 if from_block is None else from_block.level |
| 86 | 97 | if from_level > level: |
| 87 | 98 | if not from_block.has_as_last_step(with_step): |
| 88 | raise ValueError('%s is a non-final step in an inner block' % with_.name) | |
| 99 | self.step_error('%s is a non-final step in an inner block' % with_.name) | |
| 89 | 100 | try: |
| 90 | 101 | hypothesis.term.match(with_step.term, unifier) |
| 91 | 102 | except ValueError as e: |
| 92 | 103 | unifier_str = ", ".join(["%s -> %s" % (k, v) for k, v in unifier.iteritems()]) |
| 93 | raise ValueError("In %s, could not match '%s' with '%s' with unifier '%s': %s" % (step.var.name, hypothesis.term, with_step.term, unifier_str, e)) | |
| 104 | self.step_error( | |
| 105 | "could not match '%s' with '%s' with unifier '%s': %s" % ( | |
| 106 | hypothesis.term, with_step.term, unifier_str, e | |
| 107 | ), class_=ReasoningError | |
| 108 | ) | |
| 94 | 109 | with_term = with_step.term |
| 95 | 110 | with_terms.append(with_term) |
| 96 | 111 | if hypothesis.has_attribute('unique'): |
| 97 | 112 | if with_term in self.used_atoms: |
| 98 | raise ValueError("In %s, '%s' has already been used as an atom in this proof" % (step.by.name, with_term)) | |
| 113 | self.step_error("'%s' has already been used as an atom in this proof" % (step.by.name, with_term)) | |
| 99 | 114 | |
| 100 | 115 | instance = rule.conclusion.subst(unifier) |
| 101 | assert instance.is_ground(), "Not all variables replaced during rule instantiation" | |
| 116 | if not instance.is_ground(): | |
| 117 | self.step_error("Not all variables replaced during rule instantiation") | |
| 102 | 118 | |
| 103 | 119 | instance = instance.resolve_substs(unifier) |
| 104 | 120 | |
| 105 | 121 | if instance != step.term: |
| 106 | raise ValueError("%s does not follow from %s with %s - it would be %s." % ( | |
| 122 | self.step_error("%s does not follow from %s with %s - it would be %s." % ( | |
| 107 | 123 | step.term, step.by.name, ' ; '.join([str(t) for t in with_terms]), instance |
| 108 | )) | |
| 124 | ), class_=ReasoningError) | |
| 109 | 125 | |
| 110 | 126 | step.term.collect_atoms(self.used_atoms) |
| 127 | ||
| 128 | def step_error(self, message, class_=ProofStructureError): | |
| 129 | message = "In %s, %s" % (self.current_step.var.name, message) | |
| 130 | raise class_(message) | |