(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"))
(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 "eprintf.scm")
(import drscheme:tool^
dracula-language-interface^)
(export dracula-language^)
(define acl2-language-name/version "Dracula ACL2")
(drscheme:language:register-capability
'drscheme:special:uninstall-acl2-tool
(flat-named-contract "boolean" boolean?)
#f)
(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) acl2-language-name/version))
(define mbl% (drscheme:language:simple-module-based-language->module-based-language-mixin
drscheme:language:simple-module-based-language%))
(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 Languages" acl2-language-name/version))
(define/override (get-one-line-summary)
"Run ACL2 programs")
(define/override (on-execute settings run-in-user-thread)
(super on-execute (if (pair? settings) (cdr settings) settings) run-in-user-thread)
(run-in-user-thread
(lambda ()
(begin
(read-square-bracket-as-paren #f)
(read-case-sensitive #f)
(read-accept-box #f)
(read-accept-reader #f)
(read-decimal-as-inexact #f)))))
(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 (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))
(super default-settings? (cdr s))))))
(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)
(let ([state 'init]
[real-module #f]
[reader (get-reader)])
(lambda ()
(case state
[(init)
(set! state 'require)
(let ([body-exps
(let loop ()
(let ([result (reader (object-name port) port)])
(if (eof-object? result)
null
(cons result (loop)))))]
[language-module (get-module)])
(let ([m (datum->syntax-object
#f
`(,#'module #%dracula-program ,language-module
(#%module-begin ,@body-exps)))])
(augment-with-expression-printing
(expand m))))]
[(require)
(set! state 'done)
(syntax
(let ([done-already? #f])
(dynamic-wind
void
(lambda ()
(eval #'(require #%dracula-program)) )
(lambda ()
(unless done-already?
(set! done-already? #t)
(current-namespace (module->namespace '#%dracula-program)))))))]
[(done) eof]))))
(define/augment (capability-value key)
(inner (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 (drscheme:language:get-capability-default key)])
capability-value key))
(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]))
(define/override (order-manuals x)
(values (list #"acl2-html-docs" #"teachpack" #"drscheme" #"help") #t))
(super-new)))
)