On this page:
1.6.1 "data-structures/ list-theory"
1.6.2 "data-structures/ structures"

1.6 ACL2 Books

1.6.1 "data-structures/list-theory"


(include-book "data-structures/list-theory" :dir :system)


(deflist <list-pred> (l) <pred>)

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.


> (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).


> (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)

> (defstructure rect
    (width (:assert (natp width)))
    (height (:assert (natp height))))

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)