diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-28 12:35:26 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-28 12:35:26 +0900 |
commit | a4008403ece7a1c4c5b6911e5070518ddce5383e (patch) | |
tree | 860d15f27da59cc5ce1745b40d5865cea095575e /blackjack.lisp | |
parent | 2a3e2ef7aab64575dfb382d2e85c31458b05b366 (diff) |
Rename functions.
rank-list-p -> rank-listp
face-list-p -> face-listp
Diffstat (limited to 'blackjack.lisp')
-rw-r--r-- | blackjack.lisp | 34 |
1 files 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)))) |