(module proof-commands mzscheme

  ;; Represents commands to issue to ACL2
  ;; corresponding to Dracula / Modular ACL2 terms.
  ;; Represented as pure s-expressions (no structs)
  ;; so they can be annotated as syntax properties
  ;; and used across phase boundaries.

  (require (lib "contract.ss")
           (lib "plt-match.ss")
           (planet "combinators.ss" ("cce" "combinators.plt" 1 4))
           (planet "contract-utils.ss" ("cobbe" "contract-utils.plt" 3 0)))

  ;; A ProofCommand is an ExprCommand, EventCommand, or ModuleCommand.

  ;; An ExprCommand is (list 'expr Expr),
  ;; where the Expr is an ACL2 expression with no logical effect.

  ;; An EventCommand is (list 'event Event)
  ;; where the Event is an ACL2 event with a logical effect that may be undone.

  ;; A ModuleCommand is (list 'module Modular (Listof Event))
  ;; where the Events are ACL2 events that may be undone,
  ;; and Modular is the term which contains them.

  (provide/contract
   [proof-command? predicate/c]
   [expr-command? predicate/c]
   [event-command? predicate/c]
   [module-command? predicate/c]
   [make-expr-command (-> syntax? (eta expr-command?))]
   [make-event-command (-> syntax? (eta event-command?))]
   [make-module-command (-> syntax? (listof syntax?) (eta module-command?))]
   [expr-command-term (-> (eta expr-command?) syntax?)]
   [event-command-term (-> (eta event-command?) syntax?)]
   [module-command-outer (-> (eta module-command?) syntax?)]
   [module-command-inner (-> (eta module-command?) (listof syntax?))]
   [proof-command->sexp (-> (eta proof-command?) sexp/c)])

  (define (expr-command? v)
    (match v
      [(list 'expr (? syntax?)) #t]
      [_ #f]))

  (define (event-command? v)
    (match v
      [(list 'event (? syntax?)) #t]
      [_ #f]))

  (define (module-command? v)
    (match v
      [(list 'module (? syntax?) (list (? syntax?) ...)) #t]
      [_ #f]))

  (define proof-command?
    (disjoin expr-command? event-command? module-command?))

  (define (make-expr-command expr)
    (list 'expr expr))

  (define (make-event-command event)
    (list 'event event))

  (define (make-module-command source event-list)
    (list 'module source event-list))

  (define expr-command-term cadr)
  (define event-command-term cadr)
  (define module-command-outer cadr)
  (define module-command-inner caddr)

  (define (deep-syntax->datum v)
    (cond
     [(syntax? v) (syntax-object->datum v)]
     [(pair? v) (cons (deep-syntax->datum (car v))
                      (deep-syntax->datum (cdr v)))]
     [else v]))

  (define proof-command->sexp deep-syntax->datum)

  )