Contract.rkt

(define-struct/contract nand-gate
  ([xin boolean?]
   [yin boolean?])
  #:transparent)

(define-syntax not-gate
  (syntax-rules ()
   [(not-gate e) (nand-gate e e)]))

(define-syntax and-gate
  (syntax-rules ()
    [(and-gate f-expr s-expr)
     (nand-gate (nand-gate f-expr s-expr)
                (nand-gate f-expr s-expr))]))

(define-syntax or-gate
  (syntax-rules ()
    [(or-gate f-expr s-expr)
     (nand-gate (nand-gate f-expr f-expr)
                (nand-gate s-expr s-expr))]))

(define-syntax nor-gate
  (syntax-rules ()
    [(nor-gate f-expr s-expr)
     (not-gate (or-gate f-expr s-expr))]))

(define-syntax xor-gate
  (syntax-rules ()
    [(xor-gate f-expr s-expr)
     (nand-gate (nand-gate f-expr (nand-gate f-expr s-expr))
                (nand-gate s-expr (nand-gate f-expr s-expr)))]))


(define-syntax xnor-gate
  (syntax-rules ()
    [(xnor-gate f-expr s-expr)
     (nand-gate (nand-gate (nand-gate f-expr f-expr)
                           (nand-gate s-expr s-expr))
                (nand-gate f-expr s-expr))]))
     
;Now just write one evaluator, and you have everything.
; The idea is to keep core simple and checkable. I am wondering
; if this whole thing can be applied in theorem proving.

(define (eval-nand-expr expr)
  (match expr
    [(nand-gate #f #f) #t]
    [(nand-gate #f #t) #t]
    [(nand-gate #t #f) #t]
    [(nand-gate #t #t) #f]
    [(nand-gate f-expr s-expr)
     (let ([feval (eval-nand-expr f-expr)]
           [seval (eval-nand-expr s-expr)])
       (eval-nand-expr feval seval))]))


Tmp.rkt> (and-gate #t #f)
; make-nand-gate: contract violation
;   expected: boolean?
;   given: (nand-gate #t #f)
;   in: the 1st argument of
;       (-> boolean? boolean? symbol? any)
;   contract from: (struct nand-gate)
;   blaming: /Users/keep_learning/Tmp.rkt
;    (assuming the contract is correct)
;   at: /Users/keep_learning/Tmp.rkt
; Context:
;  /Applications/Racket-v7.2/collects/racket/repl.rkt:11:26
Tmp.rkt>

I understand this error because macro expression is compile time, and and-gate expension gives 
nand-gate (nand-gate #t #f)
          (nand-gate #t #f) 
So I am wondering how to write the contract to acccomodate this expression ?