A common way of defining semantics is (for example):
return v if [some other condition]
otherwise, return error
For example, consider
(define-language simple-dispatch
(e ::= v (+ e e))
(v ::= number string)
(res ::= e err)
(E ::= hole (+ E e) (+ v E)))
We could then define the reduction relation
(define s-> (reduction-relation simple-dispatch
#:domain res
(--> (in-hole E (+ number_1 number_2))
(in-hole E ,(+ number_1 number_2)))
(--> (in-hole E (+ any any))
err)))
This is the natural way to do this, because it avoids having to write individual matchers for each of the 3 failure cases (number string, string number, string string). However, it then creates the problem that running it like this:
(apply-reduction-relation s-> (term (+ 2 2)))
Shows (correctly) that it lets you reduce both to an error or to the number 4. Is there a way to make an "except" pattern that avoids having to check all of the constituent cases?
What you want to use here is a combination of
side-condition
andredex-match?
. Extending your reduction-relation gives:This just says you can take the second rule so long as the first one is not true, which is what the papers are saying implicitly, and just didn't draw out explicitly in the figure. (Note that you can use
side-condition/hidden
to get it to not draw the side condition when rendering the figure).You can use this method to scale up to any number of patterns you want to disallow.