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

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:

Some ACL2 functions are translated to infix operators, for example arithmetic operators like 'SyntaxTranslationx1 OP x2 (op x1 x2) foo(x1, ... , xn) (foo x1 ... xn)

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.

The syntax rules honor the following conventions.

- Non-terminals are in
*italics*. - Reserved words and special symbols are in
`typewriter font`. - ``a ::= b'' means that non-terminal a is defined by the patterns of b.
- Alternatives are separated by |.
- Optional terms are bracketed, [
*expr*]. - The notation x ... x indicates a non-empty sequence of x.
- The notation x c ... c x indicates a non-empty sequence of x separated by c.

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

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

'[..] | `[..] | ,@ | , | ||

` | ' | @ | :> | ||

- | + | * | / | ||

**Syntax**

literal::=boolean|string|number|characterkeyword::=:id

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

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**

The secondnumber::=octal|decimal|rationaloctal::= [-]0digit+decimal::= [-]non-zero-digitdigit*rational::=decimal/decimal

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

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 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 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.*/

An identifier may have a package prefix.

**Syntax**

id::=atom|atom:atom|atom::atomatom::=alphachar*alpha::=a..z|A..Zchar::=alpha|digit|-|_|?

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

SyntaxTranslationconstant::= constant *id* [ :type] =expr; (constant *id*expr:TYPE type :LEMMA theorem doc-string)

constant *day* = 'Mon ; constant *temp* : integer = 24 ; constant *digits* = '[0 1 2 3 4 5 6 7 8 9]; constant *three* : integer = 3;

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

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|recordrename::= typeid=id;enumeration::= typeid= enum [id, ...,id] ;list::= typeid=id* ;alist::= typeid= [id.id] ;record::= typeid= (field, ..field) ;field::=id[ :type] [ =term] ;type::=id

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" );

**Syntax**

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.expr::=exprop_1expr|relationrelation::=relationop_2relation|expr2expr2::=expr2op_3expr2|termterm::=termop_4term|unary|primaryunary::= op_5primaryprimary::= (expression) |primary.primary|<exprs>|primary[expr] |[keyid]| 'id|[expr, ... ,expr]|id( expr , ... , expr ) |statement|id|constant|literalop_1 ::=\ & | | | -> | <->op_2 ::== | == | /= | ~= | < | <= | > | >= | in | ~in | memberop_3 ::=+ | - | :> | @ | \op_4 ::=* | / | union | difference | intersect | incompatibleop_5 ::=~ | not | - | /

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 |

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.

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

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>

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;

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

| <=> | (mv-let (x y z) (mv 1 2 3) |

| <=> | (let ((a b) (c d)) |

| <=> | (let* ((a 1) (c 4)) (+ a c)) |

<a, | <=> | (mv a |

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

**Syntax**

if(expr)thenexpr[elif(expr)thenexpr]*elseexpr

if(a ~= b)thenc := 3; a * c ;;elsenil;

Infix | Translation | |

| <=> | (if x y z) |

| <=> | (if x y (if a b)) |

| <=> | (cond ((a b) (c d) (t x))) |

**Syntax**

caseexprval_1:expr_1;... val_k:expr_k;[else:expr_{k+1} ];

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

SyntaxTranslationaxiomid(defaxiom name expr :rule-classes rule-classesexpr;:rule-classes rule-classes)

(DEFAXIOM sbar (implies (bar x) (bar-zero y)) :rule-classes (:rewrite) :doc "sbar testing")Prints as:/* sbar testing */ Axiom sbarbar (x) -> bar-zero (y);:rule-classes [:rewrite] ;Parses to:(DEFAXIOM sbar (implies (bar x) (bar-zero y)) :rule-classes (:rewrite))

We do not handle IGNORE dcls, e.g (declare (ignore x)).Syntaxfunctionid(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])

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

We don't support types on the arguments of such quantified functions.Syntaxfunctionid(vars)quantifierid, ... ,id|term;quantifier::=exists|forallTranslation(DEFUN-SKid(vars) (quantifierid*term) &key doc quant-ok skolem-name thm-name)

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

Syntaxfunctionid(id , ... , id) foridfromexpr[ byexpr], [ conditionexpr] [ returnexpr] [ opexpr] [ testexpr] ;from::= in | oncondition::= when | ifop::= collect | appendtest::= forall | exists | neverTranslation(defloopid(id*) (for ((idfrom expr [ by expr ] )) [ (condition expr) ] [ (return expr) ] [ (op expr) ] [ (test expr) ] ))

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;

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.

SyntaxTranslationmacroid(id*) =term; (defmacroid(id*) `term) macroid(id*) \#term; (defmacroid(id*)term)

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

SyntaxTranslationsignatureid(id*) (defstub-signature id (id*) [ :id| <id, ... ,id> ] [id| (mvid*) ] :axiom axiom)

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

SyntaxTranslationtheoremidterm(defthmidterm:rule-classesrule-classes:rule-classesrule-classes:instructionsinstruction:instructionsinstructions:hinthints:hinthints:otf-flgotf-flg:otf-flgotf-flg:doc doc-string)

theorem eval-exp-list-val-type-prescriptionflg -> 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)

SyntaxTranslationmodule[id] (module (signature+ )(signature+event+ )[ :labelevent+id] )

modulean-element(lst) : t;local function an-element(lst)if consp(lst) then car(lst) else nil;local theorem member-equal-carlst & true-listp(lst) -> car(lst) in lst;theorem thm1null(lst) -> null(an-element(lst));theorem thm2true-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-carlst & true-listp(lst) -> car(lst) in lst;Theorem thm1 { null(lst) -> null(an-element(lst));Theorem thm2true-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))))

SyntaxTranslationtheoryid:=term;(DEFTHEORYidterm:doc :doc-string)

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

SyntaxTranslationIn-Theory (term);(IN-THEORYterm:doc :doc-string)

(in-theory (set-difference-theories (universal-theory :here) '(flatten (:executable-counterpart flatten))))Prints as:in-theory( current-theory(:here) difference '[flatten [:executable-counterpart flatten]]);

SyntaxTranslationlabelid;(deflabelid:doc doc-string)

(deflabel interp-section :doc "text")Note that we lose the :doc field, having treated it as a comment in IACL2.Prints as:/* Text */ label interp-section ;Parses to:(deflabel interp-section)

The packageSyntaxTranslationpackageid=term;(defpkgidtermdoc-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*);

**Example**

(in-package "ACL2")Prints as:in-package("ACL2");Parses to:(in-package "ACL2")

SyntaxTranslationmutual-recursion(mutual-recursion function_1 ... function_n)function_1; ... function_n;

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

SyntaxTranslationSee Mutual recursion above. (DEFUNS def1 ... defn)

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

**Example**

(include-book "sets")Prints as:include("sets");Parses to:(include-book "sets")

SyntaxTranslationverify guards; (verify-guardsid:hints hints :otf-flg otf-flg :doc doc-string)

(verify-guards flatten :hints (("Goal" :use (:instance assoc-of-app))) :otf-flg t :doc "string")Prints as:/* string */verifyguardsflatten :hints [["Goal" :use [:instance assoc-of-app ]]] :otf-flg t;

SyntaxTranslationverify termination; (verify-termination (fn dcl ... dcl))

(verify-termination fact (declare (xargs :guard (and (integerp x) (>= x 0)))))Prints as:Verifyterminationfact :guard integerp(x) & x >= 0;

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

A *cd* is a * command descriptor*.

SyntaxTranslationIACL2 ACL2 :cmdcd; :cmdcd:cmd_2(id); :cmd2idcmd::=PBT | PC | PCB | PCB! | PR | PUFF | PUFF* | UBT | UBT!cmd2::=PE | PE! | PL | PRcd::=:N | :MAX | :MIN | :X | fn | [:X -k] | [cdn] |[:SEARCH pat cd1 cd2'] | [:SEARCH pat]

:u; :oops; :pcs 12 14;:pf(fn); :pf(:definition,fn); :pf(:rewrite,fn);

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

SyntaxTranslationaref1(name, alist, i) (aref1 name alist i) aref1(name, alist, i, j) (aref2 name alist i j)

(aref1 'demo (@ a) 0)Prints as:aref1(demo, @a, 0)

SyntaxTranslationarray1p(name, alist) (array1p name alist) array2p(name, alist) (array2p name alist)

(array1p 'demo (@ a))Prints as:Array1p(demo, @a)

SyntaxTranslationaset1(name, alist i, value) (aset1 name alist i val) aset2(name, alist, i, j, value) (aset2 name alist i j val)

(assign b (aset1 'demo (@ a) 1 'one))Prints as:cb := Aset1(demo, @a, 1, 'one)

SyntaxTranslationcompress1(name, alist) (compress1 name alist) compress2(name, alist) (compress2 name alist)

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

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)

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

**Example**

(defcong set-equal iff (memb x y) 2 :rule-classes (:rewrite))Does not parsePrints as:Equivalence relation: SET-EQUAL preserves IFF for argument position 2 of MEMB(X, Y) :rule-classes [:REWRITE];

**Example**

(defequiv set-equal :rule-classes (:rewrite))Does not parse.Prints as:Equivalence relation: SET-EQUAL :rule-classes [:REWRITE];

SyntaxTranslationEvaluator (ev, ev-list) (defevaluator ev ev-list [g_1 x_{1}... x_{n1}, ((g_1 x_{1}... x_{n1}) ... ... g_k x_{1}... x_{nk}] (g_k x_{1}... x_{nk})))

(defevaluator evl evl-list ((length x) (member x y)))Does not parsePrints as:Evaluator (evl, evl-list)[length(x), x in y];

**Example**

(defrefinement equiv1 equiv2)Prints as:Refinement EQUIV1 refines EQUIV2;

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

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

(table table-name key-term value-term opterm)

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,:guardterm);