From 4bf52294c02c89c5cbd44689fcf573bb29cf1204 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sun, 24 Jan 2021 03:22:11 +0900 Subject: Refactor `add-ace-scores` function. --- blackjack.lisp | 25 ++++++++++++------------- 1 file 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)))) -- cgit v1.2.3