52 lines
1.2 KiB
Text
52 lines
1.2 KiB
Text
(defun remove-nth (i xs)
|
|
(if (or (zp i) (endp (rest xs)))
|
|
(rest xs)
|
|
(cons (first xs)
|
|
(remove-nth (1- i) (rest xs)))))
|
|
|
|
(defthm remove-nth-shortens
|
|
(implies (consp xs)
|
|
(< (len (remove-nth i xs)) (len xs))))
|
|
|
|
:set-state-ok t
|
|
|
|
(defun shuffle-r (xs ys state)
|
|
(declare (xargs :measure (len xs)))
|
|
(if (endp xs)
|
|
(mv ys state)
|
|
(mv-let (idx state)
|
|
(random$ (len xs) state)
|
|
(shuffle-r (remove-nth idx xs)
|
|
(cons (nth idx xs) ys)
|
|
state))))
|
|
|
|
(defun shuffle (xs state)
|
|
(shuffle-r xs nil state))
|
|
|
|
(defun cross-r (x ys)
|
|
(if (endp ys)
|
|
nil
|
|
(cons (cons x (first ys))
|
|
(cross-r x (rest ys)))))
|
|
|
|
(defun cross (xs ys)
|
|
(if (or (endp xs) (endp ys))
|
|
nil
|
|
(append (cross-r (first xs) ys)
|
|
(cross (rest xs) ys))))
|
|
|
|
(defun make-deck ()
|
|
(cross '(ace 2 3 4 5 6 7 8 9 10 jack queen king)
|
|
'(hearts diamonds clubs spades)))
|
|
|
|
(defun print-card (card)
|
|
(cw "~x0 of ~x1~%" (car card) (cdr card)))
|
|
|
|
(defun print-deck (deck)
|
|
(if (endp deck)
|
|
nil
|
|
(progn$ (print-card (first deck))
|
|
(print-deck (rest deck)))))
|
|
|
|
(defun draw-from-deck (deck)
|
|
(mv (first deck) (rest deck)))
|