auto-bindings

(in-package "GL")

(include-book "gobject-types")

(include-book "../misc/numlist")

(include-book "std/util/bstar" :dir :system)

(program)

(defxdoc auto-bindings
  :parents (reference shape-specs)
  :short "Simplified shape specifiers for @(':g-bindings')."
  :long "<p>The @('auto-bindings') function lets you create simple @(see
shape-specs) in an easy way.  Here is an example:</p>

@({
 (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
                ))
})

<p>This is good because</p>

<ul>

<li>you don't have to think about sign bits and do a bunch of stupid arithmetic
to figure out the next free index, and</li>

<li>you can painlessly extend the bindings when you want to add a new variable
without having to update a bunch of indices.</li>

</ul>

<p>Auto-bindings are more limited than shape-specs.  Except for the special
@(':mix') command, you can only write:</p>

@({
    (: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.
})

<p>The @(':rev') command reverses the order of the bits produced by directives inside it.</p>

<p>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.</p>

<p>The @(':seq') and @(':mix') commands can be nested to produce complicated
interleavings.</p>

<p>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.:</p>
@({
 (:mix (:int a 7)
       (:seq (:int b 4) (:skip 3)))
 })
<p>produces</p>
@({
 ((A (:G-INTEGER 0 2 4 6 8 9 10))
  (B (:G-INTEGER 1 3 5 7)))
 })
<p>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.</p>
")

(defxdoc flex-bindings
  :parents (reference shape-specs)
  :short "Shape specifiers for @(':g-bindings'), more flexible than @(see auto-bindings)."
  :long "<p>The @('flex-bindings') function lets you create somewhat more
complicated @(see shape-specs) than is possible with @(see auto-bindings).  We
assume familiarity with @(see auto-bindings) in this documentation.  The
specific feature @('flex-bindings') offers that auto-bindings does not is the
ability to split an integer variable into segments and generate indices for
each segment independently.</p>

@({
 (def-gl-thm foo
   ...
   :g-bindings (flex-bindings                          ; expands to:
                 ;; auto-bindings list -- generates indices
                 ((:int a1 10)
                  (:rev (:mix (:int a2 13)
                              (:int b1 13)))
                  (:int b2 10))
                 :arrange         ;; generate shape spec bindings from the indices
                 ((:int a a1 a2)  ;; a is a g-integer, indices are a1's appended to a2's
                  (:int b b1 b2)))) 
})

<p>The first argument is just a list of auto-bindings (though the syntax
differs trivially in that flex-bindings takes them in a single argument whereas
@(see auto-bindings) uses @('&rest args')).  They are used to generate indices,
but not the actual g-bindings.  We generate from these a mapping from each
variable name to its list of indices.</p>

<p>The @(':arrange') argument, if provided, must be a list consisting of the
following sorts of forms: </p>

<ul>
<li>@('(:int a b c ...)') means generate an integer shape-spec binding for
variable @('a'), consisting of the appended indices of @('b'), @('c'), etc.,
from the auto-bindings form.</li>
<li>@('(:int a)') means generate an integer shape-spec binding for variable
@('a') using the indices of @('a') from the auto-bindings form.</li>
<li>@('(:bool a)') means generate a Boolean binding for variable @('a'),
using the index of @('a') from the auto-bindings form.</li>
<li>@('(:bool a b)') means generate a Boolean binding for variable @('a'),
using the index of @('b') from the auto-bindings form.</li>
</ul>

<p>If the @(':arrange') argument is not provided, @(see flex-bindings) acts
just like @(see auto-bindings) -- it generates an entry for each variable
mentioned in the auto-bindings.</p>")

(defun ab-sum
  (x)
  (if (atom x)
    0
    (+ (car x) (ab-sum (cdr x)))))

(defun ab-all-equal
  (x val)
  (if (atom x)
    t
    (and (equal (car x) val)
      (ab-all-equal (cdr x) val))))

(mutual-recursion (defun auto-bind-len
    (x)
    (case (first x)
      (:bool 1)
      (:int (third x))
      (:rev (auto-bind-len (cadr x)))
      (:skip (second x))
      (t (ab-sum (auto-bind-len-list (cdr x))))))
  (defun auto-bind-len-list
    (x)
    (if (atom x)
      nil
      (cons (auto-bind-len (car x))
        (auto-bind-len-list (cdr x))))))

(mutual-recursion (defun auto-bind-xlate
    (x inside-mix-p)
    (if (not (true-listp x))
      (er hard?
        'auto-bind-xlate
        "Auto-binding not even a true-listp: ~x0"
        x)
      (case (first x)
        (:bool (cond (inside-mix-p (er hard?
                'auto-bind-xlate
                "Auto-bindings of :bool aren't allowed directly inside mix: ~x0"
                x))
            ((and (= (len x) 2) (legal-variablep (second x))) (list :bool (second x) 1))
            (t (er hard?
                'auto-bind-xlate
                "Auto-binding is invalid: ~x0"
                x))))
        ((:nat :int) (if (and (= (len x) 3)
              (legal-variablep (second x))
              (natp (third x)))
            (list :int (second x)
              (if (eq (first x) :nat)
                (+ 1 (third x))
                (third x)))
            (er hard?
              'auto-bind-xlate
              "Auto-binding is invalid: ~x0"
              x)))
        (:mix (b* (((unless (<= 3 (len x))) (er hard?
                 "Auto-binding is invalid: mix with too few elements: ~x0"
                 x)) (elems (auto-bind-xlate-list (cdr x) t))
              (lens (auto-bind-len-list elems))
              ((unless (ab-all-equal (cdr lens) (car lens))) (er hard?
                  'auto-bind-xlate
                  "Lengths inside :mix must agree: ~x0 has lengths ~x1"
                  elems
                  lens)))
            (cons :mix elems)))
        (:seq (cons :seq (auto-bind-xlate-list (cdr x) nil)))
        (:rev (cond ((= (len x) 2) (list :rev (auto-bind-xlate (cadr x) inside-mix-p)))
            (t (er hard?
                'auto-bind-xlate
                "Auto-binding is invalid: ~x0"
                x))))
        (:skip (if (and (= (len x) 2) (natp (second x)))
            x
            (er hard?
              'auto-bind-xlate
              "Auto-binding is invalid: ~x0"
              x)))
        (otherwise (er hard?
            'auto-bind-xlate
            "Auto-binding has unrecognized type: ~x0"
            x)))))
  (defun auto-bind-xlate-list
    (x inside-mix-p)
    (if (atom x)
      nil
      (cons (auto-bind-xlate (car x) inside-mix-p)
        (auto-bind-xlate-list (cdr x) inside-mix-p)))))

(mutual-recursion (defun auto-bind-generate
    (x free-idx by)
    (case (car x)
      ((:bool :int) (b* (((list type var len) x))
          (list (cons var
              (if (eq type :bool)
                (list free-idx)
                (numlist free-idx by len))))))
      (:rev (let ((len (auto-bind-len (cadr x))))
          (auto-bind-generate (cadr x)
            (+ free-idx (* by (1- len)))
            (- by))))
      (:mix (auto-bind-generate-mix (cdr x)
          free-idx
          by
          (* by (len (cdr x)))))
      (:seq (auto-bind-generate-seq (cdr x) free-idx by))
      (:skip nil)
      (otherwise (er hard?
          'auto-bind-generate
          "Should never happen: not translated: ~x0"
          x))))
  (defun auto-bind-generate-mix
    (x free-idx interleave-by inner-by)
    (if (atom x)
      nil
      (append (auto-bind-generate (car x)
          free-idx
          inner-by)
        (auto-bind-generate-mix (cdr x)
          (+ free-idx interleave-by)
          interleave-by
          inner-by))))
  (defun auto-bind-generate-seq
    (x free-idx by)
    (if (atom x)
      nil
      (append (auto-bind-generate (car x) free-idx by)
        (auto-bind-generate-seq (cdr x)
          (+ (* by (auto-bind-len (car x))) free-idx)
          by)))))

(mutual-recursion (defun auto-bind-skips
    (x free-idx by)
    (case (car x)
      ((:bool :int) nil)
      (:rev (let ((len (auto-bind-len (cadr x))))
          (auto-bind-skips (cadr x)
            (+ free-idx (* by (1- len)))
            (- by))))
      (:mix (auto-bind-skips-mix (cdr x)
          free-idx
          by
          (* by (len (cdr x)))))
      (:seq (auto-bind-skips-seq (cdr x) free-idx by))
      (:skip (numlist free-idx by (cadr x)))
      (otherwise (er hard?
          'auto-bind-generate
          "Should never happen: not translated: ~x0"
          x))))
  (defun auto-bind-skips-mix
    (x free-idx interleave-by inner-by)
    (if (atom x)
      nil
      (append (auto-bind-skips (car x) free-idx inner-by)
        (auto-bind-skips-mix (cdr x)
          (+ free-idx interleave-by)
          interleave-by
          inner-by))))
  (defun auto-bind-skips-seq
    (x free-idx by)
    (if (atom x)
      nil
      (append (auto-bind-skips (car x) free-idx by)
        (auto-bind-skips-seq (cdr x)
          (+ (* by (auto-bind-len (car x))) free-idx)
          by)))))

(defun auto-bind-index-map
  (n skiptable len offset acc)
  (if (mbe :logic (zp (- (nfix len) (nfix n)))
      :exec (eql n len))
    acc
    (if (hons-get n skiptable)
      (auto-bind-index-map (1+ (lnfix n))
        skiptable
        len
        (1+ offset)
        acc)
      (auto-bind-index-map (1+ (lnfix n))
        skiptable
        len
        offset
        (hons-acons n (- n offset) acc)))))

(defun auto-bind-remap-indices-list
  (x indexmap)
  (b* (((when (atom x)) nil) (look (hons-get (car x) indexmap))
      ((unless look) (er hard?
          'auto-bind-remap-index-list
          "Auto-bindings programming error: skipped index is present in auto-bindings")))
    (cons (cdr look)
      (auto-bind-remap-indices-list (cdr x) indexmap))))

(defun auto-bind-remap-indices-table
  (x indexmap)
  (if (atom x)
    nil
    (cons (cons (caar x)
        (auto-bind-remap-indices-list (cdar x) indexmap))
      (auto-bind-remap-indices-table (cdr x) indexmap))))

(defun flex-bindings-append-auto-vars
  (vars auto-alist)
  (if (atom vars)
    nil
    (append (b* ((auto-look (assoc (car vars) auto-alist)) ((unless auto-look) (er hard?
              'flex-bindings-arrange
              "Missing auto-binding for ~x0"
              (car vars))))
        (cdr auto-look))
      (flex-bindings-append-auto-vars (cdr vars)
        auto-alist))))

(defun flex-bindings-arrange1
  (x auto-alist)
  (b* (((when (atom x)) (er hard?
         'flex-bindings-arrange
         "Invalid arrange-list entry: ~x0"
         x)) ((cons key args) x)
      ((unless (and (consp args)
           (symbol-listp args)
           (not (member nil args)))) (er hard?
          'flex-bindings-arrange
          "Invalid arrange-list entry: ~x0 -- args must be a ~
                        nonempty list of nonnil symbols"
          x)))
    (case key
      (:bool (b* ((len (len args)) ((unless (or (eql len 1) (eql len 2))) (er hard?
                'flex-bindings-arrange
                "Invalid arrange-list entry: ~x0"
                x))
            (varname (first args))
            (autoname (if (eql len 2)
                (second args)
                (first args)))
            (auto-look (assoc autoname auto-alist))
            ((unless auto-look) (er hard?
                'flex-bindings-arrange
                "Missing auto-binding for ~x0"
                autoname))
            (indices (cdr auto-look))
            ((unless (eql (len indices) 1)) (er hard?
                'flex-bindings-arrange
                "Boolean ~x0 assigned to wide auto-binding variable ~x1"
                varname
                autoname)))
          (list varname (g-boolean (car indices)))))
      (:int (b* ((len (len args)) (varname (car args))
            (auto-vars (if (eql len 1)
                args
                (cdr args))))
          (list varname
            (g-integer (flex-bindings-append-auto-vars auto-vars
                auto-alist)))))
      (otherwise (er hard?
          'flex-bindings-arrange
          "Invalid arrange-list entry: ~x0 -- must begin with :bool or :int.")))))

(defun flex-bindings-arrange
  (arrange-list auto-alist)
  (if (atom arrange-list)
    nil
    (cons (flex-bindings-arrange1 (car arrange-list)
        auto-alist)
      (flex-bindings-arrange (cdr arrange-list)
        auto-alist))))

(mutual-recursion (defun auto-bindings-collect-arrange
    (x)
    (case (car x)
      ((:bool :int) (b* (((list type var) x))
          (list (list type var))))
      (:skip nil)
      (otherwise (auto-bindings-list-collect-arrange (cdr x)))))
  (defun auto-bindings-list-collect-arrange
    (x)
    (if (atom x)
      nil
      (append (auto-bindings-collect-arrange (car x))
        (auto-bindings-list-collect-arrange (cdr x))))))

(defun flex-bindings-fn
  (auto-bindings arrange-list start)
  (b* ((xlated-bindings (auto-bind-xlate-list auto-bindings nil)) (auto-alist (auto-bind-generate-seq xlated-bindings start 1))
      (skips (auto-bind-skips-seq xlated-bindings start 1))
      (skiptable (make-fast-alist (pairlis$ skips nil)))
      (indexmap (auto-bind-index-map 0
          skiptable
          (ab-sum (auto-bind-len-list xlated-bindings))
          0
          nil))
      (auto-alist-remapped (auto-bind-remap-indices-table auto-alist
          indexmap))
      (arrange-list (or arrange-list
          (auto-bindings-list-collect-arrange xlated-bindings))))
    (flex-bindings-arrange arrange-list
      auto-alist-remapped)))

(defmacro flex-bindings
  (auto-bindings &key arrange (start '0))
  `(flex-bindings-fn ',GL::AUTO-BINDINGS
    ',GL::ARRANGE
    ,GL::START))

(defun flex-param-bindings
  (in-alist)
  (b* (((when (atom in-alist)) nil) (case1 (car in-alist))
      ((unless (and (true-listp case1)
           (or (eql (len case1) 2)
             (and (eql (len case1) 4)
               (eq (nth 2 case1) :arrange))))) (er hard?
          'flex-param-bindings
          "Unsupported entry in flex-param-bindings: ~x0"
          case1))
      ((list params
         auto-bindings
         ?arrange-keyword
         arrange) case1))
    (cons (list params
        (flex-bindings-fn auto-bindings arrange 0))
      (flex-param-bindings (cdr in-alist)))))

(defun auto-bindings-fn
  (x)
  (flex-bindings-fn x nil 0))

(defmacro auto-bindings
  (&rest args)
  `(auto-bindings-fn ',GL::ARGS))