From 88a1c32a92f59d9b52460f4224c82a3db0c802e3 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 23 Dec 2016 15:21:17 -0800 Subject: [PATCH] fixing field handling, extending to actions --- ivy/ivy_compiler.py | 74 ++++++++++++++++++++++++++++----------------- ivy/ivy_to_cpp.py | 4 ++- test/field1.ivy | 7 ++++- 3 files changed, 55 insertions(+), 30 deletions(-) diff --git a/ivy/ivy_compiler.py b/ivy/ivy_compiler.py index 5689fff..a09aa94 100644 --- a/ivy/ivy_compiler.py +++ b/ivy/ivy_compiler.py @@ -112,6 +112,16 @@ class TopContext(Context): expr_context = None top_context = None +def pull_args(args,num,sym,top): + if len(args) < num: + raise IvyError(None,'not enough arguments to {}'.format(sym)) + if top and len(args) > num: + raise IvyError(None,'too many arguments to {}'.format(sym)) + res = args[:num] + del args[:num] + return res + + def compile_field_reference_rec(symbol_name,args,top=False): try: sym = ivy_logic.find_polymorphic_symbol(symbol_name) @@ -119,50 +129,58 @@ def compile_field_reference_rec(symbol_name,args,top=False): parent_name,child_name = iu.parent_child_name(symbol_name) if parent_name == 'this': raise IvyError(None,"unknown symbol: {}".format(symbol_name)) - base = compile_field_reference_rec(parent_name,args) + try: + base = compile_field_reference_rec(parent_name,args) + except IvyError: + raise IvyError(None,"unknown symbol: {}".format(symbol_name)) sort = base.sort sort_parent,sort_child = iu.parent_child_name(sort.name) destr_name = iu.compose_names(sort_parent,child_name) + if expr_context and top_context and destr_name in top_context.actions: + args.insert(0,base) + return field_reference_action(destr_name,args,top) sym = ivy_logic.find_polymorphic_symbol(destr_name) args.insert(0,base) if hasattr(sym.sort,'dom') and len(sym.sort.dom) > 0: - if len(args) < len(sym.sort.dom): - raise IvyError(None,'not enough arguments to {}'.format(sym)) - if top and len(args) > len(sym.sort.dom): - raise IvyError(None,'too many arguments to {}'.format(sym)) - res = sym(*args[:len(sym.sort.dom)]) - del args[:len(sym.sort.dom)] + res = sym(*pull_args(args,len(sym.sort.dom),sym,top)) return res return sym +def field_reference_action(actname,args,top): + nformals = len(top_context.actions[actname][0]) + return compile_inline_call(ivy_ast.Atom(actname,[]),pull_args(args,nformals,actname,top)) + def compile_field_reference(symbol_name,args): return compile_field_reference_rec(symbol_name,args,top=True) +def compile_inline_call(self,args): + params,returns = top_context.actions[self.rep] + if len(returns) != 1: + raise IvyError(self,"wrong number of return values") + # TODO: right now we can't do anything with multiple returns + sorts = [cmpl_sort(r.sort) for r in returns] + ress = [] + for sort in sorts: + res = ivy_logic.Symbol('loc:'+str(len(expr_context.local_syms)),sort) + expr_context.local_syms.append(res) + ress.append(res()) + expr_context.code.append(CallAction(*([ivy_ast.Atom(self.rep,args)]+ress))) + return ivy_ast.Tuple(*ress) + sort = cmpl_sort(returns[0].sort) + res = ivy_logic.Symbol('loc:'+str(len(expr_context.local_syms)),sort) + expr_context.local_syms.append(res) + with ASTContext(self): + if len(params) != len(args): + raise iu.IvyError(self,"wrong number of input parameters (got {}, expecting {})".format(len(args),len(params))) + args = [sort_infer(a,cmpl_sort(p.sort)) for a,p in zip(args,params)] + expr_context.code.append(CallAction(ivy_ast.Atom(self.rep,args),res)) + return res() + def compile_app(self): 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: - params,returns = top_context.actions[self.rep] - if len(returns) != 1: - raise IvyError(self,"wrong number of return values") - # TODO: right now we can't do anything with multiple returns - sorts = [cmpl_sort(r.sort) for r in returns] - ress = [] - for sort in sorts: - res = ivy_logic.Symbol('loc:'+str(len(expr_context.local_syms)),sort) - expr_context.local_syms.append(res) - ress.append(res()) - expr_context.code.append(CallAction(*([ivy_ast.Atom(self.rep,args)]+ress))) - return ivy_ast.Tuple(*ress) - sort = cmpl_sort(returns[0].sort) - res = ivy_logic.Symbol('loc:'+str(len(expr_context.local_syms)),sort) - expr_context.local_syms.append(res) - with ASTContext(self): - if len(params) != len(args): - raise iu.IvyError(self,"wrong number of input parameters (got {}, expecting {})".format(len(args),len(params))) - args = [sort_infer(a,cmpl_sort(p.sort)) for a,p in zip(args,params)] - expr_context.code.append(CallAction(ivy_ast.Atom(self.rep,args),res)) - return res() + return compile_inline_call(self,args) try: return (ivy_logic.Equals if self.rep == '=' else ivy_logic.find_polymorphic_symbol(self.rep))(*args) except: diff --git a/ivy/ivy_to_cpp.py b/ivy/ivy_to_cpp.py index ee62692..7d719c3 100755 --- a/ivy/ivy_to_cpp.py +++ b/ivy/ivy_to_cpp.py @@ -97,6 +97,8 @@ def varname(name): name = name.name if name in special_names: return special_names[name] + if name.startswith('"'): + return name name = name.replace('loc:','loc__').replace('ext:','ext__').replace('___branch:','__branch__').replace('prm:','prm__') name = re.sub(puncs,'__',name) @@ -209,7 +211,7 @@ struct hash_thunk { R &operator[](const D& arg){ std::pair::iterator,bool> foo = memo.insert(std::pair(arg,R())); R &res = foo.first->second; - if (foo.second) + if (foo.second && fun) res = (*fun)(arg); return res; } diff --git a/test/field1.ivy b/test/field1.ivy index 833fbf5..9ef2d49 100644 --- a/test/field1.ivy +++ b/test/field1.ivy @@ -16,12 +16,17 @@ object baz = { type t = struct { foo(X:q) : bool } + action blarg(inp:t) returns (out:t) = { + out := inp + } } individual bif(Y:q) : baz.t action b(y:q,z:q) = { - assert bif(z).foo(y) + assert bif(z).foo(y); + assert bif(z).blarg.foo(y) } interpret q -> bv[1] +