• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Defset
      • Specific-types
      • Deftypes
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
      • Defvisitors
      • Defomap
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Fty-extensions
• Fty
• Omaps

Defomap

Generate a fixtype of omaps whose keys and values have specified fixtypes.

Include-book Form

(include-book "kestrel/fty/defomap" :dir :system)

Introduction

This is analogous to deflist, defalist, and defset. Besides the fixtype itself, this macro also generates some theorems about the fixtype. Future versions of this macro may generate more theorems, as needed.

Aside from the recognizer, fixer, and equivalence for the fixtype, this macro does not generate any operations on the typed omaps. Instead, the generic omap operations can be used on typed omaps. This macro generates theorems about the use of these generic operations on typed omaps.

Future versions of this macro may be modularized to provide a ``sub-macro'' that generates only the recognizer and theorems about it, without the fixtype (and without the fixer and equivalence), similarly to std::deflist and std::defalist. That sub-macro could be called omap::defomap.

This macro differs from defmap, which generates an alist.

General Form

(defomap type
         :key-type ...
         :val-type ...
         :pred ...
         :fix ...
         :equiv ...
         :parents ...
         :short ...
         :long ...

Inputs

type

The name of the new fixtype.

:key-type

The (existing) fixtype of the keys of the new map fixtype.

:val-type

The (existing) fixtype of the values of the new map fixtype.

:pred
:fix
:equiv

The name of the recognizer, fixer, and equivalence for the new fixtype.

The defaults are type followed by -p, -fix, and -equiv.

:parents
:short
:long

These are used to generate XDOC documentation for the topic name.

If any of these is not supplied, the corresponding component is omitted from the generated XDOC topic.

This macro currently does not perform a thorough validation of its inputs. Erroneous inputs may result in failures of the generated events. Errors should be easy to diagnose, also since this macro has a very simple and readable implementation. Future versions of this macro should perform more thorough input validation.

Generated Events

The following are generated, inclusive of XDOC documentation:

• The recognizer, the fixer, the equivalence, and the fixtype.
• Several theorems about the recognizer, fixer, equivalence, and omap operations applied to this type of omaps.