(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-list-p (x)
  (declare (xargs :guard t))
  (cond ((consp x)
         (and (rankp (car x))
              (rank-list-p (cdr x))))
        (t (null x))))

(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 nat-list-p (x)
  (declare (xargs :guard t))
  (cond ((consp x)
         (and (natp (car x))
              (nat-list-p (cdr x))))
        (t (null x))))

(defun sum (x)
  (declare (xargs :guard (nat-list-p 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-list-p (x)
  (declare (xargs :guard t))
  (cond ((consp x)
         (and (facep (car x))
              (face-list-p (cdr x))))
        (t (null x))))

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

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

(defthm natp/score-without-aces
  (implies (rank-list-p 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-list-p x)
           (natp (ace-count x))))

(defun add-ace-scores (s ac)
  (declare (xargs :guard (and (natp s)
                              (natp ac))))
  (cond
   ((zerop 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 score* (rl)
  (declare (xargs :guard (rank-list-p rl)))
  (add-ace-scores (score-without-aces rl)
                  (ace-count rl)))

(defthm natp/score*-1
  (implies (rank-list-p rl)
           (natp (+ (sum (filter-natp rl))
                    (* 10 (len (filter-facep rl)))))))

(defthm natp/score*
  (implies (rank-list-p rl)
           (natp (score* rl))))

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

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

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

(defun judge/score (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/ranks (player dealer)
  (declare (xargs :guard (and (rank-list-p player)
                              (rank-list-p dealer))
                  :guard-hints (("Goal"
                                 :hands-off (score)
                                 :use (scorep/score)))))
  (judge/score (score player)
               (score dealer)))

(defthm bust-and-lose
  (equal (judge/score '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 (= (score* rs) 12)
         (equal (score (cons new rs)) 'BUST))))

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