(in-package "ACL2")

(include-book "standard-52-card-deck/top")

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

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

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

(defmacro rank-face-list-to-score (x)
  `(* 10 (len ,x)))

(defmacro score-without-aces (x)
  `(+ (sum (rank-natp-filter ,x))
      (rank-face-list-to-score (rank-facep-filter ,x))))

(defthm natp-score-without-aces
  (let ((s (score-without-aces x)))
    (and (integerp s)
         (<= 0 s))))

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

(defthm natp-ace-count
  (and (integerp (ace-count x))
       (<= 0 (ace-count x))))

(defmacro add-ace-scores (s ac)
  `(cond
     ((equal ,ac 0) ,s)
     ((< (+ ,s 10) 21) (+ ,s 11 (- ,ac 1)))
     (t (+ ,s 1 (- ,ac 1)))))

(defthm natp-add-ace-scores
  (implies (and (integerp x)
                (<= 0 x)
                (integerp y)
                (<= 0 y))
           (let ((s (add-ace-scores x y)))
             (and (integerp s)
                  (<= 0 s)))))

(defmacro nat-score (x)
  `(add-ace-scores (score-without-aces ,x)
                   (ace-count ,x)))

(defthm natp-nat-score
  (implies (rank-listp x)
           (and (integerp (nat-score x))
                (<= 0 (nat-score x))))
  :rule-classes (:rewrite :forward-chaining))

(defmacro score (x)
  `(cond
     ((and (< 21 (nat-score ,x))) 'BUST)
     ((and (equal (len ,x) 2) (equal (nat-score ,x) 21))
      'NATURAL-BLACKJACK)
     (t (nat-score ,x))))

(defmacro scorep (x)
  `(or (equal ,x 'bust)
       (equal ,x 'natural-blackjack)
       (if (integerp ,x)
           (if (< ,x 0)
               nil
               (< ,x 22))
           nil)))

(defthm natp-sum
  (implies (nat-listp x)
           (and (integerp (sum x))
                (<= 0 (sum x))))
  :rule-classes (:rewrite :forward-chaining))

(defthm nat-listp-rank-natp-filter
  (implies (rank-listp x)
           (rank-nat-listp (rank-natp-filter x)))
  :rule-classes (:rewrite :forward-chaining))

(defthm scorep-score
  (implies (rank-listp x)
           (scorep (score x))))

(defmacro score-judge (player 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)))

(defmacro judge (player dealer)
  `(score-judge (score (card-list-to-rank-list ,player))
                (score (card-list-to-rank-list ,dealer))))

(defmacro judgementp (x)
  `(or (equal ,x 'NATURAL-BLACKJACK)
       (equal ,x 'BUST)
       (equal ,x 'LOSE)
       (equal ,x 'WIN)
       (equal ,x 'PUSH)))

(defthm judgementp-score-judge
  (judgementp (score-judge p d)))

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

(defthm if-draw-a-face-card-and-have-a-ace-card-only-then-natural-blackjack
  (implies (and (rank-facep face)
                (rank-acep ace))
           (equal (score (list ace face))
                  'NATURAL-BLACKJACK)))

(defun no-rank-acep (x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      t
      (and (not (rank-acep (car x)))
           (no-rank-acep (cdr x)))))

(defthm if-draw-a-face-when-12-then-bust
  (implies (and (rank-listp rs)
                (no-rank-acep rs)
                (rank-facep face)
                (equal (nat-score rs) 12))
           (equal (score (cons face rs)) 'BUST)))

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