		Search-engine friendly clone of the ACL2 documentation.

Syntax-for-tools

Defpred

Generate predicates over the C abstract syntax for tools, along with theorems about the predicates.

Introduction

The C abstract syntax for tools consists of a large collection of (fix)types. This macro automates the creation of predicates over those types; it also generates theorems about the predicates. The user provides information that is specific to the desired predicates, and the macro integrates it into generated boilerplate. The predicates may be unary, i.e. operating over the abstract syntax constructs only, or there may be extra arguments, which are passed through recursively.

General Form

(defpred suffix
         :extra-args ...  ; default nil
         :default    ...  ; no default
         :override   ...  ; default nil
         :parents    ...  ; no default
         :short      ...  ; no default
         :long       ...  ; no default
  )

Inputs

suffix

Suffix for the generated predicate names. The name of each generated predicate is <type>-<suffix>, where <type> is the type that the predicate operates on, and <suffix> is the value of this input, which must be a symbol. The predicate name is interned in the same package as <suffix>.
This input should generally terminate in p, according to the ACL2 predicate naming convention. For instance, if this input is goodp, then the predicate generated for expressions, whose type is expr, is expr-goodp.

:extra-args — default nil

Extra arguments of the predicates, which are passed unchanged to the recursively calls.
This must be a list of extended formals which defpred puts into the generated defines.

:default — no default

Default result of the predicates, used as described in the Section `Generated Events' below.
This must be a boolean, either t or nil.

:override — default nil

Specifies which boilerplate results should be overridden. It is used as described in the Section `Generated Events' below.
This must be a parenthesized list (ovrd1 ... ovrd<n>), with <n> >= 0, where each ovrd<i> has one of two possible forms:
A pair (<type> <term>), where <type> is a fty::defprod or fty::deftagsum of the abstract syntax (e.g. tyname or expr), and <term> is an (untranslated) term whose only free variables may be <type> and the formals specified in :extra-args.
A triple (<type> <kind> <term>), where <type> is a fty::deftagsum of the abstract syntax (e.g. expr), <kind> is a keyword identifying one of the summands of the type, and <term> is an (untranslated) term whose only free variables may be <type> and the formals specified in :extra-args.

:parents
:short
:long

These, if present, are added to the generated XDOC topic described in the Section `Generated Events' below.

Generated Events

abstract-syntax-<suffix>

An XDOC topic whose name is obtained by adding, at the end of the symbol abstract-syntax-, the symbol specified in the suffix input. If any of the :parents, :short, or :long inputs are provided, they are added to this XDOC topic. This XDOC topic is generated with defxdoc+, with :order-topics t, so that the other generated events (described below), which all have this XDOC topic as parent, are listed in order as subtopics.

For each type <type> designated in the `Types for Which Predicates Are Generated' below, a predicate over the type, defined as follows:
If <type> is a fty::defprod:
If the :override input includes an element (<type> <term>), the predicate is defined to return <term>.
If the :override input does not include any element of the form (<type> <term>), the predicate is defined to return the conjuntion of the predicates generated for the fields' types applied to the respective fields. It is always the case that at least one field has a type for which a predicate is generated.
If <type> is a fty::deftagsum:
If the :override input includes an element (<type> <term>), the predicate is defined to return <term>.
Otherwise, the predicate is defined via <type>-case, and the case for each keyword <kind> is as follows:
If the :override input includes an element (<type> <kind> <term>), the case is defined to return <term>.
If the :override input does not include any element of the form (<type> <kind> <term>):
If the summand corresponding to <kind> has no fields of a type for which a predicate is generated, the case is defined to return the boolean specified by the :default input.
If the summand corresponding to <kind> has at least one field of a type for which a predicate is generated, the case is defined to return the conjuntion of the predicates generated for the fields' types applied to the respective fields of the summand.
If <type> is a fty::deflist, the predicate is defined recursively, as the conjunction of the predicate generated for the element type applied to each element of the list; the conjunction is t if the list is empty.
If <type> is a fty::defoption, the predicate is defined to return t on nil, and the predicate generated for the based type on non-nil.
If <type> is a fty::defomap, which is only the case for filepath-transunit-map, the predicate is defined recursively, as the conjunction of the predicate generated for the value type applied to each value of the map; the conjunction is t if the map is empty.

Accompanying list type theorems.

For each list type designated in the `Types for Which Predicates Are Generated' below, we generate a std::deflist for the predicates, which automatically generates theorems. The enablement of these theorems is determined by std::deflist; currently defpred does not modify that for any of those theorems.

Accompanying omap type theorems.

For each omap type <type> designated in the `Types for Which Predicates Are Generated' below, whose value type <valtype> is also designated there, but whose key type <keytype> is not, we generate the following theorems, whose exact form can be inspected with pe or similar command:
<type>-<suffix>-when-emptyp
<type>-<suffix>-of-update
<valtype>-<suffix>-of-head-when-<type>-<suffix>.
<type>-<suffix>-of-tail
These theorems are all disabled, and added to the generated ruleset described below.

abstract-syntax-<suffix>-rules

A ruleset with the theorems that accompany the predicates, except for the ones that accompany the list type predicates.

The theorems that accompany the predicates are generated as part of the define and defines that define the predicates, after the ///.

Types for Which Predicates Are Generated

A predicate is generated for the following types of the abstract syntax:

All the types in the mutually recursive clique exprs/decls/stmts.
The types type-spec-list, expr/tyname, declor/absdeclor, decl/stmt, fundef, fundef-option, extdecl, extdecl-list, transunit, filepath-transunit-map, and transunit-ensemble.

Subtopics

Defpred-implementation: Implementation of defpred.