[plt-scheme] redex: discarding a sub-syntactic form

From: Eric Tanter (etanter at dcc.uchile.cl)
Date: Sat Sep 12 16:38:27 EDT 2009


I have another question with redex:

I have a syntactic category:
(igv l f (with igv igv))

I want to define a reduction rule for the "atomic" cases where igv is  
either l or f,
and another one for the "compounded" case (with igv igv).

If I do so and don't put a side condition, then of course the  
reduction relation becomes non-determinist.

So I'm trying to add a side condition for the atomic case that  
discards the compounded case. Something like:

    (side-condition (not (eq? (term igv) (term (with igv_1 igv_2)))))

this however does not seem to do the job. I tried with (not  
(match... )) but then I get an error related to with ("with: used  
outside of reduction-relation").
I really want to say "where igv is not of the form (with x y)".

Any clue/suggestion?

Thanks in advance,

-- Éric

Posted on the users mailing list.