|( name spec )|
Describes the external bindings of a module, introducing a name and a set of specifications. Specifications comprise the following three forms:
( sig-name (arg-name ))
Describes the name and arity of a function. For example, the signature ( f (x y)) can be used to describe:
( f (x y) ( y x))
It can also describe a stub:
( f (x y) )
The names of the arguments is not significant; ( f (x y)) also describes:
( f (a b) ( a b))
The name of the function and number of arguments are significant; ( f (x y)) does not describe:
( g (x y z) )
( 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, ( f=identify ( (f x) x)) describes the following conjecture:
( f=identity ( (f x) x))
A contract may also describe an axiom:
( f=identity ( (f x) x))
The contract’s name and body cannot be changed; ( f=identify ( (f x) x)) does not describe:
( f-is-identity ( x (f x)))
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 :
|( mulop (x y))|
|( (mulop a (mulop b c))|
|(mulop (mulop a b) c))))|
The interface ICommutative includes IAssociative and further constrains mulop to be commutative:
|( (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:
|( addop (x y))|
|( (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 , , and .
|( addall (xs))|
|( mulall (x ys))|
|( ( bs)|
|( (mulop a (addall bs))|
|(addall (mulall a bs))))))|
|( name body )|
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.
( 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:
( IAssociative (mulop times))
( 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.
( IAssociative (mulop ))
The module MDistributive provides an implementation of IDistributive:
|( add (a b) ( a b))|
|( mul (a b) ( a b))|
|( IAssociative (addop add))|
|( ICommutative (addop add))|
|( IDistributive (addop add) (mulop mul)))|
The module MDistributeLists provides an implementation of IDistributeLists for any implementation of IDistributive:
|( IAssociative (addop a))|
|( ICommutative (addop a))|
|( IDistributive (addop a) (mulop m))|
|( add (xs)|
|( ( ( xs))|
|(a ( xs) (add ( xs)))))|
|( mul (x ys)|
|( ( xs)|
|( (m x ( ys)) (mul x ( ys)))))|
|( IDistributeLists (addall add) (mulall mul)))|
|( 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.
( 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.
A complete Modular ACL2 program is a sequence of interfaces, modules (including compound modules), module invocations, and expressions.
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.
|(mulop (addop 1 2) 3)|
|( path )|
Loads all the definitions from each Modular ACL2 file specified by a path into the current file.