Add blackjack.lisp

1 files changed, 165 insertions, 0 deletions

diff --git a/blackjack.lisp b/blackjack.lisp
new file mode 100644
index 0000000..4e197f4
--- /dev/null
+++ b/blackjack.lisp
@@ -0,0 +1,165 @@
+(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)
+                  :guard-hints (("Goal" :use natp/score*))))
+  (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" :use scorep/score-1)))
+
+(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" :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)))
+