#lang scheme

(require "../proof/proof.ss" "../acl2/rep.ss" "../acl2/acl2.ss")

;; A TermState is:
;;  (make-term-state Loc (Or Sexp #f) (or Sexp Boolean) (Or Interaction #f))
;; An Interaction is (make-interaction String String String String Status)
;; A Status is 'admitted, 'failed, 'failed+edited, or #f.
(define-struct term-state (loc sexp saved output) #:prefab)
(define-struct interaction (initial input output final tree status) #:prefab)

(define (term-state-populate old new)
  (match (list old new)
    [(list (struct term-state [_ old-sexp _ (app interaction-status 'admitted)])
           (struct term-state [_ (and new-sexp (not old-sexp)) _ _]))
     (error 'term-state-populate
            "mismatch between ~s and ~s"
            old-sexp new-sexp)]
    [(list (struct term-state [_ _ saved output])
           (struct term-state [loc sexp _ _]))
     (make-term-state loc sexp saved output)]))

(define (term-state-edit state)
  (struct-copy term-state state
               [output (interaction-edit (term-state-output state))]))

(define (interaction-edit inter)
  (struct-copy interaction inter
               [status (status-edit (interaction-status inter))]))

(define (status-edit status)
  (if (eq? status 'failed) 'failed+edited status))

(define (term-state-active? v)
  (and (term-state? v) (interaction? (term-state-output v))))

(define (term-state-has-input? v)
  (and (term-state? v) (not (false? (term-state-sexp v)))))

(define (empty-term-state loc) (make-term-state loc #f #f #f))

(define (initial-term-state term)
  (make-term-state (term-loc term) (term-sexp term) #f #f))

(define (term-state-update-acl2 state acl2)
  (struct-copy term-state state [output (acl2->interaction acl2)]))

(define (term-state-start-acl2 state acl2 saved)
  (struct-copy term-state state
               [saved saved]
               [output (acl2->interaction acl2)]))

(define (term-state-save-before-sexp state)
  '(absolute-to-relative-command-number
    (max-absolute-command-number (w state))
    (w state)))

(define (term-state-restore-saved-sexp state)
  `(ubu! ,(term-state-saved state)))

(define (term-state-stop-acl2 state)
  (struct-copy term-state state [saved #f] [output #f]))

(define (term-state-initial-prompt state)
  (interaction-initial (term-state-output state)))

(define (term-state-acl2-input state)
  (interaction-input (term-state-output state)))

(define (term-state-acl2-output state)
  (interaction-output (term-state-output state)))

(define (term-state-final-prompt state)
  (interaction-final (term-state-output state)))

(define (term-state-proof-tree state)
  (interaction-tree (term-state-output state)))

(define (term-state-total-output state)
  (string-append (term-state-initial-prompt state)
                 (term-state-acl2-input state)
                 (term-state-acl2-output state)))

(define (term-state-finished? state)
  (symbol? (interaction-status (term-state-output state))))

(define (term-state-admitted? state)
  (and (term-state-saved state)
       (equal? 'admitted (interaction-status (term-state-output state)))))

(define (term-state-edited? state)
  (equal? 'failed+edited (interaction-status (term-state-output state))))

(define (acl2->interaction acl2)
  (make-interaction (acl2-initial-prompt acl2)
                    (acl2-input acl2)
                    (acl2-output acl2)
                    (acl2-final-prompt acl2)
                    (acl2-proof-tree acl2)
                    (if (acl2-done? acl2)
                        (if (acl2-admitted? acl2) 'admitted 'failed)
                        #f)))

(provide/contract
 [term-state? (-> any/c boolean?)]
 [term-state-active? (-> any/c boolean?)]
 [term-state-has-input? (-> any/c boolean?)]
 [empty-term-state (-> loc? (and/c term-state?
                                   (not/c term-state-has-input?)
                                   (not/c term-state-active?)))]
 [initial-term-state (-> term? (and/c term-state?
                                      term-state-has-input?
                                      (not/c term-state-active?)))]
 [term-state-populate (-> term-state? term-state? term-state?)]
 [term-state-edit (-> term-state? term-state?)]
 [term-state-start-acl2
  (-> (and/c term-state? (not/c term-state-active?))
      acl2?
      (or/c sexp/c boolean?)
      term-state-active?)]
 [term-state-stop-acl2
  (-> term-state-active? (and/c term-state? (not/c term-state-active?)))]
 [term-state-save-before-sexp (-> term-state? sexp/c)]
 [term-state-restore-saved-sexp (-> term-state-admitted? sexp/c)]
 [term-state-update-acl2 (-> term-state-active? acl2? term-state-active?)]
 [term-state-sexp (-> term-state-has-input? (or/c sexp/c #f))]
 [term-state-loc (-> term-state? loc?)]
 [term-state-finished? (-> term-state-active? boolean?)]
 [term-state-admitted? (-> term-state-active? boolean?)]
 [term-state-edited? (-> term-state-active? boolean?)]
 [term-state-initial-prompt (-> term-state-active? string?)]
 [term-state-acl2-input (-> term-state-active? string?)]
 [term-state-acl2-output (-> term-state-active? string?)]
 [term-state-final-prompt (-> term-state-active? string?)]
 [term-state-proof-tree (-> term-state-active? string?)]
 [term-state-total-output (-> term-state-active? string?)])