diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-24 03:22:11 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-24 03:22:11 +0900 |
| commit | 4bf52294c02c89c5cbd44689fcf573bb29cf1204 (patch) | |
| tree | aec5da40a71f8da8e6c2a30c4949f00c35cc398d | |
| parent | 39fd88dcb3bc75e19bab8beb3c9b8838f8468d4c (diff) | |
Refactor `add-ace-scores` function.
| -rw-r--r-- | blackjack.lisp | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/blackjack.lisp b/blackjack.lisp index 83c9c5c..353fc2a 100644 --- a/blackjack.lisp +++ b/blackjack.lisp @@ -89,12 +89,11 @@ (defun add-ace-scores (s ac) (declare (xargs :guard (and (natp s) - (natp ac)) - :measure (acl2-count ac))) + (natp ac)))) (cond ((zerop ac) s) - ((<= (+ s (* ac 11)) 21) (+ s (* ac 11))) - ((natp ac) (add-ace-scores (+ s 1) (- ac 1))))) + ((<= (+ s 11) 21) (+ s 11 (- ac 1))) + (t (+ s 1 (- ac 1))))) (defthm natp/add-ace-scores (implies (and (natp x) (natp y)) @@ -130,7 +129,8 @@ (defthm scorep/score (implies (rank-list-p x) - (scorep (score x)))) + (scorep (score x))) + :hints (("Goal" :hands-off (add-ace-scores)))) (defun judge/score (player dealer) (declare (xargs :guard (and (scorep player) @@ -149,9 +149,12 @@ (defun judge/ranks (player dealer) (declare (xargs :guard (and (rank-list-p player) - (rank-list-p dealer)))) - (judge/score (score player) - (score dealer))) + (rank-list-p dealer)) + :guard-hints (("Goal" + :hands-off (score) + :use (scorep/score))))) + (judge/score (score player) + (score dealer))) (defthm bust-and-lose (equal (judge/score 'BUST x) 'LOSE)) @@ -167,8 +170,4 @@ (rankp new) (<= (score* (list r1 r2)) 11)) (not (equal (score (list new r1 r2)) - 'BUST))) - :hints (("Goal" - :expand ((add-ace-scores r2 1) - (add-ace-scores r1 1) - (add-ace-scores (+ r1 r2) 1))))) + 'BUST)))) |