(defun acep (x)
  (declare (xargs :guard t))
  (eq x 'A))

(defun facep (x)
  (declare (xargs :guard t))
  (case x
    ((J Q K) t)
    (t nil)))

(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))
                  :measure (acl2-count ac)))
  (cond
   ((zerop ac) s)
   ((<= (+ s (* ac 11)) 21) (+ s (* ac 11)))
   ((natp ac) (add-ace-scores (+ 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))))

(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))))
    (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)))