from .. import graph
__all__ = ['CallStack', 'StackFrame']
[docs]
class CallStack(object):
def __init__(self):
self.frames = []
[docs]
def realpath(self):
for frame in self.frames:
for part in frame.realpath:
yield part
[docs]
def push(self, arg=None):
frame = StackFrame(arg)
self.frames.append(frame)
[docs]
def pop(self):
self.frames.pop()
[docs]
class StackFrame(object):
def __init__(self, arg=None):
self.obj = arg
@property
def realpath(self):
return self.obj.realpath
[docs]
def set_from(self, arg):
self.obj = arg
def with_N_stackframe(N_body):
'''
Wraps the N function.
Performs stack manipulations for N. Creates an instance of of WalkState,
pushes it onto the stack, and adds it to the call.
'''
def N(rts, var):
C = rts.C
state = graph.walk(var.root, realpath=var.realpath)
# The guards crossed on the way to the start of the walk, for
# record_failure (rts_setfunctions.py).
state.base_guards = set(var.guards)
C.callstack.push(state)
try:
return N_body(rts, var, state)
finally:
C.callstack.pop()
return N
def with_hnf_stackframe(hnf_body):
'''
Wraps the hnf function.
Performs stack manipulations for hnf. Pushes the inductive varible onto the
stack.
'''
def hnf(rts, var, typedef=None, values=None, **kwds):
C = rts.C
C.callstack.push(var)
try:
return hnf_body(rts, var, typedef, values, **kwds)
finally:
C.callstack.pop()
return hnf