From 1ad357b55e6f237bd93b2e2622b6fd99ada1d926 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 4 Mar 2016 14:20:02 -0500 Subject: [PATCH] separate out mlish queens test --- tapl/tests/mlish-tests.rkt | 44 --------- tapl/tests/mlish/queens.mlish | 148 +++++++++++++++++++++++++++++ tapl/tests/run-all-mlish-tests.rkt | 1 + 3 files changed, 149 insertions(+), 44 deletions(-) create mode 100644 tapl/tests/mlish/queens.mlish diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt index 53cd0d1..6a04ce6 100644 --- 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 new file mode 100644 index 0000000..d618b15 --- /dev/null +++ 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 index 937ea47..22e40c7 100644 --- 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")