A predecessor of the defrstobj library that wasn't based on abstract stobjs.
This legacy version of record-like stobjs was written by Jared Davis before ACL2 supported abstract stobjs. As a result, many tricks and twists are needed to effectively hide the true nature of the stobj and to be able to treat it like a record.
The legacy version isn't bad—we used this version of rstobjs for our microcode model at Centaur Technology for a couple of years. But we eventually became irritated with how long it took to define rstobjs with many fields (it's quadratic in the number of fields). It's likely that a sufficiently motivated person could speed this up, and we considered a way of doing so.
But ultimately, we decided that with abstract stobjs, we could reimplement defrstobj in a much simpler way. The new approach, implemented by Sol Swords, avoids this quadratic cost, and also has a couple of other nice features. For instance:
So today there is little reason to use the legacy version. Use the new, more modern defrstobj instead!
Rather than delete the original version, we decided to put it into the
Record Like Stobjs
Copyright (C) 2011-2012 Centaur Technology.
Centaur Technology Formal Verification Group 7600-C N. Capital of Texas Highway, Suite 300 Austin, TX 78731, USA.
License: (An MIT/X11-style license)
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: