(in-package "ACL2-USER") (defun reset (stobj) (declare (ignore stobj)) (list (list 'nodes ) (list 'robots) (list 'last-node 0))) (defun add-node (stobj row col) (list (assoc 'robots stobj) (list 'last-node (1+ (cadr (assoc 'last-node stobj)))) (append (assoc 'nodes stobj) (list (list (cons 'row row) (cons 'col col) (list 'exits) (list 'occupant) (list 'bids) (cons 'id (1+ (cadr (assoc 'last-node stobj))))))))) (defun get-node (id nodes) (cond ((not (proper-consp nodes)) nil) ((equal id (cdr (assoc 'id (car nodes)))) (car nodes)) (t (get-node id (cdr nodes))))) (defun clean-alist (alist assocs new-alist) (if (not (proper-consp alist)) new-alist (clean-alist (cdr alist) (append assocs (if (member (caar alist) assocs) nil (list (caar alist)))) (append new-alist (if (member (caar alist) assocs) nil (list (car alist))))))) (defun dedup-ids (nodes new-nodes) (if (not (proper-consp nodes)) new-nodes (dedup-ids (cdr nodes) (append new-nodes (if (get-node (cdr (assoc 'id (car nodes))) new-nodes) nil (list (car nodes))))))) (defun add-exit (alist from to) (let* ((nodes (cdr (assoc 'nodes alist))) (node (get-node from nodes)) (new-exits (append (assoc 'exits node) (list to)))) (list (assoc 'robots alist) (assoc 'last-node alist) (append (list 'nodes ) (dedup-ids (append (list (clean-alist (append (list new-exits) node) nil nil)) (cdr (assoc 'nodes alist))) nil))))) (defun fill-one-row (col-down row-no stobj) (if (zp col-down) stobj (fill-one-row (1- (abs col-down)) row-no (add-node stobj row-no col-down)))) (defun connect-ids (stobj ids) (if (not (proper-consp ids)) stobj (connect-ids (add-exit stobj (caar ids) (cdar ids)) (cdr ids)))) (defun col-max-row (nodes row last-max) (if (not (proper-consp nodes)) last-max (col-max-row (cdr nodes) row (if (< last-max (if (equal row (cdr (assoc 'row (car nodes)))) (cdr (assoc 'col (car nodes))) 0)) (cdr (assoc 'col (car nodes))) last-max)))) (defun change-last-node-id (stobj new-node-id) (clean-alist (append (list (list 'last-node new-node-id)) stobj) nil nil)) (defun fill-grid (stobj n-cols downfrom-row) (if (zp downfrom-row) stobj (fill-grid (fill-one-row n-cols downfrom-row stobj) n-cols (1- (abs downfrom-row))))) (defun right-pair-row (row-start col-offset neighbors) (if (zp col-offset) neighbors (right-pair-row row-start (1- col-offset) (append (list (cons (1- (+ row-start col-offset)) (1- (+ row-start col-offset 1))) (cons (1- (+ row-start col-offset 1)) (1- (+ row-start col-offset)))) neighbors)))) (defun pair-rows (row-1-start row-2-start col-offset neighbors) (if (zp col-offset) neighbors (pair-rows row-1-start row-2-start (1- col-offset) (append (list (cons (+ row-1-start col-offset) (+ row-2-start col-offset)) (cons (+ row-2-start col-offset) (+ row-1-start col-offset))) neighbors)))) (defun connect-grid-rows (stobj col-max row) (if (zp row) stobj (connect-grid-rows (connect-ids stobj (right-pair-row (1+ (* (1- row) col-max)) (1- col-max) nil)) (abs col-max) (1- (Abs row))))) (defun connect-grid-cols (stobj col-max row) " row confusingly is 0-indexed. (one less than dim len) " (if (zp row) stobj (connect-grid-cols (connect-ids stobj (pair-rows (* (1- row) col-max) (* row col-max) col-max nil)) col-max (1- row)))) (defun make-connected-grid (stobj row-max col-max) (connect-grid-cols (connect-grid-rows (fill-grid (reset stobj) col-max row-max) col-max row-max) col-max (1- row-max)))