(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
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define default-repeat 50)
  (define default-limit 2500)
  (define current-limit (make-parameter #f))

  ;; 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 (keyword-identifier? stx)
    (and (identifier? stx)
         (regexp-match? #rx"^:" (symbol->string (syntax-e stx)))))

  (define-for-syntax (name-identifier? stx)
    (and (identifier? stx)
         (not (keyword-identifier? stx))))

  (define-for-syntax (positive-constant? stx)
    (and (syntax? stx)
         (exact-positive-integer? (syntax-e stx))))

  (define-for-syntax (extract-options stx)
    (syntax-case stx ()
      [(keyword value . rest)
       (and (keyword-identifier? #'keyword)
            (not (keyword-identifier? #'value)))
       (with-syntax ([(((k v) ...) . body)
                      (extract-options #'rest)])
         (syntax/loc stx
           (((keyword value) (k v) ...) . body)))]
      [(keyword . rest)
       (keyword-identifier? #'keyword)
       (syntax-error #'keyword "no value provided")]
      [body (syntax/loc stx (() . body))]))

  (define-for-syntax (parse-options stx)
    (with-syntax ([(opts . rest) (extract-options stx)])
      (cons (sort (syntax->list #'opts) text<? #:key stx-car) #'rest)))

  (define-for-syntax (get-clause-options src var stx)
    (syntax-case stx (:limit :value :where)

      ;; Subsets of the options:
      [((:limit limit) (:value value) (:where where)) #'(limit value where)]
      [((:limit limit) (:value value)) #'(limit value 't)]
      [((:limit limit) (:where where)) #'(limit (random-acl2-sexp) where)]
      [((:value value) (:where where)) #'((current-limit) value where)]
      [((:limit limit)) #'(limit (random-acl2-sexp) 't)]
      [((:value value)) #'((current-limit) value 't)]
      [((:where where)) #'((current-limit) (random-acl2-sexp) where)]
      [() #'((current-limit) (random-acl2-sexp) 't)]

      ;; Error:
      [((key val) ...)
       (raise-syntax-error
        #f
        (format "Unsupported list of variable options: ~s"
                (syntax->datum #'(key ...)))
        src var)]))

  (define-for-syntax (parse-clauses src stx)
    (syntax-case stx ()
      [() null]
      [(var . rest)
       (name-identifier? #'var)
       (with-syntax ([(opts . vars) (parse-options #'rest)])
         (with-syntax ([(limit value where)
                        (get-clause-options src #'var #'opts)])
           (cons #'(var value where limit) (parse-clauses src #'vars))))]
      [(var . rest)
       (raise-syntax-error
        #f "expected a variable, possibly followed by options" #'src #'var)]))

  (define-for-syntax (expand-defproperty stx)
    (syntax-case stx (:repeat :limit)
      [(orig name ((:limit limit) (:repeat repeat)) (var ...) body opt ...)
       (with-syntax ([((lhs rhs hyp lim) ...)
                      (parse-clauses #'orig #'(var ...))])
         (syntax/loc #'orig
           (begin
             (define-syntax (name stx*)
               (raise-syntax-error
                #f
                "DoubleCheck properties may not be used as expressions."
                stx*))
             (add-property!
              (lambda ()
                (let* ([the-limit limit])
                  (test-random
                   #:name (symbol->string 'name)
                   #:repeat repeat
                   #:limit the-limit
                   ([lhs (syntax-parameterize ([dracula-random? #t]) rhs)
                         #:where (acl2-true? hyp)
                         #:limit (parameterize ([current-limit the-limit]) lim)]
                    ...)
                   (with-check-info
                    (['check-expect
                      `(check-expect (let ((lhs ',lhs) ...) body) t)])
                    (check-acl2-true body)))))))))]

      [(orig name ((:limit limit)) (var ...) body opt ...)
       (expand-defproperty
        #'(orig name
                ((:limit limit) (:repeat default-repeat))
                (var ...) body opt ...))]

      [(orig name ((:repeat repeat)) (var ...) body opt ...)
       (expand-defproperty
        #'(orig name
                ((:limit default-limit) (:repeat repeat))
                (var ...) body opt ...))]

      [(orig name () (var ...) body opt ...)
       (expand-defproperty
        #'(orig name
                ((:limit default-limit) (:repeat default-repeat))
                (var ...) body opt ...))]

      [(orig name ((key val) ...) (var ...) body opt ...)
       (raise-syntax-error
        #f
        (format "Unsupported list of defproperty options: ~s"
                (syntax->datum #'(key ...)))
        #'orig)]

      [(orig name ((key val) ...) . rest)
       (raise-syntax-error
        #f
        (format "Expected variables, a body, and theorem options, got: ~s"
                (syntax->datum #'rest))
        #'orig #'rest)]

      [_ (raise-syntax-error 'defproperty "internal error" stx)]))

  (define-syntax (macro:defproperty stx)
    (syntax-case stx ()
      [(_ orig name . rest)
       (name-identifier? #'name)
       (with-syntax ([(options . body) (parse-options #'rest)])
         (expand-defproperty
          #'(orig name options . body)))]
      [(_ orig other . rest)
       (raise-syntax-error
        #f
        (format "expected a property name, got: ~s"
                (syntax->datum #'other))
        #'orig #'other)]
      [(_ orig . rest)
       (raise-syntax-error
        #f
        "expected a property name, variables, and a body, got nothing"
        #'orig)]
      [_ (raise-syntax-error 'defproperty "internal error" stx)]))

  #|
  (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)))

  (define-for-syntax (make-rename/original-transformer id)
    (lambda (stx)
      (with-syntax ([src stx] [dst id])
        (syntax-case stx ()
          [(head . rest)
           (identifier? #'head)
           (syntax/loc stx (dst src . rest))]
          [head
           (identifier? #'head)
           (syntax/loc stx (dst . src))]))))

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

  (define-signature teachpack^
    [

     ;; Random macros
     (define-syntaxes (defproperty)
       (make-rename/original-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!))

  )