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 |
;;============================================================================== |
|