From 53b5a8a663a3132eceb71ae4257d0e6cccdadf41 Mon Sep 17 00:00:00 2001 From: Calvin Loncaric Date: Mon, 2 Jul 2018 17:16:20 -0700 Subject: [PATCH] Enumerate let-expressions Fixes #38. --- cozy/synthesis/enumeration.py | 10 ++++++++++ tests/synthesis.py | 9 +++++++++ 2 files changed, 19 insertions(+) diff --git a/cozy/synthesis/enumeration.py b/cozy/synthesis/enumeration.py index 6bb8ad66..510354e3 100644 --- a/cozy/synthesis/enumeration.py +++ b/cozy/synthesis/enumeration.py @@ -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)): diff --git a/tests/synthesis.py b/tests/synthesis.py index e2a0dea5..3c92faad 100644 --- a/tests/synthesis.py +++ b/tests/synthesis.py @@ -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)