(module with-prover-time-limit mzscheme
  (require "../private/planet.ss")
  (require-for-syntax-cce/scheme)
  (provide with-prover-time-limit)
  
  (define error-str
    "Expected a positive rational or a singleton list containing a positive rational, but got ~s instead")
  
  (define (valid-timeout-value? timeout-val)
    (or (and (rational? timeout-val)
             (positive? timeout-val))
        (and (pair? timeout-val)
             (rational? (car timeout-val))
             (positive? (car timeout-val))
             (null? (cdr timeout-val)))))
  
  (define-syntax (with-prover-time-limit stx)
    (syntax-case* stx (:loosen-ok) text=?
      [(_ timeout form :loosen-ok ok?) 
       (quasisyntax/loc stx
         ;; `form' is usually a top-level definition (or defthm),
         ;; so we need to expand into `begin'.
         (begin (define timeout-val timeout)
                (unless (valid-timeout-value? timeout-val)
                  (raise-syntax-error 'with-prover-time-limit 
                                      (format error-str timeout-val)
                                      (quote-syntax #,stx)
                                      (quote-syntax #,#'timeout)))
                form))]
      [(_ timeout form)
       (syntax/loc stx (with-prover-time-limit timeout form :loosen-ok t))])))