Редекс не соответствует

Question

Распространенным способом определения семантики является (например):

return v if [some other condition]
otherwise, return error

Например, рассмотрим

(define-language simple-dispatch
   (e ::= v (+ e e))
   (v ::= number string)
   (res ::= e err)
   (E ::= hole (+ E e) (+ v E)))

Мы могли бы тогда определить отношение редукции

(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)))

Это естественный способ сделать это, потому что он избегает необходимости писать отдельные совпадения для каждого из 3 случаев сбоя (номер строки, номер строки, строка строки). Тем не менее, это создает проблему, которая работает так:

(apply-reduction-relation s-> (term (+ 2 2)))

Показывает (правильно), что это позволяет вам уменьшить число ошибок до числа 4. Есть ли способ создать шаблон "кроме", который позволяет избежать проверки всех составляющих случаев?

Answer 1

То, что вы хотите использовать здесь, является комбинацией side-condition а также redex-match?, Расширение вашего редукционного отношения дает:

(define s-> (reduction-relation simple-dispatch
  #:domain res
  (--> (in-hole E (+ number_1 number_2))
       (in-hole E ,(+ (term number_1) (term number_2))))
  (--> (in-hole E (+ any_1 any_2))
       err
       (side-condition
        (not (redex-match? simple-dispatch
                           (+ number number)
                           (term (+ any_1 any_2))))))))

Это просто говорит о том, что вы можете принять второе правило, если первое не соответствует действительности, о чем неявно говорится в статьях, и просто не было явно указано на рисунке. (Обратите внимание, что вы можете использовать side-condition/hidden чтобы он не рисовал боковое условие при рендеринге фигуры).

Вы можете использовать этот метод для масштабирования до любого количества шаблонов, которые вы хотите запретить.