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:1: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:2:0: application: bad syntax in: (top/error . | even-listp) | | > (even-listp (list 1 3 5)) | eval:3:0: application: bad syntax in: (top/error . | even-listp) | | > (even-listp 'not-a-list) | eval:4: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 (radius2) (circle3 | radius2)) (defun weak-circle-p (x) (weak-circle-p4 x)) | (defun circle-p (x) (circle-p5 x)) (defun circle-radius (x) | (circle-radius7 x))) | | > (circle 10) | eval:6:0: application: bad syntax in: (top/error . circle) | | > (circle-radius (circle 10)) | eval:7:0: application: bad syntax in: (top/error . | circle-radius) | | > (circle-p (circle 10)) | eval:8:0: application: bad syntax in: (top/error . circle-p) | | > (circle-p 'not-a-circle) | eval:9:0: application: bad syntax in: (top/error . circle-p) | | mutual-recursion: defined outside of begin-below at: HERE | in: (mutual-recursion (defun rect (temp16 temp17) (rect18 | temp16 temp17)) (defun weak-rect-p (x) (weak-rect-p19 x)) | (defun rect-p (x) (rect-p20 x)) (defun rect-width (x) | (rect-width22 x)) (defun rect-height (x) (rect-height23 x))) | | > (rect 10 20) | eval:11:0: application: bad syntax in: (top/error . rect) | | > (rect-width (rect 10 20)) | eval:12:0: application: bad syntax in: (top/error . | rect-width) | | > (rect-height (rect 10 20)) | eval:13:0: application: bad syntax in: (top/error . | rect-height) | | > (rect-p (rect 10 20)) | eval:14:0: application: bad syntax in: (top/error . rect-p) | | > (rect-p (rect -10 -20)) | eval:15:0: application: bad syntax in: (top/error . rect-p) | | > (rect-p 'not-a-rect) | eval:16:0: application: bad syntax in: (top/error . rect-p) |
|