Ракетка: пользовательский предикат для использования в контракте

Question

Я пишу небольшой проект для домашних животных в Racket и использую Gregor lib для обработки дат.

У меня есть функция, которая принимает две даты (от Грегора, не из стандартной библиотеки), и я хотел бы добавить контракт на нее. В контракте должно быть указано, что дата первого аргумента должна быть меньше / раньше даты второго аргумента.

В Грегоре мы можем добиться этого, используя (date <=? X y) </a> или аналогичный предикат, но я не могу понять, как объединить его с контрактами.

 (contract-out
          [process-dates (->i ([x date?]
                               [y (x) (and/c date?
                                             (date>=? x))])])

не будет работать, и нет предиката date>=?/c из коробки.

Так что я думаю, что мне нужно будет написать такие предикаты самостоятельно, поэтому я хотел бы знать, как это сделать. Я просмотрел источники Racket и обнаружил, что стандартные функции довольно сложны для воспроизведения.

Есть ли более простой способ добиться того, чего я хочу?

Answer 1

Самый простой способ - использовать lambda:

(->i ([x date?]
      [y (x) (and/c date? (lambda (y) (date>=? y x)))])
     [_ any/c])

Один недостаток заключается в том, что в случае нарушения договора сообщение об ошибке будет содержать ??? вместо лямбда-выражения.Если вы хотите, чтобы там печаталось что-то более значимое, вы можете сделать что-то вроде следующего:

(define (date>=/c x)
  (flat-named-contract
   `(date>=/c ,x)
   (lambda (y) (date>=? y x))))
....
(->i ([x date?]
      [y (x) (and/c date? (date>=/c x))])
     [_ any/c])

Если вы хотите еще более точный контроль над сообщением об ошибке, вы можете попробовать использовать flat-contract-with-explanation.

Answer 2

Хотя ответ Райана великолепен, я обнаружил, что эту проблему можно решить следующим образом, используя предварительное условие:

(->i ([x date?]
      [y date?])
    #:pre (x y) (date<=? x y)
    ;; ...
 )