commit 1ad357b55e6f237bd93b2e2622b6fd99ada1d926
parent 965778d9f071a0cf767c3def2c4238e3c471b06d
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 4 Mar 2016 14:20:02 -0500
separate out mlish queens test
Diffstat:
3 files changed, 149 insertions(+), 44 deletions(-)
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -167,50 +167,6 @@
[Nil -> lst2]
[Cons x xs -> (Cons x (append xs lst2))]))
-;; n-queens --------------------
-(define-type Queen (Q Int Int))
-
-(define (safe? [q1 : Queen] [q2 : Queen] → Bool)
- (match q1 with
- [Q x1 y1 ->
- (match q2 with
- [Q x2 y2 ->
- (not (or (= x1 x2) (= y1 y2) (= (abs (- x1 x2)) (abs (- y1 y2)))))])]))
-(define (safe/list? [qs : (List Queen)] → Bool)
- (match qs with
- [Nil -> #t]
- [Cons q1 rst -> (all? (λ ([q2 : Queen]) (safe? q1 q2)) rst)]))
-(define (valid? [lst : (List Queen)] → Bool)
- (all? safe/list? (tails lst)))
-
-(define (nqueens [n : Int] → (List Queen))
- (let* ([process-row
- (λ ([r : Int] [all-possible-so-far : (List (List Queen))])
- (foldr
- (λ ([qs : (List Queen)] [new-qss : (List (List Queen))])
- (append
- (map (λ ([c : Int]) (Cons (Q r c) qs)) (build-list n add1))
- new-qss))
- Nil
- all-possible-so-far))]
- [all-possible (foldl process-row (Cons Nil Nil) (build-list n add1))])
- (let ([solns (filter valid? all-possible)])
- (match solns with
- [Nil -> Nil]
- [Cons x xs -> x]))))
-
-(check-type nqueens : (→ Int (List Queen)))
-(check-type (nqueens 1)
- : (List Queen) ⇒ (Cons (Q 1 1) Nil))
-(check-type (nqueens 2) : (List Queen) ⇒ (Nil {Queen}))
-(check-type (nqueens 3) : (List Queen) ⇒ (Nil {Queen}))
-(check-type (nqueens 4)
- : (List Queen)
- ⇒ (Cons (Q 3 1) (Cons (Q 2 4) (Cons (Q 1 2) (Cons (Q 4 3) Nil)))))
-(check-type (nqueens 5)
- : (List Queen)
- ⇒ (Cons (Q 4 2) (Cons (Q 3 4) (Cons (Q 2 1) (Cons (Q 1 3) (Cons (Q 5 5) Nil))))))
-
;; end infer.rkt tests --------------------------------------------------
diff --git a/tapl/tests/mlish/queens.mlish b/tapl/tests/mlish/queens.mlish
@@ -0,0 +1,148 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; function polymorphic in list element
+(define-type (List X)
+ Nil
+ (Cons X (List X)))
+
+(typecheck-fail
+ (match (Cons 1 Nil) with
+ [Nil -> 1])
+ #:with-msg "match: clauses not exhaustive; missing: Cons")
+(typecheck-fail
+ (match (Cons 1 Nil) with
+ [Cons x xs -> 1])
+ #:with-msg "match: clauses not exhaustive; missing: Nil")
+
+;; list fns ----------
+
+; map: tests whether match and define properly propagate 'expected-type
+(define (map [f : (→ X Y)] [lst : (List X)] → (List Y))
+ (match lst with
+ [Nil -> Nil]
+ [Cons x xs -> (Cons (f x) (map f xs))]))
+(check-type map : (→ (→ X Y) (List X) (List Y)))
+(check-type map : (→ (→ Y X) (List Y) (List X)))
+(check-type map : (→ (→ A B) (List A) (List B)))
+(check-not-type map : (→ (→ A B) (List B) (List A)))
+(check-not-type map : (→ (→ X X) (List X) (List X))) ; only 1 bound tyvar
+
+; nil without annotation; tests fn-first, left-to-right arg inference
+; does work yet, need to add left-to-right inference in #%app
+(check-type (map add1 Nil) : (List Int) ⇒ (Nil {Int}))
+(check-type (map add1 (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ (Cons 2 (Cons 3 (Cons 4 Nil))))
+(typecheck-fail (map add1 (Cons "1" Nil))
+ #:with-msg (expected "Int, (List Int)" #:given "String, (List Int)"))
+(check-type (map (λ ([x : Int]) (+ x 2)) (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ (Cons 3 (Cons 4 (Cons 5 Nil))))
+;; ; doesnt work yet: all lambdas need annotations
+;; (check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
+
+(define (filter [p? : (→ X Bool)] [lst : (List X)] → (List X))
+ (match lst with
+ [Nil -> Nil]
+ [Cons x xs -> (if (p? x)
+ (Cons x (filter p? xs))
+ (filter p? xs))]))
+(define (filter/guard [p? : (→ X Bool)] [lst : (List X)] → (List X))
+ (match lst with
+ [Nil -> Nil]
+ [Cons x xs #:when (p? x) -> (Cons x (filter p? xs))]
+ [Cons x xs -> (filter p? xs)]))
+(check-type (filter zero? Nil) : (List Int) ⇒ (Nil {Int}))
+(check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ (Nil {Int}))
+(check-type (filter zero? (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 0 Nil))
+(check-type (filter (λ ([x : Int]) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 1 (Cons 2 Nil)))
+(check-type (filter/guard zero? Nil) : (List Int) ⇒ (Nil {Int}))
+(check-type (filter/guard zero? (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ (Nil {Int}))
+(check-type (filter/guard zero? (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 0 Nil))
+(check-type
+ (filter/guard (λ ([x : Int]) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 1 (Cons 2 Nil)))
+; doesnt work yet: all lambdas need annotations
+;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2))
+
+(define (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y)
+ (match lst with
+ [Nil -> base]
+ [Cons x xs -> (f x (foldr f base xs))]))
+(define (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y)
+ (match lst with
+ [Nil -> acc]
+ [Cons x xs -> (foldr f (f x acc) xs)]))
+
+(define (all? [p? : (→ X Bool)] [lst : (List X)] → Bool)
+ (match lst with
+ [Nil -> #t]
+ [Cons x xs #:when (p? x) -> (all? p? xs)]
+ [Cons x xs -> #f]))
+
+(define (tails [lst : (List X)] → (List (List X)))
+ (match lst with
+ [Nil -> (Cons Nil Nil)]
+ [Cons x xs -> (Cons lst (tails xs))]))
+
+(define (build-list [n : Int] [f : (→ Int X)] → (List X))
+ (if (zero? (sub1 n))
+ (Cons (f 0) Nil)
+ (Cons (f (sub1 n)) (build-list (sub1 n) f))))
+(check-type (build-list 1 add1) : (List Int) ⇒ (Cons 1 Nil))
+(check-type (build-list 3 add1) : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 Nil))))
+(check-type (build-list 5 sub1)
+ : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 (Cons 0 (Cons -1 Nil))))))
+
+(define (append [lst1 : (List X)] [lst2 : (List X)] → (List X))
+ (match lst1 with
+ [Nil -> lst2]
+ [Cons x xs -> (Cons x (append xs lst2))]))
+
+;; n-queens --------------------
+(define-type Queen (Q Int Int))
+
+(define (safe? [q1 : Queen] [q2 : Queen] → Bool)
+ (match q1 with
+ [Q x1 y1 ->
+ (match q2 with
+ [Q x2 y2 ->
+ (not (or (= x1 x2) (= y1 y2) (= (abs (- x1 x2)) (abs (- y1 y2)))))])]))
+(define (safe/list? [qs : (List Queen)] → Bool)
+ (match qs with
+ [Nil -> #t]
+ [Cons q1 rst -> (all? (λ ([q2 : Queen]) (safe? q1 q2)) rst)]))
+(define (valid? [lst : (List Queen)] → Bool)
+ (all? safe/list? (tails lst)))
+
+(define (nqueens [n : Int] → (List Queen))
+ (let* ([process-row
+ (λ ([r : Int] [all-possible-so-far : (List (List Queen))])
+ (foldr
+ (λ ([qs : (List Queen)] [new-qss : (List (List Queen))])
+ (append
+ (map (λ ([c : Int]) (Cons (Q r c) qs)) (build-list n add1))
+ new-qss))
+ Nil
+ all-possible-so-far))]
+ [all-possible (foldl process-row (Cons Nil Nil) (build-list n add1))])
+ (let ([solns (filter valid? all-possible)])
+ (match solns with
+ [Nil -> Nil]
+ [Cons x xs -> x]))))
+
+(check-type nqueens : (→ Int (List Queen)))
+(check-type (nqueens 1)
+ : (List Queen) ⇒ (Cons (Q 1 1) Nil))
+(check-type (nqueens 2) : (List Queen) ⇒ (Nil {Queen}))
+(check-type (nqueens 3) : (List Queen) ⇒ (Nil {Queen}))
+(check-type (nqueens 4)
+ : (List Queen)
+ ⇒ (Cons (Q 3 1) (Cons (Q 2 4) (Cons (Q 1 2) (Cons (Q 4 3) Nil)))))
+(check-type (nqueens 5)
+ : (List Queen)
+ ⇒ (Cons (Q 4 2) (Cons (Q 3 4) (Cons (Q 2 1) (Cons (Q 1 3) (Cons (Q 5 5) Nil))))))
diff --git a/tapl/tests/run-all-mlish-tests.rkt b/tapl/tests/run-all-mlish-tests.rkt
@@ -1,4 +1,5 @@
#lang racket
(require "mlish-tests.rkt")
+(require "mlish/queens.mlish")
(require "mlish/trees.mlish")
(require "mlish/chameneos.mlish")
