#|
Need to manage custodians better.
|#
(module acl2-controller mzscheme
  
  (require (lib "class.ss")
           (lib "mred.ss" "mred")
           (lib "framework.ss" "framework")
           (lib "unit.ss")
           (lib "tool.ss" "drscheme")
           (lib "port.ss")
           
           "admit-dialog.scm"
           "acl2-proof-window.scm"
           "acl2-process.scm"
           "../language/find-acl2.scm"
           )

  (provide acl2-controller%)
  
  (define (display-admit-failure-dialog parent)
    (message-box "Failed to admit definitions"
                 (string-append
                  "ACL2 failed to admit your definitions.  To discover why, click Start ACL2 "
                  "and try admitting your definitions interactively.")
                 parent
                 '(ok stop)))
  
  ;; This controller mediates between the DrS GUI and
  ;; an instance of acl2-process%.
  (define acl2-controller%
    (class* object% ()
      
      (field [acl2-process #f])
      (field [acl2-proof-window #f])
      (field [acl2-custodian #f])
      
      ;; Invoked when the proof console closes
      (define/public (proof-window-closed) (shutdown-acl2))
      
      (define/public (start-acl2 path)
        (set! acl2-custodian (make-custodian))
        (parameterize ([current-eventspace (make-eventspace)])
          (set! acl2-proof-window
                (new acl2-proof-window%
                     [parent #f]
                     [notify-controller-of-close 
                      (lambda () (send this proof-window-closed))])))
        (parameterize ([current-custodian acl2-custodian])
          (set! acl2-process 
                (new acl2-process% 
                     [acl2-output-port (send acl2-proof-window get-write-port)]
                     [path path]
                     [send-new-prooftree 
                      (lambda (tree) 
                        (send acl2-proof-window set-proof-tree tree))]))
          (with-handlers ([exn:fail:user?
                           (lambda (e)
                             (set! acl2-proof-window #f)
                             (custodian-shutdown-all acl2-custodian)
                             (set! acl2-custodian #f)
                             (raise e))])
            (send acl2-process start!)
            (send acl2-proof-window show #t))))
      
      
      (define/public (shutdown-acl2)
        (when acl2-process 
          (send acl2-process stop!)
          (set! acl2-process #f))
        (when acl2-custodian 
          (custodian-shutdown-all acl2-custodian)
          (set! acl2-proof-window #f)
          (set! acl2-custodian #f)))
      
      ;; -> boolean
      ;; Produce #t if ACL2 admits the definitions window, #f otherwise.
      (define/public (admit-definitions-window dt drs-frame)
        (let ([admitted?
               (let ([exprs (send dt get-s-expressions)])
                 (if (null? exprs)
                     #t
                     (send (new admit-dialog%
                                [parent drs-frame] 
                                [expressions exprs])
                           admit!)))])
          (unless admitted? (display-admit-failure-dialog drs-frame))
          admitted?))
      
      (define/public (admit-next dt)
        (let ([expr-str (send dt get-next-unadmitted-sexp)])
          (and 
           expr-str
           (if (or (string-ci=? expr-str ":q")
                   (string-ci=? expr-str "(good-bye)"))
               (begin (send dt highlight-next-unadmitted-sexp #f)
                      (message-box ":q or (good-bye) found in definitions window"
                                   (format "Use the Stop Prover button to stop ACL2 instead of sending ~a via the Admit button" expr-str)
                                   #f ;drscheme-frame
                                   '(ok stop))
                      #f)
               (let ([admitted? (send acl2-process send-to-repl expr-str)])
                 (send dt highlight-next-unadmitted-sexp admitted?)
                 admitted?)))))

      (define/public (admit-sexp sexp)
        (send acl2-process send-to-repl sexp))

      (define/public (admit-event expr)
        (send acl2-process repl-event expr))
      
      (define/public (admit-all dt)
        (with-handlers ([exn:fail? void])
          (let loop ()
            (when (admit-next dt)
              (loop)))))
      
      (define/public (undo-all)
        (send acl2-process reset-acl2))

      (define (acl2-filename str)
        (let* ([sys-type (system-path-convention-type)])
          (case sys-type
            [(unix) str]
            [(windows) (regexp-replace* "\\\\" str "/")]
            [else (error 'acl2-filename
                         "cannot build path for unknown system type ~s"
                         sys-type)])))

      (define/public (certify-book filename)
        (send acl2-process reset-acl2)
        (send acl2-process
              send-to-repl
              `(certify-book ,(acl2-filename filename) 1)))
      
      ;; definitions:text<%> -> void
      (define/public (undo-last dt)
        (let ([was-event-form? (send dt unhighlight-last-admitted)])
          (when was-event-form? (send acl2-process undo-last))))
      
      (define/public (interrupt-acl2) 
        (send acl2-process interrupt))
      
      (super-new)))
  )