/usr/share/emacs/site-lisp/agda/agda2-queue.el is in agda-mode 2.4.0.2-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 | ;;; agda2-queue.el --- Simple FIFO character queues.
(defun agda2-queue-empty ()
"Creates a new empty FIFO character queue.
Queues are represented as pairs. The car contains the queue. If
the queue is empty, then the cdr contains the symbol nil, and
otherwise it points to the queue's last cons-cell."
(cons nil nil))
(defun agda2-queue-is-prefix-of (prefix queue)
"Returns a non-nil result iff the string PREFIX is a prefix of QUEUE.
Linear in the length of PREFIX."
(let ((queue (car queue))
(prefix (append prefix nil)))
(while (and (consp queue) (consp prefix)
(equal (car queue) (car prefix)))
(pop queue)
(pop prefix))
(null prefix)))
(defun agda2-queue-enqueue (queue string)
"Adds the characters in STRING to the end of QUEUE.
This function updates QUEUE destructively, and is linear in the
length of STRING."
(let ((chars (append string nil)))
(when (consp chars)
(if (null (cdr queue))
(setcar queue chars)
(setcdr (cdr queue) chars))
(setcdr queue (last chars))))
queue)
(defun agda2-queue-from-string (string)
"Creates a new FIFO containing the characters in STRING.
Linear in the length of STRING."
(agda2-queue-enqueue (agda2-queue-empty) string))
(defun agda2-queue-to-string (queue)
"Constructs a string containing all the characters in QUEUE.
Linear in the length of QUEUE."
(concat "" (car queue)))
(provide 'agda2-queue)
|