Skip to content

Instantly share code, notes, and snippets.

@zenna
Created March 7, 2017 20:08
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save zenna/2666c967c0f88618ef52735edc0447b0 to your computer and use it in GitHub Desktop.
:-O
class Axiom(object):
def __init__(self, lhs, rhs, name):
self.lhs = lhs
self.rhs = rhs
self.name = name
def q_ax(empty, push, pop, items):
nitems = len(items)
axioms = []
eqqueue = empty
eqqueues = [eqqueue]
for i in range(nitems):
orig_eqqueue = eqqueue
(push_eqqueue,) = push(orig_eqqueue, items[i]) # pushed the item onto the eqqueue
eqqueues.append(push_eqqueue)
pop_eqqueue = push_eqqueue
for j in range(i+1):
# Item equivalence
(pop_eqqueue, pop_item) = pop(pop_eqqueue) # when you pop item from queue
axiom = Axiom((pop_item,), (items[j],), 'item-eq%s-%s' %(i, j))
axioms.append(axiom)
# Eqqueue equivalence, Case 1: Orig queue was empty
if i==j:
axiom = Axiom((pop_eqqueue,), (empty,), 'eqqueue-eq%s-%s' %(i, i))
axioms.append(axiom)
# Eqqueue equivalence, Case 2: Orig queue had items
else:
(test_pop_eqqueue, test_pop_item) = pop(orig_eqqueue)
(test_push_eqqueue, ) = push(test_pop_eqqueue, items[i])
axiom = Axiom((pop_eqqueue,), (test_push_eqqueue,), 'eqqueue-eq%s-%s' %(i, i)) #queue.push(i)[0].pop()[0] == queue.pop()[0].push(i)[0]
axioms.append(axiom)
# Set next queue to support one more item
eqqueue=push_eqqueue
return axioms
empty = deque()
def push(q, i):
q.append(i)
return (q,)
def pop(q):
i = q.popleft()
return (q, i)
items = [3,1,5,6]
axioms = q_ax(empty, push, pop, items)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment