(module proof-syntax mzscheme

  (require (lib "contract.ss")
           (lib "etc.ss")
           "proof-commands.scm"
           (planet "contract-utils.ss" ("cobbe" "contract-utils.plt" 3 0)))

  (provide/contract
   [proof? predicate/c]
   [expr? predicate/c]
   [event? predicate/c]
   [modular? predicate/c]
   [make-proof (-> syntax? proof-command? (eta proof?))]
   [make-expr (-> syntax? syntax? (eta expr?))]
   [make-event (-> syntax? syntax? (eta event?))]
   [make-modular (-> syntax? (listof syntax?) syntax? (eta modular?))]
   [get-command (-> (eta proof?) proof-command?)]
   [extract-commands (-> any/c (listof proof-command?))])

  ;; A Proof is (syntax-property Syntax key ProofCommand)

  (define key 'dracula-proof-key)

  (define (get stx)
    (syntax-property stx key))

  (define (put stx cmd)
    (syntax-property stx key cmd))

  (define (get-command stx)
    (let loop ([prop (get stx)])
      (cond
       [(proof-command? prop) prop]
       [(pair? prop) (loop (cdr prop))]
       [else #f])))

  (define (proof? v)
    (and (syntax? v) (get-command v) #t))

  (define (expr? v)
    (and (syntax? v) (expr-command? (get-command v))))

  (define (event? v)
    (and (syntax? v) (event-command? (get-command v))))

  (define (modular? v)
    (and (syntax? v) (module-command? (get-command v))))

  (define (make-proof stx cmd)
    (put stx cmd))

  (define (make-expr expr stx)
    (put stx (make-expr-command expr)))

  (define (make-event event stx)
    (put stx (make-event-command event)))

  (define (make-modular modular terms stx)
    (put stx (make-module-command modular terms)))

  ;; Extract proof commands from an s-expression containing syntax objects.
  ;; Allow for the possibility that begin-splicing has duplicated commands.
  (define (extract-commands v)
    (extract v null))

  ;; Extract proof commands from v, inserted before subsequent commands cmds.
  (define (extract v cmds)
    (cond
     [(syntax? v)
      (cond [(get-command v) => (lambda (cmd) (add cmd cmds))]
            [else (extract (syntax-e v) cmds)])]
     [(pair? v)
      (extract (car v) (extract (cdr v) cmds))]
     [else cmds]))

  ;; Add a command to a list, removing consecutive duplicates.
  (define (add cmd cmds)
    (cond
     [(null? cmds) (list cmd)]
     [(eq? cmd (car cmds)) cmds]
     [else (cons cmd cmds)]))

  )