{"push_id":1674196956,"size":1,"distinct_size":1,"ref":"refs/heads/generalize-assocs","head":"0ce2195578cb61e1b13da74f96f27ca3a41a6925","before":"1a1dd1fded74c55d085e18737ab71723004d3427","commits":[{"sha":"0ce2195578cb61e1b13da74f96f27ca3a41a6925","author":{"name":"Keshav Kini","email":"cb7179ceebe6878e08f7b19f595a1a5115facc9e@oracle.com"},"message":"Make patbind-assocs easily generalizable\n\nThis commit generalizes and factors out some of the guts of\npatbind-assocs so that they can later be reused to create similar\npatbind functions for other (possibly user-defined) alist-backed data\nstructures.\n\nSuppose you have a datastructure which is backed by an alist but is\ndesigned to be used via accessor and updater functions, which are\nanalogous to `assoc` and `acons` but do something slightly more\ncomplicated.\n\nImagine for example an alist representing a polynomial by mapping\nmonomials to their coefficients, where only non-zero coefficients are\nactually stored.  Then you might have\n\n    (defun assoc-polynomial (x alist)\n      (or (assoc x alist)\n          (cons x 0)))\n\n    (defun acons-polynomial (key datum alist)\n      (if (equal key 0)\n          (delete-assoc key alist)\n        (acons key datum (delete-assoc key alist))))\n\nThis commit will allow you to write a patbind function using\ndef-b*-binder so that you can grab multiple coefficients from a\npolynomial in a single b* binding:\n\n    (def-b*-binder polynomial-assocs\n      :body (body-for-assocs 'assoc-polynomial\n                              args forms rest-expr))\n\n    (b* (((polynomial-assocs (a1 1) (a3 3) (a5 5))\n          my-polynomial))\n      (f a1 a3 a5))","distinct":true,"url":"https://api.github.com/repos/kini/acl2/commits/0ce2195578cb61e1b13da74f96f27ca3a41a6925"}]}
{"actor":{"display_login":"kini"}}