Fty
FTY is a macro library for introducing new data types and writing
type-safe programs in ACL2. It automates a systematic discipline for working
with types that allows for both efficient reasoning and execution.
FTY, short for fixtype, is a library for type-safe
programming in ACL2. It provides significant automation for introducing new
data types and using data types according to the ``fixtype discipline.'' Following this discipline allows
you to write type-safe programs that support efficient reasoning (by minimizing
the need for type-related hypotheses) and also have good execution
efficiency.
FTY has been used extensively at Centaur Technology for data structures in
large libraries like ACL2::vl and ACL2::sv.
Here are the major components of FTY, roughly in order from low-level to
high-level utilities:
- deffixtype — Records the associations between type predicates,
fixing functions, and equivalence relations, and can automatically generate
equivalence relations for your types. These associations are used by the
higher-level fty macros.
- basetypes — Sets up the deffixtype associations for many
common ACL2 base types (numbers, symbols, strings, ...).
- deffixequiv and deffixequiv-mutual — Macros that
automate the (otherwise tedious) congruence proofs required for each function
that follows the fixtype discipline.
- defprod, deflist, etc. — Macros for introducing new
simple data types.
- deftypes — Macro for generating mutually recursive data types,
built on top of defprod, (see deflist), etc.
Subtopics
- Deftagsum
- Define a (possibly recursive) tagged union, a.k.a. ``sum of
products'' type.
- Defprod
- Define a new product type, like a struct in C, following the
fty-discipline.
- Defflexsum
- Define a (possibly recursive) sum of products type.
- Defbitstruct
- Define a bitvector type with accessors for its fields.
- Deflist
- Define a list type with a fixing function, supported by deftypes.
- Defalist
- Define an alist type with a fixing function, supported by deftypes.
- Defbyte
- Introduce a fixtype of
unsigned or signed bytes of a specified size.
- Deffixequiv
- A macro for automatically proving boilerplate theorems that show a
function has the appropriate congruences for its typed arguments.
- Defresult
- Introduce a fixtype for good results and error results.
- Deffixtype
- Define a new type for use with the fty-discipline.
- Defoption
- Define an option type.
- Fty-discipline
- The fixtype approach to type-safe programming in ACL2.
- Fold
- Notion of general folds for fixtypes.
- Fty-extensions
- Extensions of FTY in the Kestrel Books.
- Defsubtype
- Introduce a fixtype that
is a subtype of the given fixtype.
- Defset
- Generate a fixtype
of osets
whose elements have a specified fixtype.
- Deftypes
- Generate mutually recursive types with equivalence relations and
fixing functions.
- Specific-types
- Various specific fixtypes.
- Defflatsum
- Introduce a fixtype for
the flat (i.e. not tagged) sum of disjoint fixtypes.
- Deflist-of-len
- Introduce a fixtype of
lists of a specified length.
- Defbytelist
- Introduce a fixtype of
true lists of unsigned or signed bytes of a specified size.
- Fty::basetypes
- A book that associates many built-in ACL2 predicates with
suitable fixing functions and equivalence relations, for use in the fty-discipline.
- Defomap
- Generate a fixtype
of omaps
whose keys and values have specified fixtypes.
- Defvisitors
- Generate visitor functions across types using a visitor template.
- Deffixtype-alias
- Introduce an alias of an existing fixtype.
- Deffixequiv-sk
- A variant of deffixequiv for defun-sk functions.
- Defunit
- Generate a singleton fixtype.
- Multicase
- Macro that allows matching on multiple sum types or enums at once.
- Deffixequiv-mutual
- Like deffixequiv, but for mutually-recursive functions.
- Fty::baselists
- A book that associates various built-in ACL2 list recognizers with
suitable fixing functions and equivalence relations, for use in the fty-discipline.
- Def-enumcase
- Introduce a case macro for an enum type, compatible with multicase
- Defmap
- Define an alist type with a fixing function that drops pairs with malformed keys rather than fixing them.
