From a4008403ece7a1c4c5b6911e5070518ddce5383e Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Thu, 28 Jan 2021 12:35:26 +0900
Subject: Rename functions.

rank-list-p -> rank-listp
face-list-p -> face-listp
---
 blackjack.lisp | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/blackjack.lisp b/blackjack.lisp
index 47a5c20..41b49b0 100644
--- a/blackjack.lisp
+++ b/blackjack.lisp
@@ -24,11 +24,11 @@
     (t (and (natp x)
             (<= x 21)))))
 
-(defun rank-list-p (x)
+(defun rank-listp (x)
   (declare (xargs :guard t))
   (cond ((consp x)
          (and (rankp (car x))
-              (rank-list-p (cdr x))))
+              (rank-listp (cdr x))))
         (t (null x))))
 
 (defun filter-natp (x)
@@ -50,24 +50,24 @@
          (cons (car x) (filter-facep (cdr x))))
         (t (filter-facep (cdr x)))))
 
-(defun face-list-p (x)
+(defun face-listp (x)
   (declare (xargs :guard t))
   (cond ((consp x)
          (and (facep (car x))
-              (face-list-p (cdr x))))
+              (face-listp (cdr x))))
         (t (null x))))
 
 (defun face-list-to-score (x)
-  (declare (xargs :guard (face-list-p x)))
+  (declare (xargs :guard (face-listp x)))
   (* 10 (length x)))
 
 (defun score-without-aces (rl)
-  (declare (xargs :guard (rank-list-p rl)))
+  (declare (xargs :guard (rank-listp rl)))
   (+ (sum (filter-natp rl))
      (face-list-to-score (filter-facep rl))))
 
 (defthm natp/score-without-aces
-  (implies (rank-list-p x)
+  (implies (rank-listp x)
            (natp (score-without-aces x))))
 
 (defun ace-count (x)
@@ -77,7 +77,7 @@
         (t (ace-count (cdr x)))))
 
 (defthm natp/ace-count
-  (implies (rank-list-p x)
+  (implies (rank-listp x)
            (natp (ace-count x))))
 
 (defun add-ace-scores (s ac)
@@ -93,21 +93,21 @@
            (natp (add-ace-scores x y))))
 
 (defun score* (rl)
-  (declare (xargs :guard (rank-list-p rl)))
+  (declare (xargs :guard (rank-listp rl)))
   (add-ace-scores (score-without-aces rl)
                   (ace-count rl)))
 
 (defthm natp/score*-1
-  (implies (rank-list-p rl)
+  (implies (rank-listp rl)
            (natp (+ (sum (filter-natp rl))
                     (* 10 (len (filter-facep rl)))))))
 
 (defthm natp/score*
-  (implies (rank-list-p rl)
+  (implies (rank-listp rl)
            (natp (score* rl))))
 
 (defun score (rl)
-  (declare (xargs :guard (rank-list-p rl)))
+  (declare (xargs :guard (rank-listp rl)))
   (let ((s (score* rl)))
     (cond
      ((and (< 21 s)) 'BUST)
@@ -116,12 +116,12 @@
      (t s))))
 
 (defthm scorep/score-1
-  (implies (rank-list-p x)
+  (implies (rank-listp x)
            (natp (+ (sum (filter-natp x))
                     (* 10 (len (filter-facep x)))))))
 
 (defthm scorep/score
-  (implies (rank-list-p x)
+  (implies (rank-listp x)
            (scorep (score x)))
   :hints (("Goal" :hands-off (add-ace-scores))))
 
@@ -141,8 +141,8 @@
    (t 'PUSH)))
 
 (defun judge/ranks (player dealer)
-  (declare (xargs :guard (and (rank-list-p player)
-                              (rank-list-p dealer))
+  (declare (xargs :guard (and (rank-listp player)
+                              (rank-listp dealer))
                   :guard-hints (("Goal"
                                  :hands-off (score)
                                  :use (scorep/score)))))
@@ -164,7 +164,7 @@
          (equal (score (cons new rs)) 'BUST))))
 
 (defthm safe-hit
-  (implies (and (rank-list-p rs)
+  (implies (and (rank-listp rs)
                 (rankp new)
                 (<= (score* rs) 11))
            (not (equal (score (cons new rs)) 'BUST))))
-- 
cgit v1.2.3