Skip to content

Commit

Permalink
add lobsters example
Browse files Browse the repository at this point in the history
  • Loading branch information
izgzhen committed Oct 23, 2018
1 parent 1869354 commit e9b8c5f
Show file tree
Hide file tree
Showing 2 changed files with 47 additions and 1 deletion.
2 changes: 1 addition & 1 deletion cozy/codegen/cxx.py
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,7 @@ def construct_concrete(self, t : Type, e : Exp, out : Exp):
self.construct_map(t, e, out))
elif isinstance(t, THandle):
return SEscape("{indent}{lhs} = {rhs};\n", ["lhs", "rhs"], [out, e])
elif is_scalar(t):
elif is_scalar(t) or isinstance(t, TTuple):
return SEscape("{indent}{lhs} = {rhs};\n", ["lhs", "rhs"], [out, e])
else:
h = extension_handler(type(t))
Expand Down
46 changes: 46 additions & 0 deletions examples/lobsters.ds
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
// https://github.com/lobsters/lobsters
Lobsters:
type HiddenToUser = {
story_id : Int,
user_id : Int
}
type StoryTag = {
story_id : Int,
tag_id : Int
}
handletype Vote = {
id : Int,
user_id : Int,
comment_id : Int
}
handletype Story = {
merged_story_id : Int,
is_expired : Bool,
created_at : Int,
vote_count : Int,
hidden_to_users : Bag<HiddenToUser>,
tags : Bag<StoryTag>,
votes : Bag<Vote>
}
state stories : Bag<Story>
state votes : Bag<Vote>
invariant unique [ v.val.id | v <- votes ];
invariant all [ v in votes | s <- stories, v <- s.val.votes ];
query selectStoryVotes(p1: Int, p2 : Int, p3 : Int, p4 : Int)
[ (s, [ v | v <- s.val.votes,
v.val.comment_id == 0,
v.val.user_id == p4 ])
| s <- stories,
s.val.merged_story_id == 0,
s.val.is_expired == false,
s.val.vote_count > 0,
not (exists [ u | u <- s.val.hidden_to_users, u.user_id == p1 ]),
not (exists [ t | t <- s.val.tags, t.tag_id == p2 ]),
s.val.created_at > p3 ]
op insertVote(v : Vote)
assume not (exists [ v0 | v0 <- votes, v0.val.id == v.val.id ]);
votes.add(v);

op insertStory(s : Story)
assume all [ v in votes | v <- s.val.votes ];
stories.add(s);

0 comments on commit e9b8c5f

Please sign in to comment.