Странное нарушение контракта при вынесении приговора

Question

У меня есть judgement со следующим контрактом:

(define-judgment-form DynamicLam
  #:mode     (down I I O O)
  #:contract (down Γ e Γ e)

  [----------------"Lambda"
   (down Γ_0 z_0 Γ_0 z_0)]
  ;; rest of the code ...
)

Когда я запускаю это:

(define empty (term ()))
(redex-match? DynamicLam Γ empty)
(redex-match? DynamicLam e lam1^*)
(redex-match? DynamicLam z lam1^*)
(judgment-holds (down empty lam1^* empty lam1^*))

Я вернусь:

#t

#t

#t

.. вниз: входные значения суждения не соответствуют контракту; (неизвестные выходные значения обозначены _) контракт: (вниз Γ e Γ e) значения: (вниз пустой lam1^* _ _)

Но в этом нет смысла, потому что я явно использовал redex-match? выше, чтобы проверить:

• Который empty совпадения Γ
• Который lam1^* совпадения e
• И кроме того, что lam1^* совпадения z.

Что мне не хватает? Есть ли что-то еще о значении#:contract чем просто соответствие Γ e Γ e?

Answer 1

I solved the problem by changing the #:mode to (down I I I I) instead of (down I I O O), and changing

(judgment-holds (down empty lam1^* empty lam1^*))

to

(judgment-holds (down ,empty ,lam1^* ,empty ,lam1^*))

The , change makes a lot of sense to me but I still do not understand why the two outputs needed to be inputs, so if someone can either edit this answer to explain that, or provide a comment or another answer explaining that subtlety, that would be fantastic.