search

ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

Abstracting sub-expressions #171

Closed conal closed 8 years ago

conal commented 8 years ago

I'd like to abstract out all sub-expressions meeting some given criterion, resulting in a multi-beta-redex, i.e.,

e ==> (\ v1 ... vn -> e[r1->v1,...,rn->vn]) r1 ... rn

where the ri are the subterms of the LHS that satisfy the criterion, and the vi are fresh variables, and the ri don't contain variables that go out of scope.

I haven't found a simple & efficient construction out of given combinators. I'd rather not painstakingly verify that the vi don't occur freely in the ri.

It's easier for me to see how to define a let counterpart:

e ==> let { v1 = r1; ...; vn = rn } in e[r1->v1,...,rn->vn]

but then I've lost the non-occurrence property, so I don't know how to convert to a multi-beta-redex,

(let { v1 = r1; ...; vn = rn } in e) ==> (\ v1 ... vn -> e) r1 ... rn

without having to verify that the vi don't occur freely in the ri.

After tinkering with this one for a while, I thought I'd ask whether this puzzle is already solved well.

xich commented 8 years ago

Sorry, not ignoring this, just haven't had time to play around with it yet.

I think if you had the recursive-let expression, you could write a rewrite to pick out one binding into an enclosing non-recursive let (failing if any of the recursive bindings are in the RHS of the new non-recursive binding... and if it fails, inlining that binding to undo the abstraction). Then just iterate that to get a big pile of nested non-recursive let expressions, which would be straightforward to convert to lambdas.

conal commented 8 years ago

Thanks. Given your suggestion and my current specialized solution, I'm closing the ticket.