Nested Stobjs

Matt Kaufmann
ACL2 Seminar
March 26, 2013

Abstract:

  Matt Kaufmann will talk about a new ACL2 feature: nested stobjs,
  that is, stobjs having fields that are stobjs (or arrays of stobjs).
  This will be an informal talk that briefly reviews single-threaded
  objects (also see :DOC stobj), and then introduces nested stobjs
  using demos.  As time allows there may be discussion of
  implementation issues and possible extensions.  Questions will be
  strongly encouraged!

Contents of this directory:

README                     this file
essay.txt                  "Essay on Nested Stobjs" from an ACL2 source file
log.txt                    shell log for demo (may add just a bit of annotation upon request)
nested-stobj-tests.lisp    demo file (ultimately to be found in books/misc/)
patch.lisp                 an annotated patch file, included for reference
remarks.txt                annotations added to the above patch file
stobj-review.lisp          review of stobjs

============================================================

PLAN FOR THE TALK:

1. INTRO:
   I wanted to give this talk today rather than waiting, since people
   are around and since later seminars might be busy with practice
   talks.

Note that as of today (3/26/2013), nested stobjs are not yet in the
ACL2 development snapshot.  I expect to complete that task this week.
This is a relatively big ACL2 development project.  Time spent so far
on nested stobjs:

 5.00 December
28.00 January
 2.00 February
29.25 March
-----
64.25 TOTAL so far (more than 1.5 weeks full-time equivalent!)

Remaining: Documentation, a few comments, a tracing bug, a small
technical question about oneify (whatever that is!), maybe a bit more
testing (e.g., stobjs within stobjs within stobjs).  There is also
some future work.

2. Review of stobjs (stobj-review.lisp).

3. Discussion of nested stobjs as quick run-through of some of the
   Essay on Nested Stobjs (essay.txt).

4. Demo (nested-stobj-tests.lisp), or at least part of it.

   Note: The demo is really a file I've developed for testing my
   implementation of nested stobjs.  There isn't an "interesting"
   application there.  However, from the trivial examples I assume
   that one can see how interesting examples would follow the same
   patterns.

5. If time remains, discussion of some implementation issues
   (remarks.txt and, as needed, patch.lisp).