(module proof-controller mzscheme

  (require (lib "class.ss")
           (lib "unit.ss")
           (lib "pretty.ss")
           (lib "async-channel.ss")
           (lib "mred.ss" "mred")
           "../../gui/acl2-controller.scm"
           "../expansion/proof-commands.scm"
           "proof-signatures.scm"
           "proof-interfaces.scm")

  (provide proof-controller@)

  (define (command->syntaxes cmd)
    (cond
     [(expr-command? cmd) (list (syntax/loc (expr-command-term cmd) t))]
     [(event-command? cmd) (list (event-command-term cmd))]
     [(module-command? cmd)
      (append (list (datum->syntax-object #f '(defconst *proving-module* t)))
              (module-command-inner cmd)
              (list (syntax/loc (module-command-outer cmd)
                      (ubt! '*proving-module*))))]))

  (define (syntaxes->string stxs)
    (apply string-append (map syntax->string stxs)))

  (define (syntax->string stx)
    (format
     "~a\n"
     (parameterize ([pretty-print-columns 80])
       (pretty-format (syntax-object->datum stx)))))

  ;; message-window : String String -> Void
  ;; Open a NON-MODAL message window.
  (define (message-window title msg)
    (define (callback . _)
      (send frame show #f)
      (async-channel-put channel (void)))
    (define channel (make-async-channel #f))
    (define frame (new frame% [label title]))
    (define panel (new vertical-panel% [parent frame]))
    (define text
      (new text-field%
           [parent panel]
           [label "Message:"]
           [init-value msg]
           [style '(multiple hscroll vertical-label)]
           [enabled #f]))
    (define button
      (new button% [parent panel] [label "OK"] [callback callback]))
    (send frame show #t)
    (yield channel))

  (define-unit proof-controller@
    (import proof-interfaces^)
    (export proof-controller^)

    (define proof-controller%
      (class* object% (proof-controller<%>)
        (super-new)

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  FIELDS
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (init-field observer)

        (define acl2 (new acl2-controller%))

        ;; proof-channel : (Channelof (Channel/EOF ProofCommand))
        (define proof-channel (make-channel))

        ;; stop-channel : (Channelof #t)
        (define stop-channel (make-channel))

        (thread (lambda () (control-inactive)))

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  OBSERVER NOTIFICATION
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        ;; Sends messages to the observer in the current eventspace thread.
        (define-syntax (observe stx)
          (syntax-case stx ()
            [(ob msg arg ...)
             (with-syntax ([(var ...) (generate-temporaries #'(arg ...))])
               (syntax/loc stx
                 (let ([var arg] ...)
                   (queue-callback
                    (lambda ()
                      (send observer msg var ...))
                    #f))))]))

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  CONTROL THREAD METHODS
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (define/private (control-inactive)
          (send acl2 shutdown-acl2)
          (observe proof-term-clear-all)
          (observe proof-active #f)
          (sync (start-event) (stop-event)))

        (define/private (start-event)
          (handle-evt proof-channel (lambda (ch) (control-start ch))))

        (define/private (control-start command-channel)
          (send acl2 start-acl2 "/Users/cce/Local/ACL2/saved_acl2")
          (observe proof-active #t)
          (control-prove-commands command-channel))

        (define/private (control-prove-commands command-channel)
          (sync
           (prove-command-event command-channel)
           (stop-event)))

        (define/private (prove-command-event command-channel)
          (handle-evt command-channel
                      (lambda (cmd)
                        (if (eof-object? cmd)
                            (sync (stop-event))
                            (control-prove-terms (command->syntaxes cmd)
                                                 command-channel)))))

        (define/private (stop-event)
          (handle-evt stop-channel
                      (lambda (_) (control-inactive))))

        (define/private (control-prove-terms terms command-channel)
          (if (null? terms)
              (control-prove-commands command-channel)
              (control-prove-term (car terms) (cdr terms) command-channel)))

        (define/private (control-prove-term term terms command-channel)
          (sync
           (prove-term-event term terms command-channel)
           (stop-event)))

        (define/private (prove-term-event term terms command-channel)
          (observe proof-term-attempt term)
          (sync
           (handle-evt (send acl2 admit-event (syntax-object->datum term))
                       (lambda (proved?)
                         (if proved?
                             (begin
                               (observe proof-term-success term)
                               (control-prove-terms terms command-channel))
                             (begin
                               (observe proof-term-failure term)
                               (sync (stop-event))))))
           (stop-event)))

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  CALLER THREAD METHODS
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  EXTERNAL METHODS
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (define/public (start command-channel)
          (yield (channel-put-evt proof-channel command-channel)))

        (define/public (stop)
          (yield (channel-put-evt stop-channel #t)))

        )))

  )