Closed izgzhen closed 6 years ago
Could you clarify this issue? Cozy can already generate code for tuples.
https://github.com/izgzhen/cozy/tree/lobsters
cozy examples/lobsters.ds --java examples/Lobsters.java
_var268 : Bag<Story> = stories
Lobsters:
type HiddenToUser = { story_id : Int, user_id : Int }
type StoryTag = { story_id : Int, tag_id : Int }
type Vote = Vote
type Story = Story
state _var268 : Bag<Story>
query selectStoryVotes(p1 : Int, p2 : Int, p3 : Int):
Map {s -> (s, ((s).val).votes)} (Filter {s -> ((((((((s).val).created_at > p3) and (not (exists Map {t -> t} (Filter {t -> ((t).tag_id == p2)} (((s).val).tags))))) and (not (exists Map {u -> u} (Filter {u -> ((u).user_id == p1)} (((s).val).hidden_to_users))))) and (((s).val).vote_count > 0)) and (((s).val).is_expired == false)) and (((s).val).merged_story_id == 0))} (_var268))
Code generation failed!
Implementation was dumped to /tmp/failed_codegen.py
Traceback (most recent call last):
File "/home/zgzhen/projects/cozy/.venv/bin/cozy", line 11, in <module>
load_entry_point('cozy', 'console_scripts', 'cozy')()
File "/home/zgzhen/projects/cozy/cozy/main.py", line 175, in run
codegen.JavaPrinter(out=out, boxed=(not args.unboxed)).visit(impl, state_map, share_info, abstract_state=ast.spec.statevars)
File "/home/zgzhen/projects/cozy/cozy/codegen/java.py", line 687, in visit
res = super().visit(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/common.py", line 281, in visit
return f(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/codegen/java.py", line 87, in visit_Spec
self.visit(op)
File "/home/zgzhen/projects/cozy/cozy/codegen/java.py", line 687, in visit
res = super().visit(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/common.py", line 281, in visit
return f(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/codegen/java.py", line 124, in visit_Query
self.visit(SForEach(x, q.ret, SEscape("{indent}_callback.accept({x});\n", ["x"], [x])))
File "/home/zgzhen/projects/cozy/cozy/codegen/java.py", line 687, in visit
res = super().visit(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/common.py", line 281, in visit
return f(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/codegen/cxx.py", line 599, in visit_SForEach
self.for_each(iter, lambda x: SSeq(SDecl(loop_var, x), body))
File "/home/zgzhen/projects/cozy/cozy/codegen/cxx.py", line 533, in for_each
lambda v: body(iterable.transform_function.apply_to(v)))
File "/home/zgzhen/projects/cozy/cozy/codegen/cxx.py", line 543, in for_each
return self.for_each(iterable.e, lambda x: SIf(iterable.predicate.apply_to(x), body(x), SNoOp()))
File "/home/zgzhen/projects/cozy/cozy/codegen/cxx.py", line 574, in for_each
return self.for_each_native(x, iterable, body(x))
File "/home/zgzhen/projects/cozy/cozy/codegen/java.py", line 560, in for_each_native
self.visit(body)
File "/home/zgzhen/projects/cozy/cozy/codegen/java.py", line 687, in visit
res = super().visit(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/common.py", line 281, in visit
return f(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/codegen/cxx.py", line 824, in visit_SIf
self.visit(s.then_branch)
File "/home/zgzhen/projects/cozy/cozy/codegen/java.py", line 687, in visit
res = super().visit(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/common.py", line 281, in visit
return f(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/codegen/cxx.py", line 817, in visit_SSeq
self.visit(ss)
File "/home/zgzhen/projects/cozy/cozy/codegen/java.py", line 687, in visit
res = super().visit(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/common.py", line 281, in visit
return f(x, *args, **kwargs)
File "/home/zgzhen/projects/cozy/cozy/codegen/cxx.py", line 813, in visit_SDecl
return self.declare(s.var.with_type(t), s.val)
File "/home/zgzhen/projects/cozy/cozy/codegen/cxx.py", line 800, in declare
self.visit(self.construct_concrete(v.type, initial_value, v))
File "/home/zgzhen/projects/cozy/cozy/codegen/cxx.py", line 281, in construct_concrete
raise NotImplementedError("t: {}\ne: {}\nout: {}\n".format(t, e, out))
NotImplementedError: t: TTuple((THandle('Story', TRecord((('merged_story_id', TInt()), ('is_expired', TBool()), ('created_at', TInt()), ('vote_count', TInt()), ('hidden_to_users', TBag(TRecord((('story_id', TInt()), ('user_id', TInt()))))), ('tags', TBag(TRecord((('story_id', TInt()), ('tag_id', TInt()))))), ('votes', TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt()))))))))), TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt())))))))
e: ETuple((EVar('_x1364').with_type(THandle('Story', TRecord((('merged_story_id', TInt()), ('is_expired', TBool()), ('created_at', TInt()), ('vote_count', TInt()), ('hidden_to_users', TBag(TRecord((('story_id', TInt()), ('user_id', TInt()))))), ('tags', TBag(TRecord((('story_id', TInt()), ('tag_id', TInt()))))), ('votes', TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt())))))))))), EGetField(EGetField(EVar('_x1364').with_type(THandle('Story', TRecord((('merged_story_id', TInt()), ('is_expired', TBool()), ('created_at', TInt()), ('vote_count', TInt()), ('hidden_to_users', TBag(TRecord((('story_id', TInt()), ('user_id', TInt()))))), ('tags', TBag(TRecord((('story_id', TInt()), ('tag_id', TInt()))))), ('votes', TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt())))))))))), 'val').with_type(TRecord((('merged_story_id', TInt()), ('is_expired', TBool()), ('created_at', TInt()), ('vote_count', TInt()), ('hidden_to_users', TBag(TRecord((('story_id', TInt()), ('user_id', TInt()))))), ('tags', TBag(TRecord((('story_id', TInt()), ('tag_id', TInt()))))), ('votes', TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt()))))))))), 'votes').with_type(TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt())))))))).with_type(TTuple((THandle('Story', TRecord((('merged_story_id', TInt()), ('is_expired', TBool()), ('created_at', TInt()), ('vote_count', TInt()), ('hidden_to_users', TBag(TRecord((('story_id', TInt()), ('user_id', TInt()))))), ('tags', TBag(TRecord((('story_id', TInt()), ('tag_id', TInt()))))), ('votes', TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt()))))))))), TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt()))))))))
out: EVar('_x1363').with_type(TTuple((THandle('Story', TRecord((('merged_story_id', TInt()), ('is_expired', TBool()), ('created_at', TInt()), ('vote_count', TInt()), ('hidden_to_users', TBag(TRecord((('story_id', TInt()), ('user_id', TInt()))))), ('tags', TBag(TRecord((('story_id', TInt()), ('tag_id', TInt()))))), ('votes', TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt()))))))))), TBag(THandle('Vote', TRecord((('id', TInt()), ('user_id', TInt()), ('comment_id', TInt()))))))))
Also, code here looks really confusing to me
Yes, code generation is a mess. Most of my hours went into making the synthesis part work, with codegen almost as an afterthought. It is a poorly-documented maze of tricky invariants and unspecified contracts.
I will start cleaning it up in the coming days as I work on #49. In the meantime:
declare
generates code to define a new variable. The variable is either uninitialized or initialized with a value depending on whether initial_value
is given.construct_concrete
overwrites an L-value with a new value. It is used as a subroutine for declare
, which works by declaring an uninitialized variable and then invoking construct_concrete
to initialize it.@Calvin-L I think this issue is blocked on implementing the shallow copy for Java backend?
For clarification, who is assigned to the "shallow copy for Java backend" task?