3 Modular ACL2

This section defines the Modular ACL2 language provided by Dracula. For a gentler introduction, see (part ("(planet guide.scrbl (cce dracula.plt 8 1) guide)" "modular")) in (part ("(planet guide.scrbl (cce dracula.plt 8 1) guide)" "top")).

3.1 Interfaces

(interface name spec ...)

spec   =   (sig sig-name (arg-name ...))     |   (sig sig-name (arg-name ...) (res-name ...))     |   (con con-name expr)     |   (include ifc-name)

Describes the external bindings of a module, introducing a name and a set of specifications. Specifications comprise the following three forms:

(sig sig-name (arg-name ...))

(sig sig-name (arg-name ...) (res-name ...))

Describes the name, arity, and (optionally) multiple return values of a function. For example, the signature (sig f (x y)) can be used to describe:

  (defun f (x y) (cons y x))

It can also describe a stub:

  (defstub f (x y) t)

The names of the arguments is not significant; (sig f (x y)) also describes:

  (defun f (a b) (cons a b))

The name of the function and number of arguments are significant; (sig f (x y)) does not describe:

  (defstub g (x y z) t)

Signatures may also describe functions/stubs with multiple return values. The signature (sig f (a b) (c d)) describes the function:

  (defun f (x y) (mv x y))

and the signature:

  (defstub f (x y) (mv x y))

(con con-name body-expr)

Describes a logical contract with the given name and body. The body of a contract may refer to ACL2 primitives, as well as signatures within the same interface or any included interface.

For example, (con f=identify (equal (f x) x)) describes the following conjecture:

  (defthm f=identity (equal (f x) x))

A contract may also describe an axiom:

  (defaxiom f=identity (equal (f x) x))

The contract’s name and body cannot be changed; (con f=identify (equal (f x) x)) does not describe:

  (defthm f-is-identity (equal x (f x)))

(include ifc-name)

Imports one interface into another. It may refer to any previously-defined interface. Contracts following the include may refer to signatures from the included interface.

Include specifications also entail an obligation; if interface C includes B and B includes A, then C must include A as well. This obligation may be relaxed in the future, so that including B will automatically include A.

For example, the interface IAssociative contains a signature describing a binary function and a contract constraining it to be associative. The contract mulop-associative refers to the signature mulop as well as the built-in ACL2 function equal:

(interface IAssociative

(sig mulop (x y))

(con mulop-associative

(equal (mulop a (mulop b c))

(mulop (mulop a b) c))))

The interface ICommutative includes IAssociative and further constrains mulop to be commutative:

(interface ICommutative

(include IAssociative)

(con mulop-commutative

(equal (mulop a b) (mulop b a))))

The interface IDistributive includes ICommutative, introduces a new function addop, and states a contract that mulop distributes over addop. Note that IDistributive must also include IAssociative to satisfy the obligation from ICommutative:

(interface IDistributive

(include IAssociative)

(include ICommutative)

(sig addop (x y))

(con addop/mulop-distributive

(equal (mulop a (addop b c))

(addop (mulop a b) (mulop a c)))))

The interface IDistributeLists extends IDistributive with functions that perform addop and mulop on lists. Its contract addall/mulall-distributive refers to its own signatures, the imported signatures mulop and addop, and the built-in functions equal, implies, and proper-consp.

(module IDistributeLists

(include IAssociative)

(include ICommutative)

(include IDistributive)

(sig addall (xs))

(sig mulall (x ys))

(con addall/mulall-distributive

(implies (proper-consp bs)

(equal (mulop a (addall bs))

(addall (mulall a bs))))))

3.2 Modules

(module name body ...)

body   =   def     |   expr     |   (import ifc-name (ext-name int-name) ...)     |   (export ifc-name (ext-name int-name) ...)

Defines a composable, verifiable program fragment, introducing a name and a set of body forms. Forms may be definitions, expressions, import declarations, or export declarations.

(import ifc-name (ext-name int-name) ...)

Makes the bindings of any previously defined interface available inside a module. The module may use signatures as function names and rely on contracts as axioms. If an imported interface includes any other interfaces, the module must import them as well.

An import declaration may optionally bind some or all of the interface’s external names to different internal names inside the module. For instance, the following import declaration binds mulop from IAssociative to times:

  (import IAssociative (mulop times))

(export ifc-name (ext-name int-name) ...)

Makes the implementation of a previously defined interface available to clients of a module. The module must provide a definition (internal, imported, or ACL2 built-in) for each signature in the interface; these definitions must satisfy the interface’s contracts. If the interface includes other interfaces, the module must either import or export them as well.

The export declaration may supply definitions whose internal names differ from their external signaturse. For instance, the following export declaration provides the builtin ACL2 function * as mulop to implement IAssociative.

  (export IAssociative (mulop *))

The module MDistributive provides an implementation of IDistributive:

(module MDistributive

(defun add (a b) (+ a b))

(defun mul (a b) (* a b))

(export IAssociative (addop add))

(export ICommutative (addop add))

(export IDistributive (addop add) (mulop mul)))

The module MDistributeLists provides an implementation of IDistributeLists for any implementation of IDistributive:

(module MDistributive

(import IAssociative (addop a))

(import ICommutative (addop a))

(import IDistributive (addop a) (mulop m))

(defun add (xs)

(if (endp (cdr xs))

(car xs)

(a (car xs) (add (cdr xs)))))

(defun mul (x ys)

(if (endp xs)

nil

(cons (m x (car ys)) (mul x (cdr ys)))))

(export IDistributeLists (addall add) (mulall mul)))

(link name mod-name ...)

Creates a composable program fragment by joining together multiple modules. External names are resolved to link one module’s imports to another’s exports; the export must come before the import to prevent cyclic dependencies. Internal names are kept separate; lexical scope is not violated.

  (link MDist MDistributive MDistributeLists)

The compound module MDist links together MDistributive with MDistributeLists. The result is a module that exports both IDistributive and IDistributeLists. It has no imports; the import of MDistributeLists is resolved to the export of MDistributive. Despite the duplicate definitions of add and mul in the component modules, there are no name clashes in MDist; addop and mulop are based on the functions from MDistributive, while addall and mulall are based on the functions from MDistributeLists.

3.3 Programs

A complete Modular ACL2 program is a sequence of interfaces, modules (including compound modules), module invocations, and expressions.

(invoke mod-name)

Makes the exported bindings of a fully-linked module available at the top level of a program. The invocation of MDist defines addop, mulop, addall, and mulall.

(invoke MDist)

(mulop (addop 1 2) 3)

(require path ...)

Loads all the definitions from each Modular ACL2 file specified by a path into the current file.