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 ``

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.

- 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. - Deffixtype
- Define a new type for use with the fty-discipline.
- Defresult
- Introduce a fixtype for good and error results.
- Deffixequiv
- A macro for automatically proving boilerplate theorems that show a function has the appropriate congruences for its typed arguments.
- Fty-discipline
- The fixtype approach to type-safe programming in ACL2.
- Defoption
- Define an option type.
- Defsubtype
- Introduce a
fixtype that is a subtype of the given fixtype. - Fty-extensions
- Extensions of FTY in the Kestrel Books.
- Deftypes
- Generate mutually recursive types with equivalence relations and fixing functions.
- 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. - Defset
- Generate a
fixtype of osets whose elements have a specified fixtype. - Fty::basetypes
- A book that associates many built-in ACL2 predicates with suitable fixing functions and equivalence relations, for use in the fty-discipline.
- Defvisitors
- Generate visitor functions across types using a visitor template.
- Deffixtype-alias
- Introduce an alias of an existing fixtype.
- Specific-types
- Various specific fixtypes.
- Defomap
- Generate a
fixtype of omaps whose keys and values have specified fixtypes. - Deffixequiv-sk
- A variant of
`deffixequiv`for`defun-sk`functions. - Defunit
- Generate a singleton fixtype.
- 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.
- Defmap
- Define an alist type with a fixing function that drops pairs with malformed keys rather than fixing them.