#|
Defines a class that whose instances manage connections to the external
ACL2 process.  
|#

#| NOTES:
The interrupt method in acl2-process% is broken.  

In principle, we could trigger an interrupt signal using 
(*acl2-control* 'interrupt), but that would only send the signal
to the shell script process that has spawned the ACL2/LISP process.
Also, on Windows, MzScheme doesn't guarantee that 'interrupt would do anything.
|#
(module acl2-process mzscheme
  (require (lib "async-channel.ss")
           (lib "process.ss")
           (lib "class.ss")
           (lib "port.ss")
           (lib "etc.ss")
           (lib "moddep.ss" "syntax")
           (lib "mred.ss" "mred")) ;; for yield
  (require "../language/find-acl2.scm"
           "../language/acl2-module-v.scm"
           "windows-interrupt.scm"
           "../language/acl2-path-to-lisp-command.scm")
  (provide acl2-process%)
  
  (error-print-width 500)
  
  #;(require (file "eprintf.scm"))
  (define err-port (current-error-port))
  
  (define stars-re "\\*\\*\\*\\*\\*\\*\\*\\*") ;; matches "********"
  (define failure-re
    (string-append stars-re " FAILED " stars-re
                   "  See :DOC failure  "
                   stars-re " FAILED " stars-re))
  (define failure-str 
    "******** FAILED ********  See :DOC failure  ******** FAILED ********")
  (define error-re "ACL2 Error in")
  (define raw-lisp-re "RAW LISP")
  
  (define raw-lisp-bytes #"RAW LISP")
  
  (define prompt-re "ACL2 !>")
  
  (define proof-tree-start-re "#<\\\\<0")
  (define proof-tree-start-bytes #"#<\\<0")
  (define proof-tree-stop-re "#>\\\\>")
  
  (define done-str "|||this-symbol-indicates-that-ACL2-is-done|||")
  (define done-bytes #"|\\|\\|\\|this-symbol-indicates-that-ACL2-is-done\\|\\|\\||")
  (define done-sym (string->symbol done-str))
  (define done-re "\\|\\\\\\|\\\\\\|\\\\\\|this-symbol-indicates-that-ACL2-is-done\\\\\\|\\\\\\|\\\\\\|\\|")
  
  (define (send-done port)
    (write `(intern ,done-str "ACL2") port))
  
  #;(define fail-or-error-or-prompt-re
      (regexp (string-append failure-re "|" error-re "|" prompt-re)))
  
  #;(define fail-or-error-or-done-re
      (regexp (string-append failure-re "|" error-re "|" done-re)))
  
  (define pftree/done-re
    (regexp (string-append proof-tree-start-re "|" done-re)))
  
  (define fail/error/pftree/done-re
    (regexp (string-append failure-re "|" 
                           error-re "|" 
                           ;; raw-lisp-re "|"
                           proof-tree-start-re "|" done-re)))
  
  (define (copy-rest in-> ->out)
    (regexp-match done-re in-> 0 #f ->out)
    (regexp-match prompt-re in-> 0 #f ->out)
    #;(let ([tid (thread (lambda () (copy-port in-> ->out)))])
        (sync/timeout/enable-break 2 tid)
        (kill-thread tid)))
  
  (define (extract-prooftree from->)
    (let ([proof-tree-port (open-output-string)])
      (regexp-match proof-tree-stop-re from-> 0 #f proof-tree-port)
      (get-output-string proof-tree-port)))
  
  (define (spawn/connect-output status-channel acl2-> ->console send-new-prooftree)
    (thread 
     (lambda ()
       ;; Throw away banner text from "Initialized with" to the prompt
       (regexp-match "Initialized with" acl2-> 0 #f ->console)
       (regexp-match prompt-re acl2-> 0 #f)
       (let loop ()
         (let* ([matched
                 (let ([m (regexp-match fail/error/pftree/done-re
                                        acl2-> 0 #f ->console)])
                   (if m
                       (car m)
                       (raise-user-error 
                        'acl2-output-thread
                        "Output matches none of fail|error|pftree|done")))]
                
                [status
                 (cond [(equal? matched done-bytes) #t]
                       [(equal? matched proof-tree-start-bytes) 'proof-tree-start]
                       #;[(equal? matched raw-lisp-bytes) 'raw-lisp]
                         [else #f])])
           (case status
             [(proof-tree-start)
              (send-new-prooftree (extract-prooftree acl2->))]
             #;[(raw-lisp) '???]
             [(#t) (async-channel-put status-channel #t)]
             [(#f) (begin
                     (display matched ->console)
                     (flush-acl2-input acl2-> ->console send-new-prooftree)
                     (async-channel-put status-channel #f))])
           (loop))))))
  
  (define (flush-acl2-input acl2-> ->console send-new-prooftree)
    (let loop ()
      (let* ([matched (car (regexp-match pftree/done-re
                                         acl2-> 0 #f ->console))]
             [status (cond [(equal? matched done-bytes) 'done]
                           [(equal? matched proof-tree-start-bytes) 'proof-tree-start])])
        (case status
          [(done) 'done]
          [(proof-tree-start)
           (begin (send-new-prooftree (extract-prooftree acl2->))
                  (loop))]))))
  
  (define acl2-process%
    (class object% ()
      (init-field send-new-prooftree)
      (init-field [acl2-output-port err-port])
      (init-field [path (find-acl2)])
      
      (field [status-channel (make-async-channel)])
      
      (define process-alive? #f)
      
      (define-values (*acl2->me* *me->acl2* *PID* *acl2-error->me* *acl2-control*)
        (values #f #f #f #f #f))
      
      (define output-thread #f)
      
      (define/private (initialize-acl2-environment!)
        (for-each (lambda (x) (send this send-to-repl x))
                  `(:start-proof-tree
                    (set-ld-pre-eval-print t state)
                    (add-include-book-dir :teachpacks ,teachpack-path))))
      
      ;; -> pid or raises exn.
      (define/public (start!)
        (when (not process-alive?)
          (set!-values (*acl2->me* *me->acl2* *PID* *acl2-error->me* *acl2-control*)
                       (apply values
                              (apply process* (acl2-path->command-list path))))
          (case (*acl2-control* 'status)
            [(running) 
             (begin
               (set! process-alive? #t)
               (set! output-thread 
                     (spawn/connect-output status-channel *acl2->me* acl2-output-port
                                           send-new-prooftree))
               (initialize-acl2-environment!))]
            [else (raise-user-error 'acl2-process%::start 
                                    "Failed to start ACL2 (using this path: ~a)"
                                    path)])
          *PID*))
      
      (define/public (stop!)
        (when *acl2-control*
          (when output-thread (kill-thread output-thread))
          (*acl2-control* 'kill)
          #|
          (write-string "#. :q (good-bye)" *me->acl2*)
          (newline *me->acl2*)
          (flush-output *me->acl2*)
          |#
          
          (close-input-port *acl2->me*)
          (close-input-port *acl2-error->me*)
          (close-output-port *me->acl2*)
          (set!-values (process-alive? *acl2->me* *me->acl2* *PID* 
                                       *acl2-error->me* *acl2-control*)
                       (apply values (build-list 6 (lambda _ #f))))
          ))
      
      (define error-str
        (string-append 
         "Dracula currently only works on Windows, Unix, and "
         "Mac OS X.  You appear to be running on ~a.  Please file"
         " a bug report and include this message!"))
      
      (define/public (interrupt)
        (case (system-type 'os)
          [(windows) 
           (begin (windows-interrupt path *PID*)
                  (send-to-repl "#."))]
          [(unix macosx) 
           (begin (*acl2-control* 'interrupt) 
                  (send-to-repl "#."))]
          [else (raise-user-error 'Interrupt-ACL2
                                  error-str
                                  (system-type 'os))]))
      
      (define/public (undo-last)
        (send-to-repl ':u))
      
      (define/public (reset-acl2)
        (string->repl ":ubt! 1")
        (initialize-acl2-environment!))
      
      (define/public (send-to-repl s-exp)
        (when (not process-alive?)
          (start!))
        (if (string? s-exp)
            (string->repl s-exp)
            (s-exp->repl s-exp)))
      
      (define (string->repl str)
        (write-string str *me->acl2*)
        (newline *me->acl2*)
        (send-done *me->acl2*)
        (newline *me->acl2*)
        (flush-output *me->acl2*)
        (yield status-channel))
      
      (define/public (s-exp->repl s-exp)
        (write s-exp *me->acl2*)
        (newline *me->acl2*)
        (send-done *me->acl2*)
        (newline *me->acl2*)
        (flush-output *me->acl2*)
        (yield status-channel))
      
      (super-new)))
  
  )