Glorious return to ACL2 game programming (do you remember last
time?)
ldbeth asked after seeing my #1=(1 2 3 . #1#) wzard game
structure whether I could represent circular lists without sharp
quote syntax. Well
(let ((foo '(1 2 3))) (setf (cdr (last foo)) foo))
but one of the As in ACL2 is Applicative, so we don't have SETF
neither
so I have used an alist and not-true-listps so when cdr returns
a symbol it means cdr-assoc the alist.
Since ACL2 enforces single-threadedness, I don't think there's
ever a problem except for informality. So let's add some
formality. |#
(defun %cdrs (measure list alist)
(if (or (zp measure) (not (natp measure))) list
(let ((next-measure (- measure 1))
(next-list (cdr (if (symbolp (cdr list))
(assoc (cdr list) alist)
list))))
(%cdrs next-measure next-list alist))))
;;;We don't have to worry about SETFability since we're
applicative.
;;;I'm figuring... If it's a true list, %cdrs 1 is trivial and
%cdrs n is (%cdrs (1- n) (%cdrs 1 list alist) alist) to get some
recursion going.
(defthm stepwise-nil-alist-%cdrs
(implies (and (listp list) (equal alist nil) (equal n (length
list))) (equal (%cdrs n list alist) (%cdrs 1 (%cdrs (1- n)
list alist) alist))))
;;;Since we can reach the end of a list one step at a time
;;;can we get from what I seem to have called (cons b e)
;;;to (cons e d) in the continuation alist?
(defthm last-cdr-symbol
(implies (and (symbolp e) (equal list (append a (cons b e)))
(equal alist (list (cons e d))))
(equal (%cdrs 1 (last list) alist) d)))
;;;So we can mostly get through one im/proper list, but can we
get to the next?
(defthm composite-%cdrs
(implies (and (listp a) (listp b) (not (null b)) (symbolp foo)
(not (null foo)) (equal list (append a (cons whatever foo)))
(equal alist (list (cons foo b))) (equal n (length list)))
(equal (%cdrs n list alist) b)))
;;;There's (always) more to do but it seems like our
faux-circularity is working. ;;;Oh that's actually equivalent to
the last one I guess. Actually all of them ;;;were trivial.
#|
It took me a while to be able to write anything at all acl2
would accept from me. Then I got back into the zone of mostly
saying trivial things. The automated prover took
111 steps for the admission of %cdrs,
2620 steps for STEPWISE-NIL-ALIST-%CDRS
1093 steps for LAST-CDR-SYMBOL
and
1778 for composite-%cdrs
I feel very efficient when my machine does thousands of things
for me.
|#
