Internal representations of symbolic bit vectors.

GL's core symbolic arithmetic functions operate on lists of bfrs, which may be interpreted either as signed or unsigned symbolic integers.

For unsigned bit vectors this is entirely straightforward. We use an LSB-first encoding of the bits, so the car of a BFR list represents the least significant bit of the natural number, a la logcar, whereas the cdr of the BFR represents its more significant bits, a la logcdr.

For signed bit vectors, we use a similar encoding except that we interpret the final bit of the number as the sign bit. So, when working on a signed bit vector, we generally use scdr instead of just cdr.

- Scdr
- Like logcdr for signed bvecs.
- Bfr-list->s
- Signed interpretation of a BFR list under some environment.
- Bfr-eval-list
- Evaluate a list of BFRs, return the list of the (Boolean) results.
- Bfr-scons
- Like logcons for signed bvecs.
- Bfr-ucons
- Like logcons for unsigned bvecs.
- Bfr-list->u
- Unsigned interpretation of a BFR list under some environment.
- Bfr-sterm
- Promote a single BFR into a signed, one-bit bvec, i.e., the resulting value under bfr-list->s is either 0 or -1, depending on the environment.
- Bfr-snorm
- Pbfr-list-depends-on
- V2i
- Convert a (pure constant) signed bvec into an integer.
- N2v
- Convert a natural into a corresponding unsigned bvec (with constant bits).
- V2n
- Convert an unsigned bvec into the corresponding natural.
- S-endp
- Are we at the end of a signed bit vector?
- I2v
- Convert an integer into a corresponding signed bvec (with constant bits).
- First/rest/end
- Deconstruct a signed bit vector.
- Bool->sign
- Interpret a sign bit as an integer: true → -1, false → 0.