From 9527ce441b5f28cc25b2ae8e9462e2450d68dcb0 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 21 Aug 2021 18:07:56 +0900
Subject: Rename functions and theorems.

---
 blackjack.lisp | 69 +++++++++++++++++++++++++++++++---------------------------
 1 file changed, 37 insertions(+), 32 deletions(-)

(limited to 'blackjack.lisp')

diff --git a/blackjack.lisp b/blackjack.lisp
index 41b49b0..91a055d 100644
--- a/blackjack.lisp
+++ b/blackjack.lisp
@@ -26,10 +26,15 @@
 
 (defun rank-listp (x)
   (declare (xargs :guard t))
-  (cond ((consp x)
-         (and (rankp (car x))
-              (rank-listp (cdr x))))
-        (t (null x))))
+  (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)))
@@ -66,7 +71,7 @@
   (+ (sum (filter-natp rl))
      (face-list-to-score (filter-facep rl))))
 
-(defthm natp/score-without-aces
+(defthm natp-score-without-aces
   (implies (rank-listp x)
            (natp (score-without-aces x))))
 
@@ -76,7 +81,7 @@
         ((acep (car x)) (+ 1 (ace-count (cdr x))))
         (t (ace-count (cdr x)))))
 
-(defthm natp/ace-count
+(defthm natp-ace-count
   (implies (rank-listp x)
            (natp (ace-count x))))
 
@@ -88,69 +93,69 @@
    ((<= (+ s 11) 21) (+ s 11 (- ac 1)))
    (t (+ s 1 (- ac 1)))))
 
-(defthm natp/add-ace-scores
+(defthm natp-add-ace-scores
   (implies (and (natp x) (natp y))
            (natp (add-ace-scores x y))))
 
-(defun score* (rl)
+(defun nat-score (rl)
   (declare (xargs :guard (rank-listp rl)))
   (add-ace-scores (score-without-aces rl)
                   (ace-count rl)))
 
-(defthm natp/score*-1
+(defthm natp-nat-score-1
   (implies (rank-listp rl)
            (natp (+ (sum (filter-natp rl))
                     (* 10 (len (filter-facep rl)))))))
 
-(defthm natp/score*
+(defthm natp-nat-score
   (implies (rank-listp rl)
-           (natp (score* rl))))
+           (natp (nat-score rl))))
 
 (defun score (rl)
   (declare (xargs :guard (rank-listp rl)))
-  (let ((s (score* 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
+(defthm scorep-score-1
   (implies (rank-listp x)
            (natp (+ (sum (filter-natp x))
                     (* 10 (len (filter-facep x)))))))
 
-(defthm scorep/score
+(defthm scorep-score
   (implies (rank-listp x)
            (scorep (score x)))
   :hints (("Goal" :hands-off (add-ace-scores))))
 
-(defun judge/score (player dealer)
+(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/ranks (player dealer)
+    ((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)))))
-  (judge/score (score player)
+                                 :use (scorep-score)))))
+  (score-judge (score player)
                (score dealer)))
 
 (defthm bust-and-lose
-  (equal (judge/score 'BUST x) 'LOSE))
+  (equal (score-judge 'BUST x) 'LOSE))
 
 (defthm draw-a-face-and-blackjack
   (implies (facep r)
@@ -160,11 +165,11 @@
 (defthm bust-12
   (let ((rs '(K 2))
         (new 'J))
-    (and (= (score* rs) 12)
+    (and (= (nat-score rs) 12)
          (equal (score (cons new rs)) 'BUST))))
 
 (defthm safe-hit
   (implies (and (rank-listp rs)
                 (rankp new)
-                (<= (score* rs) 11))
+                (<= (nat-score rs) 11))
            (not (equal (score (cons new rs)) 'BUST))))
-- 
cgit v1.2.3