#|
Implements DrS's language interface.
|#
(module dracula-language (lib "a-unit.ss")
  (require (lib "class.ss")
           (lib "contract.ss")
           (lib "mred.ss" "mred")
           (lib "framework.ss" "framework")
           (lib "tool.ss" "drscheme")
           (lib "unit.ss")
           (lib "async-channel.ss")
           (lib "contract.ss")
           (lib "list.ss")
           (lib "getinfo.ss" "setup")
           (lib "etc.ss")
           (only scheme/file get-preference)
           (only test-engine/scheme-gui make-formatter)
           (only test-engine/scheme-tests scheme-test-data test-format test-execute)
           (lib "test-display.scm" "test-engine")
           )
  
  (require "printer.scm"
           "acl2-module-v.scm"
           (prefix acl2: "acl2-reader.scm")
           "dracula-language-sig.scm"
           "dracula-language-interface-sig.scm"
           "acl2-settings.scm"
           "config-panel.scm")
  
  ;(require "tool-name.scm")
  (require "eprintf.scm")
  
  (import drscheme:tool^
          dracula-language-interface^)
  (export dracula-language^)

  (define dracula-language-section "Dracula Languages")
  (define dracula-language-name
    (format "Dracula v~s.~s" pkg-major pkg-minor))
  
  (define dracula-language-number/major 5000)
  (define dracula-language-number/minor
    (- 1000 (* 100 pkg-major) pkg-minor))
  
  (drscheme:language:register-capability 
   'drscheme:special:uninstall-acl2-tool
   (flat-named-contract "boolean" boolean?)
   #f)
  
  ;; Language-Settings -> String
  ;; Produces the name of the language
  (define (extract-language-level settings)
    (let* ([language (drscheme:language-configuration:language-settings-language settings)])
      (car (last-pair (send language get-language-position)))))
  
  (define (is-acl2? settings)
    (string=? (extract-language-level settings) dracula-language-name))
  
  (define mbl% (drscheme:language:simple-module-based-language->module-based-language-mixin
                drscheme:language:simple-module-based-language%))
  
  (define drs-eventspace (current-eventspace))

  (define acl2-mbl%
    (class* mbl% (drscheme:language:module-based-language<%>)
      (define/override (get-module) acl2-module-v)
      (define/override (get-transformer-module) acl2-module-v)
      
      (define/override (get-reader) 
        (lambda args
          (let ([v (apply acl2:read-syntax args)])
            (if (eof-object? v)
                v
                (namespace-syntax-introduce v)))))
      
      (define/override (get-language-position) 
        (list dracula-language-section dracula-language-name))
      (define/override (get-language-numbers)
        (list dracula-language-number/major
              dracula-language-number/minor))
      (define/override (get-one-line-summary) "Run ACL2 programs")
      
      ;; Tries to admit definitions before allowing access to interactions
      ;; (when the settings say so).
      (define/override (on-execute settings run-in-user-thread)
        (let* ([drscheme-ns (current-namespace)]
               [test-engine-path
                ((current-module-name-resolver)
                 'test-engine/scheme-tests #f #f)])
          (run-in-user-thread
           (lambda ()
             (namespace-attach-module drscheme-ns test-engine-path)
             (namespace-require test-engine-path)
             (scheme-test-data
              (list (drscheme:rep:current-rep) drs-eventspace test-display%))
             (test-execute (get-preference 'tests:enable? (lambda () #t)))
             (test-format
              (make-formatter
               (lambda (v o) (render-value/format v settings o 40))))
             )))
        (super on-execute
               (if (pair? settings) (cdr settings) settings)
               run-in-user-thread))
      
      (define/override (render-value/format value settings port width)
        (unless (void? value)
          (super render-value/format
                 (acl2-convert value) 
                 (if (pair? settings) (cdr settings) settings)
                 port
                 width)))
      
      (super-new [module (get-module)]
                 [language-position (get-language-position)])))
  
  (define acl2-language/no-manual% 
    (drscheme:language:module-based-language->language-mixin acl2-mbl%))
  
  (define dracula-settings/c (cons/c acl2-settings? drscheme:language:simple-settings?))
  (define dracula-language%
    (class* acl2-language/no-manual% (dracula-language<%>)
      (object-contract 
       [default-settings  [-> dracula-settings/c]]
       [default-settings? [dracula-settings/c . -> . boolean?]]
       [marshall-settings? [dracula-settings/c . -> . any]]
       [unmarshall-settings? [any/c . -> . dracula-settings/c]])
      
      (inherit get-reader get-module)
      
      (define/public (dracula-language?) #t)

      (define/override (create-executable settings parent filename)
        (message-box "Create Executable: Error"
                     "Sorry, Dracula does not support creating executables."
                     #f '(ok stop))
        (void))
      
      (define/override (config-panel parent)
        (attach-config-panel! parent (super config-panel parent)))
      
      (define/override (default-settings) 
        (cons default-acl2-settings (super default-settings)))
      
      (define/override (default-settings? s)
        (and (pair? s)
             (let ([s/acl2 (car s)]
                   [d/acl2 default-acl2-settings])
               (and (eq? (acl2-settings-admit-before-run? s/acl2)
                         (acl2-settings-admit-before-run? d/acl2))
                    (equal? (acl2-settings-acl2-loc s/acl2)
                            (acl2-settings-acl2-loc d/acl2))))))
      
      (define/override (marshall-settings s)
        (if (pair? s)
            (cons (marshall-acl2-settings (car s))
                  (super marshall-settings (cdr s)))
            (super marshall-settings s)))
      
      (define/override (unmarshall-settings v)
        (if (pair? v)
            (cons (unmarshall-acl2-settings (car v))
                  (super unmarshall-settings (cdr v)))
            (super unmarshall-settings v)))
      
      (define/override (front-end/complete-program port settings)

        (define reader (get-reader))
        (define name (object-name port))

        (define (read-all)
          (let* ([next (reader name port)])
            (if (eof-object? next)
                null
                (cons next (read-all)))))

        (define (build-module)
          (begin0
            (augment-with-expression-printing
             (expand
              (datum->syntax-object
               #f
               `(,#'module #%dracula-program ,(get-module)
                  (#%module-begin ,@(read-all))))))
            (set! go require-module)))

        (define (require-module)
          (begin0
            #'(require '#%dracula-program)
            (set! go open-module)))

        (define (open-module)
          (begin0
            #'(current-namespace (module->namespace '(quote #%dracula-program)))
            (set! go done)))

        (define (done) eof)

        (define go build-module)

        (lambda () (go)))
      
      ;; CAPABILITIES
      (define/augment (capability-value key)
        (case key
          [(drscheme:define-popup) (cons "(def" "(defun ...)")]
          [(drscheme:language-menu-title) "Dracula"]
          [(drscheme:special:insert-fraction
            drscheme:special:insert-lambda
            drscheme:special:insert-image
            drscheme:special:insert-comment-box
            drscheme:special:insert-gui-tool
            drscheme:special:slideshow-menu-item
            drscheme:special:insert-text-box
            drscheme:special:xml-menus) #f]
          [(drscheme:special:uninstall-acl2-tool) #t]
          [else (inner (drscheme:language:get-capability-default key)
                       capability-value key)]))
      
      ;; adapted from collects/lang/htdp-langs.ss
      (define (augment-with-expression-printing stx)
        (syntax-case stx (module #%plain-module-begin define-values define-syntaxes)
          [(module name lang (#%plain-module-begin 
                              (define-values (pe) _body)
                              bodies ...))
           (with-syntax ([print-results
                          (lambda results
                            (let ([rep (drscheme:rep:current-rep)])
                              (when rep
                                (send rep display-results/void results))))])
             #'(module name lang
                 (#%plain-module-begin
                  (define-values (pe) (values print-results))
                  bodies ...)))]
          [_else stx]))
      
      (super-new)))
  )