Syntax of IACL2

April 1, 1997. Michael K. Smith

Copyright (C) 1996-97 Computational Logic, Inc. (CLI). All rights reserved.

Introduction

IACL2 is an infix dialect of ACL2. The intent is to provide a more conventional interface to the theorem prover, lowering some of the barriers to its adoption for specification as well as proof. This document describes the mapping between IACL2 and ACL2. As such, it does not constitute an introduction to IACL2 for an ACL2 novice.

IACL2 wraps two components, a parser and a printer, around ACL2. The printer will print anything that ACL2 will produce. But the parser does not parse all of these forms. Some will most likely be permanently considered ``expert'' forms that can only be entered using the native s-expression syntax of ACL2.

The typical relation between IACL2 and ACL2 forms is shown below:

  Syntax              Translation
  x1 OP x2            (op x1 x2)
  foo(x1, ... , xn)   (foo x1 ... xn)

Some ACL2 functions are translated to infix operators, for example arithmetic operators like ' +' and relations like '<'. Functions for which we have not provided an infix form print as the standard notation for a function call vs. the Lisp prefix notation.

The parser will parse forms that the printer will not print back identically. And the printer will print more forms than the parser will handle. But for syntacticly well formed input, the following relation should hold:

     parse(print(parse(input))) = parse(input)
Note that IACL2 relies on ACL2 to enforce many restrictions. For example, the requirement that constants begin and end with '*' is not checked by the IACL2 parser, but by ACL2 itself. So while the stand-alone IACL2 parser can perform a quick preliminary syntactic check, an IACL2 file cannot be consider syntactically acceptable until its translation has passed through ACL2.

Notation

The syntax rules honor the following conventions.

The lexical rules are similar, with the distinction that their terminal character components are not separated by whitespace.

Reserved Words and Special Symbols

Reserved Words
and append assoc atom axiom binary-*
binary-+ binary-@ bit boolean case case-match
certify certify! char collect complex congruence
consp constant current current-theory difference disable
e0-ord-< elif else enable enum equivalence
evaluator exists for forall function function-theory
guards if if* iff ignore implies
in in-package include incompatible integer intersect
label lambda load local macro member
module null never nil not mutual-recursion
of on or package quote ratio
rational record return signature signed-byte skip-proofs
t string symbol standard-char table termination
then theorem theory theory-invariant thm to
type typedef union universal-theory unless unsigned-byte
verify when word
Special Symbols
= == := ~= /=
< > <= >= \#
-> <-> \ | not
'[..] `[..] ,@ ,
` ' @ :>
- + * /

Literals, Identifiers, Constants

Syntax

literal     ::= boolean | string | number | character 
keyword     ::= :id

Literals

Boolean

In IACL2, t is a reserved word for boolean true, and nil is used for boolean false. Any non-NIL value is considered true.

Syntax

boolean ::=  t |  nil

Numbers

We support optionally signed decimal and octal integer literals and optionally signed decimal rationals. An octal literal begins with a ' 0'. Note that we do not support complex literals.

Syntax

number      ::= octal | decimal | rational
octal       ::= [  - ]  0 digit+
decimal     ::= [  - ] non-zero-digit digit*
rational    ::= decimal/decimal
The second decimal of a rational cannot be signed.

 01,  0177         octal literals
 1,  -77,  200     decimal literals
 4/32,  -13/100    rational literals

Strings

We support standard string syntax. A " is quoted in a string by preceding it with a backslash, e.g. "ab\"cd" or "\"".

 "This is a string"
 "\"" 
 "foo\"bar" 

Characters

Characters are surrounded by single quotes, e.g. 'a'. A number of special characters using slash notation are also supported.

 '\n'    newline
 '\t'    tab
 '\b'    rub
 '\f'    page

Comments

Comments are indicated by the C /* ... */ convention. We depend on the C preprocessor to remove them. Note that the fact that we use CPP means that you can also use the other preprocessor supported conventions like \#include, \#define, etc.

Examples

/* This is a comment */

/* This is a multi-line comment, which can go on for some time.*/

Identifiers

An identifier may have a package prefix.

Syntax

id      ::= atom | atom:atom | atom::atom
atom    ::= alpha char*
alpha   ::=  a ..  z |  A ..  Z
char    ::= alpha | digit |  - |  _ |  ?

Constant Declarations (DEFCONST)

A constant name must begin and end with an asterisk ( *).

Syntax                                            Translation
constant ::= constant  *id* [ : type ] = expr  ;    (constant *id* expr
                                                         :TYPE type 
                                                         :LEMMA theorem doc-string)
Examples
constant *day*  = 'Mon ;
constant *temp* : integer = 24 ;
constant *digits* = '[0 1 2 3 4 5 6 7 8 9];
constant *three* : integer  = 3;
Examples
(const *digits* '(0 1 2 3 4 5 6 7 8 9))

Prints as:

constant *digits* = '[0 1 2 3 4 5 6 7 8 9];

Parses to:

(const *digits* '(0 1 2 3 4 5 6 7 8 9))

constant *three* : integer = 3; Parses to: (const *three* 3 :type integer :lemma (integerp *three*)) Macro expands to: (progn (defconst *three* 3) (defthm constant-three-type (integerp *three*) :rule-classes nil))

Types, including Enumerations, Lists, Alists, Records

Any function of a single argument can function as a type. Such functions should not themselves have typed arguments (guards). E.g. '1+' is not a permissible type. A non-NIL return from f(x) indicates that x satisfies the requirements of the type f.

Primitive Types
Name Translation
integer INTEGERP
atom ATOM
boolean BOOLEANP
bit (OR (EQUAL x 1) (EQUAL x 0))
character CHARACTERP
complex COMPLEX-RATIONALP
cons CONSP
nil NIL
null (NULL x)
ratio (AND (RATIONALP x)(NOT (INTEGERP x)))
rational RATIONALP
string STRINGP
symbol SYMBOLP
signed-byte INTEGERP
unsigned-byte UNSIGNED-BYTEP
standard-char STANDARD-CHARP

The parser accepts a number of so-called type definitions, which are converted to the appropriate ACL2 function definitions. We support special constructors for simple enumeration types, records, lists, and association lists. These are based on a set of libraries that are pre-loaded into IACL2, as do the looping and quantified function constructors. We make sure that functions that may be used as types have their guards checked by inserting (DECLARE (XARGS :verify-guards T )) into the translation to ACL2. We have suppressed this in some of the examples below.

Syntax

typedef    ::= rename | enumeration | list | alist | record
rename     ::= type id = id  ;
enumeration::= type id = enum  [ id , ..., id  ]  ;
list       ::= type id = id *  ;
alist      ::= type id =  [ id . id  ]  ;
record     ::= type id =  ( field , .. field  ) ;
field      ::= id [ : type ] [ = term ]  ;
type       ::= id
Examples
type foo = integer ;

Parses to:

(DEFUN foo (x) (INTEGERP x))

Prints as:

function foo (x)  integerp(x)  ;

type foo = integer *; Parses to: (DEFLIST foo (l) INTEGERP) Prints as: type foo = integer *;

type foo = [integer . character] *; Parses to: (DEFALIST foo (l) (INTEGERP . CHARACTERP)) Prints as: type foo = [integer . character] *;

type bar = enum [a, b, c]; Parses to: (DEFUN bar (x) (MEMBER-EQUAL x '(a b c))) Prints as: function bar(x) x in '[a b c] ;

type PERSON = record ( name : string := "John", age : integer := 19, sex : string := "male"); Parses to: (DEFSTRUCTURE MAKE-person (name (:assert (STRINGP name) :rewrite)(:default "John")) (age (:assert (INTEGERP age) :rewrite)(:default 19)) (sex (:assert (STRINGP sex) :rewrite)(:default "male")) (:options :guards (:predicate person)(:conc-name NIL) (:keyword-constructor key-person) (:keyword-updater update-person))) Prints as: type PERSON = record ( name : string := "John", age : integer := 19, sex : string := "male" );

Expressions

Syntax

expr        ::= expr op_1 expr | relation
relation    ::= relation op_2 relation | expr2
expr2       ::= expr2 op_3 expr2 | term
term        ::= term op_4 term | unary | primary
unary       ::= op_5 primary
primary     ::= ( expression ) | primary . primary | 
                <exprs > | primary [ expr ] | 
                [key id  ] | 'id | 
                [ expr , ... , expr  ] |
                id ( expr , ... , expr ) |
                statement | 
                id | constant | literal

op_1        ::=  \ & | | | -> | <-> 
op_2        ::=  =  | == | /= | ~= | < | <= | > | >= | in | ~in | member 
op_3        ::=  +  | - | :> | @ | \ 
op_4        ::=  *  | / | union | difference | intersect | incompatible 
op_5        ::=  ~ | not | - | / 
The infix operators in the table below are listed in order of increasing precedence, with equal precedence operators grouped together. Binary operators are left or right associative as indicated below.

IACL2 ACL2 Associates
a -> b <=> (implies a b) right
a <-> b <=> (iff a b) right
a \ b <=> (and a b) right
a | b <=> (or a b) right
not a <=> (not a)
a = b <=> (equal a b) left
a == b <=> (= a b) left
a eq b <=> (eq a b) left
a ~= b <=> (not (equal a b)) left
a /= b <=> (/= a b) left
a in b <=> (member a b) left
a ~in b <=> (not (member a b)) left
a < b <=> ( < a b) left
a <= b <=> ( <= a b) left
a > b <=> ( > a b) left
a >= b <=> ( >= a b) left
a e0-ord-< b <=> ( e0-ord-< a b) left
a @ b <=> (append a b) right
b \ a <=> (assoc a b) left
a :> b <=> (cons a b) right
b difference a <=> (difference a b) left
b intersect a <=> (intersect a b) left
b union a <=> (union a b) left
b incompatible a <=> (incompatible a b) left
a + b <=> (+ a b) right
a - b <=> (- a b) left
a * b <=> (* a b) right
a / b <=> (/ a b) left

'a

<=> (quote a)
[a, b, c, d] <=> (list a b c d)
'[a b c d] <=> '(a b c d)

Infix Translation
a & b & c & d <=> (and a (and b (and c d )))
a & (b & (c & d)) <=> (and a (and b (and c d)))
((a & b) & c) & d <=> (and (and (and a b) c) d)
(3 + 2) - (3 + 4) <=> (- (+ 3 2) (+ 3 4))
x * y * y = x * y * y <=> (equal (* x (* y y)) (* x (* y y)))
2 + 3 + 3 + 3 <=> (+ 2 (+ 3 (+ 3 3 )))
(2 + 3) + 3 + 3 <= (+ (+ 2 3) (+ 3 3))
((2 + 3) + 3) + 3 <= (+ (+ (+ 2 3) 3) 3)
2 + (3 + (3 + 3)) <=> (+ 2 (+ 3 (+ 3 3)))
2 + 3 + 4 + 5 <= (+ 2 3 4 5)
1 - 2 - 3 - 4 <= (- 1 2 3 4)
1 - 2 - 3 - 4 <=> (- (- (- 1 2) 3) 4)
2 * 3 * 4 * 5 <= (* 2 3 4 5)
1 * 2 * 3 * 4 <=> (* 1 (* 2 (* 3 4)))
1 / 2 / 3 <=> (/ (/ 1 2) 3)
(1 / 2) * 3 => (* (/ 1 2) 3)
1 / 2 * 3 <=> (* (/ 1 2) 3))
2/3 * 1 <=> (* 2/3 1))
1/2/3/4 => (/ 1/2 3/4)
1/2 / 3/4 <= (/ 1/2 3/4)
1 / 2 / 3 / 4 <= (/ 1 2 3 4)
1 / 2 / 3 / 4 <=> (/ (/ (/ 1 2) 3) 4)
not not a <=> (not (not a))
-x <=> (- x)
(- x) => (- x)
-4 <=> -4

Arrays

ACL2's support for arrays is sufficiently unusual that we do not provide any special support for them. In fact, we use the syntax a[i] to represent the ACL2 list operation (nth a i). See the appendix.

Statements

Before we present the syntax of blocks we will describe multiple-valued forms and assignment, which are used in blocks.

Multiple Values

Functions normally return a single value. They can return multiple values. To create an expression returning multiple values use angle brackets as shown below.

Syntax

<expr , ... , expr>

Assignment

Assignments have the effect of ' let*' variable introduction in ACL2. They can only appear in blocks that terminate in a non-assignment expression. In the case of multiple valued assignments ( mv-let), the list of variables is enclosed in angle brackets.

Syntax

assignment ::=  id  := expr  ;  | <id , ... , id>  := expr  ;

Blocks

A block is an apparent sequence of statements, separated by ' ;' and enclosed in braces, '' and ''. It is in fact a let*. There may only be one expression following a sequence of assignments. The value of that expression is the value of the block.

Syntax

block ::=  { [ assignment ... assignment ] expr ; } 
Infix Translation
 { <X, Y, Z> := <1, 2, 3>;
   expr } ;
<=>
 (mv-let (x y  z) (mv 1 2 3) expr)
 { a := b;
   c := d;
   expr } ;
<=>
 (let ((a b)
       (c d))
    expr)
 { a := 1; 
   c := 4;
   a + c   } ; 
<=>
 (let* ((a 1)
        (c 4))
    (+ a c))
 <a, expr> 
<=>
 (mv a expr)

Flow of Control

IACL2 depends on recursion for much of its control flow. We provide two conditional ``statements'' (actually expressions), if and case expressions. In addition there is limited support for an iterative style of function definition (see iterative functions).

If statement

Syntax

if (expr) then expr 
[ elif (expr) then expr ]* 
else expr
Example
if (a ~= b) then 
   c := 3;
   a * c ;   ;
else
   nil;
Infix Translation
if x then y else z 
<=>
(if x y z)
if x then y              
  elif a then b 
<=>
(if x y (if a b))
if a then b              
 elif c then d           
   else x 
<=>
(cond ((a b)                       
       (c d)                       
       (t x)))

Case statement

Syntax

case  expr  
      val_1  : expr_1 ; 
      ... 
      val_k  : expr_k ; 
      [ else  : expr_{k+1} ]   ;
Example
case day 
 'mon : 1;
 'tue : 2;
 'wed : 3;
 'thu : 4;
 'fri : 5;
  else : 0; ;

Parses to:

(CASE day ('mon 1 )
          ('tue 2 )
          ('wed 3 )
          ('thu 4 )
          ('fri 5 )
          (OTHERWISE 0 ))

Basic Events

Axioms (DEFAXIOM)

Syntax                            Translation
axiom id  expr                     (defaxiom name expr 
    :rule-classes rule-classes  ;               :rule-classes rule-classes)
Example
(DEFAXIOM sbar 
        (implies (bar x) (bar-zero y))
        :rule-classes (:rewrite)
        :doc "sbar testing")  

Prints as:

/* sbar testing */
Axiom sbar 
 bar (x) -> bar-zero (y); 
 :rule-classes [:rewrite] ;

Parses to:

(DEFAXIOM sbar 
        (implies (bar x) (bar-zero y))
        :rule-classes (:rewrite))  

Functions (DEF)

Syntax    
function id ( vars [ | expr ] ) [ : type ]
     term          
     [dcl ... dcl];

vars    ::= [ var , ... , var ]
var     ::= id [ : type ]

Translation
(def id ( vars ) 
     [dcl ... dcl]
     term 
     :TYPE type
     :LEMMA theorem 
     :DISABLE [T | F])

We do not handle IGNORE dcls, e.g (declare (ignore x)).

Examples

function foo (x , y)  x + y   ;

Parses to:

(def foo (x y) (+ x y) :DISABLE T)

function foo (x : integer, y : integer | bar(x)): integer if x < y then 1 + x else y - 1 ; :measure p(x); Parses to: (def foo (x y) (DECLARE (TYPE INTEGER x) (TYPE INTEGER y) (XARGS :guard (bar x)) (XARGS :measure (p x))) (IF (< x y)(+ 1 x)(- y 1)) :TYPE INTEGER :LEMMA (IMPLIES (AND (INTEGERP x)(INTEGERP y)) (INTEGERP (foo x y))) :DISABLE T) Macro expands to: (progn (defun foo(x y) (DECLARE (TYPE INTEGER x) (TYPE INTEGER y) (XARGS :guard (bar x)) (XARGS :measure (p x))) (IF (< x y) (+ 1 x) (- y 1))) (defthm defun-foo-type (IMPLIES (AND (INTEGERP x)(INTEGERP y)) (INTEGERP (foo x y)))))

DEF is a macro which has DEFUN syntax. In addition, it takes keywords. :TYPE specifies the function type and :LEMMA is a constructed theorem asserting that if the arguments are of the right type then the function will return a value of the function type.

Functions with Quantifiers (DEFUN-SK)

Syntax 
function id ( vars )
 quantifier id , ... , id | term   ; 
quantifier ::= exists | forall

Translation
(DEFUN-SK id ( vars ) (quantifier id* term)
          &key doc quant-ok skolem-name thm-name)
We don't support types on the arguments of such quantified functions.

Example

function some-x-y-p-and-q(z)
 exists x, y |  p(x, y, z) & q(x, y, z)   ;

Parses to:

(DEFUN-SK some-x-y-p-and-q (z)
 (exists (x y)
         (and (p x y z)
              (q x y z))))

Iterative Functions (DEFLOOP)

Syntax                          
function id (id , ... , id)         
 for id from expr [ by expr ], 
      [ condition expr ]                  
      [ return expr ]                 
      [ op expr ]                      
      [ test expr ]   ;      

from     ::= in | on
condition::= when | if 
op       ::= collect | append 
test     ::= forall | exists | never

Translation
(defloop id (id*)
  (for ((id from expr  [ by expr ] ))
       [ (condition expr) ] 
       [ (return expr) ] [ (op expr) ] [ (test expr) ] ))

Example
function all-keyword(l)
 for x in l, when keywordp(x), collect x   ;

Parses to:

(DEFLOOP all-keyword (l)
  (FOR ((x IN l)) (WHEN (keywordp x) (COLLECT x))))

(defloop keyword-listp (l) "Recognizes lists of keywords." (declare (xargs :guard t)) (for ((x in l)) (always (keywordp x)))) Prints as: /* Recognizes lists of keywords. */ Function keyword-listp(l) for x in l, forall keywordp(x) :guard t;

Macros (DEFMACRO)

We support two forms of macro definition in IACL2. A ``substitution macro'' is one that can be expressed as a simple back-quoted form, substituting the bindings of the macro variables for their occurence within the body (e.g. like a CPP macro). If the body is a substitution macro, then the syntax is ``macro foo(a,b) = ...''. If you need to create a macro that is other than a simple substitution macro, an arbitrary constructive function, use ``macro foo(a,b) \# f(a,b)''. We don't allow `&' keywords.

Syntax                            Translation
macro id (id*) = term ;          (defmacro id (id*) `term)

macro id (id*) \# term ;         (defmacro id (id*) term)
Examples
macro key-name(name) = name[1];

Parses to:

(DEFMACRO key-name(name) `(NTH 1 ,name))

key-name(x) Macro expands to: x[1]

macro static-name(name) \# name[1]; Parses to: (DEFMACRO static-name(name) (NTH 1 name))

static-name('[a, b, c]) Macro expands to: 'b

Signature (DEFSTUB)

Syntax                            Translation
signature id (id*)               (defstub-signature id (id*) 
     [ : id | < id , ... , id > ]            [ id | (mv id*) ] 
                                             :axiom axiom)
Examples
signature test1 (x, y, state) ;

Parses to:

(defstub-signature test1 (x y state) T)

Prints as:

signature test1(x, y, state) : t;

signature subr1 (x, y, state) : < T, state>; Parses to: (defstub-signature subr1 (x y state) (MV T state))

signature subr2(x, y, state) : foo; Parses to: (defstub-signature subr2 (x y state) foo :AXIOM (foo (subr2 x y state)))

signature subr3 (x : integer, y : boolean) : < integer, character>; Parses to: (defstub-signature subr3 (x y) (mv integer character) :axiom (implies (and (integerp x) (booleanp y)) (mv (subr3 x y)))) Macro expands to: (progn (defstub subr3 (x y) (mv integer character))

(defaxiom signature-subr1-axiom (x y) (implies (and (integerp x) (booleanp y)) (mv (subr3 x y)))))

Theorems (DEFTHM)

Syntax                            Translation
theorem id  term                  (defthm id term
     :rule-classes rule-classes             :rule-classes rule-classes
     :instructions instruction              :instructions instructions
     :hint        hints                     :hint         hints
     :otf-flg     otf-flg                   :otf-flg      otf-flg
                                              :doc          doc-string)
Example
theorem eval-exp-list-val-type-prescription
 flg -> true-listp (eval-exp-plus-val (flg, x, vs)) ;   
 :rule-classes :type-prescription;

Parses to:

(DEFTHM eval-exp-list-val-type-prescription
 (implies flg 
          (true-listp (eval-exp-plus-val flg x vs)))
 :RULE-CLASSES :TYPE-PRESCRIPTION)

Complex Events

Modules (ENCAPSULATE)

Syntax                            Translation
module [ id ]                     (module ( signature+ ) 
      signature+                     ( event+ )  
      event+                         [ :label id ] )
Example
module 
 an-element(lst) : t;  
 local function an-element(lst)
         if consp(lst) then car(lst)
              else nil   ;
  local theorem member-equal-car
          lst & true-listp(lst) -> car(lst) in lst   ;
  theorem thm1  null(lst) -> null(an-element(lst))   ;
  theorem thm2
   true-listp(lst) & ~(null(lst)) -> an-element(lst) in lst   ;   ;

Parses to:

(MODULE ((an-element (lst) t))
  (local (def an-element (lst)
           (if (consp lst) (car lst) nil)))
  (local (defthm member-equal-car
            (implies (and lst (true-listp lst))
                     (member-equal (car lst) lst))))
  (defthm thm1
     (implies (null lst) (null (an-element lst))))
  (defthm thm2
     (implies (and (true-listp lst)
                   (not (null lst)))
              (member-equal (an-element lst) lst))))

Module foo an-element(lst) : t; local Function an-element(lst) IF consp(lst) then car(lst) else nil ; local Theorem member-equal-car lst & true-listp(lst) -> car(lst) in lst ; Theorem thm1 { null(lst) -> null(an-element(lst)) ; Theorem thm2 true-listp(lst) & (null(lst)) -> an-element(lst) in lst }; ; Prints as: (MODULE ((an-element (lst) T)) (local (def an-element (lst) (if (consp lst)(car lst)nil) :disable t)) (local (defthm member-equal-car (implies (and lst (true-listp lst)) (member-equal (car lst)lst)))) (defthm thm1 (implies (null lst) (null (an-element lst)))) (defthm thm2 (implies (and (true-listp lst) (not (null lst))) (member-equal (an-element lst)lst))) :label foo) Macro expands to: (progn (DEFLABEL foo-start) (MODULE ((an-element (lst) T)) (local (def an-element (lst) (if (consp lst)(car lst)nil) :disable t)) (local (defthm member-equal-car (implies (and lst (true-listp lst)) (member-equal (car lst)lst)))) (defthm thm1 (implies (null lst) (null (an-element lst)))) (defthm thm2 (implies (and (true-listp lst) (not (null lst))) (member-equal (an-element lst)lst)))) (DEFTHEORY foo (set-difference-theories (current-theory :here) (current-theory 'foo-start))))

Theory, In-Theory

Theory (DEFTHEORY)

Syntax                            Translation
theory id := term  ;        (DEFTHEORY id term :doc :doc-string)
Examples
theory ava-op-fns := 
            current-theory(:here) 
 difference union-theories(function-theory('ava-op-fns-start), disable(moo));

Parses to:

(deftheory ava-op-fns
  (set-difference-theories
    (current-theory :here)
    (union-theories (function-theory 'ava-op-fns-start )(disable moo))))

In-theory

Syntax                            Translation
In-Theory (term) ;                (IN-THEORY term :doc :doc-string)
Example
(in-theory (set-difference-theories
             (universal-theory :here)
             '(flatten (:executable-counterpart flatten))))

Prints as:

in-theory(            current-theory(:here)
           difference '[flatten [:executable-counterpart flatten]]);

Labels (DEFLABEL)

Syntax                            Translation
label id  ;                       (deflabel id :doc doc-string)
Example
(deflabel interp-section :doc "text")

Prints as:

/* Text */
label interp-section ;

Parses to:

(deflabel interp-section)
Note that we lose the :doc field, having treated it as a comment in IACL2.

Packages

Package (DEFPKG)

Syntax                            Translation
package id = term  ;              (defpkg id term doc-string)
The package id must be a string.

Example

(defpkg "my-pkg"
        (union-eq *acl2-exports*
                  *common-lisp-symbols-from-main-lisp-package*))

Prints as:

package "my-pkg" = union-eq(*acl2-exports*,
                         *common-lisp-symbols-from-main-lisp-package*);

IN-PACKAGE

Example

(in-package "ACL2")

Prints as:

in-package("ACL2")  ;

Parses to:

(in-package "ACL2")

Mutual Recursion

Mutual-Recursion

Syntax                            Translation
mutual-recursion                  (mutual-recursion function_1 ... function_n)
      function_1; 
      ... 
      function_n; 
Example
(mutual-recursion
 (defun evenlp (x)
   (if (consp x) (oddlp (cdr x)) t))
 (defun oddlp (x)
   (if (consp x) (evenlp (cdr x)) nil)))

Prints as:

mutual-recursion 

 function evenlp(x)
  if consp(x) then oddlp(cdr(x))
     else t    ;

 function oddlp(x)
  if consp(x) then evenlp(cdr(x))
     else nil    ;
   ;

DEFUNS

Syntax                            Translation
See Mutual recursion above.       (DEFUNS def1 ... defn)
Example
(defuns
 (evenlp (x)
   (if (consp x) (oddlp (cdr x)) t))
 (oddlp (x)
   (if (consp x) (evenlp (cdr x)) nil)))

Prints as:

mutual-recursion
  function evenlp(x)
         if consp(x) then oddlp(cdr(x))
                else t   ;
  function oddlp(x)
         if consp(x) then evenlp(cdr(x))
                else nil   ;
   ;

Include (INCLUDE-BOOK)

Example

(include-book "sets")

Prints as:

include("sets");

Parses to:

(include-book "sets")

Commands

Verify Guards

Syntax                            Translation
verify guards;                    (verify-guards id
                                                  :hints        hints
                                                  :otf-flg      otf-flg
                                                  :doc          doc-string)
Example
(verify-guards flatten
               :hints (("Goal" :use (:instance assoc-of-app)))
               :otf-flg t
               :doc "string")

Prints as:

/* string */
verify guards flatten
 :hints [["Goal" :use [:instance assoc-of-app ]]]
 :otf-flg t;

Verify Termination

Syntax                            Translation
verify termination;               (verify-termination (fn dcl ... dcl))
Example
(verify-termination  fact
 (declare (xargs :guard (and (integerp x) (>= x 0)))))

Prints as:

Verify termination fact
      :guard integerp(x) & x >= 0;

Other Commands

Commands typed to IACL2 must be terminated by a `;'.

A cd is a command descriptor.

Syntax                 Translation
IACL2                    ACL2          
                                                   
:cmd cd;               :cmd cd                 
:cmd_2(id);            :cmd2 id          
         
cmd      ::=  PBT | PC  | PCB | PCB! | PR | PUFF | PUFF* | UBT | UBT!          
cmd2     ::=  PE  | PE! | PL  | PR           
          
cd       ::=  :N | :MAX | :MIN | :X | fn | [:X -k] | [cd n] |            
              [:SEARCH pat cd1 cd2'] | [:SEARCH pat]  
Examples
:u;                   
:oops;                
:pcs 12 14;

:pf(fn); :pf(:definition,fn); :pf(:rewrite,fn);

:pbt [:x -3]; :ubt [:search foo];

Arrays

Array operations just translate into standard function calls.

Aref

Functions suffixed with a '1' deal with one dimensional arrays and functions suffixed with a '2' deal with two dimensional arrays.

Syntax                            Translation
aref1(name, alist, i)             (aref1 name alist i)         
aref1(name, alist, i, j)          (aref2 name alist i j)       
Example
(aref1 'demo (@ a) 0)

Prints as:

aref1(demo, @a, 0)

Arrayp

Syntax                        Translation
array1p(name, alist)          (array1p name alist) 
array2p(name, alist)          (array2p name alist) 
Example
(array1p 'demo (@ a))

Prints as:

Array1p(demo, @a)

Aset

Syntax                            Translation
aset1(name, alist i, value)       (aset1 name alist i val) 
aset2(name, alist, i, j, value)   (aset2 name alist i j val) 
Example
(assign b (aset1 'demo (@ a) 1 'one))

Prints as:

cb := Aset1(demo, @a, 1, 'one)

Compress

Syntax                            Translation
compress1(name, alist)            (compress1 name alist) 
compress2(name, alist)            (compress2 name alist) 
Example
(assign a (compress1 'demo 
                     '((:header :dimensions (5)
                                :maximum-length 15
                                :default uninitialized
                                :name demo)
                       (0 . zero))))

Prints as:

a := Compress1(demo, '[[:header :dimensions[5]
                       :maximum-length 15 
                       :default uninitialized 
                       :name demo]
                       [0 . zero]]
              );

Other Array Functions

ACL2 Syntax:                 ACL2:                        IACL2:

(default name alist)        (default 'demo (@ a))         default(demo, @a)
(dimensions name alist)     (dimensions 'demo (@ a))      dimensions(demo, @a)
(header name alist)         (header 'demo (@ a)           header(demo,@a)       
(maximum-length name alist) (maximun-length 'demo (@ a))  maximun-length('demo, @a)

Printed, But Not Parsed

The following events cannot be input directly into IACL2. You need to create ACL2 books to support the the use of these advanced features.

Equivalence relation

DEFCONG

Example

(defcong set-equal iff (memb x y) 2
        :rule-classes (:rewrite))

Prints as:

Equivalence relation: SET-EQUAL preserves IFF
 for argument position 2 of MEMB(X, Y)
 :rule-classes [:REWRITE];
Does not parse

DEFEQUIV

Example

(defequiv set-equal 
        :rule-classes (:rewrite))

Prints as:

Equivalence relation: SET-EQUAL 
 :rule-classes [:REWRITE];
Does not parse.

Evaluator

Syntax                            Translation
Evaluator (ev, ev-list)     (defevaluator  ev ev-list
    [g_1 x1 ... xn1,           ((g_1 x1 ... xn1)
     ...            ...
     g_k x1 ... xnk ]           (g_k x1 ... xnk)))
Example
(defevaluator evl evl-list
  ((length x) (member x y)))

Prints as:

Evaluator (evl, evl-list)  [ length(x), x in y  ];
Does not parse

Refinement (DEFREFINEMENT)

Example

(defrefinement equiv1 equiv2)

Prints as:

Refinement EQUIV1 refines EQUIV2;

CHOOSE (DEFCHOOSE)

Example
(defchoose choose-x-for-p-and-q (x) (y z)
  (and (p x y z)
       (q x y z)))

Prints as:

Choose choose-x-for-p-and-q(x) (y, z) 
 p(x, y, z)  &  q(x, y, z)  ;

SET and TABLE Events

All these events are printed and parsed as function calls.

Infix Translation
set-compile-fns(term); <=> (set-compile-fns term)
set-ignore-ok(flg); <=> (set-ignore-ok flg)
set-inhibit-warnings(s1 s2); <=> (set-inhibit-warnings s1 s2)
set-invisible-fns-alist(alist); <=> (set-invisible-fns-alist alist)
set-irrelevant-formals-ok(flg); <=> (set-irrelevant-formals-ok flg)
set-measure-function(name); <=> (set-measure-function name)
set-verify-guards-eagerness(n); <=> (set-verify-guards-eagerness n)
set-well-founded-relation(rel); <=> (set-well-founded-relation rel)

Tables

        (table table-name key-term value-term op term)
Examples
 ACL2                                  INFIX

(table tests 25) table(tests,25); (table tests) table(tests); (table tests nil nil :clear) table(tests, nil, nil, :clear); (table tests nil (foo 7) :clear) table(tests, nil, foo(7),:clear); (table tests nil nil :guard) table(tests, nil, nil,:guard); (table tests nil nil :guard term) table(tests, nil, nil,:guard term);