Simplified shape specifiers for

The

(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

(: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

The

The

The

(: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