1.6 ACL2 Books
1.6.1 "data-structures/list-theory"
(include-book "data-structures/list-theory" :dir :system)
|
|
|
Dracula supports the
deflist form for defining new list types from the
"data-structures/list-theory" book. It defines the predicate
<list-pred>, recognizing lists whose elements satisfy
<pred>.
The
(l) identifies the list as the predicate’s only parameter; ACL2
supports other parameter lists but Dracula currently does not.
Examples: |
| > (deflist even-listp (l) evenp) | eval:613:0: defun: defined outside of begin-below | at: HERE | in: (defun even-listp (l) (cond ((null? l) (quote t)) | ((pair? l) (if (not (member (evenp (car l)) (quote (nil | ())))) (even-listp (cdr l)) (quote ()))) (else (quote ())))) | | > (even-listp (list 2 4 6)) | eval:614:0: application: bad syntax | in: (top/error . even-listp) | | > (even-listp (list 1 3 5)) | eval:615:0: application: bad syntax | in: (top/error . even-listp) | | > (even-listp 'not-a-list) | eval:616:0: application: bad syntax | in: (top/error . even-listp) |
|
1.6.2 "data-structures/structures"
(include-book "data-structures/structures" :dir :system)
|
|
(defstructure <name> field ...)
| | | | field | | = | | <field-name> | | | | | | | (<field-name> (:assert <guard-expr>)) |
|
|
Dracula supports the
defstructure form for defining new structure types
from the "data-structures/structures" book. It defines a constructor
<name>, a predicate
<name>-p a weak predicate
weak-<name>-p, and a selector
<name>-<field-name> for each
field, with optional guards for the structure and each field which are
incorporated into the predicate (but not the weak predicate).
Examples: |
| > (defstructure circle radius) | mutual-recursion: defined outside of begin-below | at: HERE | in: (mutual-recursion (defun circle (radius53) (circle54 | radius53)) (defun weak-circle-p (x) (weak-circle-p55 x)) | (defun circle-p (x) (circle-p56 x)) (defun circle-radius (x) | (circle-radius58 x))) | | > (circle 10) | eval:618:0: application: bad syntax | in: (top/error . circle) | | > (circle-radius (circle 10)) | eval:619:0: application: bad syntax | in: (top/error . circle-radius) | | > (circle-p (circle 10)) | eval:620:0: application: bad syntax | in: (top/error . circle-p) | | > (circle-p 'not-a-circle) | eval:621:0: application: bad syntax | in: (top/error . circle-p) | | mutual-recursion: defined outside of begin-below | at: HERE | in: (mutual-recursion (defun rect (temp67 temp68) (rect69 | temp67 temp68)) (defun weak-rect-p (x) (weak-rect-p70 x)) | (defun rect-p (x) (rect-p71 x)) (defun rect-width (x) | (rect-width73 x)) (defun rect-height (x) (rect-height74 x))) | | > (rect 10 20) | eval:623:0: application: bad syntax | in: (top/error . rect) | | > (rect-width (rect 10 20)) | eval:624:0: application: bad syntax | in: (top/error . rect-width) | | > (rect-height (rect 10 20)) | eval:625:0: application: bad syntax | in: (top/error . rect-height) | | > (rect-p (rect 10 20)) | eval:626:0: application: bad syntax | in: (top/error . rect-p) | | > (rect-p (rect -10 -20)) | eval:627:0: application: bad syntax | in: (top/error . rect-p) | | > (rect-p 'not-a-rect) | eval:628:0: application: bad syntax | in: (top/error . rect-p) |
|