queens.mlish (6494B)
1 #lang s-exp "../../mlish.rkt" 2 (require "../rackunit-typechecking.rkt") 3 4 ;; function polymorphic in list element 5 (define-type (List X) 6 Nil 7 (Cons X (List X))) 8 9 (typecheck-fail 10 (match (Cons 1 Nil) with 11 [Nil -> 1]) 12 #:with-msg "clauses not exhaustive; missing\\: Cons") 13 (typecheck-fail 14 (match (Cons 1 Nil) with 15 [Cons x xs -> 1]) 16 #:with-msg "clauses not exhaustive; missing: Nil") 17 18 ;; list fns ---------- 19 20 ; map: tests whether match and define properly propagate 'expected-type 21 (define (map [f : (→ X Y)] [lst : (List X)] → (List Y)) 22 (match lst with 23 [Nil -> Nil] 24 [Cons x xs -> (Cons (f x) (map f xs))])) 25 (check-type map : (→/test (→ X Y) (List X) (List Y))) 26 (check-type map : (→/test {Y X} (→ Y X) (List Y) (List X))) 27 (check-type map : (→/test (→ A B) (List A) (List B))) 28 (check-not-type map : (→/test (→ A B) (List B) (List A))) 29 (check-not-type map : (→/test (→ X X) (List X) (List X))) ; only 1 bound tyvar 30 31 ; map: alt signature syntax 32 (define (map2 f lst) 33 : (→ X Y) (List X) → (List Y) 34 (match lst with 35 [Nil -> Nil] 36 [Cons x xs -> (Cons (f x) (map2 f xs))])) 37 (check-type map2 : (→/test (→ X Y) (List X) (List Y))) 38 (check-type map2 : (→/test {Y X} (→ Y X) (List Y) (List X))) 39 (check-type map2 : (→/test (→ A B) (List A) (List B))) 40 (check-not-type map2 : (→/test (→ A B) (List B) (List A))) 41 (check-not-type map2 : (→/test (→ X X) (List X) (List X))) ; only 1 bound tyvar 42 43 ; nil without annotation; tests fn-first, left-to-right arg inference 44 ; does work yet, need to add left-to-right inference in #%app 45 (check-type (map add1 Nil) : (List Int) ⇒ Nil) 46 (check-type (map add1 (Cons 1 (Cons 2 (Cons 3 Nil)))) 47 : (List Int) ⇒ (Cons 2 (Cons 3 (Cons 4 Nil)))) 48 (typecheck-fail (map add1 (Cons "1" Nil)) 49 #:with-msg "expected: Int\n *given: String") 50 (check-type (map (λ ([x : Int]) (+ x 2)) (Cons 1 (Cons 2 (Cons 3 Nil)))) 51 : (List Int) ⇒ (Cons 3 (Cons 4 (Cons 5 Nil)))) 52 ;; ; doesnt work yet: all lambdas need annotations 53 ;; (check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5)) 54 55 (define (filter [p? : (→ X Bool)] [lst : (List X)] → (List X)) 56 (match lst with 57 [Nil -> Nil] 58 [Cons x xs -> (if (p? x) 59 (Cons x (filter p? xs)) 60 (filter p? xs))])) 61 (define (filter/guard [p? : (→ X Bool)] [lst : (List X)] → (List X)) 62 (match lst with 63 [Nil -> Nil] 64 [Cons x xs #:when (p? x) -> (Cons x (filter p? xs))] 65 [Cons x xs -> (filter p? xs)])) 66 (check-type (filter zero? Nil) : (List Int) ⇒ Nil) 67 (check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) 68 : (List Int) ⇒ Nil) 69 (check-type (filter zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) 70 : (List Int) ⇒ (Cons 0 Nil)) 71 (check-type 72 (filter 73 (λ ([x : Int]) (not (zero? x))) 74 (Cons 0 (Cons 1 (Cons 2 Nil)))) 75 : (List Int) ⇒ (Cons 1 (Cons 2 Nil))) 76 (check-type (filter/guard zero? Nil) : (List Int) ⇒ Nil) 77 (check-type (filter/guard zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) 78 : (List Int) ⇒ Nil) 79 (check-type (filter/guard zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) 80 : (List Int) ⇒ (Cons 0 Nil)) 81 (check-type 82 (filter/guard 83 (λ ([x : Int]) (not (zero? x))) 84 (Cons 0 (Cons 1 (Cons 2 Nil)))) 85 : (List Int) ⇒ (Cons 1 (Cons 2 Nil))) 86 ; doesnt work yet: all lambdas need annotations 87 ;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2)) 88 89 (define (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y) 90 (match lst with 91 [Nil -> base] 92 [Cons x xs -> (f x (foldr f base xs))])) 93 (define (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y) 94 (match lst with 95 [Nil -> acc] 96 [Cons x xs -> (foldr f (f x acc) xs)])) 97 98 (define (all? [p? : (→ X Bool)] [lst : (List X)] → Bool) 99 (match lst with 100 [Nil -> #t] 101 [Cons x xs #:when (p? x) -> (all? p? xs)] 102 [Cons x xs -> #f])) 103 104 (define (tails [lst : (List X)] → (List (List X))) 105 (match lst with 106 [Nil -> (Cons Nil Nil)] 107 [Cons x xs -> (Cons lst (tails xs))])) 108 109 (define (build-list [n : Int] [f : (→ Int X)] → (List X)) 110 (if (zero? (sub1 n)) 111 (Cons (f 0) Nil) 112 (Cons (f (sub1 n)) (build-list (sub1 n) f)))) 113 114 (check-type (build-list 1 add1) 115 : (List Int) ⇒ (Cons 1 Nil)) 116 (check-type (build-list 3 add1) 117 : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 Nil)))) 118 (check-type (build-list 5 sub1) 119 : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 (Cons 0 (Cons -1 Nil)))))) 120 121 ;; map + filter + fold + build example 122 (define INPUT (build-list 1000 number->string)) 123 (check-type (foldl + 0 (filter even? (map string->number INPUT))) : Int -> 249500) 124 125 (define (append [lst1 : (List X)] [lst2 : (List X)] → (List X)) 126 (match lst1 with 127 [Nil -> lst2] 128 [Cons x xs -> (Cons x (append xs lst2))])) 129 130 ;; n-queens -------------------- 131 (define-type Queen (Q Int Int)) 132 133 (define (safe? [q1 : Queen] [q2 : Queen] → Bool) 134 (match q1 with 135 [Q x1 y1 -> 136 (match q2 with 137 [Q x2 y2 -> 138 (not (or (= x1 x2) 139 (= y1 y2) 140 (= (abs (- x1 x2)) 141 (abs (- y1 y2)))))])])) 142 143 (define (safe/list? [qs : (List Queen)] → Bool) 144 (match qs with 145 [Nil -> #t] 146 [Cons q1 rst -> 147 (all? (λ ([q2 : Queen]) (safe? q1 q2)) rst)])) 148 149 (define (valid? [lst : (List Queen)] → Bool) 150 (all? safe/list? (tails lst))) 151 152 (define (nqueens [n : Int] → (List Queen)) 153 (let* ([process-row 154 (λ ([r : Int] 155 [all-possible-so-far : (List (List Queen))]) 156 (foldr 157 (λ ([qs : (List Queen)] 158 [new-qss : (List (List Queen))]) 159 (append 160 (map 161 (λ ([c : Int]) (Cons (Q r c) qs)) 162 (build-list n add1)) 163 new-qss)) 164 Nil 165 all-possible-so-far))] 166 [all-possible 167 (foldl process-row 168 (Cons Nil Nil) 169 (build-list n add1))]) 170 (let ([solns (filter valid? all-possible)]) 171 (match solns with 172 [Nil -> Nil] 173 [Cons x xs -> x])))) 174 175 (check-type nqueens : (→ Int (List Queen))) 176 (check-type (nqueens 1) : (List Queen) ⇒ (Cons (Q 1 1) Nil)) 177 (check-type (nqueens 2) : (List Queen) ⇒ Nil) 178 (check-type (nqueens 3) : (List Queen) ⇒ Nil) 179 (check-type (nqueens 4) 180 : (List Queen) 181 ⇒ (Cons (Q 3 1) (Cons (Q 2 4) 182 (Cons (Q 1 2) (Cons (Q 4 3) Nil))))) 183 (check-type (nqueens 5) 184 : (List Queen) 185 ⇒ (Cons (Q 4 2) (Cons (Q 3 4) 186 (Cons (Q 2 1) (Cons (Q 1 3) (Cons (Q 5 5) Nil))))))