(module doublecheck scheme

  (require (lib "unit.ss")
           ;;(lib "etc.ss")
           "../language/defun.scm"
           "../private/planet.ss"
           scheme/gui/dynamic
           (planet schematics/schemeunit:2:10/test)
           scheme/stxparam
           (for-syntax syntax/stx scheme/stxparam-exptime))
  (require-fasttest-for-doublecheck)
  (require-for-syntax-cce/scheme)
  (require-cce/scheme)

  (provide teachpack^ teachpack@ dracula-random?)

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  RANDOM GENERATOR FUNCTIONS
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (random-acl2-boolean) (r:random-choice 't '()))
  (define (random-acl2-symbol) (r:random-symbol))
  (define (random-acl2-string) (r:random-string))
  (define (random-acl2-char) (r:random-char))
  (define (random-acl2-number) (r:random-exact))
  (define (random-acl2-rational) (r:random-rational))
  (define (random-acl2-integer) (r:random-integer))
  (define (random-acl2-natural) (r:random-natural))
  (define (random-acl2-between lo hi) (r:random-integer/uniform lo hi))
  (define (random-acl2-data-size) (r:random-natural/geometric 1/4 0))

  (define (random-acl2-element-of l)
    (list-ref l (random-acl2-between 0 (- (length l) 1))))

  (define (random-acl2-atom)
    (r:random-case
     (random-acl2-boolean)
     (random-acl2-symbol)
     (random-acl2-string)
     (random-acl2-char)
     (random-acl2-number)))

  (define (random-acl2-sexp-of/proc make-atom size)
    (if (<= size 0)
        (make-atom)
        (let* ([left (random-acl2-between 0 (- size 1))]
               [right (- size left 1)])
          (cons (random-acl2-sexp-of/proc make-atom left)
                (random-acl2-sexp-of/proc make-atom right)))))

  (define-syntax (random-acl2-sexp-of stx)
    (syntax-case stx (:size)
      [(_ atom :size size)
       (syntax/loc stx
         (random-acl2-sexp-of/proc (lambda () atom) size))]
      [(_ atom)
       (syntax/loc stx
         (random-acl2-sexp-of atom :size (random-acl2-data-size)))]))

  (define (random-acl2-sexp)
    (random-acl2-sexp-of (random-acl2-atom)))

  (define (random-acl2-list-of/proc make-elem size)
    (if (<= size 0)
        '()
        (cons (make-elem) (random-acl2-list-of/proc make-elem (- size 1)))))

  (define-syntax (random-acl2-list-of stx)
    (syntax-case stx (:size)
      [(_ elem :size size)
       (syntax/loc stx
         (random-acl2-list-of/proc (lambda () elem) size))]
      [(_ elem)
       (syntax/loc stx
         (random-acl2-list-of elem :size (random-acl2-data-size)))]))

  (define-for-syntax (expand-random-case-args stx)
    (syntax-case stx (:weight)
      [() stx]
      [(:weight . _)
       (syntax-error (stx-car stx)
                     "got :weight keyword instead of an expression")]
      [(arg :weight)
       (syntax-error (stx-car (stx-cdr stx))
                     "got :weight keyword without a weight")]
      [(arg :weight :weight . _)
       (syntax-error (stx-car (stx-cdr (stx-cdr stx)))
                     "got duplicate :weight keyword")]
      [(arg :weight wt . rest)
       (quasisyntax/loc stx
         (arg #:weight wt #,@(expand-random-case-args #'rest)))]
      [(arg . rest)
       (quasisyntax/loc stx
         (arg #,@(expand-random-case-args #'rest)))]
      [_ (syntax-error
          stx
          "expected a sequence of arguments with :weight keywords")]))

  (define-syntax (random-acl2-case stx)
    (parameterize ([current-syntax stx])
      (syntax-case stx ()
        [(_ . rest)
         (quasisyntax/loc stx
           (r:random-case #,@(expand-random-case-args #'rest)))])))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  RANDOM GENERATOR MACROS (unusable in regular code)
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define-syntax-parameter dracula-random? #f)

  (define-for-syntax (make-random-transformer id)
    (lambda (stx)
      (if (syntax-parameter-value #'dracula-random?)
          (syntax-case stx ()
            [(_ . rest) (quasisyntax/loc stx (#,id . rest))]
            [_ id])
          (raise-syntax-error
           #f
           "cannot be used outside random testing"
           stx))))

  (define-syntax (macro:defrandom stx)
    (syntax-case stx ()
      [(_ f (arg ...) body)
       (with-syntax ([(formal ...) (generate-temporaries #'(arg ...))]
                     [g (syntax-local-introduce #'f)])
         (syntax/loc stx
           (begin (defun g (arg ...)
                    (syntax-parameterize ([dracula-random? #t]) body))
                  (define-syntax f (make-random-transformer #'g)))))]))

  (define-syntax (define-random-macro stx)
    (syntax-case stx ()
      [(_ macro (function arg ...))
       (syntax/loc stx
         (macro:defrandom
          macro (arg ...)
          (function arg ...)))]))

  (define-syntax macro:random-case
    (make-random-transformer #'random-acl2-case))
  (define-syntax macro:random-list-of
    (make-random-transformer #'random-acl2-list-of))
  (define-syntax macro:random-sexp-of
    (make-random-transformer #'random-acl2-sexp-of))

  (define-random-macro macro:random-boolean (random-acl2-boolean))
  (define-random-macro macro:random-symbol (random-acl2-symbol))
  (define-random-macro macro:random-char (random-acl2-char))
  (define-random-macro macro:random-string (random-acl2-string))
  (define-random-macro macro:random-number (random-acl2-number))
  (define-random-macro macro:random-rational (random-acl2-rational))
  (define-random-macro macro:random-integer (random-acl2-integer))
  (define-random-macro macro:random-natural (random-acl2-natural))
  (define-random-macro macro:random-between (random-acl2-between lo hi))
  (define-random-macro macro:random-atom (random-acl2-atom))
  (define-random-macro macro:random-sexp (random-acl2-sexp))
  (define-random-macro macro:random-data-size (random-acl2-data-size))
  (define-random-macro macro:random-element-of (random-acl2-element-of l))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  DEFPROPERTY and CHECK-PROPERTIES
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  ;; reversed-properties : (Listof (-> TestSuite))
  ;; Mutable variable holding thunks generated but not run so far.
  ;; Each thunk constructs a test suite for a doublecheck property.
  (define reversed-properties null)

  (define (add-property! prop)
    (set! reversed-properties
          (cons prop reversed-properties)))

  (define (acl2-true? v)
    (not (or (eq? v 'nil) (eq? v '()))))

  (define-check (check-acl2-true v)
    (unless (acl2-true? v)
      (fail-check)))

  (define-for-syntax (expand-defproperty-clause stx)
    (syntax-case stx (:value)
      [(var guard :value expr)
       (syntax/loc stx
         (var (syntax-parameterize ([dracula-random? #t]) expr)
              #:limit 2500
              #:where (acl2-true? guard)))]
      [(var guard)
       (expand-defproperty-clause
        (syntax/loc stx
          (var guard :value (random-acl2-sexp))))]))

  (define-syntax (macro:defproperty stx)
    (syntax-case stx ()
      [(form name (clause ...) body . rest)
       (with-syntax* ([([lhs rhs opt ...] ...)
                       (map expand-defproperty-clause
                            (syntax->list #'(clause ...)))])
         (syntax/loc stx
           (begin
             (define-syntax (name stx*)
               (raise-syntax-error #f "cannot be used in an expression" stx*))
             (add-property!
              (lambda ()
                (test-random #:name (symbol->string 'name)
                             #:repeat 50
                             ([lhs rhs opt ...] ...)
                             (with-check-info
                              (['check-expect
                                `(check-expect
                                  (let ((lhs ',lhs) ...) body)
                                  t)])
                              (check-acl2-true body))))))))]))

  (define (get-ui/name file value)
    (dynamic-require
     `(planet ,file ("schematics" "schemeunit.plt" 2 10))
     value))

  (define (get-test-ui)
    (if (gui-available?)
        (lambda (test)
          (thread
           (lambda ()
             ((get-ui/name "graphical-ui.ss" 'test/graphical-ui) test))))
        (get-ui/name "text-ui.ss" 'test/text-ui)))

  (define (check-properties!)
    (when (cons? reversed-properties)
      (let* ([properties (reverse reversed-properties)])
        (set! reversed-properties null)
        ((get-test-ui)
         (apply test-suite "DoubleCheck" (map call properties)))
        't)))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  SIGNATURE AND UNIT
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define-signature teachpack^
    [

     ;; Random macros
     (define-syntaxes (defproperty)
       (make-rename-transformer #'macro:defproperty))
     (define-syntaxes (defrandom)
       (make-rename-transformer #'macro:defrandom))
     (define-syntaxes (random-case)
       (make-rename-transformer #'macro:random-case))

     ;; Random primitive types
     (define-syntaxes (random-boolean)
       (make-rename-transformer #'macro:random-boolean))
     (define-syntaxes (random-symbol)
       (make-rename-transformer #'macro:random-symbol))
     (define-syntaxes (random-char)
       (make-rename-transformer #'macro:random-char))
     (define-syntaxes (random-string)
       (make-rename-transformer #'macro:random-string))
     (define-syntaxes (random-number)
       (make-rename-transformer #'macro:random-number))
     (define-syntaxes (random-rational)
       (make-rename-transformer #'macro:random-rational))
     (define-syntaxes (random-integer)
       (make-rename-transformer #'macro:random-integer))
     (define-syntaxes (random-natural)
       (make-rename-transformer #'macro:random-natural))

     ;; Random custom atoms
     (define-syntaxes (random-data-size)
       (make-rename-transformer #'macro:random-data-size))
     (define-syntaxes (random-between)
       (make-rename-transformer #'macro:random-between))

     ;; Random atoms and s-expressions
     (define-syntaxes (random-atom)
       (make-rename-transformer #'macro:random-atom))
     (define-syntaxes (random-sexp)
       (make-rename-transformer #'macro:random-sexp))

     ;; Random higher-order data
     (define-syntaxes (random-list-of)
       (make-rename-transformer #'macro:random-list-of))
     (define-syntaxes (random-sexp-of)
       (make-rename-transformer #'macro:random-sexp-of))

     ;; Random selection
     (define-syntaxes (random-element-of)
       (make-rename-transformer #'macro:random-element-of))

     ;; Boilerplate function
     check-properties

     ])

  (define-unit teachpack@
    (import)
    (export teachpack^)

    (define check-properties check-properties!))

  )