|
|
|---|
|
|
|
|---|
Book naming conventions assumed by ACL2
See pathname for background on ACL2 pathnames.
ACL2 defines a ``full-book-name'' to represent an absolute filename of a book. This is typically a ``full-book-name string'' or simply ``full-book-string'': an absolute filename for the book. At the end of this topic we mention a second representation, the sysfile; but until then, our discussion of full-book-names is restricted to the special (but common) case of full-book-strings.
A full-book-name string may be divided into contiguous sections: a ``directory string'', a ``familiar name'' and an ``extension''. See pathname for the definitions of ``absolute,'' ``filename string,'' and other notions pertaining to naming files. Below we exhibit the three sections of one such string:
"/usr/home/smith/project/arith.lisp"
"/usr/home/smith/project/" ; directory string
"arith" ; familiar name
".lisp" ; extension
The sections are marked by the rightmost slash and rightmost dot, as shown below.
"/usr/home/smith/project/arith.lisp"
| |
slash dot
| |
"/usr/home/smith/project/" ; directory string
"arith" ; familiar name
".lisp" ; extension
The directory string includes (and terminates with) the rightmost slash. The extension includes (and starts with) the rightmost dot. The dot must be strictly to the right of the slash so that the familiar name is well-defined and nonempty.
We conclude by discussing the other representation of full-book-names as
promised above: the sysfile, which is a pair of the form