Using ->i to allow only valid Sneetches for the McBean machine

Continuing study of contracts, specifically ->i.

I am trying to model the machine from *The Sneetches* with the most fleshed
out contract possible. Assuming a Sneetch is reduced to a boolean as per
the story's problem statement, we can model McBean's machine as:

(define (convert-sneetches stars-upon-thars? sneetches)
  (map (lambda (s) stars-upon-thars?) sneetches))

The demand for stars upon thars or the contrary is a separate parameter to
make the problem applicable to ->i, because in the story the machine is
only configured to accept Sneetches of the opposite persuasion. That is, if
the demand is for stars upon thars, only Plain-Bellies enter the machine.
So applications like (convert-sneetches #t '(#t #t #f)) are violations.

Here's my attempt at handling this:

#lang racket

; Normalizes sneetches depending on belly-star demand.
(define/contract (convert-sneetches stars-upon-thars? sneetches)
  (->i
    ([demand boolean?]
     [inputs (demand)
       (non-empty-listof
         (and/c
           boolean?
           (lambda (b) (equal? b (not demand)))))])
    (result (demand inputs)
      (non-empty-listof
        (and/c boolean? (lambda (b) (equal? b demand))))))
  (map (lambda (s) stars-upon-thars?) sneetches))

It *appears* to work, but is this correct? I'm not 100% on the binding
rules inside a contract body. If this is correct, was there a simpler way
to do this?

Thanks,
Sage

-- 
You received this message because you are subscribed to the Google Groups "Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscribe-/JYPxA39Uh5TLH3MbocFF+G/[email protected]
For more options, visit https://groups.google.com/d/optout.