diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt index 89c2b33..69a76ca 100644 --- a/tapl/mlish.rkt +++ b/tapl/mlish.rkt @@ -242,7 +242,6 @@ #'(C {τ_solved (... ...)} . args)])) ...)])) -(require racket/unsafe/ops) ;; match -------------------------------------------------- (define-syntax (match stx) (syntax-parse stx #:datum-literals (with ->) @@ -543,6 +542,14 @@ #:with (e- ...) (⇑s (start end step) as Int) (⊢ (in-range e- ...) : (Sequence Int))]) +(define-typed-syntax in-naturals/tc #:export-as in-naturals + [(_) #'(in-naturals/tc (ext-stlc:#%datum . 0))] + [(_ start) + #:with start- (⇑ start as Int) + (⊢ (in-naturals start-) : (Sequence Int))]) + + + (define-typed-syntax in-vector [(_ e) #:with [e- (ty)] (⇑ e as Vector) @@ -575,6 +582,16 @@ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body) (⊢ (for/list ([x- e-] ...) body-) : (List ty_body))]) +(define-typed-syntax for/vector + [(_ ([x:id e]...) body) + #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) + #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body) + (⊢ (for/vector ([x- e-] ...) body-) : (Vector ty_body))]) +(define-typed-syntax for*/vector + [(_ ([x:id e]...) body) + #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) + #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body) + (⊢ (for*/vector ([x- e-] ...) body-) : (Vector ty_body))]) (define-typed-syntax for*/list [(_ ([x:id e]...) body) #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) @@ -695,6 +712,11 @@ #:when (typecheck? #'ty_k #'ty_key) (⊢ (hash-has-key? h- k-) : Bool)]) +(define-typed-syntax hash-count + [(_ h) + #:with [h- _] (⇑ h as Hash) + (⊢ (hash-count h-) : Int)]) + (define-base-type String-Port) (define-primop open-output-string : (→ String-Port)) (define-primop get-output-string : (→ String-Port String)) diff --git a/tapl/tests/mlish/ack.mlish b/tapl/tests/mlish/ack.mlish index 8d8526b..b29225b 100644 --- a/tapl/tests/mlish/ack.mlish +++ b/tapl/tests/mlish/ack.mlish @@ -4,9 +4,11 @@ ;; tests cond with else (define (ack/else [m : Int] [n : Int] -> Int) - (cond [(zero? m) (add1 n)] - [(zero? n) (ack/else (sub1 m) 1)] - [else (ack/else (sub1 m) (ack/else m (sub1 n)))])) + (cond + [(zero? m) (add1 n)] + [(zero? n) (ack/else (sub1 m) 1)] + [else + (ack/else (sub1 m) (ack/else m (sub1 n)))])) (check-type (ack/else 0 0) : Int -> 1) (check-type (ack/else 1 1) : Int -> 3) @@ -14,9 +16,10 @@ (check-type (ack/else 3 4) : Int -> 125) (define (ack [m : Int] [n : Int] -> Int) - (cond [(zero? m) (add1 n)] - [(zero? n) (ack (sub1 m) 1)] - [#t (ack (sub1 m) (ack m (sub1 n)))])) + (cond + [(zero? m) (add1 n)] + [(zero? n) (ack (sub1 m) 1)] + [#t (ack (sub1 m) (ack m (sub1 n)))])) (check-type (ack 0 0) : Int -> 1) (check-type (ack 1 1) : Int -> 3) diff --git a/tapl/tests/mlish/ary.mlish b/tapl/tests/mlish/ary.mlish index 4601751..16280c2 100644 --- a/tapl/tests/mlish/ary.mlish +++ b/tapl/tests/mlish/ary.mlish @@ -10,11 +10,17 @@ [y (make-vector n 0)] [last (sub1 n)]) (begin - (for ([i (in-range n)]) (vector-set! x i (add1 i))) - (for* ([k (in-range 1000)][i (in-range last -1 -1)]) + (for ([i (in-range n)]) + (vector-set! x i (add1 i))) + (for* ([k (in-range 1000)] + [i (in-range last -1 -1)]) (vector-set! y i (+ (vector-ref x i) (vector-ref y i)))) - (tup (vector-ref y 0) (vector-ref y last))))) + (tup (vector-ref y 0) + (vector-ref y last))))) -(check-type (main (vector "100")) : (× Int Int) -> (tup 1000 100000)) -(check-type (main (vector "1000")) : (× Int Int) -> (tup 1000 1000000)) -(check-type (main (vector "10000")) : (× Int Int) -> (tup 1000 10000000)) +(check-type (main (vector "100")) + : (× Int Int) -> (tup 1000 100000)) +(check-type (main (vector "1000")) + : (× Int Int) -> (tup 1000 1000000)) +(check-type (main (vector "10000")) + : (× Int Int) -> (tup 1000 10000000)) diff --git a/tapl/tests/mlish/chameneos.mlish b/tapl/tests/mlish/chameneos.mlish index 2ae8df3..f4b9757 100644 --- a/tapl/tests/mlish/chameneos.mlish +++ b/tapl/tests/mlish/chameneos.mlish @@ -2,11 +2,15 @@ (require "../rackunit-typechecking.rkt") (define-type Color Red Yellow Blue) + (define-type (Option X) None (Some X)) + (define-type-alias Meet (× (Channel (Option (× Color String))) (× Color String))) + (define-type-alias Result (× Int Int)) + (define-type-alias MeetChan (Channel Meet)) (define-type-alias ResultChan (Channel Result)) @@ -63,7 +67,8 @@ (define (sleeper [ch-meet : MeetChan] [ch-res : ResultChan] [ch : (Channel (Option (× Color String)))] - [name : String] [c : Color] [met : Int] [same : Int] -> Unit) + [name : String] [c : Color] [met : Int] [same : Int] + -> Unit) (begin (channel-put ch-meet (tup ch (tup c name))) (match (channel-get ch) with @@ -72,12 +77,14 @@ [other-col other-name -> (begin (sleep 0) - (sleeper ch-meet ch-res ch - name (change c other-col) - (add1 met) (+ same (if (string=? name other-name) 1 0))))])] + (sleeper + ch-meet ch-res ch + name (change c other-col) + (add1 met) (+ same (if (string=? name other-name) 1 0))))])] [None -> (channel-put ch-res (tup met same))]))) -(define (creature [c : Color] [ch-meet : MeetChan] [ch-res : ResultChan] -> Thread) +(define (creature [c : Color] [ch-meet : MeetChan] [ch-res : ResultChan] + -> Thread) (thread (λ () (let ([ch (make-channel {(Option (× Color String))})] @@ -96,4 +103,17 @@ [ths (map (λ ([c : Color]) (creature c ch-meet ch-res)) inits)]) (map (λ ([c : Color]) (channel-get ch-res)) inits))) -(check-type (go 100 (list Blue Red Yellow)) : (List Result)) +(check-type (go 100 (list Blue Red Yellow)) + : (List Result) + -> (list (list 67 0) + (list 66 0) + (list 67 0))) + +(check-type (go 1000 (list Blue Red Yellow Red Yellow Blue)) + : (List Result) + -> (list (list 333 0) + (list 333 0) + (list 333 0) + (list 333 0) + (list 334 0) + (list 334 0))) diff --git a/tapl/tests/mlish/fasta.mlish b/tapl/tests/mlish/fasta.mlish index 51fdde2..fe754be 100644 --- a/tapl/tests/mlish/fasta.mlish +++ b/tapl/tests/mlish/fasta.mlish @@ -29,7 +29,7 @@ (check-type line-length : Int) -(define (repeat-fasta [header : String][N : Int][sequence : String] -> String) +(define (repeat-fasta [header : String] [N : Int] [sequence : String] -> String) (let* ([out (open-output-string)] [len (string-length sequence)] [buf (make-string (+ len line-length))]) @@ -49,11 +49,10 @@ (define IM 139968) (define IM.0 (fx->fl IM)) -(define V - (let ([v (make-vector IM)]) - (for ([id (in-range IM)]) - (vector-set! v id (modulo (+ IC (* id IA)) IM))) - v)) +(define V + (for/vector ([id (in-range IM)]) + (modulo (+ IC (* id IA)) IM))) + (check-type V : (Vector Int)) (define (random-next [cur : Int] -> Int) (vector-ref V cur)) @@ -133,24 +132,27 @@ (n-randoms buf out lookup-str last R)] [else R]))))]) (get-output-string out)))) + (define n 10) + (check-type (repeat-fasta ">ONE Homo sapiens alu\n" (* n 2) +alu+) : String -> ">ONE Homo sapiens alu\nGGCCGGGCGCGGTGGCTCAC\n") + (define res1 (random-fasta ">TWO IUB ambiguity codes\n" (* n 3) IUB 42)) + (define res2 (match res1 with [R str -> (random-fasta ">THREE Homo sapiens frequency\n" (* n 5) HOMOSAPIEN R)])) + (check-type (proj res1 1) : String -> ">TWO IUB ambiguity codes\nattRtBtaDtatVataKatgaatcccgDtY\n") -;taaaWKatgWRattaNBttctNagggcgWt\n") -;; should be cttBtatcatatgctaKggNcataaaSatg ? + (check-type (proj res2 1) : String -> (string-append ">THREE Homo sapiens frequency\n" - "atttgcggaaacgacaaatattaacacatcatcagagtaccataaaggga\n" - #;"agggctccaaatcataaagaggaatatattattacacgattagaaaccca\n")) -;; should be taaatcttgtgcttcgttagaagtctcgactacgtgtagcctagtgtttg ? + "atttgcggaaacgacaaatattaacacatcatcagagtaccataaaggga\n")) + (define (mk-fasta [n : Int] -> String) (let ([res1 (repeat-fasta ">ONE Homo sapiens alu\n" (* n 2) +alu+)] @@ -160,5 +162,30 @@ [R str -> (random-fasta ">THREE Homo sapiens frequency\n" (* n 5) HOMOSAPIEN R)])]) (string-append res1 (proj res2 1) (proj res3 1)))) + (provide mk-fasta) -(check-type (mk-fasta 100) : String) + +(check-type (mk-fasta 100) + : String + -> (string-append + ">ONE Homo sapiens alu\n" + "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGA\n" + "TCACCTGAGGTCAGGAGTTCGAGACCAGCCTGGCCAACATGGTGAAACCCCGTCTCTACT\n" + "AAAAATACAAAAATTAGCCGGGCGTGGTGGCGCGCGCCTGTAATCCCAGCTACTCGGGAG\n" + "GCTGAGGCAGGAGAATCGCT\n" + ">TWO IUB ambiguity codes\n" + "attRtBtaDtatVataKatgaatcccgDtYtcccNaNgtRttNtatttatcctSaRataW\n" + "taatNtNctaatctttggMtMttKtYtMHagBttagcMKMttttcWaactgcSttgaaac\n" + "gtcatHagHtgtaHVgtcattatgRcaVcaatctcWgaNtttVaaYcaaaataYtgWgtt\n" + "acttMgtHHgagtattaaaKSgtBgacaaggSaaRttVaVDHttRgctagtaaacgaaac\n" + "ttcRNtgcatttSagBtHttNRaatgtctattcaSaRYcgtatSattttttttgaBgagD\n" + ">THREE Homo sapiens frequency\n" + "gaagacaggtgtaacgtgggaaaatctctagtaaagctttgatcagcggagacgcgatca\n" + "acagatcctttatatcgcgaaacttctctctatcagcgaactaaggagggcgacaatccg\n" + "agctgttccggaccaaaccctgaaagtacgactctgctctaataaagtcaaaacgtagaa\n" + "gactagatacaattatactgacaacaaaaaaaagttgcgtgcacaagagtacgatgtttg\n" + "accgccagttattatgacgagggtgagaacaagtcaggctaaagtagaagagcaccatag\n" + "gtatcagtttaactgagtaaatgcgaatgcgtgactttaaataagcctgcgtgtgtcaaa\n" + "actctacaatatctttgttatattattgaatcattctggatttgaggcagtggagcatac\n" + "tgtataaaataatttttcggtgggtcaaaaataaatttcaattaagacgttaaggataat\n" + "gaaatgactcaatctaaggt\n")) diff --git a/tapl/tests/mlish/fibo.mlish b/tapl/tests/mlish/fibo.mlish index 0871885..7857ce2 100644 --- a/tapl/tests/mlish/fibo.mlish +++ b/tapl/tests/mlish/fibo.mlish @@ -2,8 +2,10 @@ (require "../rackunit-typechecking.rkt") (define (fib [n : Int] -> Int) - (cond [(< n 2) 1] - (else (+ (fib (- n 2)) (fib (sub1 n)))))) + (cond + [(< n 2) 1] + [else + (+ (fib (- n 2)) (fib (sub1 n)))])) (define (main [args : (Vector String)] -> Int) (let ([n (if (= (vector-length args) 0) @@ -12,6 +14,9 @@ (fib n))) (check-type (main (vector "0")) : Int -> 1) + (check-type (main (vector "1")) : Int -> 1) + (check-type (main (vector "2")) : Int -> 2) + (check-type (main (vector "22")) : Int -> 28657) diff --git a/tapl/tests/mlish/hash.mlish b/tapl/tests/mlish/hash.mlish index 2d8e32f..ef43086 100644 --- a/tapl/tests/mlish/hash.mlish +++ b/tapl/tests/mlish/hash.mlish @@ -8,7 +8,12 @@ (let ([j (add1 i)]) (tup (number->string j 16) j)))]) (for/sum ([i (in-range 1 (add1 n))] - #:when (hash-ref hash (number->string i))) + #:when + (hash-ref hash (number->string i))) 1))) +(check-type (main (vector "2000")) : Int -> 799) + +(check-type (main (vector "20000")) : Int -> 4999) + (check-type (main (vector "200000")) : Int -> 30999) diff --git a/tapl/tests/mlish/knuc.mlish b/tapl/tests/mlish/knuc.mlish index 1f73086..a334274 100644 --- a/tapl/tests/mlish/knuc.mlish +++ b/tapl/tests/mlish/knuc.mlish @@ -3,7 +3,7 @@ (require-typed mk-fasta #:from "fasta.mlish") -(define (all-counts [len : Int][dna : String] -> (Hash String (Ref Int))) +(define (all-counts [len : Int] [dna : String] -> (Hash String (Ref Int))) (let ([table (hash {String (Ref Int)})]) (for ([s (in-range (- (string-length dna) len) -1 -1)]) (let ([key (make-string len)]) @@ -16,22 +16,15 @@ (:= b (add1 (deref b)))))) table)) -;; (define (write-freqs table) -;; (let* ([content (hash-map table (lambda (k v) (cons k (unbox v))))] -;; [total (exact->inexact (apply + (map cdr content)))]) -;; (for ([a (sort content > #:key cdr)]) -;; (printf "~a ~a\n" -;; (car a) -;; (real->decimal-string (* 100 (/ (cdr a) total)) 3))))) - -#;(define (write-one-freq [table : (Hash String (Ref Int))][key : String] -> Unit) - (let ([cnt (hash-ref table key (box 0))]) - (printf "~a\t~a\n" (unbox cnt) key))) (define dna (let* ([in (mk-fasta 100000)] ;; Skip to ">THREE ..." - [rst (head (tail (regexp-match (regexp ">THREE Homo sapiens frequency\n(.*)$") in)))]) + [rst + (head (tail + (regexp-match + (regexp ">THREE Homo sapiens frequency\n(.*)$") + in)))]) (let ([s (open-output-string)]) ;; Copy everything but newlines to s: (for ([l (in-lines rst)]) @@ -41,15 +34,26 @@ (check-type dna : String) -(check-type (all-counts 1 dna) : (Hash String (Ref Int))) -;; ;; 1-nucleotide counts: -;; (write-freqs (all-counts 1 dna)) -;; (newline) +;; 1-nucleotide counts: +(define counts1 (all-counts 1 dna)) -(check-type (all-counts 2 dna) : (Hash String (Ref Int))) -;; ;; 2-nucleotide counts: -;; (write-freqs (all-counts 2 dna)) -;; (newline) +(check-type counts1 : (Hash String (Ref Int))) + +(check-type (hash-count counts1) : Int -> 4) + +;; 2-nucleotide counts: +(define counts2 (all-counts 2 dna)) + +(check-type counts2 : (Hash String (Ref Int))) + +(check-type (hash-count counts2) : Int -> 16) + +;; 2-nucleotide counts: +(define counts3 (all-counts 3 dna)) + +(check-type counts3 : (Hash String (Ref Int))) + +(check-type (hash-count counts3) : Int -> 64) ;; Specific sequences: (check-type @@ -61,5 +65,3 @@ 0))) : (List Int) -> (list 5861 1776 176 0 0)) - #;(write-one-freq (all-counts (string-length seq) dna) - seq) diff --git a/tapl/tests/mlish/matrix.mlish b/tapl/tests/mlish/matrix.mlish new file mode 100644 index 0000000..8bd6871 --- /dev/null +++ b/tapl/tests/mlish/matrix.mlish @@ -0,0 +1,73 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define-type-alias Matrix (Vector (Vector Int))) + +(define size 30) + +(define (vector-map [f : (→ X Y)] [v : (Vector X)] -> (Vector Y)) + (for/vector ([x (in-vector v)]) (f x))) + +(define (mkmatrix [rows : Int] [cols : Int] -> Matrix) + (for/vector ([i (in-range rows)] + [count (in-range 1 (* rows cols) cols)]) + (for/vector ([j (in-range cols)] + [x (in-naturals count)]) + x))) + +(check-type (mkmatrix 3 4) : Matrix + -> (vector (vector 1 2 3 4) + (vector 5 6 7 8) + (vector 9 10 11 12))) + +(check-type (mkmatrix 3 3) + : Matrix + -> (vector (vector 1 2 3) + (vector 4 5 6) + (vector 7 8 9))) + +(check-type (mkmatrix 4 3) + : Matrix + -> (vector (vector 1 2 3) + (vector 4 5 6) + (vector 7 8 9) + (vector 10 11 12))) + +(define (num-cols [mx : Matrix] -> Int) + (let ((row (vector-ref mx 0))) + (vector-length row))) + +(define (num-rows [mx : Matrix] -> Int) + (vector-length mx)) + +(define (vec-mult [v1 : (Vector Int)] [v2 : (Vector Int)] -> Int) + (for/sum ([x (in-vector v1)] + [y (in-vector v2)]) + (* x y))) + +(define (mmult [m1 : Matrix] [m2 : Matrix] -> Matrix) + (for/vector ([row (in-vector m1)]) + (for/vector ([col-num (in-range (num-cols m2))]) + (let ([col + (vector-map + (λ ([r : (Vector Int)]) (vector-ref r col-num)) + m2)]) + (vec-mult row col))))) + +(check-type (mmult (mkmatrix 3 3) (mkmatrix 3 3)) + : Matrix + -> (vector (vector 30 36 42) + (vector 66 81 96) + (vector 102 126 150))) + +(check-type (mmult (mkmatrix 2 3) (mkmatrix 3 2)) + : Matrix + -> (vector (vector 22 28) + (vector 49 64))) + +(check-type (mmult (mkmatrix 4 3) (mkmatrix 3 4)) + : Matrix + -> (vector (vector 38 44 50 56) + (vector 83 98 113 128) + (vector 128 152 176 200) + (vector 173 206 239 272))) diff --git a/tapl/tests/mlish/queens.mlish b/tapl/tests/mlish/queens.mlish index d618b15..999ff3d 100644 --- a/tapl/tests/mlish/queens.mlish +++ b/tapl/tests/mlish/queens.mlish @@ -56,7 +56,10 @@ : (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)))) +(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)))) @@ -64,7 +67,9 @@ (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)))) + (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)) @@ -93,8 +98,11 @@ (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 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)))))) @@ -111,25 +119,38 @@ [Q x1 y1 -> (match q2 with [Q x2 y2 -> - (not (or (= x1 x2) (= y1 y2) (= (abs (- x1 x2)) (abs (- y1 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)])) + [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))]) + (λ ([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))]) + (λ ([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] @@ -138,11 +159,15 @@ (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 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))))) + ⇒ (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)))))) + ⇒ (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/mlish/trees.mlish b/tapl/tests/mlish/trees.mlish index 9fa508f..4bbbc11 100644 --- a/tapl/tests/mlish/trees.mlish +++ b/tapl/tests/mlish/trees.mlish @@ -8,17 +8,24 @@ (define (make [item : Int] [depth : Int] -> (Tree Int)) (if (zero? depth) (Leaf item) - (let ([item2 (* item 2)] [depth2 (sub1 depth)]) + (let ([item2 (* item 2)] + [depth2 (sub1 depth)]) (Node (make (sub1 item2) depth2) item (make item2 depth2))))) (define tree1 (make 4 1)) (define tree2 (make 3 2)) -(check-type tree1 : (Tree Int) -> (Node (Leaf 7) 4 (Leaf 8))) + +(check-type tree1 + : (Tree Int) -> (Node (Leaf 7) 4 (Leaf 8))) + (check-type tree2 : (Tree Int) - -> (Node (Node (Leaf 9) 5 (Leaf 10)) 3 (Node (Leaf 11) 6 (Leaf 12)))) + -> (Node + (Node (Leaf 9) 5 (Leaf 10)) + 3 + (Node (Leaf 11) 6 (Leaf 12)))) (define (sum [t : (Tree Int)] -> Int) (match t with @@ -30,8 +37,10 @@ (define (check/acc [t : (Tree Int)] [acc : Int] -> Int) (match t with - [Leaf v -> (+ acc v)] - [Node l v r -> (check/acc l (- acc (check/acc r 0)))])) + [Leaf v -> + (+ acc v)] + [Node l v r -> + (check/acc l (- acc (check/acc r 0)))])) (define (check [t : (Tree Int)] -> Int) (check/acc t 0)) diff --git a/tapl/tests/run-all-mlish-tests.rkt b/tapl/tests/run-all-mlish-tests.rkt index 48fb42f..278a2da 100644 --- a/tapl/tests/run-all-mlish-tests.rkt +++ b/tapl/tests/run-all-mlish-tests.rkt @@ -11,3 +11,4 @@ (require "mlish/hash.mlish") ;(require "mlish/heapsort.mlish") (require "mlish/knuc.mlish") +(require "mlish/matrix.mlish")