(defconst *aces* '(A))
(defconst *faces* '(J Q K))

(defun acep (x)
  (declare (xargs :guard t))
  (and (member x *aces*) t))

(defun facep (x)
  (declare (xargs :guard t))
  (and (member x *faces*) t))

(defun rankp (x)
  (declare (xargs :guard t))
  (or (acep x)
      (facep x)
      (and (natp x)
           (<= 2 x)
           (<= x 10))))

(defun scorep (x)
  (declare (xargs :guard t))
  (case x
    ((BUST NATURAL-BLACKJACK) t)
    (t (and (natp x)
            (<= x 21)))))

(defun rank-listp (x)
  (declare (xargs :guard t))
  (if (atom x)
      (null x)
      (and (rankp (car x))
           (rank-listp (cdr x)))))

(defthm rank-listp-to-true-listp
  (implies (rank-listp x)
           (true-listp x))
  :rule-classes :forward-chaining)

(defun filter-natp (x)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) nil)
        ((natp (car x))
         (cons (car x) (filter-natp (cdr x))))
        (t (filter-natp (cdr x)))))

(defun sum (x)
  (declare (xargs :guard (nat-listp x)))
  (cond ((endp x) 0)
        (t (+ (car x) (sum (cdr x))))))

(defun filter-facep (x)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) nil)
        ((facep (car x))
         (cons (car x) (filter-facep (cdr x))))
        (t (filter-facep (cdr x)))))

(defun face-listp (x)
  (declare (xargs :guard t))
  (cond ((consp x)
         (and (facep (car x))
              (face-listp (cdr x))))
        (t (null x))))

(defun face-list-to-score (x)
  (declare (xargs :guard (face-listp x)))
  (* 10 (length x)))

(defun score-without-aces (rl)
  (declare (xargs :guard (rank-listp rl)))
  (+ (sum (filter-natp rl))
     (face-list-to-score (filter-facep rl))))

(defthm natp-score-without-aces
  (implies (rank-listp x)
           (natp (score-without-aces x))))

(defun ace-count (x)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) 0)
        ((acep (car x)) (+ 1 (ace-count (cdr x))))
        (t (ace-count (cdr x)))))

(defthm natp-ace-count
  (implies (rank-listp x)
           (natp (ace-count x))))

(defun add-ace-scores (s ac)
  (declare (xargs :guard (and (natp s)
                              (natp ac))))
  (cond
   ((zip ac) s)
   ((<= (+ s 11) 21) (+ s 11 (- ac 1)))
   (t (+ s 1 (- ac 1)))))

(defthm natp-add-ace-scores
  (implies (and (natp x) (natp y))
           (natp (add-ace-scores x y))))

(defun nat-score (rl)
  (declare (xargs :guard (rank-listp rl)))
  (add-ace-scores (score-without-aces rl)
                  (ace-count rl)))

(defthm natp-nat-score-1
  (implies (rank-listp rl)
           (natp (+ (sum (filter-natp rl))
                    (* 10 (len (filter-facep rl)))))))

(defthm natp-nat-score
  (implies (rank-listp rl)
           (natp (nat-score rl))))

(defun score (rl)
  (declare (xargs :guard (rank-listp rl)))
  (let ((s (nat-score rl)))
    (cond
     ((and (< 21 s)) 'BUST)
     ((and (= (len rl) 2) (= s 21))
      'NATURAL-BLACKJACK)
     (t s))))

(defthm scorep-score-1
  (implies (rank-listp x)
           (natp (+ (sum (filter-natp x))
                    (* 10 (len (filter-facep x)))))))

(defthm scorep-score
  (implies (rank-listp x)
           (scorep (score x)))
  :hints (("Goal" :hands-off (add-ace-scores))))

(defun score-judge (player dealer)
  (declare (xargs :guard (and (scorep player)
                              (scorep dealer))))
  (cond
    ((and (equal player 'NATURAL-BLACKJACK)
          (equal dealer 'NATURAL-BLACKJACK))
     'PUSH)
    ((equal player 'NATURAL-BLACKJACK) 'WIN)
    ((equal dealer 'NATURAL-BLACKJACK) 'LOSE)
    ((equal player 'BUST) 'LOSE)
    ((equal dealer 'BUST) 'WIN)
    ((< player dealer) 'LOSE)
    ((> player dealer) 'WIN)
    (t 'PUSH)))

(defun judge (player dealer)
  (declare (xargs :guard (and (rank-listp player)
                              (rank-listp dealer))
                  :guard-hints (("Goal"
                                 :hands-off (score)
                                 :use (scorep-score)))))
  (score-judge (score player)
               (score dealer)))

(defthm bust-and-lose
  (equal (score-judge 'BUST x) 'LOSE))

(defthm draw-a-face-and-blackjack
  (implies (facep r)
           (equal (score (list 'A r))
                  'NATURAL-BLACKJACK)))

(defthm bust-12
  (let ((rs '(K 2))
        (new 'J))
    (and (= (nat-score rs) 12)
         (equal (score (cons new rs)) 'BUST))))

(defthm safe-hit
  (implies (and (rank-listp rs)
                (rankp new)
                (<= (nat-score rs) 11))
           (not (equal (score (cons new rs)) 'BUST))))