[racket] [redex] side-condition matching upon errors

From: Eric Tanter (etanter at dcc.uchile.cl)
Date: Tue Sep 3 22:10:15 EDT 2013

Hi,

Strangely, `side-condition' matches when the associated expression fails with an error. 

For instance, using the redex tutorial example, if one writes:

  [(types Γ x_1 t_1)
   (side-condition (/ 1 0))
   ------------------------------------
   (types (x_2 : t_2 Γ) x_1 t_1)]

Then the rule applies, as if it was (side-condition #t).

Of course, (/ 1 0) is not really realistic, but the same happens if one writes:

  [(types Γ x_1 t_1)
   (side-condition (different x_1 x_2))
   ------------------------------------
   (types (x_2 : t_2 Γ) x_1 t_1)]

and forgets to define `different' (assuming it is a standard Redex metafunction)... Instead of a nice error that `different' is undefined, the rule silently applies.

I understand that anything that is not #f is true, but arguably this should not apply to an error. Or is there a good reason why this is so?

Cheers,

-- Éric


Posted on the users mailing list.