#lang scheme/base

(require (for-syntax scheme/base "syntax.ss" "proof.ss"))

(provide #%annotate-term #%annotate-part #%annotate-proof
         #%dracula-expr #%dracula-event
         #%dracula-keyword #%dracula-special-event)

(define-for-syntax (expand-wrapper stx)
  (syntax-case stx ()
    [(_ term) #'term]))

(define-syntax #%dracula-expr expand-wrapper)
(define-syntax #%dracula-event expand-wrapper)
(define-syntax #%dracula-keyword expand-wrapper)

(define-syntax (#%dracula-special-event stx)
  (syntax-case stx ()
    [(_ special term) #'term]))

(define-for-syntax (annotate/single term stx)
  (quasisyntax/loc stx
    (begin
      #,(case (syntax-local-context)
          [(expression) (annotate-term (syntax->term term) #'(values))]
          [else #`(define-values ()
                    #,(annotate-term (syntax->term term) #'(values)))])
      #,stx)))

(define-syntax (#%annotate-term stx)
  (syntax-case stx ()
    [(_ term)
     (syntax-case
         (local-expand #'term
                       (syntax-local-context)
                       (list #'#%dracula-expr
                             #'#%dracula-event
                             #'#%dracula-special-event))
         (#%dracula-expr #%dracula-event #%dracula-special-event)
       [(#%dracula-expr expr)
        (annotate/single #'term #'expr)]
       [(#%dracula-event event)
        (annotate/single #'term #'event)]
       [(#%dracula-special logical executable)
        (annotate/single #'logical #'executable)]
       [_ (raise-syntax-error
           #f "not an ACL event or expression" #'term)])]))

(define-syntax (#%annotate-part stx)
  (syntax-case stx ()
    [(_ name src body)
     (let* ([result (local-expand #'body (syntax-local-context) null)])
       (annotate-part
        (make-part (syntax-e #'name)
                   (syntax->loc #'src)
                   (get-terms result))
        result))]))

(define-syntax (#%annotate-proof stx)
  (syntax-case stx ()
    [(_ src body)
     (let* ([result (local-expand #'body (syntax-local-context) null)])
       (annotate-proof
        (apply make-proof (get-parts result))
        result))]))