(module doublecheck mzscheme

  (require (lib "unit.ss")
           (lib "etc.ss")
           "../language/defun.scm"
           (planet "test.ss" ("schematics" "schemeunit.plt" 2 10))
           (planet "graphical-ui.ss" ("schematics" "schemeunit.plt" 2 10))
           (prefix r: (planet "random.ss" ("cce" "fasttest.plt" 1 4)))
           (planet "schemeunit.ss" ("cce" "fasttest.plt" 1 4)))

  (require-for-syntax
   (planet "syntax-utils.ss" ("cce" "syntax-utils.plt" 1 1)))

  (provide teachpack^ teachpack@)

  (define properties '())

  (define random-ok? (make-parameter #f))

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

  (define (check-properties!)
    (test/graphical-ui (apply test-suite "DoubleCheck" (reverse properties)))
    (set! properties '()))

  (define (acl2->boolean v)
    (not (or (equal? v 'nil)
             (equal? v '()))))

  (define-check (check-acl2-true value)
    (unless (acl2->boolean value)
      (fail-check)))

  (define-syntax (check-property stx)
    (syntax-case stx ()
      [(cp ([var gen pred] ...) expr)
       (syntax/loc stx
         (parameterize ([random-ok? #t])
           (check-randomly ([var
                             gen
                             (parameterize ([random-ok? #f])
                               (acl2->boolean pred))]
                            ...)
                           (with-check-info
                            (['duplicate-test
                              `(let ((var (quote ,var)) ...) expr)])
                            (check-acl2-true expr)))))]))

  (define-syntax (test-property stx)
    (syntax-case stx ()
      [(tp title count ([var gen pred] ...) expr)
       (syntax/loc stx
         (apply test-suite title
                (build-list
                 count
                 (lambda (i)
                   (test-case (number->string i)
                     (check-property ([var gen pred] ...) expr))))))]))

  (define-syntax (define-property stx)
    (syntax-case stx ()
      [(dp name count ([var gen pred] ...) expr hints ...)
       (identifier? (syntax name))
       (with-syntax ([title (identifier->string-literal (syntax name))])
         (syntax/loc stx
           (add-property!
            (test-property title count
                           ([var gen pred] ...)
                           expr))))]))

  (define (wrap-generator gen)
    (lambda args
      (if (random-ok?)
          (apply gen args)
          (error (object-name gen)
                 "only runs in the header of defproperty."))))

  (define (boolean->acl2 b)
    (if b 't '()))

  (define (random-acl2-boolean . args)
    (r:random-apply boolean->acl2 (apply r:random-boolean args)))

  (define-syntax (define-generator stx)
    (syntax-case stx ()
      [(dg name (arg ...) (wt gen) ...)
       (syntax/loc stx
         (begin
           (defun name (arg ...) ((wrap-generator hidden) arg ...))
           (r:define-generator (hidden arg ...) (wt gen) ...)))]))

  (define-syntax (HO-random-apply stx)
    (syntax-case stx ()
      [(ra fn arg ...)
       (with-syntax ([(formal ...) (generate-temporaries #'(arg ...))])
         (syntax/loc stx
           ((wrap-generator r:random-apply)
            (lambda (formal ...) (fn formal ...))
            arg ...)))]))

  (define-signature teachpack^
    [ (define-syntaxes (defproperty defgenerator random-apply)
        (values
         (make-rename-transformer #'define-property)
         (make-rename-transformer #'define-generator)
         (make-rename-transformer #'HO-random-apply)))
      check-properties
      random-int-between
      random-size
      random-boolean
      random-char
      random-list-of
      random-string
      random-list
      random-symbol ])

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

    (define check-properties check-properties!)
    (define random-int-between (wrap-generator r:random-int-between))
    (define random-size (wrap-generator r:random-size))
    (define random-boolean (wrap-generator random-acl2-boolean))
    (define random-char (wrap-generator r:random-char))
    (define random-list-of (wrap-generator r:random-list-of))
    (define random-string (wrap-generator r:random-string))
    (define random-list (wrap-generator r:random-list))
    (define random-symbol (wrap-generator r:random-symbol))

    )

  )