rewriter and environment
Christoph Hoeger
maybe I am a little bit dull here but this may be due to my lack of scala experience.
Suppose I want to extend the lambda calculus from kiama's examples by references (ala Pierce).
This means that my evaluation relation (small step) is extended by the environment, e.g.:
------------------------------------
(\x.t) v_1 | S --> [x <- v_1]t | S
where S denotes the store. Although this is trivial when implemented manually, it seems complicated with kiama's rewriting rules:
val state_reduction =
rule {
case State(App (Lam (x, t), v),s) if isValue(v)
=> State(substitute(x, v, t),s)
...
}
This _does_ work. But - of course - only once, since the subterms of any lambda expression are not of type State.
So basically, I need a way to tell the rewriter to lift a term to a state.
Any ideas?
Tony Sloane
Responses below...
> maybe I am a little bit dull here but this may be due to my lack of scala experience.
>
> Suppose I want to extend the lambda calculus from kiama's examples by references (ala Pierce).
It seems that you are basing your code on the Reduce version of the Lambda2 example. Is that
correct?
> This means that my evaluation relation (small step) is extended by the environment, e.g.:
>
> ------------------------------------
> (\x.t) v_1 | S --> [x <- v_1]t | S
>
> where S denotes the store. Although this is trivial when implemented manually, it seems complicated with kiama's rewriting rules:
>
> val state_reduction =
> rule {
> case State(App (Lam (x, t), v),s) if isValue(v)
> => State(substitute(x, v, t),s)
> ...
> }
>
> This _does_ work. But - of course - only once, since the subterms of any lambda expression are not of type State.
>
> So basically, I need a way to tell the rewriter to lift a term to a state.
>
> Any ideas?
Can you give us more information about what you have tried? In the Reduce example the main rewrite strategy is
reduce (beta + arithop)
which keeps applying the beta or arithop rules until they do not apply anywhere in the term (not just at the root of the term).
How have you modified the strategy to incorporate your state_reduction rule?
cheers,
Tony
Christoph Hoeger
way beyond that little example.
My solution so far is this (example for let-expressions, but basically
every sort of expressions has such rules):
val E_LET =
rulefs {
case State(Let(x,t1,t2),s) =>
(State(t1,s) <* evalStep) <* rule {
case State(t3,s) => State(Let(x,t3,t2),s)
}
}
I add those rules as rulefs constructs to explicitly control
recursion. evalStep is the union of all those rules.
The body looks always the same though: First we apply evalStep to a
new state which is created from the child-term and the current store.
Afterwards the result is reconstructed into a new parent term. This is
severe boilerplate IMO. Having recursion explicitly is not too bad,
but since this is just a forget-about-performance-prototype I was
wondering if I could scrap that particular boilerplate code.
Tony Sloane
> My solution so far is this (example for let-expressions, but basically
> every sort of expressions has such rules):
>
> val E_LET =
> rulefs {
> case State(Let(x,t1,t2),s) =>
> (State(t1,s) <* evalStep) <* rule {
> case State(t3,s) => State(Let(x,t3,t2),s)
> }
> }
You could factor out the evaluation pattern, leaving just the deconstruction and construction of the specific terms. Something like this:
def subeval (t1 : Term, s1 : StateVal) (f: Term => Term) =
(State (t1, s1) <* evalStep) <* rule {
case State (t2, s2) =>
State (f (t2), s2)
}
where the f argument is responsible for putting the result of the sub-evaluation back into the surrounding term.
Use it like this:
val E_LET =
rulefs {
case State (Let (x, t1, t2), s) =>
subeval (t1, s) (Let (x, _, t2))
}
val E_APP =
rulefs {
case State (App (t1, t2), s) =>
subeval (t1, s) (App (_, t2))
}
How does that look? The wildcards in the f parameters look nice as "holes" to be filled.
You might even be able to hide the rulefs and s argument threading by abstracting the term deconstruction in a similar way.
cheers,
Tony
P.S. In the upcoming 1.2.0 version, you won't be able to use a Term as a strategy because we've removed the implicit conversion. It was causing too many weird bugs because it essentially meant that anything could be used as a strategy. So, for "State (t1, s1)" in subeval above, you'll need to write "build (State (t1, s1))" to create the builder strategy explicitly.