Commit 6a20513f841d4ccc9b3c100c69ac63b0a398d632 - Eqthy

Refactor into `objects` module, and small flake8 cleanups. Chris Pressey 2 years ago

5 changed file(s) with 26 addition(s) and 16 deletion(s). Raw diff Collapse all Expand all

-0

src/eqthy/main.py less more

+14

-0

src/eqthy/objects.py less more

	0	"""Objects in the Eqthy document structure."""
	1	from collections import namedtuple
	2
	3	Document = namedtuple('Document', ['axioms', 'theorems'])
	4	Axiom = namedtuple('Axiom', ['name', 'eqn'])
	5	Theorem = namedtuple('Theorem', ['name', 'eqn', 'steps'])
	6	Step = namedtuple('Step', ['eqn', 'hint'])
	7
	8	# hints
	9
	10	Reflexivity = namedtuple('Reflexivity', [])
	11	Substitution = namedtuple('Substitution', ['term', 'variable'])
	12	Congruence = namedtuple('Congruence', ['variable', 'term'])
	13	Reference = namedtuple('Reference', ['name', 'side'])

-13

src/eqthy/parser.py less more

0		from collections import namedtuple
1
	0	from eqthy.objects import (
	1	Document, Axiom, Theorem, Step,
	2	Reflexivity, Substitution, Congruence, Reference
	3	)
2	4	from eqthy.scanner import Scanner, EqthySyntaxError
3	5	from eqthy.terms import Term, Variable, Eqn
4	6

16	18	# Term := Var \| Ctor ["(" [Term {"," Term} ")"].
17	19
18	20
19		Document = namedtuple('Document', ['axioms', 'theorems'])
20		Axiom = namedtuple('Axiom', ['name', 'eqn'])
21		Theorem = namedtuple('Theorem', ['name', 'eqn', 'steps'])
22		Step = namedtuple('Step', ['eqn', 'hint'])
23		Reflexivity = namedtuple('Reflexivity', [])
24		Substitution = namedtuple('Substitution', ['term', 'variable'])
25		Congruence = namedtuple('Congruence', ['variable', 'term'])
26		Reference = namedtuple('Reference', ['name', 'side'])
27
28
29	21	class Parser(object):
30	22	def __init__(self, text, filename):
31	23	self.scanner = Scanner(text, filename)

40	32	while self.scanner.on('theorem'):
41	33	theorems.append(self.theorem())
42	34	if not (axioms or theorems):
43		raise EqthySyntaxError(self.scanner.filename, self.scanner.line_number, "Eqthy document is empty")
	35	raise EqthySyntaxError(
	36	self.scanner.filename,
	37	self.scanner.line_number,
	38	"Eqthy document is empty"
	39	)
44	40	return Document(axioms=axioms, theorems=theorems)
45	41
46	42	def axiom(self):

-1

src/eqthy/terms.py less more

124	124
125	125
126	126	def all_rewrites(pattern, substitution, term):
127		"""Given a term, and a rule (a pattern and a substitution), return
	127	"""Given a rule (a pattern and a substitution) and a term, return
128	128	a list of the terms that would result from rewriting the term
129	129	in all the possible ways by the rule."""
130	130

-2

src/eqthy/verifier.py less more

0		# TODO: these should probably come from a "eqthy.hints" module
1		from eqthy.parser import Reflexivity, Substitution, Congruence, Reference
	0	from eqthy.objects import Reflexivity, Substitution, Congruence, Reference
2	1	from eqthy.terms import Eqn, all_rewrites, render, RewriteRule, replace
3	2
4	3