		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 unary predicates over those types; it also generates theorems about the theorems. The user provides information that is specific to the desired predicates, and the macro integrates it into generated boilerplate.

General Form

(defpred suffix
         :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.

: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 variable is <type>.
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 variable is <type>.

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

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.

The details of the predicates are given next.

For each type <type> designated above, 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.

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

Subtopics

Defpred-implementation: Implementation of defpred.