On this page:
defdata
all
enum
oneof
range
record

8 Data Definitions

syntax

(defdata name type)

 
type = singleton
  | simple-type
  | (enum lst-expr)
  | (oneof type type)
  | (range numeric-type range-constraints)
  | (list type ...)
  | (cons type type)
  | (listof type)
  | (record (field-name . type) ...)
     
simple-type = all
  | boolean
  | symbol
  | string
  | numeric-type
     
numeric-type = rational
  | integer
  | nat
  | pos
     
range-constraints = (num-expr lt _ lt num-expr)
  | (num-expr lt _)
  | (_ lt num-expr)
     
lt = <
  | <=
Defines the function namep as a recognizer for the given type.

Singletons:
> (defdata one 1)
> (onep 1)

t

List Types:
> (defdata natlist (listof nat))
> (natlistp nil)

t

> (natlistp (list 2 3 5 8))

t

> (natlistp (list 2 3 -5 8))

nil

type

all

type

(enum lst-expr)

> (defdata traffic-light (enum (list 'red 'yellow 'green)))
> (traffic-lightp 'red)

t

> (traffic-lightp 'green)

t

> (traffic-lightp 'blue)

nil

type

(oneof type ...)

> (defdata intstr (oneof integer string))
> (intstrp 5)

t

> (intstrp -2)

t

> (intstrp "oconto")

t

> (intstrp 'watermelon)

nil

> (intstrp "watermelon")

t

> (defdata spiral (oneof nil (cons spiral spiral)))
> (spiralp nil)

t

> (spiralp (cons nil nil))

t

> (spiralp (cons (cons nil (cons nil nil)) nil))

t

> (spiralp (cons (cons (cons nil (cons nil nil))
                       (cons (cons nil nil) nil))
                 (cons nil
                       (cons (cons nil (cons nil nil)) nil))))

t

> (spiralp (cons (cons nil (cons "watermelon" nil)) nil))

nil

type

(range numeric-type range-constraints)

 
numeric-type = rational
  | integer
  | nat
  | pos
     
range-constraints = (num-expr lt _ lt num-expr)
  | (num-expr lt _)
  | (_ lt num-expr)
     
lt = <
  | <=
> (defdata probability (range rational (0 <= _ <= 1)))
> (probabilityp 1/2)

t

> (probabilityp 2)

nil

> (probabilityp 0)

t

> (probabilityp 1)

t

> (defdata big-nat (range integer (24601 < _)))
> (big-natp 4)

nil

> (big-natp 3827)

nil

> (big-natp 13372462)

t

type

(record (field-name . type) ...)

> (defdata fullname
    (record (first . string) (last . string)))
> (defconst *x* (fullname "David" "Smith"))
> *x*

(fullname "David" "Smith")

> (fullnamep *x*)

t

> (fullnamep "David")

nil

> (fullname-first *x*)

"David"

> (fullname-last *x*)

"Smith"

> (equal *x* (fullname "David" "Smith"))

t