getting call by reference to work with method calls

This commit is contained in:
Ken McMillan 2017-11-20 18:34:19 -08:00
Родитель 96885e59d7
Коммит aaed5702ef
3 изменённых файлов: 45 добавлений и 33 удалений

Просмотреть файл

@ -206,8 +206,8 @@ module sequence_iterator(range) = {
instantiate order_iterator(range)
action next(x:t) returns (y:t)
action prev(y:t) returns (x:t)
action next(x:t) returns (x:t)
action prev(x:t) returns (x:t)
object spec = {
...
@ -215,18 +215,18 @@ module sequence_iterator(range) = {
assert ~is_end(x)
}
after next {
assert X <= val(x) & is_end(y)
| ~(val(x) < Y & Y < val(y))
& val(x) < val(y) & ~is_end(y)
assert X <= val(old x) & is_end(x)
| ~(val(old x) < Y & Y < val(x))
& val(old x) < val(x) & ~is_end(x)
}
before prev {
assert is_end(y) | exists X. X < val(y)
assert is_end(x) | exists X. X < val(x)
}
after prev {
assert ~is_end(x);
assert X <= val(x) & is_end(y)
| ~(val(x) < Y & Y < val(y))
& val(x) < val(y) & ~is_end(y)
assert X <= val(x) & is_end(old x)
| ~(val(x) < Y & Y < val(old x))
& val(x) < val(old x) & ~is_end(old x)
}
}
@ -234,13 +234,13 @@ module sequence_iterator(range) = {
...
implement next {
if range.is_max(val(x)) {
y := end
x := end
} else {
y := create(range.next(val(x)))
x := create(range.next(val(x)))
}
}
implement prev {
x := create(range.prev(val(y)))
x := create(range.prev(val(x)))
}
}

Просмотреть файл

@ -219,6 +219,7 @@ def compile_inline_call(self,args):
return None
def compile_app(self):
with ReturnContext(None):
args = [a.compile() for a in self.args]
# handle action calls in rhs of assignment
if expr_context and top_context and self.rep in top_context.actions:
@ -362,12 +363,12 @@ def compile_local(self):
LocalAction.cmpl = compile_local
def compile_assign(self):
rhs = self.args[1]
if (isinstance(rhs,ivy_ast.App) or isinstance(rhs,ivy_ast.Atom)):
if top_context and rhs.rep in top_context.actions:
c = CallAction(rhs,self.args[0])
c.lineno = self.lineno
return c.cmpl()
# rhs = self.args[1]
# if (isinstance(rhs,ivy_ast.App) or isinstance(rhs,ivy_ast.Atom)):
# if top_context and rhs.rep in top_context.actions:
# c = CallAction(rhs,self.args[0])
# c.lineno = self.lineno
# return c.cmpl()
code = []
local_syms = []
with ExprContext(code,local_syms):
@ -379,9 +380,13 @@ def compile_assign(self):
code.append(AssignAction(lhs,rhs))
else:
with top_sort_as_default():
args = [a.compile() for a in self.args]
# args = [a.compile() for a in self.args]
args = [self.args[0].compile()]
with ReturnContext([args[0]]):
args.append(self.args[1].compile())
if isinstance(args[1],ivy_ast.Tuple):
raise IvyError(self,"wrong number of values in assignment");
if args[1] is not None:
asorts = [a.sort for a in args]
with ASTContext(self):
if im.module.is_variant(*asorts):

Просмотреть файл

@ -969,8 +969,13 @@ def emit_native(header,impl,native,classname):
def annotate_action(action):
def action_assigns(p):
return any(p in sub.modifies() for sub in action.iter_subactions())
def is_struct(sort):
return (il.is_uninterpreted_sort(sort) and
(sort.name in im.module.native_types or sort.name in im.module.sort_destructors))
action.param_types = [RefType() if any(p == q for q in action.formal_returns)
else ValueType() if action_assigns(p) else ConstRefType()
else ValueType() if action_assigns(p) or not is_struct(p.sort) else ConstRefType()
for p in action.formal_params]
def return_type(p):
for idx,q in enumerate(action.formal_params):
@ -3090,6 +3095,7 @@ ia.AssumeAction.emit = emit_assume
def emit_call(self,header):
if target.get() in ["gen","test"]:
indent(header)
header.append('___ivy_stack.push_back(' + str(self.unique_id) + ');\n')
code = []
@ -3125,6 +3131,7 @@ def emit_call(self,header):
self.args[1].emit(header,code)
code.append(' = ' + retval + ';\n')
header.extend(code)
if target.get() in ["gen","test"]:
indent(header)
header.append('___ivy_stack.pop_back();\n')