		Search-engine friendly clone of the ACL2 documentation.

Rlp-error

Rlp-error-case

Case macro for the different kinds of rlp-error structures.

This is an ACL2::fty sum-type case macro, typically introduced by fty::defflexsum or fty::deftagsum. It allows you to safely check the type of a rlp-error structure, or to split into cases based on its type.

Short Form

In its short form, rlp-error-case allows you to safely check the type of a rlp-error structure. For example:

(rlp-error-case x :no-bytes)

is essentially just a safer alternative to writing:

(equal (rlp-error-kind x) :no-bytes)

Why is using rlp-error-case safer? When we directly inspect the kind with equal, there is no static checking being done to ensure that, e.g., :no-bytes is a valid kind of rlp-error structure. That means there is nothing to save you if, later, you change the kind keyword for this type from :no-bytes to something else. It also means you get no help if you just make a typo when writing the :no-bytes symbol. Over the course of developing VL, we found that such issues were very frequent sources of errors!

Long Form

In its longer form, rlp-error-case allows you to split into cases based on the kind of structure you are looking at. A typical example would be:

(rlp-error-case x
  :no-bytes ...
  :fewer-bytes-than-short-length ...
  :fewer-bytes-than-length-of-length ...
  :fewer-bytes-than-long-length ...
  :leading-zeros-in-long-length ...
  :non-optimal-short-length ...
  :non-optimal-long-length ...
  :subtree ...
  :extra-bytes ...
  :branch-tree ...
  :leading-zeros-in-scalar ...)

It is also possible to consolidate ``uninteresting'' cases using :otherwise.

For convenience, the case macro automatically binds the fields of x for you, as appropriate for each case. That is, in the :no-bytes case, you can use fty::defprod-style foo.bar style accessors for x without having to explicitly add a no-bytes b* binder.