List abstractions
; [X] N [N -> X] -> [List-of X]
; constructs a list by applying f to 0, 1, ..., (sub1 n)
; (build-list n f) == (list (f 0) ... (f (- n 1)))
(define (build-list n f) ...)
; [X] [X -> Boolean] [List-of X] -> [List-of X]
; produces a list from those items on lx for which p holds
(define (filter p lx) ...)
; [X] [List-of X] [X X -> Boolean] -> [List-of X]
; produces a version of lx that is sorted according to cmp
(define (sort lx cmp) ...)
; [X Y] [X -> Y] [List-of X] -> [List-of Y]
; constructs a list by applying f to each item on lx
; (map f (list x-1 ... x-n)) == (list (f x-1) ... (f x-n))
(define (map f lx) ...)
; [X] [X -> Boolean] [List-of X] -> Boolean
; determines whether p holds for every item on lx
; (andmap p (list x-1 ... x-n)) == (and (p x-1) ... (p x-n))
(define (andmap p lx) ...)
; [X] [X -> Boolean] [List-of X] -> Boolean
; determines whether p holds for at least one item on lx
; (ormap p (list x-1 ... x-n)) == (or (p x-1) ... (p x-n))
(define (ormap p lx) ...)
Foldr and Foldl
Folds a list of values into one value from the left or right:
> (foldr string-append "" (list "a" "b" "c"))
"abcd"
> (foldl string-append "" (list "a" "b" "c"))
"dcba"
Foldr does it with the first element first, so
(cons "a"
(cons "b"
(cons "c"
(cons "d" '()))))
becomes
(string-append "a"
(string-append "b"
(string-append "c"
(string-append "d" ""))))
"abcd"
And Foldl does the last element first, sop
(cons "a"
(cons "b"
(cons "c"
(cons "d" '()))))
becomes
(string-append "d"
(string-append "c"
(string-append "b"
(string-append "a" ""))))
"dcba"
where "" is the base case in both cases.
Build list
Perfect squares example:
; perfect-squares : Nat -> [List-of Nat]
; produce a list of the first k perfect squares
(check-expect (perfect-squares 0)
'())
(check-expect (perfect-squares 1)
(list 1))
(check-expect (perfect-squares 5)
(list 1 4 9 16 25))
(define (perfect-squares k)
(build-list k make-perfect-square))
;; make-perfect-square : Nat -> Nat
;; produce the square of 1 plus the input
(check-expect (make-perfect-square 0) 1)
(check-expect (make-perfect-square 1) 4)
(define (make-perfect-square n)
(sqr (add1 n)))
Andmap and Ormap
ISL List Abstraction: andmap/ormap
- andmap: does the predicate return true for all the elements of the list?
- If you cannot come up with a counter-example, the answer is yes
- ormap: does the predicate return true for any the elements of the list?