►Dracula: Reference Manual
▼1 ACL2
On this page:
case
case-match
cond
if
let
let*
mv-let
  ← prev  up  next → 

1.2 Expressions

Dracula supports these built-in expression forms.

(<function-name> expr ...)
Call a function by writing a sequence starting with its name, followed by expressions to compute its arguments. See Functions and Macros for a list of the functions provided by Dracula, or Events and Definitions to learn how to define your own.

Examples:

> (identity 'VALUE)

'VALUE

> (reverse "a man a plan a canal panama")

"amanap lanac a nalp a nam a"

(case expr (x1 val1) ...)
Checks the value of expr against x1 using eql. If it matches, val1 is returned. Otherwise, it checks any the subsequent branches. The optional otherwise branch is evaluated whenever all the ones before it failed. If no branches match (and an otherwise branch is not given), the case statement returns nil.

Examples:

> (case (+ 6 4)
        (11 10)
        (10 7)
        (otherwise 'error))

7

> (case 6 (5 'match))

'()

(case-match expr (pattern declaration body)...+)
Returns the value of the body that corresponds to the first matching pattern.

See ACL2’s documentation for the pattern language used by case-match. The declaration expressions are optional.

Examples:

> (defconst *list* (list 1 2 3 2 1))

eval:612:0: defconst: defined outside of begin-below at:

here in: (defconst *list* (list 1 2 3 2 1))

> (case-match *list*
    ((x x y z z)
     (list z y x))
    ((x y z y x)
     (list x y z)))

eval:613:0: application: bad syntax in: (top/error . *list*)

(cond (x1 y1)...)
Checks the xs in the given order, and returns the corresponding y for the first x to not evaluate to nil. If no xs match, the cond statement returns nil.

Examples:

> (cond
   ((< -5 0) (* -1 -5))
   (t -5))

5

> (cond (nil 'no) (t 'yes))

'yes

> (cond (nil 'no))

'()

(if p q r)
Returns r if p evaluates to nil; otherwise returns q.

Examples:

> (if (< 0 3) 'yes 'no)

'yes

> (if (< 3 0) 'yes 'no)

'no

> (if 5 'yes 'no)

'yes

> (if 'blah 'yes 'no)

'yes

> (if nil (+ "str" 'sym) 5)

5

(let ((var1 term1)...)  body)
Used for binding local variables. All terms are effectively evaluated in parallel; no term may refer to a variable that is bound in the same let expression.

Examples:

> (let ((x 4)) (+ x 6))

10

> (let ((a 1) (b 2)) (+ a b))

3

> (let ((a 1) (b (1+ a))) b)

eval:624:0: application: bad syntax in: (top/error . a)

(let* ((var1 term1)...)  body)
Used for binding local variables. All terms are evaluated sequentially, so they may refer to other variables defined in the same let expression

Examples:

> (let* ((x 4)) (+ x 6))

10

> (let* ((a 1) (b 2)) (+ a b))

3

> (let* ((a 1) (b (1+ a))) b)

2

(mv-let (var1 var2 var...)
        (mv term1 term2 term...)
        body)
Binds each var to its corresponding term in the mv expression, then evaluates the body.

Example:

> (mv-let (x y z)
          (mv 1 2 3)
          (list x y z))

'(1 2 3)

-

  ← prev  up  next →