		Search-engine friendly clone of the ACL2 documentation.

Auto-bindings

Simplified shape specifiers for :g-bindings.

The auto-bindings function lets you create simple shape-specs in an easy way. Here is an example:

(def-gl-thm foo
  ...
  :g-bindings (auto-bindings                          ; expands to:
               (:nat opcode 8)                        ; g-integer with indices 0-8
               (:int multiplier 16)                   ; g-integer with indices 9-25
               (:bool enable)                         ; g-boolean with index 26
               (:mix (:nat a-bus 128)                 ; }  g-integers whose indices are interleaved,
                     (:nat b-bus 128)                 ; }  27 to 414 -- see below
                     (:rev (:seq (:nat c-bus 64)      ; } 
                                 (:skip 64))))   ; }
               (:rev (:nat fixup-bits 4))       ; g-integer with indices 420-415
               ))

This is good because

you don't have to think about sign bits and do a bunch of stupid arithmetic to figure out the next free index, and
you can painlessly extend the bindings when you want to add a new variable without having to update a bunch of indices.

Auto-bindings are more limited than shape-specs. Except for the special :mix command, you can only write:

(:bool var)  -- expands to a g-boolean shape-specifier
(:int var n) -- expands to a g-integer with n bits (signed 2's complement)
(:nat var n) -- equivalent to (:int var (+ 1 n))
(:skip n)    -- takes up space in a :mix, but doesn't generate bindings.

The :rev command reverses the order of the bits produced by directives inside it.

The :mix command interleaves the bits of the elements inside it. Currently we only allow mix to contain elements that are all the same size.

The :seq and :mix commands can be nested to produce complicated interleavings.

The :skip command can be used to pad out a :mix command so as to interleave a shorter variable with part of a longer variable. E.g.:

(:mix (:int a 7)
      (:seq (:int b 4) (:skip 3)))

produces

((A (:G-INTEGER 0 2 4 6 8 9 10))
 (B (:G-INTEGER 1 3 5 7)))

That is, the first part of a is mixed with b but once the bits of b run out, the rest of the bits of a are simply in sequence.