Modular ACL2

_Modular ACL2_

Modular ACL2 is a (currently experimental) language that introduces interfaces
and modules to ACL2 programs.  Top level forms may be interface or module
definitions, module invocations, or expressions.  Definitions and expressions
within modules and interfaces are as in the Dracula language.

------------------------------------------------------------

> (interface NAME (sig FUN (ARG ...)) ... (con THM EXPR) ...)

Interface definitions provide a name, signatures (name and arguments) for
functions, and contracts (name and expression) representing properties of those
functions.

Example:

;; The closed-function-ifc declared a predicate 'pred' and a function 'f'
;; such that f is closed over the set of values satisfying pred.
(interface closed-function-ifc
  (sig pred (x))
  (sig f (x))
  (con f-closed-over-pred
    (implies (pred x) (pred (f x)))))

------------------------------------------------------------

> (module NAME IMPORTS EXPORTS SHARING DEF ... ASSIGN)
  where IMPORTS = (import (TAG : IFC) ...)
   and  EXPORTS = (export (TAG : IFC) ...)
   and  SHARING = (sharing (NAME ...) ...)
   and  ASSIGN = (assign (TAG (FUN <- NAME) ...) ...)

Primitive module definitions provide a name, external description (imports,
exports, and sharing), and internal implementation (definitions and assignment
clauses) for a module.

The IMPORTS clause declares interfaces imported by the module and assigns a tag
to each.  The names (of signatures and contracts) from the interface are
prefixed with the tag, so the name f from an interface tagged I is I.f from
within the module.  The module implementer may assume that the interface's
signatures correspond to functions satisfying the appropriate contracts.

The EXPORTS clause declares interfaces exported by the module.  Names are
tagged similarly to imports for purposes of the module's external description
(see SHARING clause below).  The tags for imported and exported modules must
all be unique.

The SHARING clause declares signatures from multiple interfaces that describe
the same function; the implementation of these functions must arise from a
single definition.  This is useful for importing or exporting a single function
known to satisfy the contracts of multiple interfaces.  Names in the sharing
clauses, whether from imports or exports, use tagged names.

The DEFs represent standard Dracula definitions (defun, defthm, etc.) within
the module.  Each module lives in a separate namespace, so multiple modules may
declare functions or theorems (internally) by the same name without clashing.

The ASSIGN clause declares the internal function names exported for each of the
module's exports.  Each subclause starts with a tag, and proceeds to name the
external (untagged) and internal name for each exported function.  The internal
names may be internal definitions, imported names, or ACL2 primitives.

Examples:

;; This module has no imports.  It provides the closed function interface with
;; tag DOUBLE, providing integerp for the predicate and a function that doubles
;; its input for the function f.
;; The contracts of closed-function-ifc require double to be closed over
;; integerp, which ACL2 will attempt to verify when the module is submitted.
(module double-closed-over-integerp
  (import)
  (export (DOUBLE : closed-function-ifc))
  (sharing)

  (defun double (x) (+ x x))

  (assign (DOUBLE (pred <- integerp) (f <- double))))

;; This module imports two closed functions (tagged A and B) and exports
;; another (tagged AB).
;; According to the sharing clause, A, B, and AB all share the function pred.
;; Writing (sharing (A.pred B.pred AB.pred)) would have been equivalent.
;; The body of the module defines composed, which composes f from A with f from
;; B, and exports the imported predicate as AB.pred and composed as AB.f.
;; The module system will verify that AB.pred is provided from one of the
;; imports, and ACL2 will attempt to verify that the function composed is
;; closed over that predicate.
(module compose-closed-functions
  (import (A : closed-function-ifc)
          (B : closed-function-ifc))
  (export (AB : closed-function-ifc))
  (sharing (A.pred B.pred) (AB.pred A.pred))

  (defun composed (x) (A.f (B.f x)))

  (assign (AB (pred <- B.pred) (f <- composed))))

------------------------------------------------------------

> (compound NAME IMPORTS EXPORTS SHARING (link (TAG ...) <- MOD (ARG ...)))
  where IMPORTS = (import (TAG : IFC) ...)
   and  EXPORTS = (export (TAG : IFC) ...)
   and  SHARING = (sharing (NAME ...) ...)

Compound modules declared a name, imported interfaces, exported interfaces, and
sharing declarations just as for primitive modules.  Their body defines a
sequence of linked modules.  Each linked module takes its imports from each
ARG, which must be taken from imported tags or prior linked tags, and
correspond to the imported tags from MOD in order (not by name).  The exported
tags from MOD (again by order) are assigned to each TAG for use below.  The
compound module's final exports are taken from the TAGs (this time by name,
exporting only those declared in the EXPORTS clause).

Example:

;; This module links double-closed-over-integerp (vacuously), providing no
;; imports and naming its single export DOUBLE.  It then provides DOUBLE as
;; both imports of compose-closed-functions, naming the resulting export as
;; QUADRUPLE, since composing DOUBLE.f with itself results in a function that
;; quadruples its argument.
;; Because compose-closed-functions requires that its arguments share their
;; predicate, the module system will verify that DOUBLE.pred is the same as
;; DOUBLE.pred (which it obviously is).
;; ACL2 will not have any new verification obligations from this compound
;; module, as double-closed-over-integerp and compose-closed-functions have
;; already been verified.
(compound quadruple-closed-over-integerp
  (import)
  (export (QUADRUPLE : closed-function-ifc))
  (sharing)

  (link (DOUBLE) <- double-closed-over-integerp ())
  (link (QUADRUPLE) <- compose-closed-functions (DOUBLE DOUBLE)))

------------------------------------------------------------

> (invoke MOD)

Invokes a module of no imports, defining its exported functions at the top
level by their external names.

Example:

;; Invokes the compound module quadruple-closed-over-integerp, defining the
;; functions QUADRUPLE.pred and QUADRUPLE.f at the top level.
(invoke quadruple-closed-over-integerp)

(QUADRUPLE.f 2) ;; should produce 8