Applicative game media now instantiated. I started with three goals in mind
for media: Must be able to play sound, must be convenient to structure
complex autostereogram illusions, and must be convenient for plain text as
well. To this end I have selected common lisp (duh) format control strings
and arguments as my universal media control. It is a complete programming
language built around pretty printing. Because it can do anything, sound and
complex lispy post-processing are easy. A simple convention and say, SDL2
will also let me drive pixel mapped graphics via format control strings in
the future too. ACL2 is not suitable itself for media side effects. Its role
is constrained to proving the applicative logic of the game's state to the
media representation namely the format controls and their arguments. Let's
look at my tictacto, though it could also be baduk which would be cooler
actually. The game will be expressed as a proven (in some senses) acl2
applicative function on a list stored in a single threaded object, followed
by a normal lisp - sbcl - evaluating acl2's media output.
Clearly I can maintain state in the game-state single threaded object, and I
allege deterministically produce a common lisp format expression media
depiction of the game state evaluable to some literal media which in this
case is a three by three game board that gets hugged and kissed. Text is
convenient here and always, but all sorts of media control is possible and
fairly convenient.
On the topic of ACL2 particularly, you might notice that my measure
conjectures are always trivial, and the way I have expressed myself has not
required any lemmas or particular rewrite rules from me. I think it is good
that my robot team mate needs relatively little input from me. I will
revisit this towards the end of this post. For now, let me present my ACL2
logic.
;;Same everything as before; I am noting game-state here since it is used.
(defstobj game-state
(sparse-objects :type t :initially nil)
(subject-cursor :type integer :initially 0)
(object-cursor :type integer :initially 0)
(chars-in :type t :initially nil))
;;Transform the game sparse objects (actually dense here) into a lisp format
(defun get-lisp-format (input fmt-ctls fmt-args)
(if (= 0 (length input)) `(format t ,(concatenate 'string "~{" fmt-ctls "~}") ',fmt-args)
(get-lisp-format (cdr input)
(concatenate 'string fmt-ctls (cdr (assoc 'fmt-ctl (car input))))
(append fmt-args (cdr (assoc 'fmt-args (car input)))))))
;;Change the character displayed without changing the control string,
;;By prepending a new fmt-args since lisp/acl2's assoc only finds
;;first matches. Yes this function is terribly named.
(defun row-col2char (row col char input output)
(if (= 0 (length input)) output
(let ((pushp (if (subsetp-equal `((row . ,row) (col . ,col)) (car input))
`((fmt-args . (,char)))
nil)))
(row-col2char row col char (cdr input)
(append output (list (append pushp (car input))))))))
;;That was everything functional, onto
;;;game-state
;;I'm not trying to prove I have handled every side-effect error scenario with my stobj
;;Hence I am declaring verify-guards to nil for stateful functions here.
(defun new-game (game-state)
(declare (xargs :stobjs (game-state) :verify-guards nil))
(update-sparse-objects (new-tictacto-board) game-state))
Easy easy easy. The trouble I mentioned yesterday is not visible anywhere
because I decided to just use a simple element by element O(n) filtering of
an input list into an output list for everything. What I had been working on
was pulling out subsequences relying on some well-ordering I will look at in
a moment complicated by col-min and col-max not necessarily being the edges
of a row. Anyway, everything is pretty great now without even trying.
I keep saying common lisp format can and is appropriate for arbitrary media
because it furnishes arbitrary functionality like this (on top of its
iteration, gotos, logic and so on):
(in-package cl-user)
(defun beep-if-true (stream bool-arg &rest flags)
(declare (ignore flags))
(format stream "~@[~1@*~]" bool-arg #\Bel))
(format t "~/cl-user::beep-if-true/" t)
(format t "~/cl-user::beep-if-true/" nil)
;I assume my hacky scripting and
;typos achieved the following
which is normally used to craft a response to put into the stream at the
function call position, but does not necessarily have to. For example it
could enqueue post processing of the output, or drive Simple Directmedia
Layer 2 through ecl's sffi.
Something I did not end up using explicitly in this example is that I
modified my insertion sort from before to sort lists having row and col
conses in row-major order. The only change was this:
which, accepted trivially, did not change the logic of my acl2
'insert-sorted or 'insertion-sort. By always being sorted through
'insert-sorted
(defun insert-sorted (a b result)
(if (= 0 (length b)) (append result (list a))
(let ((final-tail (leq-pushp a b)))
(if final-tail (append result final-tail)
(insert-sorted a (cdr b) (append result (list (car b))))))))
I trivially avoid lots of pathological cases. The reason that I have not had
any lemmas or fiddly rewrite rules so far is that I am not proving any very
strong theorems. Regarding insertion sort
(defun insertion-sort (input result)
(if (= 0 (length input)) result
(insertion-sort (cdr input)
(insert-sorted (car input) result nil))))
I checked weak theorems like
(thm (implies (< (cdr (assoc 'row a)) (cdr (assoc 'row b)))
(= (search (list a) (insertion-sort (list a b) nil))
0)))
or in English, if I 'insertion-sort (list a b) and a's row is less than b's,
a is in position 0. The usual stronger theories of a sorting function are
that the output is in fact sorted, and that the output is some permutation
of the input. I think a weak theory like- in this kind of scenario, a will
be in position 0 is often useful on its own. These weak theories are not
usually worth lodging as rewrite rules. When I was thumbing through an ACL2
book, I found the book's insertion sort example, which required proving some
supporting lemmas in order to admit the function. My form didn't need any
though.
The next two things I want for a game, being a notion of a clock and network
multiplayer are mostly about side effects. I de finitely need some healthier
networking. I will develop a clock and some networking on other topics, then
introduce them to my theory of games afterwards.
---
Post script
Ultimately I expect to do: acl2 -> ecl -> sdl2 executable preserving the
logic of acl2.
