Skip to content

Commit

Permalink
Enumerate let-expressions
Browse files Browse the repository at this point in the history
Fixes #38.
  • Loading branch information
Calvin-L committed Jul 3, 2018
1 parent c6f9966 commit 53b5a8a
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 0 deletions.
10 changes: 10 additions & 0 deletions cozy/synthesis/enumeration.py
Original file line number Diff line number Diff line change
Expand Up @@ -308,6 +308,16 @@ def build_lambdas(bag, pool, body_size):
for lam_body in self.enumerate(inner_context, body_size, pool):
yield ELambda(v, lam_body)

# Let-expressions
for (sz1, sz2) in pick_to_sum(2, size - 1):
for x in self.enumerate(context, sz1, pool):
bag = ESingleton(x).with_type(TBag(x.type))
for lam in build_lambdas(bag, pool, sz2):
e = ELet(x, lam).with_type(lam.body.type)
# if x == EBinOp(EVar("x"), "+", EVar("x")):
# e._tag = True
yield e

# Iteration
for (sz1, sz2) in pick_to_sum(2, size - 1):
for bag in collections(self.enumerate(context, sz1, pool)):
Expand Down
9 changes: 9 additions & 0 deletions tests/synthesis.py
Original file line number Diff line number Diff line change
Expand Up @@ -65,3 +65,12 @@ def test_map_discovery2(self):
spec = EIn(y, EStateVar(xs))
assert retypecheck(spec)
assert check_discovery(spec=spec, expected=lambda e: (isinstance(e, EMapGet) or isinstance(e, EHasKey)) and isinstance(e.map, EStateVar) and valid(EEq(e, spec)), args=[y], state_vars=[xs])

def test_let_discovery(self):
x = EVar("x").with_type(INT)
spec = ESum([x, x, x, x])
assert retypecheck(spec)
y = EVar("y").with_type(INT)
goal = ELet(ESum([x, x]), ELambda(y, ESum([y, y])))
assert retypecheck(goal)
assert check_discovery(spec=spec, args=[x], expected=goal)

0 comments on commit 53b5a8a

Please sign in to comment.