2.6 "list-utilities"

(include-book "list-utilities" :dir :teachpacks)

Documentation under construction.

;;===== Module: list-utilities =================================================

;;

;; Defining

;;   (break-at-nth n xs)

;;   (break-at-set delimiters xs)

;;   (break-at delimiter xs)

;;   (take-to-set delimiters xs)

;;   (take-to delimiter xs)

;;   (drop-set delimiters xs)

;;   (drop-past delimiter xs)

;;     = (drop-thru delimiter xs)

;;   (drop-past-n-delimiters n delimiter xs)

;;     = (drop-thru-n-delimiters n delimiter xs)

;;   (packets-set delimiters xs)

;;   (packets delimiter xs)

;;   (tokens delimiters xs)

;;   (replicate n x)

;;   (pad-left width pad xs)

;;   (chrs->str character-list)

;;   (str->chrs string)

;;   (words str)

;;==============================================================================

;;====== Function: (break-at-nth n xs) =========================================

;;

;;  Returns list with two elements

;;    (1) the first n elements of xs

;;    (2) xs without its first n elements

;;

;;  Pre : (and (integerp n)

;;             (>= n 0)

;;             (true-listp xs))

;;  Post: (and (= (min n (length xs))

;;                (length (car (break-at-nth n xs))))

;;             (equal (append (car  (break-at-nth n xs))

;;                            (cadr (break-at-nth n xs)))

;;                    xs))

;;==============================================================================

;;====== Function: (break-at-set delimiters xs) ================================

;;

;;  Returns list with two elements

;;    (1) the portion of xs that precedes its first element that is a

;;        member of the list delimiters

;;    (2) the portion of xs beginning with its first element that is a

;;        member of the list delimiters

;;

;;  Pre : (and (true-listp delimiters)

;;             (true-listp xs))

;;  Post: (and (equal (append (car (break-at-set ds xs))

;;                            (cadr (break-at-set ds xs)))

;;                    xs)

;;             (implies (consp (cadr (break-at-set ds xs)))

;;                      (member-equal (caadr (break-at-set ds xs)) ds)))

;;             (implies (member-equal d ds)

;;                      (not (member-equal d (car (break-at-set ds xs))))))

;;==============================================================================

;;====== Function: (break-at x xs) =============================================

;;

;;  Returns list with two elements

;;    (1) the portion of xs that precedes the first element equal to x

;;    (2) the portion of xs beginning with the first element equal to x

;;

;;  Pre : (true-listp xs)

;;  Post: (and (equal (append (car (break-at x xs)) (cadr (break-at x xs)))

;;                    xs)

;;             (implies (consp (cadr (break-at d xs)))

;;                      (member-equal (caadr (break-at-set d xs)) ds)))

;;             (implies (member-equal d ds)

;;                      (not (member-equal d (car (break-at d xs))))))

;;==============================================================================

;;====== Function: (take-to-set delimiters xs) =================================

;;

;;  Returns the part of xs that precedes its first element that is a member

;;  of the list delimiters

;;

;;  Pre : (and (true-listp delimiters)

;;             (true-listp xs))

;;  Post: (and (true-listp (take-to-set delimiters xs))

;;             (implies (member-equal d delimiters)

;;                      (not (member-equal d (take-to-set delimiters xs))))

;;             (implies (and (equal (append (take-to-set delimiters xs)

;;                                          ys)

;;                                  xs)

;;                           (consp ys))

;;                      (member-equal (car ys) delimiters)))

;;==============================================================================

;;====== Function: (take-to x xs) ==============================================

;;

;;  Returns the part of xs that precedes the first element equal to x

;;

;;  Pre : (true-listp xs)

;;  Post: (and (true-listp (take-to x xs))

;;             (not (member-equal x (take-to x xs)))

;;             (implies (member-equal x xs)

;;                      (equal (append (take-to x xs)

;;                                     (list x)

;;                                     (drop-past x xs))))

;;             (implies (not (member-equal x xs))

;;                      (equal (take-to x xs) xs)))

;;==============================================================================

;;===== Function: (drop-set delimiters xs) =====================================

;;

;;  Returns the part of xs that follows the maximal contiguous block of

;;  delimiters beginning at the first element of xs

;;

;;  Pre:  (true-listp xs)

;;  Post: (and (true-listp (drop-set delimiters xs))

;;             (implies (consp (drop-set delimiters xs))

;;                      (not (member (car (drop-set delimiters xs))

;;                                   delimiters)))

;;             (implies (and (equal (append ds (drop-set delimiters xs))

;;                                  xs)

;;                           (member d ds))

;;                      (member d delimiters)))

;;==============================================================================

;;===== Function: (drop-past delimiter xs) =====================================

;;

;;  Returns the part of xs that follows the first element equal to x

;;

;;  Pre:  (true-listp xs)

;;  Post: (and (true-listp (drop-past delimiter xs))

;;             (implies (member-equal x xs)

;;                      (equal (append (take-to delimiter xs)

;;                                     (list x)

;;                                     (drop-past delimiter xs))))

;;             (implies (not (member-equal delimiter xs))

;;                      (equal (drop-past delimiter xs) nil)))

;;==============================================================================

;;====== Function: (drop-past-n-delimiters n delimiter xs) =====================

;;

;;  Returns the part of xs that follows the first n occurances of x

;;

;;  Pre : (and (integerp n) (>= n 0) (true-listp xs))

;;  Post: (true-listp (drop-past-n-delimiters n d xs)) ; and some other stuff

;;==============================================================================

;;====== Function: (packets-set delimiters xs) ==================================

;;

;;  Parcels a list into a list of lists

;;  Contiguous sequences from a specified set of delimiters

;;  marks separations between packets

;;

;;  Pre : (and (true-listp delimiters) (true-listp xs))

;;  Post: (true-list-listp (packets-set ds xs))

;;        and a bunch of other stuff

;;==============================================================================

;;====== Function: (packets delimiter xs) ======================================

;;

;;  Parcels a list into a list of lists

;;  A specified delimiter marks separations between packets in the given list

;;

;;  Pre : (true-listp xs)

;;  Post: (and (true-list-listp (packets d xs))

;;             (implies (and (integerp n) (>= n 0))

;;                      (equal (nth n (packets d xs))

;;                             (take-to d (drop-past-n-delimiters n d xs)))))

;;==============================================================================

;;====== Function: (tokens delimiters xs) ======================================

;;

;;  Parcels a list into a list of tokens

;;  Tokens are the sublists residing between maximally contiguous

;;  sequences of delimiters

;;

;;  Pre : (and (true-listp delimiters) (true-listp xs))

;;  Post: (true-list-listp (tokens ds xs))

;;        and a bunch of other stuff

;;==============================================================================

;;===== Function: (rep-append n x xs) ==========================================

;;

;;  Appends xs to a list consisting of n copies of x

;;

;;  Pre : (and (integerp n)

;;             (>= n 0)

;;             (true-listp xs))

;;  Post: (and (implies (member-equal y (take n (rep-append n x)))

;;                      (equal y x))

;;             (equal (length (rep-append n x xs))

;;                    (+ (length xs) n))

;;             (equal (nthcdr n (rep-append n x xs))

;;                    xs))

;;==============================================================================

;;===== Function: (replicate n x) =================================================

;;

;;  Delivers a list consisting of n copies of x

;;

;;  Pre : (and (integerp n)

;;             (>= n 0))

;;  Post: (and (implies (member-equal y (replicate n x))

;;                      (equal y x))

;;             (equal (length (replicate n x)) n))

;;==============================================================================

;;===== Function: (pad-left w p xs) ============================================

;;

;;  Pads appends xs to copies of p to make the resulting list have w elements

;;  Note: Delivers xs, as is, if xs has w or more elements

;;

;;  Pre : (and (integerp w)

;;             (>= w 0)

;;             (listp xs))

;;  Post: (and (equal (length (pad-left w p xs))

;;                    (max w (length xs)))

;;             (implies (member-equal x (take (max 0 (- w (length xs))) xs))

;;                      (equal x p)))

;;==============================================================================

;;====== Function: (chrs->str chrs) ============================================

;;

;;  Converts list of characters to string

;;

;;  Pre : (character-listp chrs)

;;  Post: (stringp (chrs->str chrs))

;;==============================================================================

;;====== Function: (str->chrs str) =============================================

;;

;;  Converts string to list of characters

;;

;;  Pre : (stringp str)

;;  Post: (character-listp (str->chrs str))

;;==============================================================================

;;====== Function: (words str) =================================================

;;

;;  Parcels a string into a list of words

;;  Words are the sublists residing between maximally contiguous

;;  spans of whitespace

;;

;;  Pre : (stringp str)

;;  Post: (string-listp (words str))

;;        and a bunch of other stuff

;;==============================================================================