diff --git a/collects/tests/typed-scheme/fail/back-and-forth.ss b/collects/tests/typed-scheme/fail/back-and-forth.ss new file mode 100644 index 00000000..3144b9a3 --- /dev/null +++ b/collects/tests/typed-scheme/fail/back-and-forth.ss @@ -0,0 +1,18 @@ +#; +(exn-pred exn:fail:contract? #rx".*contract \\(-> number\\? number\\?\\).*") + +#lang scheme/load + +(module m typed-scheme + (: f (Number -> Number)) + (define (f x) (add1 x)) + (provide f)) + +(module n scheme + (require 'm) + (f 'foo)) + +(module o typed-scheme + (require 'n)) + +(require 'o) \ No newline at end of file diff --git a/collects/tests/typed-scheme/fail/cnt-err1.ss b/collects/tests/typed-scheme/fail/cnt-err1.ss new file mode 100644 index 00000000..fa236bc8 --- /dev/null +++ b/collects/tests/typed-scheme/fail/cnt-err1.ss @@ -0,0 +1,28 @@ +#; +(exn-pred exn:fail:contract? ".*expected .*") + +#lang scheme/load + +(module tree typed-scheme + (define-type-alias Tree (Rec T (U (Pair T T) Number))) + + (: tree-sum (Tree -> Number)) + (define (tree-sum t) + (cond + [(number? t) t] + [else (+ (tree-sum (car t)) + (tree-sum (cdr t)))])) + + (provide tree-sum)) + +(module client scheme + (require 'tree) + (define (try-it bad?) + (if bad? + (tree-sum (cons 5 #f)) + (tree-sum (cons 5 6)))) + (provide try-it)) + +(require 'client) + +(try-it #t) \ No newline at end of file diff --git a/collects/tests/typed-scheme/fail/gadt.ss b/collects/tests/typed-scheme/fail/gadt.ss new file mode 100644 index 00000000..cc3458b6 --- /dev/null +++ b/collects/tests/typed-scheme/fail/gadt.ss @@ -0,0 +1,22 @@ +#lang typed-scheme +#| +data Exp a = +Num :: Int -> Exp Int +Sum :: Int -> Int -> Exp Int +Zero :: Exp Int -> Exp Bool +|# +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias top Any) + +#;(define-typed-struct (a) Exp ([flag : a])) +(define-typed-struct (a) Num ([v : number])) +(define-typed-struct (a) Zero ([e : (Un (Num number) (Zero number))])) + +(define-type-alias (Expr a) (Un (Num a) (Zero a))) + +(pdefine: (a) (ev [x : (Expr a)]) : a + (cond + [(Num? x) (Num-v x)] + [(Zero? x) (= 0 #{(#{ev :: (All (b) ((Expr b) -> b))} #{(Zero-e x) :: (Expr number)}) :: number})])) + diff --git a/collects/tests/typed-scheme/fail/set-struct.ss b/collects/tests/typed-scheme/fail/set-struct.ss new file mode 100644 index 00000000..35198dd0 --- /dev/null +++ b/collects/tests/typed-scheme/fail/set-struct.ss @@ -0,0 +1,14 @@ +#; +(exn-pred exn:fail:syntax? ".*unbound.*") + + +#lang typed-scheme + +(define-typed-struct A ([x : Number] [y : Boolean])) + +(define: (f [a : A]) : Number + (set-A-x! a 4) + (set-A-y! a #f) + (+ 4 (A-x a))) + +(display (f (make-A 11 #t))) diff --git a/collects/tests/typed-scheme/fail/set-tests.ss b/collects/tests/typed-scheme/fail/set-tests.ss new file mode 100644 index 00000000..bd359d04 --- /dev/null +++ b/collects/tests/typed-scheme/fail/set-tests.ss @@ -0,0 +1,9 @@ +;; should FAIL! + +#lang typed-scheme + +(let*: ((x : Any 1) + (f : (-> Void) (lambda () (set! x (quote foo))))) + (if (number? x) (begin (f) (add1 x)) 12)) + + \ No newline at end of file diff --git a/collects/tests/typed-scheme/main.ss b/collects/tests/typed-scheme/main.ss new file mode 100644 index 00000000..ad71d913 --- /dev/null +++ b/collects/tests/typed-scheme/main.ss @@ -0,0 +1,81 @@ +#lang scheme/base + +(provide go) + +(require (planet schematics/schemeunit/test) + (planet schematics/schemeunit/text-ui) + (planet schematics/schemeunit/graphical-ui) + mzlib/etc + scheme/match + "unit-tests/all-tests.ss") + +(define (scheme-file? s) + (regexp-match ".*[.](ss|scm)" (path->string s))) + +(define-namespace-anchor a) + +(define (exn-matches . args) + (values + (lambda (val) + (and (exn? val) + (for/and ([e args]) + (if (procedure? e) + (e val) + (begin + (regexp-match e (exn-message val))))))) + args)) + +(define (exn-pred p) + (let ([sexp (with-handlers + ([values (lambda _ #f)]) + (let ([prt (open-input-file p)]) + (begin0 (begin (read-line prt 'any) + (read prt)) + (close-input-port prt))))]) + (match sexp + [(list-rest 'exn-pred e) + (eval `(exn-matches . ,e) (namespace-anchor->namespace a))] + [_ (exn-matches ".*typecheck.*" exn:fail:syntax?)]))) + +(define (mk-tests dir loader test) + (lambda () + (define path (build-path (this-expression-source-directory) dir)) + (define tests + (for/list ([p (directory-list path)] + #:when (scheme-file? p)) + (test-case + (path->string p) + (test + (build-path path p) + (lambda () + (parameterize ([read-accept-reader #t] + [current-load-relative-directory + path]) + (with-output-to-file "/dev/null" #:exists 'append + (lambda () (loader p))))))))) + (apply test-suite dir + tests))) + +(define succ-tests (mk-tests "succeed" + (lambda (p) (dynamic-require `(file ,(path->string p)) #f)) + (lambda (p thnk) (check-not-exn thnk)))) +(define fail-tests (mk-tests "fail" + (lambda (p) (dynamic-require `(file ,(path->string p)) #f)) + (lambda (p thnk) + (define-values (pred info) (exn-pred p)) + (with-check-info + (['predicates info]) + (check-exn pred thnk))))) + +(define int-tests + (test-suite "Integration tests" + (succ-tests) + (fail-tests))) + +(define tests + (test-suite "Typed Scheme Tests" + unit-tests int-tests)) + +(define (go) (test/graphical-ui tests)) + + diff --git a/collects/tests/typed-scheme/succeed/annotation-test.ss b/collects/tests/typed-scheme/succeed/annotation-test.ss new file mode 100644 index 00000000..c8432328 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/annotation-test.ss @@ -0,0 +1,12 @@ +#lang typed-scheme +(define-type-alias top2 Any) + +(define: (x) : Number 23) + +(let: ([y : top2 x]) + y) + +(let: ([z : Number 4]) + #{z :: top2}) + +#{(x) :: top2} diff --git a/collects/tests/typed-scheme/succeed/area.ss b/collects/tests/typed-scheme/succeed/area.ss new file mode 100644 index 00000000..b37407c5 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/area.ss @@ -0,0 +1,11 @@ +#lang typed-scheme +(define-typed-struct rectangle ([width : Number] [height : Number])) +(define-typed-struct circle ([radius : Number])) + +(define-type-alias shape (U rectangle circle)) + +(define: (area [sh : shape]) : Number + (cond [(circle? sh) + (* (ann 3.1416 : Number) (circle-radius sh) (circle-radius sh))] + [else + (* (rectangle-width sh) (rectangle-height sh))])) diff --git a/collects/tests/typed-scheme/succeed/bad-map-infer.ss b/collects/tests/typed-scheme/succeed/bad-map-infer.ss new file mode 100644 index 00000000..9ce634cb --- /dev/null +++ b/collects/tests/typed-scheme/succeed/bad-map-infer.ss @@ -0,0 +1,5 @@ +#lang typed-scheme + +(: cross1 ((Listof Number) -> (Listof Number))) +(define (cross1 m) + (map (lambda: ([m1 : Number]) #{(error 'bad) :: Number}) m)) \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/barland.ss b/collects/tests/typed-scheme/succeed/barland.ss new file mode 100644 index 00000000..52e41e04 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/barland.ss @@ -0,0 +1,29 @@ +#lang typed-scheme +(define-type-alias top Any) +(define-type-alias set (top -> top)) + +(define: (autos [elt : top]) : top (memq elt '(vw saab bmw audi))) + +(define: (element-of? [elt : top] [s : set]) : top (s elt)) + +(define: (evens [elt : top]) : top (and (number? elt) (even? elt))) + +(define-typed-struct pr ([fst : top] [snd : top])) + +#;(define: (length=2? [any : top]) : boolean +(and (pair? any) + (pair? (cdr any)) + (empty? (cdr (cdr any))))) + +(define: (cartesian-product [A : set] [B : set]) : set + (lambda: ([elt : top]) + (and (pr? elt) + (element-of? (pr-fst elt) A) + (element-of? (pr-snd elt) B)))) + + + +(define: evenEuroCars : set (cartesian-product evens autos)) +#;(display (element-of? (make-pr 4 'bmw) evenEuroCars)) ; = #t +#;(display (element-of? (make-pr 'bmw 4) evenEuroCars)) ; = #f + diff --git a/collects/tests/typed-scheme/succeed/basic-tests.ss b/collects/tests/typed-scheme/succeed/basic-tests.ss new file mode 100644 index 00000000..8ca4f27a --- /dev/null +++ b/collects/tests/typed-scheme/succeed/basic-tests.ss @@ -0,0 +1,100 @@ +#lang typed-scheme +;;syntax-only requires +(require (only-in (lib "etc.ss") let+)) +(require (only-in (lib "match.ss") match)) + +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias top Any) + + ;(provide (all-defined)) +(define: x* : Number 3) + +(define #{x** : number} 3) + +#{(and 3 4) :: (Un boolean number)} +#{(and 3 4) :: (Un boolean number)} + +#;(define: match-test : number +(match 3 + [(? number? #{x number}) (+ 17 x)] + [_ 12])) + + +(define-typed-struct pt ([x : Number] [y : number])) + +(define-typed-struct (3dpt pt) ([z : number])) + +(define: x-struct : pt (make-pt 3 4)) + +(define: z-struct : 3dpt (make-3dpt 3 4 5)) + +(define: z*-struct : pt z-struct) + +(define: x-mem : number (pt-x x-struct)) + +(define: (pt-add [v : top]) : number + (cond + [(pt? v) (+ (pt-x v) (pt-y v))] + [else 0])) + +(define: (zpt-add [v : top]) : number + (cond + [(3dpt? v) (+ (pt-x v) (pt-y v))] + [else 0])) + +#;(define: (pt-add/match [v : top]) : number +(match v + [($ pt #{x number} #{y number}) (+ x y)] + [_ 0])) + +#;(pt-add/match x-struct) + +#;(define-typed-struct pt ([z number])) + +;; this had better not work +#;(define: pt-unsound : boolean +(cond [(pt? x-struct) (= (pt-z x-struct))] + [else #t])) + +(define: a-bool : boolean (pt? 6)) + +(define: blarz : number + (let*: ([x : number 3] + [y : number (+ x 1)]) + (add1 y))) + +(define: looping : number + (let: loop : number ([a : number 1] [b : number 10]) (if (> a b) 1000 (loop (add1 a) (sub1 b))))) + +#;(make-pt 'x 'y) + +(define: x : number 3) +(add1 x) +#;(define-syntax foo +(syntax-rules () + [(foo x1 y1) (= x1 y1)])) + +(define: (f [x : number] [y : number]) : number (+ x y)) +(define: (g [x : number] [y : number]) : boolean + (let+ (#;[val #{z number} #f] + [val #{x1 number} (* x x)] + [rec #{y1 number} (* y y)]) + #|(define-syntax foo + (syntax-rules () + [(foo) (= x1 y1)])) + (foo)|# + (= x1 y1))) +(g (if (g (add1 x) (add1 (add1 x))) 10 100) 30) + +(map (lambda: ([e : Number]) e) (list 1 2 3)) + + +(define: mymap : (All (a b) ((a -> b) (Listof a) -> (Listof b))) + (plambda: (a b) ([f : (a -> b)] [l : (Listof a)]) + (cond [(null? l) '()] + [else (cons (f (car l)) + (mymap f (cdr l)))]))) + +(mymap add1 (cons 1 (cons 2 (cons 3 #{'() :: (Listof number)})))) + diff --git a/collects/tests/typed-scheme/succeed/batched-queue.scm b/collects/tests/typed-scheme/succeed/batched-queue.scm new file mode 100644 index 00000000..71e1db34 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/batched-queue.scm @@ -0,0 +1,86 @@ +#lang typed-scheme +;; CHANGES +;; added annotations on all bound variables and structs +;; require typed foldl +;; made empty into a nullary function +;; added annotations on empty lists +;; added annotation on use of polymorphic functions in higher-order contexts + +;; fixme -- how do we require polymorphic functions? +#;(require (only (lib "list.ss") foldl)) +#;(require (only "typed-list.ss" foldl)) + +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias top Any) + +(define-typed-struct (a) queue ([front : (Listof a)] [rear : (Listof a)])) + + ; Invariants + ; 1. q empty <=> (null? (queue-front q)) + ; 2. elements of q = (append (queue-front q) (reverse (queue-rear q))) + + +;; fixme -- shouldn't have to be a function +(pdefine: (a) (empty) : (queue a) (make-queue #{'() :: (Listof a)} #{'() :: (Listof a)})) + +(pdefine: (a) (empty? [q : (queue a)]) : boolean + (null? (queue-front q))) + +(pdefine: (a) (insert-last [x : a] [q : (queue a)]) : (queue a) + (let ([front (queue-front q)]) + (if (null? front) + (make-queue (cons x front) '()) + (make-queue front (cons x (queue-rear q)))))) + +(define: insert : (All (a) (a (queue a) -> (queue a))) insert-last) + +(pdefine: (a) (insert* [xs : (Listof a)] [q : (queue a)]) : (queue a) + ;; fixme - annoying annotation + (foldl #{insert :: (a (queue a) -> (queue a))} q xs)) + +(pdefine: (a) (remove-first [q : (queue a)]) : (queue a) + (let ([front (queue-front q)]) + (if (null? front) + (error 'remove-first "can't remove element from empty queue; given " q) + (if (null? (cdr front)) + (make-queue (reverse (queue-rear q)) '()) + (make-queue (cdr front) (queue-rear q)))))) + +(pdefine: (a) (first+remove [q : (queue a)]) : (values a (queue a)) + (let ([front (queue-front q)]) + (if (null? front) + (error 'remove-first "can't remove element from empty queue; given " q) + (values (car front) + (if (null? (cdr front)) + (make-queue (reverse (queue-rear q)) '()) + (make-queue (cdr front) (queue-rear q))))))) + +(define: -remove : (All (a) ((queue a) -> (queue a))) remove-first) + +(pdefine: (a) (first [q : (queue a)]) : a + (when (empty? q) + (error 'first "There is no first element in an empty queue; given " q)) + (car (queue-front q))) + +(pdefine: (a) (elements: [q : (queue a)]) : (Listof a) + (append (queue-front q) + (reverse (queue-rear q)))) + +(pdefine: (a b) (fold [f : (a b -> b)] [init : b] [q : (queue a)]) : b + (foldl f + (foldl f init (queue-front q)) + (reverse (queue-rear q)))) + +(pdefine: (a) (size [q : (queue a)]) : number + ; NOTE: T(size) = O(n) + (+ (length (queue-front q)) + (length (queue-rear q)))) + +;; 12 definitions checked +;; generators removed + +;; TESTS + +(= 0 (size (empty))) + diff --git a/collects/tests/typed-scheme/succeed/broken-let-syntax.ss b/collects/tests/typed-scheme/succeed/broken-let-syntax.ss new file mode 100644 index 00000000..4fd593c9 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/broken-let-syntax.ss @@ -0,0 +1,8 @@ +#lang typed-scheme + +(let: ([x : Number 1]) + (let-syntax ([m (syntax-rules () + [(_) x])]) + (m))) + + \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/cl-tests.ss b/collects/tests/typed-scheme/succeed/cl-tests.ss new file mode 100644 index 00000000..06216592 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/cl-tests.ss @@ -0,0 +1,35 @@ +#lang typed-scheme +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias top Any) + +(define: a : (number -> number) (lambda: ([x : number]) x)) +(define: f : (case-lambda (number -> number) + (boolean boolean -> boolean)) + (case-lambda + [(#{x : number}) (add1 x)] + [(#{a : boolean} #{b : boolean}) (and a b)])) + +(define: f* : (case-lambda (number -> number) + (boolean boolean -> boolean)) + (case-lambda: + [([x : number]) (add1 x)] + [([a : boolean] [b : boolean]) (and a b)])) + +(f 5) + +(f #t #f) + +#;(f #t) + +(define-type-alias idfunty (All (a) (a -> a))) +(define-type-alias (idfunty2 a) (a -> a)) + +(define: g : (idfunty number) (lambda: ([x : number]) x)) + +(define: (h [f : (idfunty number)]) : number (f 5)) +(define: (h* [f : (idfunty2 number)]) : number (f 5)) + +(h f*) +(h* f*) + diff --git a/collects/tests/typed-scheme/succeed/cl.ss b/collects/tests/typed-scheme/succeed/cl.ss new file mode 100644 index 00000000..f7acfb1b --- /dev/null +++ b/collects/tests/typed-scheme/succeed/cl.ss @@ -0,0 +1,8 @@ +#lang typed-scheme +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias top Any) + +(define: f : (case-lambda [number -> number] [boolean boolean -> boolean]) + (case-lambda [(#{a : number}) a] + [(#{b : boolean} #{c : boolean}) (and b c)])) diff --git a/collects/tests/typed-scheme/succeed/do.ss b/collects/tests/typed-scheme/succeed/do.ss new file mode 100644 index 00000000..61cbea4e --- /dev/null +++ b/collects/tests/typed-scheme/succeed/do.ss @@ -0,0 +1,17 @@ +#lang typed-scheme + +(define-type-alias Nb Number) + +(let: ([x : Nb 3]) x) + +(let ([x '(1 3 5 7 9)]) + (let: doloop : Nb + ([x : (Listof Nb) x] + [sum : Number 0]) + (if (null? x) sum + (doloop (cdr x) (+ sum (car x)))))) + +(let ((x '(1 3 5 7 9))) + (do: : Nb ((x : (Listof Nb) x (cdr x)) + (sum : Number 0 (+ sum (car x)))) + ((null? x) sum))) diff --git a/collects/tests/typed-scheme/succeed/fix.ss b/collects/tests/typed-scheme/succeed/fix.ss new file mode 100644 index 00000000..c6294aa9 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/fix.ss @@ -0,0 +1,15 @@ +#lang typed-scheme + +(: make-recursive : (All (S T) (((S -> T) -> (S -> T)) -> (S -> T)))) +(define (make-recursive f) + (define-type-alias Tau (Rec Tau (Tau -> (S -> T)))) + ((lambda: ([x : Tau]) (f (lambda: ([z : S]) ((x x) z)))) + (lambda: ([x : Tau]) (f (lambda: ([z : S]) ((x x) z)))))) + +(: fact : (Number -> Number)) +(define fact (make-recursive + (lambda: ([fact : (Number -> Number)]) + (lambda: ([n : Number]) + (if (zero? n) + 1 + (* n (fact (- n 1)))))))) diff --git a/collects/tests/typed-scheme/succeed/foo.scm b/collects/tests/typed-scheme/succeed/foo.scm new file mode 100644 index 00000000..44074e0d --- /dev/null +++ b/collects/tests/typed-scheme/succeed/foo.scm @@ -0,0 +1,48 @@ +#lang scheme/load +(module m mzscheme + (define x 3) + (define (y z) (add1 z)) + (provide (all-defined))) + +(module bang-tests typed-scheme + (define: x : Number 1) + x + (provide x) + (set! x 4) + (when #t 3)) + + +(module trequire typed-scheme + (require 'bang-tests) + (define: y : Number x)) + +(module require-tests typed-scheme + (provide z) + (require/typed x Number 'm) + (+ x 3) + (require/typed y (Number -> Number) 'm) + (define: z : Number (y (+ x 4)))) + + +(module provide-type typed-scheme + (define-type-alias top2 Any) + + (define-typed-struct (a) container ([v : a])) + + (container-v (make-container 3)) + + (provide top2 container container-v make-container) + ) + +(module require-type typed-scheme + (require 'provide-type) + + (let: ([x : top2 3]) + x) + + (define: (f [x : (container Number)]) : Number + (container-v x)) + + (f (make-container (ann 7 : Number))) + + ) diff --git a/collects/tests/typed-scheme/succeed/hw01.scm b/collects/tests/typed-scheme/succeed/hw01.scm new file mode 100644 index 00000000..617ecb59 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/hw01.scm @@ -0,0 +1,111 @@ +#lang typed-scheme + +(: sqr (Number -> Number)) +(define (sqr x) (* x x)) + +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) + +;(require "support.ss") + +;; --------------------------------------------------------------------- +;; 2a + +;; triangle: number number -> number +;; Calculates the area of a triange +(define: (triangle [b : number] [h : number]) : number + (* b (/ h 2))) + +;; tests: +(= 4 (triangle 2 4)) +(= 20 (triangle 5 8)) + +;; --------------------------------------------------------------------- +;; 2b + +;; total-profit: integer -> number +;; Calculates profit made by the theater +(define: (total-profit [people : number]) : number + (- (* people 5) + (+ (* people .5) 20))) + +;; tests: +(= -20 (total-profit 0)) +(= 25 (total-profit 10)) + +;; --------------------------------------------------------------------- +;; 3a + +;; interest: number ->number +;; Calculates interest for a given sum +(define: (interest [sum : number]) : number + (* sum + (cond [(<= sum 1000) .04] + [(<= sum 5000) .045] + [else .05]))) + +;; tests: +(= 0 (interest 0)) +(= 20 (interest 500)) +(= 40 (interest 1000)) +(= 112.5 (interest 2500)) +(= 500 (interest 10000)) + +;; --------------------------------------------------------------------- +;; 3b + +;; how-many: int int int -> int +;; Returns the number of roots in the equation +(define: (how-many [a : number] [b : number] [c : number]) : number + (cond [(> (sqr b) (* 4 a c)) 2] + [(< (sqr b) (* 4 a c)) 0] + [else 1])) + +;; tests: +(= 1 (how-many 1 2 1)) +(= 2 (how-many 1 3 1)) +(= 0 (how-many 1 1 1)) + +;; --------------------------------------------------------------------- +;; 4 + +;; what-kind: int int int -> symbol +;; Determines the type of the eqation +(define: (what-kind [a : number] [b : number] [c : number]) : symbol + (cond [(= a 0) 'degenerate] + [(> (sqr b) (* 4 a c)) 'two] + [(< (sqr b) (* 4 a c)) 'none] + [else 'one])) + +;; tests: +(eq? 'one (what-kind 1 2 1)) +(eq? 'two (what-kind 1 3 1)) +(eq? 'none (what-kind 1 1 1)) +(eq? 'degenerate (what-kind 0 1 1)) + +;; --------------------------------------------------------------------- +;; 5 + +;; list-length: (list-of any) -> integer +;; Computes the lenght of a list +(define: (list-length [loa : (Listof top)]) : number + (if (null? loa) + 0 + (+ 1 (list-length (cdr loa))))) + +#| tail recursive version: +(define (list-length-helper loa acc) + (if (null? loa) + acc + (list-length-helper (cdr loa) (+ acc 1)))) +(define (list-length loa) + (list-length-helper loa 0)) +|# + + ;; tests: + (= 0 (list-length '())) + (= 2 (list-length '(1 2))) + (= 3 (list-length '(1 2 (1 2 3 4)))) + \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/if-splitting-test.ss b/collects/tests/typed-scheme/succeed/if-splitting-test.ss new file mode 100644 index 00000000..802d7067 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/if-splitting-test.ss @@ -0,0 +1,13 @@ +#lang typed-scheme +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) +(define-type-alias list-of Listof) +(define: l : (list-of number) + (cons 1 (cons 2 (cons 3 #{'() : (list-of number)})))) + +(define: (g [x : number]) : number + (cond [(memv x l) => car] + [else 0])) + diff --git a/collects/tests/typed-scheme/succeed/leftist-heap.ss b/collects/tests/typed-scheme/succeed/leftist-heap.ss new file mode 100644 index 00000000..b5bf4128 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/leftist-heap.ss @@ -0,0 +1,302 @@ +;;; leftist-heap.scm -- Jens Axel Søgaard -- 28th dec 2005 + +;;; LEFTIST HEAP [Okasaki, p.17-20] + +; A *Leftist heap* is a heap-ordered binary tree with the /leftist property/: +; The rank of any left child is at least as large as the rank of its right sibling. +; The *rank* of a node is the length of the its *right spine*, which is the +; rightmost path from the node to an empty node. + +;;; Time worst case +; delete-min O(log n) +; empty O(1) +; empty? O(1) +; find-min O(1) +; insert O(log n) +; union O(log n) + +;;; changes +;; annotations +;; foldl from typed-list +;; eta-expand cons (line 193) +;; added error case for one-armed if +;; need rest args +;; didn't attempt generators + +;#reader (planet "typed-reader.ss" ("plt" "typed-scheme.plt")) +;(module leftist-heap (planet "typed-scheme.ss" ("plt" "typed-scheme.plt" 3 0)) +;(module leftist-heap mzscheme + +#lang typed-scheme +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) +(define-type-alias list-of Listof) +(require + (except-in (lib "67.ss" "srfi") current-compare =? number)) + + ;; fixme - type aliases should work in require + + (require/typed current-compare (-> (top top -> number)) (lib "67.ss" "srfi")) + (require/typed =? ((top top -> number) top top -> boolean) (lib "67.ss" "srfi")) + (require/typed number) top top -> boolean) (lib "67.ss" "srfi")) + + ;;; DATA DEFINITION + + ; A HEAP is either + ; (make-heap-empty cmp) + ; or + ; (make-heap-node cmp rank elm left right) + ; where + ; cmp is a compare function, + ; rank is an integer, and + ; left and right are heaps. + + (define-typed-struct heap ([compare : comparator])) + (define-typed-struct (heap-empty heap) ()) + (define-typed-struct (a) (heap-node heap) + ([rank : number] [elm : a] [left : (Un (heap-node a) heap-empty)] [right : (Un (heap-node a) heap-empty)])) + + (define-type-alias (Heap a) (Un (heap-node a) heap-empty)) + + ;;; CORE HEAP OPERATIONS + + ;; FIXME + (: empty (All (a) (case-lambda (-> (Heap a)) (comparator -> (Heap a))))) + (define empty + (case-lambda + [() (make-heap-empty (current-compare))] + [(cmp) (make-heap-empty cmp)])) + + (define: empty? : (pred heap-empty) heap-empty?) + + (pdefine: (a) (rank [h : (Heap a)]) : number + (if (empty? h) + 0 + (heap-node-rank h))) + + (pdefine: (a) (make [x : a] [a : (Heap a)] [b : (Heap a)]) : (Heap a) + (let ([ra (rank a)] + [rb (rank b)] + [cmp (heap-compare a)]) + (if (>= ra rb) + (make-heap-node cmp (add1 rb) x a b) + (make-heap-node cmp (add1 ra) x b a)))) + + (pdefine: (a) (union [h1 : (Heap a)] [h2 : (Heap a)]) : (Heap a) + (cond + [(empty? h1) h2] + [(empty? h2) h1] + [else (let*: (;; added new bindings at simpler types + [h1 : (heap-node a) h1] + [h2 : (heap-node a) h2] + [x : a (heap-node-elm h1)] ;; FIXME - FUCK FUCK FUCK - why not x? + [y : a (heap-node-elm h2)]) + (if<=? ((heap-compare h1) x y) + (make x (heap-node-left h1) (union (heap-node-right h1) h2)) + (make y (heap-node-left h2) (union h1 (heap-node-right h2)))))])) + + (pdefine: (a) (insert [x : a] [h : (Heap a)]) : (Heap a) + (let: ([cmp : comparator (heap-compare h)]) + (union (make-heap-node cmp 1 x (make-heap-empty cmp) (make-heap-empty cmp)) + h))) + + ;; No changes other than variable annotations + (pdefine: (a) (delete [x : a] [h : (Heap a)]) : (Heap a) + (define: (delete/sf [x : a] [h : (Heap a)] [s : ((Heap a) -> (Heap a))] [f : (-> (Heap a))]) : (Heap a) + (cond + [(empty? h) + (s h)] + [(=? (heap-compare h) x (heap-node-elm h)) + (s (union (heap-node-left h) (heap-node-right h)))] + [( (Heap a))] [f : (-> (Heap a))]) : (Heap a) + (cond + [(empty? h) + (s h)] + [(=? (heap-compare h) x (heap-node-elm h)) + (s (union (delete-all x (heap-node-left h)) + (delete-all x (heap-node-right h))))] + [( a)] [f : (-> (Un #f a))]) : (Un #f a) + (if (empty? h) + (f) + (if=? (cmp x (heap-node-elm h)) + (s (heap-node-elm h)) + (inner-get (heap-node-left h) s + (lambda () (inner-get (heap-node-right h) s + f)))))) + (inner-get h (lambda: ([x : a]) x) (lambda () #f)))) + + ;;; + ;;; EXTRA OPERATIONS + ;;; + + (pdefine: (a) (delete* [xs : (list-of a)] [h : (Heap a)]) : (Heap a) + (foldl {ann delete : (a (Heap a) -> (Heap a))} h xs)) + + (pdefine: (a r) (fold [f : (a r -> r)] [b : r] [h : (Heap a)]) : r + (if (empty? h) + b + (fold f + (fold f + (f (heap-node-elm h) b) + (heap-node-left h)) + (heap-node-right h)))) + + ;; FIXME + (pdefine: (a) (elements [h : (Heap a)]) : (list-of a) + (fold (lambda: ([x : a] [l : (list-of a)]) (cons x l)) + #;#{cons : (a (list-of a) -> (list-of a))} + #{'() :: (list-of a)} h)) + + (pdefine: (a) (count [x : a] [h : (Heap a)]) : number + (let ([cmp (heap-compare h)]) + (fold (lambda: ([y : a] [s : number]) + (if=? (cmp x y) + (add1 s) + s)) + 0 h))) + + (define: list->heap : (All (a) (case-lambda (comparator (list-of a) -> (Heap a)) ((list-of a) -> (Heap a)))) + ; time: O(n) + (pcase-lambda: (a) + [([l : (list-of a)]) (list->heap (current-compare) l)] + [([cmp : comparator] [l : (list-of a)]) + (let* ([e (empty cmp)] + [hs (map (lambda: ([x : a]) (insert x e)) l)]) + ; (list heap) -> (list heap) + ; merge adjacent pairs of heaps + (define: (merge-pairs [hs : (list-of (Heap a))]) : (list-of (Heap a)) + (cond + [(or (null? hs) + (null? (cdr hs))) hs] + [else + (cons (union (car hs) (cadr hs)) + (merge-pairs (cddr hs)))])) + (if (null? hs) + e + (let: loop : (Heap a) ([hs : (list-of (Heap a)) hs]) + ; merge adjacent pairs of heaps until one is left + (cond + [(null? hs) (error 'never-happen)] + [(null? (cdr hs)) (car hs)] + [else (loop (merge-pairs hs))]))))])) + + ;; FIXME - moved to after list->heap + (pdefine: (a) (-heap . [xs : a]) : (Heap a) + (list->heap xs)) + + + (pdefine: (a) (insert* [xs : (list-of a)] [h : (Heap a)]) : (Heap a) + (union (list->heap (heap-compare h) xs) h)) + + ; select : set -> element + (pdefine: (a) (select [s : (Heap a)]) : a + (if (empty? s) + (error 'select "can't select an element from an empty heap") + (find-min s))) + + (define: singleton : (All (a) (case-lambda (a -> (Heap a)) (comparator a -> (Heap a)))) + (pcase-lambda: (a) + [([x : a]) (insert x (#{empty @ a}))] + [([cmp : comparator] [x : a]) (insert x (make-heap-empty cmp))])) + + (pdefine: (a) (size [h : (Heap a)]) : number + ; NOTE: T(size)=O(n) + (cond + [(heap-empty? h) 0] + [else (+ (size (heap-node-left h)) + 1 + (size (heap-node-right h)))])) + + #| + ;;; + ;;; support for srfi-42 + ;;; + + (define-syntax heap-ec + (syntax-rules () + [(heap-ec cmp etc1 etc ...) + (fold-ec (empty cmp) etc1 etc ... insert)])) + + (define-syntax :heap + (syntax-rules (index) + ((:heap cc var (index i) arg) + (:parallel cc (:stack var arg) (:integers i)) ) + ((:heap cc var arg) + (:do cc + (let ()) + ((t arg)) + (not (empty? t)) + (let ((var (find-min t)))) + #t + ((delete-min t)) )))) + + (define (:heap-dispatch args) + (cond + [(null? args) + 'heap] + [(and (heap? (car args))) + (:generator-proc (:heap (car args)))] + [else + #f])) + + (:-dispatch-set! + (dispatch-union (:-dispatch-ref) :heap-dispatch)) + + |# + diff --git a/collects/tests/typed-scheme/succeed/let-values-tests.ss b/collects/tests/typed-scheme/succeed/let-values-tests.ss new file mode 100644 index 00000000..fe16662b --- /dev/null +++ b/collects/tests/typed-scheme/succeed/let-values-tests.ss @@ -0,0 +1,26 @@ +#lang typed-scheme +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) +(define-type-alias list-of Listof) +(let-values ([(#{x : number} #{y : number}) (values 3 4)] + [(#{z : number}) (values 3)] + #;[(#{fact : (number -> number)}) + (lambda: ([x : number]) + (if (zero? x) 1 (* x (fact (- x 1)))))] + #;[(#{z : number}) (- x y)]) + (+ x y)) + +(letrec-values ([(#{x : number} #{y : number}) (values 3 4)]) + (+ x y)) +(letrec-values ([(#{x : number} #{y : number}) (values 3 4)] + [(#{z : number}) (- x y)] + [(#{fact : (number -> number)}) + (lambda: ([x : number]) + (if (zero? x) 1 (* x (fact (- x 1)))))]) + (+ x y)) + +(define-values (#{x : number} #{y : number}) (values 1 2)) +#;(define-values (#{z : number}) (values 1 2)) + diff --git a/collects/tests/typed-scheme/succeed/little-schemer.ss b/collects/tests/typed-scheme/succeed/little-schemer.ss new file mode 100644 index 00000000..d363763f --- /dev/null +++ b/collects/tests/typed-scheme/succeed/little-schemer.ss @@ -0,0 +1,453 @@ +#lang typed-scheme +#;(require (lib "etc.ss")) +#;(require "prims.ss") +(require (lib "match.ss") + (for-syntax scheme/base)) + +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) +(define-type-alias list-of Listof) + +(define-type-alias atom (Un Number Symbol Boolean)) + +(define: atom? : (Any -> Boolean : atom) (lambda: ([v : Any]) (if (number? v) #t (if (symbol? v) #t (boolean? v))))) + +(define-syntax (cond* stx) + (syntax-case stx (else) + [(_ [pred expr id rhs] . rest) + #'(let ([id expr]) + (if (pred id) + rhs + (cond . rest)))] + [(_ [else . rest]) #'(begin . rest)] + [(_ [p . rhs] . rest) + #'(if p (begin . rhs) + (cond* . rest))])) + +(define-type-alias lat (list-of atom)) + +(define: (lat? [l : (list-of top)]) : boolean + (cond [(null? l) #t] + [(atom? (car l)) (lat? (cdr l))] + [else #f])) + +(define: (member? [a : atom] [l : lat]) : boolean + (cond + [(null? l) #f] + [else (or (equal? a (car l)) + (member? a (cdr l)))])) + +(define: (rember [a : symbol] [l : (list-of symbol)]) : (list-of symbol) + (cond + [(null? l) l] + [(eq? (car l) a) (cdr l)] + [else (cons (car l) (rember a (cdr l)))])) + +(define: (multisubst [new : symbol] [old : symbol] [lat : (list-of symbol)]) : (list-of symbol) + (cond + [(null? lat) lat] + [(eq? (car lat) old) (cons new (multisubst new old (cdr lat)))] + [else (cons (car lat) (multisubst new old (cdr lat)))])) + +(define: (tup+ [t1 : (list-of number)] [t2 : (list-of number)]) : (list-of number) + (cond + [(null? t1) t2] + [(null? t2) t1] + [else (cons (+ (car t1) (car t2)) + (tup+ (cdr t1) (cdr t2)))])) + +(define: (len [l : (list-of top)]) : number + (cond + [(null? l) 0] + [else (add1 (len (cdr l)))])) + +(define: (pick [n : number] [lat : (list-of symbol)]) : symbol + (cond + [(zero? (sub1 n)) (car lat)] + [else (pick (sub1 n) (cdr lat))])) + +(define: (no-nums [lat : (list-of atom)]) : (list-of atom) + (cond + [(null? lat) lat] + [(number? (car lat)) (no-nums (cdr lat))] + [else (cons (car lat) (no-nums (cdr lat)))])) + +(define: (one? [n : number]) : boolean + (= n 1)) + +(define: (rempick [n : number] [lat : (list-of atom)]) : (list-of atom) + (cond + [(one? n) (cdr lat)] + [else (cons (car lat) + (rempick (sub1 n) (cdr lat)))])) + +(define: (foo2 [x : top]) : boolean + (if (number? x) (= x x) #f)) + +;; doesn't work because of and! - bug in type system +(define: (eqan? [a1 : top] [a2 : top]) : boolean + (cond [(and (number? a1) (number? a2)) (= a1 a2)] + [else (eq? a1 a2)])) + +(define: (occur [a : atom] [lat : (list-of atom)]) : number + (cond [(null? lat) 0] + [(eq? (car lat) a) (add1 (occur a (cdr lat)))] + [else (occur a (cdr lat))])) + +(define-type-alias SExp (mu x (U atom (Listof x)))) + + +;; (atom? (car l)) doesn't do anything - bug in type system +#;(define: (rember* [a : atom] [l : (list-of SExp)]) : (list-of SExp) +(cond + [(null? l) l] + [(atom? (car l)) + (cond [(eq? (car l) a) (rember* a (cdr l))] + [else (cons (car l) (rember* a (cdr l)))])] + [else (cons (rember* a (car l)) (rember* a (cdr l)))])) + +(define: (rember* [a : atom] [l : (list-of SExp)]) : (list-of SExp) + (cond + [(null? l) l] + [else + (let ([c (car l)]) + (cond + [(atom? c) + (cond [(eq? c a) (rember* a (cdr l))] + [else (cons c (rember* a (cdr l)))])] + [else (cons (rember* a c) (rember* a (cdr l)))]))])) + +(define: (insertR* [new : atom] [old : atom] [l : (list-of SExp)]) : (list-of SExp) + (cond + [(null? l) l] + [else + (let ([c (car l)]) + (cond + [(atom? c) + (cond + [(eq? c old) + (cons old (cons new (insertR* new old (cdr l))))] + [else + (cons c + (insertR* new old (cdr l)))])] + [else (cons (insertR* new old c) + (insertR* new old (cdr l)))]))])) + +(define: (occur* [a : atom] [l : (list-of SExp)]) : number + (cond* + [(null? l) 0] + [atom? (car l) c + (cond [(eq? c a) (add1 (occur* a (cdr l)))] + [else (occur* a (cdr l))])] + [else (+ (occur* a c) + (occur* a (cdr l)))])) + +(define: (member* [a : atom] [l : (list-of SExp)]) : boolean + (cond* + [(null? l) #f] + [atom? (car l) c + (or (eq? a c) (member* a (cdr l)))] + [else (or (member* a c) (member* a (cdr l)))])) + +(define: (^ [n : number] [m : number]) : number + (if (= m 0) 1 (* n (^ n (sub1 m))))) + +(define: (1st-sub-exp [ae : (list-of SExp)]) : SExp + (car ae)) + +(define: (2nd-sub-exp [ae : (list-of SExp)]) : SExp + (car (cdr (cdr ae)))) + +(define: (operator [ae : (list-of SExp)]) : SExp + (car (cdr ae))) + +(define-type-alias num-exp (Rec N (U Number (List N (U '+ '* '^) N)))) + +(define: (value [nexp : num-exp]) : number + (cond + [(atom? nexp) nexp] + [(eq? (car (cdr nexp)) '+) + (+ (value (car nexp)) + (value (car (cdr (cdr nexp)))))] + [(eq? (car (cdr nexp)) '*) + (* (value (car nexp)) + (value (car (cdr (cdr nexp)))))] + [else + (^ (value (car nexp)) + (value (car (cdr (cdr nexp)))))] + )) + +#;(define-type aexp (Un atom (list-of aexp))) + +(define: (set? [l : (list-of atom)]) : boolean + (cond + [(null? l) #t] + [(member? (car l) (cdr l)) #f] + [else (set? (cdr l))])) + +(define: (multirember [a : atom] [l : (list-of atom)]) : (list-of atom) + (cond + [(null? l) l] + [(equal? a (car l)) (multirember a (cdr l))] + [else (cons (car l) (multirember a (cdr l)))])) + +(define: (makeset [l : lat]) : lat + (cond + [(null? l) l] + [else (cons (car l) + (makeset (multirember (car l) (cdr l))))])) + +(define: (subset? [set1 : lat] [set2 : lat]) : boolean + (cond + [(null? set1) #t] + [(member? (car set1) set2) + (subset? (cdr set1) set2)] + [else #f])) + +(define: (subset2? [set1 : (list-of atom)] [set2 : (list-of atom)]) : boolean + (cond + [(null? set1) #t] + [else (and (member? (car set1) set2) + (subset? (cdr set1) set2))])) + +(define: (intersect? [set1 : (list-of atom)] [set2 : (list-of atom)]) : boolean + (cond + [(null? set1) #t] + [else (or (member? (car set1) set2) + (intersect? (cdr set1) set2))])) + +(define: (eqset? [set1 : (list-of atom)] [set2 : (list-of atom)]) : boolean + (and (subset? set1 set2) (subset? set2 set1))) + +(define: (intersect [set1 : (list-of atom)] [set2 : (list-of atom)]) : (list-of atom) + (cond + [(null? set1) set1] + [(member? (car set1) set2) + (cons (car set1) (intersect (cdr set1) set2))] + [else (intersect (cdr set1) set2)]) + ) + +(define: (union [set1 : (list-of atom)] [set2 : (list-of atom)]) : (list-of atom) + (cond + [(null? set1) set2] + [(member? (car set1) set2) + (union (cdr set1) set2)] + [else (cons (car set1) (intersect (cdr set1) set2))]) + ) + +(define: (rember-f [test? : (atom atom -> boolean)] [a : atom] [l : (list-of atom)]) : (list-of atom) + (cond + [(null? l) l] + [(test? (car l) a) (cdr l)] + [else (cons (car l) (rember-f test? a (cdr l)))])) + +(define: (rember-f-curry [test? : (atom atom -> boolean)]) : (atom lat -> lat) + (lambda: ([a : atom] [l : (list-of atom)]) + (cond + [(null? l) l] + [(test? (car l) a) (cdr l)] + [else (cons (car l) ((rember-f-curry test?) a (cdr l)))]))) + +(define: eq?-c : (atom -> (atom -> boolean)) + (lambda: ([a : atom]) + (lambda: ([x : atom]) + (eq? x a)))) + +(define: (insertR-f [test? : (atom atom -> boolean)] [new : atom] [old : atom] [l : (list-of atom)]) : (list-of atom) + (cond + [(null? l) l] + [(test? (car l) old) + (cons old (cons new (cdr l)))] + [else (cons (car l) + (insertR-f test? new old (cdr l)))])) + +(define: (seqL [new : atom] [old : atom] [l : (list-of atom)]) : (list-of atom) + (cons new (cons old l))) + + +(define: (seqR [new : atom] [old : atom] [l : (list-of atom)]) : (list-of atom) + (cons old (cons new l))) + +(define: (insertR-g [seq : (atom atom lat -> lat)] + [test? : (atom atom -> boolean)] + [new : atom] [old : atom] [l : (list-of atom)]) + : (list-of atom) + (cond + [(null? l) l] + [(test? (car l) old) + (seq new old (cdr l))] + [else (cons (car l) + (insertR-g seq test? new old (cdr l)))])) + +(define: (insertR-g-curry [seq : (atom atom (list-of atom) -> (list-of atom))]) + : ((atom atom -> boolean) atom atom (list-of atom) -> (list-of atom)) + (lambda: ([test? : (atom atom -> boolean)] + [new : atom] [old : atom] [l : (list-of atom)]) + (cond + [(null? l) l] + [(test? (car l) old) + (seq new old (cdr l))] + [else (cons (car l) + ((insertR-g-curry seq) test? new old (cdr l)))]))) + +(define: (seqS [new : atom] [old : atom] [l : lat]) : lat + (cons new l)) + +#;(define: subst : ((atom atom -> boolean) atom atom (list-of atom) -> (list-of atom)) +(insertR-g-curry seqS)) + +(define: (atom->function [x : atom]) : (number number -> number) + (case x + [(+) +] + [(*) *] + [else ^])) + +;; doesn't work - is operator really a number? (bug in type system) +;; also infinite loops checking num-exp <: SExp +#;(define: (value-new [nexp : num-exp]) : number +(cond + [(number? nexp) nexp] + [else ((atom->function (operator nexp)) + (value-new (1st-sub-exp nexp)) + (value-new (2nd-sub-exp nexp)))])) + +(define: (multiremberT [test? : (atom -> boolean)] [l : (list-of atom)]) : (list-of atom) + (cond + [(null? l) l] + [(test? (car l)) (multiremberT test? (cdr l))] + [else (cons (car l) (multiremberT test? (cdr l)))])) + +(define: (build [a : SExp] [b : SExp]) : (list-of SExp) + (cons a (cons b '()))) + +(define: (first [pair : (list-of SExp)]) : SExp + (car pair)) + +(define: (second [pair : (list-of SExp)]) : SExp + (car (cdr pair))) + +;; need to specify more about the list in the type here - type system bug +#;(define: (shift [pair : (list-of SExp)]) : (list-of SExp) +(build (first (first pair)) + (build (second (first pair)) + (second pair)))) + +(define: (collatz [n : number]) : number + (cond [(one? n) 1] + [(even? n) (collatz (/ n 2))] + [else (collatz (add1 (* 3 n)))])) + + +(define: (ack [n : number] [m : number]) : number + (cond + [(zero? n) (add1 m)] + [(zero? m) (ack (sub1 n) 1)] + [else (ack (sub1 n) + (ack n (sub1 m)))])) + + + ;(define-type-alias entry (list-of (list-of atom))) + +(define: empty-atom : (list-of (list-of atom)) '()) + +;; FIXME +(define: mymap : (All (a b) ((a -> b) (list-of a) -> (list-of b))) + (plambda: (a b) ([f : (a -> b)] [l : (list-of a)]) + (cond [(null? l) '()] + [else (cons (f (car l)) + (mymap f (cdr l)))]))) + +(mymap add1 (cons 1 (cons 2 (cons 3 '())))) + +(define-type-alias entry (list-of lat)) + +(define-type-alias table (list-of entry)) + + +(define: (new-entry [keys : (list-of atom)] + [vals : (list-of atom)]) : entry + (cons keys (cons vals empty-atom))) + +(define: (numbered? [aexp : num-exp]) : boolean + (cond + [(number? aexp) #t] + [(atom? aexp) #f] + [else (and (numbered? (car aexp)) + (numbered? (car (cdr (cdr aexp)))))])) + +(define: (lookup-in-entry-help [name : atom] [names : (list-of atom)] [values : (list-of atom)] [entry-f : (atom -> atom)]) : atom + (cond [(null? names) (entry-f name)] + [(eq? (car names) name) (car values)] + [else (lookup-in-entry-help name (cdr names) (cdr values) entry-f)])) + +(define: (lookup-in-entry [name : atom] [e : entry] [fail : (atom -> atom)]) : atom + (lookup-in-entry-help name (car e) (car (cdr e)) fail)) + +(define: extend-table : (entry table -> table) #{cons @ entry Any}) + +(define: (lookup-in-table [name : atom] [t : table] [fail : (atom -> atom)]) : atom + (cond + [(null? t) (fail name)] + [else (lookup-in-entry + name + (car t) + (lambda: ([name : atom]) + (lookup-in-table name (cdr t) fail)))])) + +(define-type-alias action (atom table -> SExp)) + +(define: (*const [e : SExp] [t : table]) : SExp + (cond + [(number? e) e] + [(eq? e #t) #t] + [(eq? e #f) #f] + [else (build 'primitive e)])) + +(define: (initial-table [name : atom]) : atom + (error)) + +(define: (*identifier [e : atom] [tbl : table]) : SExp + (lookup-in-table e tbl initial-table)) + +(define: (atom->action [e : atom]) : action + (cond + [(number? e) *const] + #;[(string? e) (error "shouldn't get strings")] ;; FIXME - had to change the code + [else + (case e + [(#t #f cons car cdr null? eq? atom? zero? add1 sub1 number?) *const] + [else *identifier])])) + +(define: (*quote [a : atom] [t : table]) : SExp (error)) +(define: (*lambda [a : atom] [t : table]) : SExp (error)) +(define: (*cond [a : atom] [t : table]) : SExp (error)) +(define: (*application [a : atom] [t : table]) : SExp (error)) + +(define: (list->action [e : (list-of SExp)]) : action + (cond* + [atom? (car e) it + (case it + [(quote) *quote] + [(lambda) *lambda] + [(cond) *cond] + [else *application])] + [else *application])) + + +(define: (expression->action [e : SExp]) : action + (cond + [(atom? e) (atom->action e)] + [else (list->action e)])) + +#;(define: (meaning [e : SExp] [t : table]) : SExp +((expression->action e) e t)) + +#;(define: (value [e : SExp]) : SExp +(meaning e '())) + +#;(provide (all-defined)) + + + diff --git a/collects/tests/typed-scheme/succeed/manual-examples.ss b/collects/tests/typed-scheme/succeed/manual-examples.ss new file mode 100644 index 00000000..47e60d8d --- /dev/null +++ b/collects/tests/typed-scheme/succeed/manual-examples.ss @@ -0,0 +1,74 @@ +#lang scheme/load +(module tlang mzscheme + (require (prefix tl: typed-scheme)) + (provide (all-from typed-scheme))) + + +(module even-odd typed-scheme + (define: (my-odd? [n : Number]) : Boolean + (if (zero? n) #f + (my-even? (- n 1)))) + + (define: (my-even? [n : Number]) : Boolean + (if (zero? n) #t + (my-odd? (- n 1)))) + + (display (my-even? 12))) + +(module date typed-scheme + + (define-typed-struct my-date ([day : Number] [month : String] [year : Number])) + + (define: (format-date [d : my-date]) : String + (format "Today is day ~a of ~a in the year ~a" (my-date-day d) (my-date-month d) (my-date-year d))) + + (display (format-date (make-my-date 28 "November" 2006))) + + ) + +(module tree typed-scheme + (define-typed-struct leaf ([val : Number])) + (define-typed-struct node ([left : (Un node leaf)] [right : (Un node leaf)])) + + (define: (tree-height [t : (Un node leaf)]) : Number + (cond [(leaf? t) 1] + [else (max (tree-height (node-left t)) + (tree-height (node-right t)))])) + + (define: (tree-sum [t : (Un node leaf)]) : Number + (cond [(leaf? t) (leaf-val t)] + [else (+ (tree-sum (node-left t)) + (tree-sum (node-right t)))]))) + +(module tree typed-scheme + (define-typed-struct leaf ([val : Number])) + (define-typed-struct node ([left : (Un node leaf)] [right : (Un node leaf)])) + + (define-type-alias tree (Un node leaf)) + + (define: (tree-height [t : tree]) : Number + (cond [(leaf? t) 1] + [else (max (tree-height (node-left t)) + (tree-height (node-right t)))])) + + (define: (tree-sum [t : tree]) : Number + (cond [(leaf? t) (leaf-val t)] + [else (+ (tree-sum (node-left t)) + (tree-sum (node-right t)))]))) + +(module add-list typed-scheme + (define: (sum-list [l : (Listof Number)]) : Number + (cond [(null? l) 0] + [else (+ (car l) (sum-list (cdr l)))]))) + +(module maybe typed-scheme + (define-typed-struct Nothing ()) + (define-typed-struct (a) Just ([v : a])) + + (define-type-alias (Maybe a) (Un Nothing (Just a))) + + (define: (find [v : Number] [l : (Listof Number)]) : (Maybe Number) + (cond [(null? l) (make-Nothing)] + [(= v (car l)) (make-Just v)] + [else (find v (cdr l))]))) + \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/match-expander-problem.ss b/collects/tests/typed-scheme/succeed/match-expander-problem.ss new file mode 100644 index 00000000..c26e3fbc --- /dev/null +++ b/collects/tests/typed-scheme/succeed/match-expander-problem.ss @@ -0,0 +1,20 @@ +#lang typed-scheme + +#;(require (lib "etc.ss")) +;(require "prims.ss") +(require (lib "match.ss")) + +(define-typed-struct pt ([x : Number] [y : Number])) + +(require (for-syntax scheme/base)) + + +(define-match-expander blah #:match (lambda (stx) (syntax-case stx () + [(_ . a) #'($ . a)]))) + +(define: (pt-add/match/blah [v : Any]) : Number + (match v + [(blah pt #{x Number} #{y Number}) (+ x y)] + [_ 0])) + + diff --git a/collects/tests/typed-scheme/succeed/mu-rec.ss b/collects/tests/typed-scheme/succeed/mu-rec.ss new file mode 100644 index 00000000..4de1546e --- /dev/null +++ b/collects/tests/typed-scheme/succeed/mu-rec.ss @@ -0,0 +1,9 @@ +#lang typed-scheme + +(define: (evenp [n : Number]) : Boolean + (if (zero? n) #t (oddp (- n 1)))) + +(define: (oddp [n : Number]) : Boolean + (if (zero? n) #f (evenp (- n 1)))) + + diff --git a/collects/tests/typed-scheme/succeed/pair-test.ss b/collects/tests/typed-scheme/succeed/pair-test.ss new file mode 100644 index 00000000..cb0fc949 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/pair-test.ss @@ -0,0 +1,8 @@ +#lang typed-scheme + +(define: x : (Number . Boolean) (cons 3 #f)) + +(define: y : Number (car x)) + +(define: z : Boolean (cdr x)) + diff --git a/collects/tests/typed-scheme/succeed/poly-struct.ss b/collects/tests/typed-scheme/succeed/poly-struct.ss new file mode 100644 index 00000000..c5750ce4 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/poly-struct.ss @@ -0,0 +1,9 @@ +#lang typed-scheme +(define-typed-struct (a) bag ([val : a])) + +(provide make-bag) + +(let: ([x : (bag Number) (make-bag #{3 :: Number})] + [y : (bag Boolean) (make-bag #{#t :: Boolean})]) + (+ 4 (bag-val x)) + (not (bag-val y))) diff --git a/collects/tests/typed-scheme/succeed/poly-tests.ss b/collects/tests/typed-scheme/succeed/poly-tests.ss new file mode 100644 index 00000000..54da1e0b --- /dev/null +++ b/collects/tests/typed-scheme/succeed/poly-tests.ss @@ -0,0 +1,27 @@ +#lang typed-scheme +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) +(define-type-alias list-of Listof) +#;(require "prims.ss") +(define: mymap : (All (a b) ((a -> b) (list-of a) -> (list-of b))) + (plambda: (a b) ([f : (a -> b)] [l : (list-of a)]) + (cond [(null? l) '()] + [else (cons (f (car l)) + (mymap f (cdr l)))]))) + +(pdefine: (a b) (mymap2 [f : (a -> b)] [l : (list-of a)]) : (list-of b) + (cond [(null? l) '()] + [else (cons (f (car l)) + (mymap2 f (cdr l)))])) + +(define: x : (list-of number) + (mymap (lambda: ([x : number]) (+ 3 x)) (cons 1 (cons 4 #{'() : (list-of number)})))) + +(define: x2 : (list-of number) + (mymap2 (lambda: ([x : number]) (+ 3 x)) (cons 1 (cons 4 #{'() : (list-of number)})))) + +(provide x2) + + diff --git a/collects/tests/typed-scheme/succeed/priority-queue.scm b/collects/tests/typed-scheme/succeed/priority-queue.scm new file mode 100644 index 00000000..f957d201 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/priority-queue.scm @@ -0,0 +1,103 @@ +;;; priority-queue.scm -- Jens Axel Søgaard +;;; PURPOSE + + ; This file implements priority queues on top of + ; a heap library. +#lang typed-scheme +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) +(define-type-alias list-of Listof) +(require (prefix-in heap: "leftist-heap.ss") + (except-in (lib "67.ss" "srfi") number-compare current-compare =? number) (lib "67.ss" "srfi")) +(require/typed current-compare (-> (top top -> number)) (lib "67.ss" "srfi")) +(require/typed =? ((top top -> number) top top -> boolean) (lib "67.ss" "srfi")) +(require/typed number) top top -> boolean) (lib "67.ss" "srfi")) + + ; a priority-queue is a heap of (cons ) + +(define-type-alias (elem a) (cons number a)) + +(define-typed-struct (a) priority-queue ([heap : (heap:Heap (elem a))])) + +(define-type-alias (pqh a) (heap:Heap (elem a))) + + ; conveniences +(pdefine: (a) (heap [pq : (priority-queue a)]) : (pqh a) (priority-queue-heap pq)) +(pdefine: (a) (pri [p : (elem a)]) : number (car p)) +(pdefine: (a) (elm [p : (elem a)]) : a (cdr p)) +(pdefine: (a) (make [h : (pqh a)]) : (priority-queue a) (make-priority-queue h)) + + ; sort after priority + ; TODO: and then element? +(pdefine: (a) (compare [p1 : (elem a)] [p2 : (elem a)]) : number + (number-compare (pri p1) (pri p2))) + + ;;; OPERATIONS + +(define: (num-elems [h : (heap:Heap (cons number number))]) : (list-of (cons number number)) + (heap:elements h)) + +(pdefine: (a) (elements [pq : (priority-queue a)]) : (list-of a) + (map #{elm :: ((elem a) -> a)} (heap:elements (heap pq)))) + +(pdefine: (a) (elements+priorities [pq : (priority-queue a)]) : (values (list-of a) (list-of number)) + (let: ([eps : (list-of (elem a)) (heap:elements (heap pq))]) + (values (map #{elm :: ((elem a) -> a)} eps) + (map #{pri :: ((elem a) -> number)} eps)))) + +(pdefine: (a) (empty? [pq : (priority-queue a)]) : boolean + (heap:empty? (heap pq))) + +(define: empty : (All (a) (case-lambda (-> (priority-queue a)) (comparator -> (priority-queue a)))) + (pcase-lambda: (a) + [() (#{empty @ a} (current-compare))] + [([cmp : comparator]) (make (#{heap:empty :: (case-lambda (-> (pqh a)) + (comparator -> (pqh a)))} cmp))])) + +(pdefine: (e r) (fold [f : ((cons number e) r -> r)] [b : r] [a : (priority-queue e)]) : r + (heap:fold f b (#{heap :: ((priority-queue e) -> (pqh e))} a))) + + +;; "bug" found - handling of empty heaps +(pdefine: (a) (find-min [pq : (priority-queue a)]) : a + (let ([h (heap pq)]) + (if (heap:heap-node? h) + (elm (heap:find-min h)) + (error "priority queue empty")))) + +(pdefine: (a) (find-min-priority [pq : (priority-queue a)]) : number + (let ([h (heap pq)]) + (if (heap:heap-node? h) + (pri (heap:find-min h)) + (error "priority queue empty")))) + +(pdefine: (a) (insert [x : a] [p : number] [pq : (priority-queue a)]) : (priority-queue a) + (make (heap:insert (#{cons :: (case-lambda (a (list-of a) -> (list-of a)) (number a -> (cons number a)))} p x) (heap pq)))) + +;; FIXME - had to insert extra binding to give the typechecker more help +;; could have done this with annotation on map, probably +(pdefine: (a) (insert* [xs : (list-of a)] [ps : (list-of number)] [pq : (priority-queue a)]) : (priority-queue a) + (let ([cons #{cons :: (case-lambda (a (list-of a) -> (list-of a)) (number a -> (cons number a)))}]) + (make (heap:insert* (map #{cons :: (number a -> (cons number a))} ps xs) (heap pq))))) + +(pdefine: (a) (delete-min [pq : (priority-queue a)]) : (priority-queue a) + (let ([h (heap pq)]) + (if (heap:heap-node? h) + (make (heap:delete-min h)) + (error "priority queue empty")))) + + +(pdefine: (a) (size [pq : (priority-queue a)]) : number + (heap:size (heap pq))) + +(pdefine: (a) (union [pq1 : (priority-queue a)] [pq2 : (priority-queue a)]) : (priority-queue a) + (make (heap:union (heap pq1) (heap pq2)))) + + +#;(require "signatures/priority-queue-signature.scm") +#;(provide-priority-queue) + diff --git a/collects/tests/typed-scheme/succeed/provide-syntax.ss b/collects/tests/typed-scheme/succeed/provide-syntax.ss new file mode 100644 index 00000000..ba99a6ed --- /dev/null +++ b/collects/tests/typed-scheme/succeed/provide-syntax.ss @@ -0,0 +1,5 @@ +#lang typed-scheme + +(define-syntax-rule (foo) 1) + +(provide foo) \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/rec-types.ss b/collects/tests/typed-scheme/succeed/rec-types.ss new file mode 100644 index 00000000..bcfa6ddc --- /dev/null +++ b/collects/tests/typed-scheme/succeed/rec-types.ss @@ -0,0 +1,40 @@ +#lang typed-scheme + +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) +(define-type-alias list-of Listof) +(define-type-alias comparator (top top -> number)) + + +(define-typed-struct (a) heap ([compare : comparator])) +(define-typed-struct (a) (heap-empty heap) ()) +(define-typed-struct (a) (heap-node heap) + ([rank : number] [elm : a] [left : (Un (heap-node a) (heap-empty a))] [right : (Un (heap-node a) (heap-empty a))])) + +(define-type-alias (Heap a) (Un (heap-empty a) (heap-node a))) + + +(pdefine: (b) (heap-size [h : (Heap b)]) : number + (cond [(heap-empty? h) 0] + [(heap-node? h) + (+ 1 (+ (#{heap-size @ b} (heap-node-left h)) + (#{heap-size @ b} (heap-node-right h))))] + ;; FIXME - shouldn't need else clause + [else (error "Never happens!")])) + + +(define-typed-struct npheap ([compare : comparator])) +(define-typed-struct (npheap-empty npheap) ()) +(define-typed-struct (npheap-node npheap) + ([rank : number] [elm : symbol] [left : (Un npheap-node npheap-empty)] [right : (Un npheap-node npheap-empty)])) + +(define-type-alias npHeap (Un npheap-empty npheap-node)) + + +(define: (npheap-size [h : npHeap]) : number + (cond [(npheap-empty? h) 0] + [else + (+ 1 (+ (npheap-size (npheap-node-left h)) + (npheap-size (npheap-node-right h))))])) diff --git a/collects/tests/typed-scheme/succeed/require-tests.ss b/collects/tests/typed-scheme/succeed/require-tests.ss new file mode 100644 index 00000000..50f16b0b --- /dev/null +++ b/collects/tests/typed-scheme/succeed/require-tests.ss @@ -0,0 +1,11 @@ +#lang scheme/load +#reader typed-scheme/typed-reader +(module bang-tests typed-scheme + (define #{x : Number} 1) + (provide x) + ) + +(module trequire typed-scheme + (require 'bang-tests) + (define: y : Number x) + (display y)) \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/scratch.ss b/collects/tests/typed-scheme/succeed/scratch.ss new file mode 100644 index 00000000..c7a9b065 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/scratch.ss @@ -0,0 +1,6 @@ +#lang typed-scheme + +(let: ((x : Any 3)) (if (number? x) (add1 x) 12)) +(let: ((v : (Un Number Boolean) #f)) (if (boolean? v) 5 (+ v 1))) + + diff --git a/collects/tests/typed-scheme/succeed/seasoned-schemer.ss b/collects/tests/typed-scheme/succeed/seasoned-schemer.ss new file mode 100644 index 00000000..361ff9ff --- /dev/null +++ b/collects/tests/typed-scheme/succeed/seasoned-schemer.ss @@ -0,0 +1,106 @@ +#lang typed-scheme +#;(require (lib "etc.ss")) +#;(require "prims.ss") +(require (lib "match.ss")) + +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) +(define-type-alias list-of Listof) +(define-type-alias atom (Un Number Symbol Boolean)) + +(define: atom? : (Any -> Boolean : atom) (lambda: ([v : Any]) (if (number? v) #t (if (symbol? v) #t (boolean? v))))) + + +(define-type-alias lat (list-of atom)) + +(define: (member? [a : atom] [l : lat]) : boolean + (cond + [(null? l) #f] + [(equal? a (car l)) #t] + [else (member? a (cdr l))])) + +(define: (two-in-a-row [l : lat]) : boolean + (cond + [(null? l) #f] + [(null? (cdr l)) #f] + [(equal? (car l) (car (cdr l))) #t] + [else (two-in-a-row (cdr l))])) + + +(define: (two-in-a-row2 [l : lat]) : boolean + (define: (two-in-a-row-b [prec : atom] [alat : lat]) : boolean + (cond + [(null? alat) #f] + [else (or (eq? (car alat) prec) + (two-in-a-row-b (car alat) (cdr alat)))])) + (cond + [(null? l) #f] + [else (two-in-a-row-b (car l) (cdr l))])) + +(define-type-alias lon (list-of number)) + +(define: (sum-of-prefixes-b [sonssf : number] [tup : lon]) : lon + (cond + [(null? tup) '()] + [else (cons (+ sonssf (car tup)) + (sum-of-prefixes-b (+ sonssf (car tup)) + (cdr tup)))])) + +(define: (sum-of-prefixes [tup : lon]) : lon + (sum-of-prefixes-b 0 tup)) + +(define: (one? [n : number]) : boolean + (= n 1)) + +(pdefine: (e) (pick [n : number] [lat : (list-of e)]) : e + (cond [(one? n) (car lat)] + [else (pick (sub1 n) (cdr lat))])) + +(define: (scramble-b [tup : lon] [rev-pre : lon]) : lon + (cond [(null? tup) '()] + [else (cons (pick (car tup) (cons (car tup) rev-pre)) + (scramble-b (cdr tup) + (cons (car tup) rev-pre)))])) + +(define: (scramble [tup : lon]) : lon + (scramble-b tup '())) + +(pick 2 (cons 'a (cons 'd (cons 'c #{'() : (list-of symbol)})))) + +(define: (multirember [a : atom] [l : lat]) : lat + (letrec ([#{mr : (lat -> lat)} + (lambda: ([l : lat]) + (cond [(null? l) l] + [(eq? a (car l)) (mr (cdr l))] + [else (cons (car l) (mr (cdr l)))]))]) + (mr l))) + +(pdefine: (e) (multirember-f [f : (e e -> boolean)] [a : e] [l : (list-of e)]) : (list-of e) + (let: mr : (list-of e) ([l : (list-of e) l]) + (cond [(null? l) l] + [(f a (car l)) (mr (cdr l))] + [else (cons (car l) (mr (cdr l)))])) + #;(letrec ([#{mr : ((list-of e) -> (list-of e))} + (lambda: ([l : (list-of e)]) + (cond [(null? l) l] + [(f a (car l)) (mr (cdr l))] + [else (cons (car l) (mr (cdr l)))]))]) + (mr l))) + +(define-type-alias set lat) + +(define: (union [set1 : set] [set2 : set]) : set + (cond [(null? set1) set2] + [(member? (car set1) set2) (union (cdr set1) set2)] + [else (cons (car set1) (union (cdr set1) set2))])) + +(define: (intersect [set1 : set] [set2 : set]) : set + (define: (I [set1 : set]) : set + (cond [(null? set1) set1] + [(member? (car set1) set2) (cons (car set1) (I (cdr set1)))] + [else (I (cdr set1))])) + (cond [(null? set2) set2] + [else (I set1)])) + diff --git a/collects/tests/typed-scheme/succeed/struct-exec.ss b/collects/tests/typed-scheme/succeed/struct-exec.ss new file mode 100644 index 00000000..01e1dd82 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/struct-exec.ss @@ -0,0 +1,4 @@ +#lang typed-scheme +(define-typed-struct/exec X ([a : Number] [b : Boolean]) [(lambda: ([x : X]) (+ 3 )) : (X -> Number)]) +((make-X 1 #f)) + \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/typed-list.ss b/collects/tests/typed-scheme/succeed/typed-list.ss new file mode 100644 index 00000000..738aa8dd --- /dev/null +++ b/collects/tests/typed-scheme/succeed/typed-list.ss @@ -0,0 +1,7 @@ +#lang typed-scheme +(provide -foldl) + +(pdefine: (a b) (-foldl [f : (a b -> b)] [e : b] [l : (Listof a)]) : b + (if (null? l) e + (foldl f (f (car l) e) (cdr l)))) + diff --git a/collects/tests/typed-scheme/succeed/varargs-tests.ss b/collects/tests/typed-scheme/succeed/varargs-tests.ss new file mode 100644 index 00000000..0ebacce8 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/varargs-tests.ss @@ -0,0 +1,48 @@ +#lang typed-scheme + + +(define-type-alias number Number) +(define-type-alias boolean Boolean) +(define-type-alias symbol Symbol) +(define-type-alias top Any) +(define-type-alias list-of Listof) +(+ (+) + (+ 1 2) + (+ 1) + (+ 3 4 5 6) + (- 1) + (- 1 2) + (- 3 4 5 6 7 (+ 45))) + +(apply + '(2 3 4)) + + +(define: f : (number boolean .. -> number) + (lambda: ([x : number] . [y : boolean]) + (if (and (pair? y) (car y)) x (- x)))) + +(define: f-cl : (number boolean .. -> number) + (case-lambda: [([x : number] . [y : boolean]) + (if (and (pair? y) (car y)) x (- x))])) + +(define: (f* [x : number] . [y : boolean]) : number + (if (and (pair? y) (car y)) x (- x))) + +(f 3) + +(f 3 #t #f) + +(apply f 3 '(#f)) + +(f* 3) + +(f* 3 #t #f) + +(apply f* 3 '(#f)) + +(f-cl 3) + +(f-cl 3 #t #f) + +(apply f-cl 3 '(#f)) + diff --git a/collects/tests/typed-scheme/succeed/vec-tests.ss b/collects/tests/typed-scheme/succeed/vec-tests.ss new file mode 100644 index 00000000..2c473365 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/vec-tests.ss @@ -0,0 +1,4 @@ +#lang typed-scheme +(define: x : (Vectorof Number) (build-vector 5 (lambda: ([x : Number]) #{0 :: Number}))) +(define: y : Number (vector-ref x 1)) + diff --git a/collects/tests/typed-scheme/unit-tests/all-tests.ss b/collects/tests/typed-scheme/unit-tests/all-tests.ss new file mode 100644 index 00000000..3092a60a --- /dev/null +++ b/collects/tests/typed-scheme/unit-tests/all-tests.ss @@ -0,0 +1,85 @@ +#lang scheme/base + +(require + "test-utils.ss" + "subtype-tests.ss" ;; done + "type-equal-tests.ss" ;; done + "remove-intersect-tests.ss" ;; done + "parse-type-tests.ss" ;; done + "type-annotation-test.ss" ;; done + "typecheck-tests.ss" + "module-tests.ss" + "infer-tests.ss") + +(require (for-syntax scheme/base mzlib/etc)) + +(require (for-syntax (private utils))) + +(require (private planet-requires)) + +(require (schemeunit)) + +(provide unit-tests) + +(define unit-tests + (apply + test-suite + "Unit Tests" + (map (lambda (f) (f)) + (list + subtype-tests + type-equal-tests + restrict-tests + remove-tests + parse-type-tests + type-annotation-tests + typecheck-tests + module-tests + fv-tests + i2-tests + combine-tests)))) + + + +(define-go + subtype-tests + type-equal-tests + restrict-tests + remove-tests + parse-type-tests + type-annotation-tests + typecheck-tests + module-tests + fv-tests + i2-tests + combine-tests) + +(define (fast) + (run + subtype-tests + type-equal-tests + restrict-tests + remove-tests + parse-type-tests + type-annotation-tests + typecheck-tests + module-tests + fv-tests + i2-tests + combine-tests)) + +(define (faster) + (run + subtype-tests + type-equal-tests + restrict-tests + remove-tests + parse-type-tests + type-annotation-tests + fv-tests + i2-tests + combine-tests)) + +;(go/gui) + + diff --git a/collects/tests/typed-scheme/unit-tests/infer-tests.ss b/collects/tests/typed-scheme/unit-tests/infer-tests.ss new file mode 100644 index 00000000..450fb313 --- /dev/null +++ b/collects/tests/typed-scheme/unit-tests/infer-tests.ss @@ -0,0 +1,122 @@ +#lang scheme/base +(require "test-utils.ss" (for-syntax scheme/base)) +(require (private planet-requires type-effect-convenience type-rep unify union infer) + (prefix-in table: (private tables))) +(require (schemeunit)) + +(define (fv . args) (list)) + +(provide fv-tests i2-tests combine-tests) + +(define-syntax-rule (fv-t ty elems ...) + (let ([ty* ty]) + (test-check (format "~a" ty*) + equal? + (fv ty*) + (list (quote elems) ...)))) + +(define (fv-tests) + (test-suite "Tests for fv" + (fv-t N) + [fv-t (-v a) a] + [fv-t (-poly (a) a)] + [fv-t (-poly (a b c d e) a)] + [fv-t (-poly (b) (-v a)) a] + [fv-t (-poly (b c d e) (-v a)) a] + [fv-t (-mu a (-lst a))] + [fv-t (-mu a (-lst (-pair a (-v b)))) b] + )) + +(define-syntax-rule (i2-t t1 t2 (a b) ...) + (test-check (format "~a ~a" t1 t2) + equal? + (infer t1 t2 (fv t1)) + (list (list a b) ...))) + +(define-syntax-rule (i2-l t1 t2 fv (a b) ...) + (test-check (format "~a ~a" t1 t2) + equal? + (infer/list t1 t2 fv) + (list (list a b) ...))) + +(define (f t1 t2) (infer t1 t2 (fv t1))) + +(define-syntax-rule (i2-f t1 t2) + (test-false (format "~a ~a" t1 t2) + (f t1 t2))) + +(define (i2-tests) + (test-suite "Tests for infer" + [i2-t (-v a) N ('a N)] + [i2-t (-pair (-v a) (-v a)) (-pair N (Un N B)) ('a (Un N B))] + [i2-t (-lst (-v a)) (-pair N (-pair N (-val null))) ('a N)] + [i2-t (-lst (-v a)) (-pair N (-pair B (-val null))) ('a (Un N B))] + [i2-t Univ (Un N B)] + + [i2-t ((-v a) . -> . (-v b)) (-> N N) ('b N) ('a N)] + [i2-l (list (-v a) (-v a) (-v b)) (list (Un (-val 1) (-val 2)) N N) '(a b) ('b N) ('a N)] + [i2-l (list (-> (-v a) Univ) (-lst (-v a))) (list (-> N (Un N B)) (-lst N)) '(a) ('a N)] + [i2-l (list (-> (-v a) (-v b)) (-lst (-v a))) (list (-> N N) (-lst (Un (-val 1) (-val 2)))) '(a b) ('b N) ('a N)] + [i2-l (list (-lst (-v a))) (list (-lst (Un B N))) '(a) ('a (Un N B))] + ;; error tests + [i2-f (-lst (-v a)) Univ])) + + + +(define-syntax-rule (co-t a b c) + (test-case (format "~a ~a" a b) + (check equal? ((combine 'co) a b) c) + (check equal? ((combine 'co) b a) c))) +(define-syntax-rule (co-f a b) + (test-case (format "fail ~a ~a" a b) + (check-exn exn:infer? (lambda () ((combine 'co) a b))) + (check-exn exn:infer? (lambda () ((combine 'co) b a))))) + +(define-syntax-rule (un-t a b c) + (test-case (format "~a ~a" a b) + (check equal? (s (g ((table:un 'co) a b))) (s c)) + (check equal? (s (g ((table:un 'co) b a))) (s c)))) +(define-syntax-rule (un-f a b) + (test-case (format "fail ~a ~a" a b) + (check-exn exn:infer? (lambda () ((table:un 'co) a b))) + (check-exn exn:infer? (lambda () ((table:un 'co) b a))))) + +;; examples for testing combine + +(define c-ex1 `(contra ,(Un N B))) +(define c-ex2 `(contra ,B)) +(define c-ex3 `(#f ,N)) +(define c-ex4 `(co ,N)) +(define c-ex5 `(co ,B)) +(define c-ex6 `fail) + +;; examples for testing table:un + +(define m-ex1 + (table:sexp->eq `((a ,c-ex3) (b ,c-ex6) (c ,c-ex5) (d ,c-ex1)))) +(define m-ex2 + (table:sexp->eq `((a ,c-ex4) (b ,c-ex4) (c ,c-ex2) (d ,c-ex2)))) +(define m-ex3 + (table:sexp->eq `((a ,c-ex4) (b ,c-ex4) (c ,c-ex2) (d ,c-ex5)))) + + +(define (combine-tests) + (test-suite "Combine/Table Union Tests" + (co-t c-ex1 c-ex2 c-ex2) + (co-t c-ex2 c-ex2 c-ex2) + (co-f c-ex3 c-ex2) + (co-f c-ex4 c-ex5) + (co-t c-ex5 c-ex2 `(both ,B)) + (co-t c-ex5 c-ex6 c-ex5) + [co-t c-ex3 c-ex4 c-ex4] + [un-t m-ex1 m-ex2 `((b (co ,N)) (a (co ,N)) (c (both ,B)) (d (contra ,B)))] + [un-f m-ex1 m-ex3])) + + +(define (g e) (table:to-sexp e)) + +(define (s e) + (sort e (lambda (a b) (stringstring (car a)) (symbol->string (car b)))))) + + +(define-go fv-tests i2-tests combine-tests) diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss new file mode 100644 index 00000000..e279d74b --- /dev/null +++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss @@ -0,0 +1,78 @@ +#lang scheme/base +(require "test-utils.ss" (for-syntax scheme/base)) +(require (private planet-requires type-comparison parse-type type-rep + type-effect-convenience tc-utils type-environments + type-name-env init-envs union)) + +(require (except-in (private base-env))) + +(require (schemeunit)) + +(provide parse-type-tests) + +(define-syntax (run-one stx) + (syntax-case stx () + [(_ ty) #'(parameterize ([current-tvars initial-tvar-env] + [current-orig-stx #'here] + [orig-module-stx #'here] + [expanded-module-stx #'here]) + (parse-type (syntax ty)))])) + +(define-syntax (pt-test stx) + (syntax-case stx () + [(_ ts tv) #'(pt-test ts tv () initial-tvar-env)] + [(_ ts tv tys) #'(pt-test ts tv tys initial-tvar-env)] + [(_ ty-stx ty-val ((nm ty) ...) tvar-env) + #`(test-case #,(format "~a" (syntax->datum #'ty-stx)) + (parameterize ([current-tvars tvar-env]) + #;(initialize-type-name-env initial-type-names) + (register-type-name #'nm ty) ... + (check type-equal? (parse-type (syntax ty-stx)) ty-val)))])) + +(define-syntax pt-tests + (syntax-rules () + [(_ nm [elems ...] ...) + (test-suite nm + (pt-test elems ...) ...)])) + +(define (parse-type-tests) + (pt-tests + "parse-type tests" + [Number N] + [Any Univ] + [(All (Number) Number) (-poly (a) a)] + [(Number . Number) (-pair N N)] + [(list-of Boolean) (make-Listof B)] + [(Vectorof (Listof Symbol)) (make-Vector (make-Listof Sym))] + [(pred Number) (make-pred-ty N)] + [(values Number Boolean Number) (-values (list N B N))] + [(Number -> Number) (-> N N)] + [(Number -> Number) (-> N N)] + [(Number Number Number Boolean -> Number) (N N N B . -> . N)] + [(Number Number Number .. -> Boolean) ((list N N) N . ->* . B)] + ;[((. Number) -> Number) (->* (list) N N)] ;; not legal syntax + [(Un Number Boolean) (Un N B)] + [(Un Number Boolean Number) (Un N B)] + [(Un Number Boolean 1) (Un N B)] + [(All (a) (list-of a)) (-poly (a) (make-Listof a))] + [(case-lambda (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B] + [(N N) N])] + [1 (-val 1)] + [#t (-val #t)] + [#f (-val #f)] + ["foo" (-val "foo")] + + [(poly-lst Number) (make-Listof N) ((poly-lst (-poly (a) (make-Listof a)))) + #;(extend-env (list 'poly-lst) (list (-poly (a) (make-Listof a))) initial-type-names)] + + [a (-v a) () (extend-env (list 'a) (list (-v a)) + initial-tvar-env)] + + )) + + +(define (go) + (run parse-type-tests)) + + + diff --git a/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss new file mode 100644 index 00000000..ff8763a8 --- /dev/null +++ b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss @@ -0,0 +1,69 @@ +#lang scheme/base +(require "test-utils.ss" (for-syntax scheme/base)) +(require (private type-rep type-effect-convenience planet-requires remove-intersect unify subtype union)) + +(require (schemeunit)) + +(define-syntax (restr-tests stx) + (syntax-case stx () + [(_ [t1 t2 res] ...) + #'(test-suite "Tests for intersect" + (test-check (format "Restrict test: ~a ~a" t1 t2) type-compare? (restrict t1 t2) res) ...)])) + +(define (restrict-tests) + (restr-tests + [N (Un N Sym) N] + [N N N] + [(Un (-val 'foo) (-val 6)) (Un N Sym) (Un (-val 'foo) (-val 6))] + [N (-mu a (Un N Sym (make-Listof a))) N] + [(Un N B) (-mu a (Un N Sym (make-Listof a))) N] + [(-mu x (Un N (make-Listof x))) (Un Sym N B) N] + [(Un N -String Sym B) N N] + + [(-lst N) (-pair Univ Univ) (-pair N (-lst N))] + ;; FIXME + #; + [-Listof -Sexp (-lst (Un B N -String Sym))] + #; + [-Sexp -Listof (-lst -Sexp)] + )) + +(define-syntax (remo-tests stx) + (syntax-case stx () + [(_ [t1 t2 res] ...) + (syntax/loc stx + (test-suite "Tests for remove" + (test-check (format "Remove test: ~a ~a" t1 t2) type-compare? (remove t1 t2) res) ...))])) + +(define (remove-tests) + (remo-tests + [(Un N Sym) N Sym] + [N N (Un)] + [(-mu x (Un N Sym (make-Listof x))) N (Un Sym (make-Listof (-mu x (Un N Sym (make-Listof x)))))] + [(-mu x (Un N Sym B (make-Listof x))) N (Un Sym B (make-Listof (-mu x (Un N Sym B (make-Listof x)))))] + [(Un (-val #f) (-mu x (Un N Sym (make-Listof (-v x))))) + (Un B N) + (Un Sym (make-Listof (-mu x (Un N Sym (make-Listof x)))))] + [(Un (-val 'foo) (-val 6)) (Un N Sym) (Un)] + [(-> (Un Sym N) N) (-> N N) (Un)] + [(Un (-poly (a) (make-Listof a)) (-> N N)) (-> N N) (-poly (a) (make-Listof a))] + [(Un Sym N) (-poly (a) N) Sym] + [(-pair N (-v a)) (-pair Univ Univ) (Un)] + )) + +(define-go + restrict-tests + remove-tests) + +(define x1 + (-mu list-rec + (Un + (-val '()) + (-pair (-mu x (Un B N -String Sym (-val '()) (-pair x x))) + list-rec)))) +(define x2 + (Un (-val '()) + (-pair (-mu x (Un B N -String Sym (-val '()) (-pair x x))) + (-mu x (Un B N -String Sym (-val '()) (-pair x x)))))) +(provide remove-tests restrict-tests) + diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss new file mode 100644 index 00000000..6b1082f6 --- /dev/null +++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss @@ -0,0 +1,126 @@ +#lang scheme/base + +(require "test-utils.ss") + +(require (private subtype type-rep type-effect-convenience + planet-requires init-envs type-environments union)) + +(require (schemeunit) + (for-syntax scheme/base)) + +(provide subtype-tests) + +(define-syntax (subtyping-tests stx) + (define (single-test stx) + (syntax-case stx (FAIL) + [(FAIL t s) (syntax/loc stx (test-check (format "FAIL ~a" '(t s)) (lambda (a b) (not (subtype a b))) t s))] + [(t s) (syntax/loc stx (test-check (format "~a" '(t s)) subtype t s))])) + (syntax-case stx () + [(_ cl ...) + (with-syntax ([(new-cl ...) (map single-test (syntax->list #'(cl ...)))]) + (syntax/loc stx + (begin (test-suite "Tests for subtyping" + new-cl ...))))])) + +(define (subtype-tests) + (subtyping-tests + ;; trivial examples + (Univ Univ) + (N Univ) + (B Univ) + (Sym Univ) + (-Void Univ) + #;(Sym Dyn) + #;(Dyn N) + [N N] + [(Un (-pair Univ (-lst Univ)) (-val '())) (-lst Univ)] + [(-pair N (-pair N (-pair (-val 'foo) (-val '())))) (-lst Univ)] + [(-pair N (-pair N (-pair (-val 'foo) (-val '())))) (-lst (Un N Sym))] + [(-pair (-val 6) (-val 6)) (-pair N N)] + [(-val 6) (-val 6)] + ;; unions + [(Un N) N] + [(Un N N) N] + [(Un N Sym) (Un Sym N)] + [(Un (-val 6) (-val 7)) N] + [(Un (-val #f) (Un (-val 6) (-val 7))) (Un N (Un B Sym))] + [(Un (-val #f) (Un (-val 6) (-val 7))) (-mu x (Un N (Un B Sym)))] + [(Un N (-val #f) (-mu x (Un N Sym (make-Listof x)))) + (-mu x (Un N Sym B (make-Listof x)))] + ;; sexps vs list*s of nums + [(-mu x (Un N Sym (make-Listof x))) (-mu x (Un N Sym B (make-Listof x)))] + [(-mu x (Un N (make-Listof x))) (-mu x (Un N Sym (make-Listof x)))] + [(-mu x (Un N (make-Listof x))) (-mu y (Un N Sym (make-Listof y)))] + ;; a hard one + [-NE -Sexp] + ;; simple function types + ((Univ . -> . N) (N . -> . Univ)) + [(Univ Univ Univ . -> . N) (Univ Univ N . -> . N)] + ;; simple list types + [(make-Listof N) (make-Listof Univ)] + [(make-Listof N) (make-Listof N)] + [FAIL (make-Listof N) (make-Listof Sym)] + [(-mu x (make-Listof x)) (-mu x* (make-Listof x*))] + [(-pair N N) (-pair Univ N)] + [(-pair N N) (-pair N N)] + ;; from page 7 + [(-mu t (-> t t)) (-mu s (-> s s))] + [(-mu s (-> N s)) (-mu t (-> N (-> N t)))] + ;; polymorphic types + [(-poly (t) (-> t t)) (-poly (s) (-> s s))] + [FAIL (make-Listof N) (-poly (t) (make-Listof t))] + [(-poly (a) (make-Listof (-v a))) (make-Listof N)] ;; + [(-poly (a) N) N] + + [(-val 6) N] + [(-val 'hello) Sym] + [((Un Sym N) . -> . N) (-> N N)] + [(-poly (t) (-> N t)) (-mu t (-> N t))] + ;; not subtypes + [FAIL (-val 'hello) N] + [FAIL (-val #f) Sym] + [FAIL (Univ Univ N N . -> . N) (Univ Univ Univ . -> . N)] + [FAIL (N . -> . N) (-> Univ Univ)] + [FAIL (Un N Sym) N] + [FAIL N (Un (-val 6) (-val 11))] + [FAIL Sym (-val 'Sym)] + [FAIL (Un Sym N) (-poly (a) N)] + ;; bugs found + [(Un (-val 'foo) (-val 6)) (Un (-val 'foo) (-val 6))] + [(-poly (a) (make-Listof (-v a))) (make-Listof (-mu x (Un (make-Listof x) N)))] + [FAIL (make-Listof (-mu x (Un (make-Listof x) N))) (-poly (a) (make-Listof a))] + ;; case-lambda + [(cl-> [(N) N] [(B) B]) (N . -> . N)] + ;; special case for unused variables + [N (-poly (a) N)] + [FAIL (cl-> [(N) B] [(B) N]) (N . -> . N)] + ;; varargs + [(->* (list N) Univ B) (->* (list N) N B)] + [(->* (list Univ) N B) (->* (list N) N B)] + [(->* (list N) N B) (->* (list N) N B)] + [(->* (list N) N B) (->* (list N) N Univ)] + [(->* (list N) N N) (->* (list N N) N)] + [(->* (list N) N N) (->* (list N N N) N)] + [(->* (list N N) B N) (->* (list N N) N)] + [FAIL (->* (list N) N B) (->* (list N N N) N)] + [(->* (list N N) B N) (->* (list N N B B) N)] + + [(-poly (a) (cl-> [() a] + [(N) a])) + (cl-> [() (-pair N (-v b))] + [(N) (-pair N (-v b))])] + + [(-poly (a) ((Un (-base 'foo) (-struct 'bar #f (list N a) #f)) . -> . (-lst a))) + ((Un (-base 'foo) (-struct 'bar #f (list N (-pair N (-v a))) #f)) . -> . (-lst (-pair N (-v a))))] + [(-poly (a) ((-struct 'bar #f (list N a) #f) . -> . (-lst a))) + ((-struct 'bar #f (list N (-pair N (-v a))) #f) . -> . (-lst (-pair N (-v a))))] + + [(-poly (a) (a . -> . (make-Listof a))) ((-v b) . -> . (make-Listof (-v b)))] + [(-poly (a) (a . -> . (make-Listof a))) ((-pair N (-v b)) . -> . (make-Listof (-pair N (-v b))))] + + (FAIL (-poly (a b) (-> a a)) (-poly (a b) (-> a b))) + + )) + +(define-go + subtype-tests) diff --git a/collects/tests/typed-scheme/unit-tests/test-utils.ss b/collects/tests/typed-scheme/unit-tests/test-utils.ss new file mode 100644 index 00000000..83455624 --- /dev/null +++ b/collects/tests/typed-scheme/unit-tests/test-utils.ss @@ -0,0 +1,58 @@ +#lang scheme/base +(provide (all-defined-out)) + +(require scheme/require-syntax + scheme/match + (for-syntax scheme/base)) + +(define-require-syntax private + (lambda (stx) + (syntax-case stx () + [(_ id ...) + (andmap identifier? (syntax->list #'(id ...))) + (with-syntax ([(id* ...) (map (lambda (id) (datum->syntax + id + (string->symbol + (string-append + "typed-scheme/private/" + (symbol->string (syntax-e id)))))) + (syntax->list #'(id ...)))]) + #`(combine-in id* ...))]))) + +(require (private planet-requires type-comparison utils)) + +(require (schemeunit)) + +(define (mk-suite ts) + (match (map (lambda (f) (f)) ts) + [(list t) t] + [ts (apply test-suite "Combined Test Suite" ts)])) + +(define (run . ts) + (test/text-ui (mk-suite ts))) + +(define (run/gui . ts) + (test/graphical-ui (mk-suite ts))) + + +(define-syntax (define-go stx) + (syntax-case stx () + [(_ args ...) + (with-syntax + ([go (datum->syntax stx 'go)] + [go/gui (datum->syntax stx 'go/gui)] + [(tmps ...) (generate-temporaries #'(args ...))]) + #'(define-values (go go/gui) + (let ([tmps args] ...) + (values (lambda () (run tmps ...)) + (lambda () (run/gui tmps ...))))))])) + +(define-syntax (check-type-equal? stx) + (syntax-case stx () + [(_ nm a b) + #`(test-check nm type-equal? a b)])) +(define-syntax (check-tc-result-equal? stx) + (syntax-case stx () + [(_ nm a b) + #`(test-check nm tc-result-equal? a b)])) + diff --git a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss new file mode 100644 index 00000000..0e04a221 --- /dev/null +++ b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss @@ -0,0 +1,46 @@ +#lang scheme/base + +(require "test-utils.ss" (for-syntax scheme/base)) +(require (private planet-requires type-rep type-comparison type-effect-convenience union subtype)) +(require (schemeunit)) + +(provide type-equal-tests) + + +(define-syntax (te-tests stx) + (define (single-test stx) + (syntax-case stx (FAIL) + [(FAIL t s) #'((test-check (format "FAIL ~a" '(t s)) (lambda (a b) (not (type-equal? a b))) t s) + (test-check (format "FAIL ~a" '(s t)) (lambda (a b) (not (type-equal? a b))) s t))] + [(t s) (syntax/loc stx + ((test-check (format "~a" '(t s)) type-equal? t s) + (test-check (format "~a" '(s t)) type-equal? s t)))])) + (syntax-case stx () + [(_ cl ...) + (with-syntax ([((cl1 cl2) ...) (map single-test (syntax->list #'(cl ...)))]) + #'(test-suite "Tests for type equality" + cl1 ... cl2 ...))])) + +(define (type-equal-tests) + (te-tests + [N N] + [(Un N) N] + [(Un N Sym B) (Un N B Sym)] + [(Un N Sym B) (Un Sym B N)] + [(Un N Sym B) (Un Sym N B)] + [(Un N Sym B) (Un B (Un Sym N))] + [(Un N Sym) (Un Sym N)] + [(-poly (x) (-> (Un Sym N) x)) (-poly (xyz) (-> (Un N Sym) xyz))] + [(-mu x (Un N Sym x)) (-mu y (Un N Sym y))] + ;; found bug + [FAIL (Un (-mu heap-node (-struct 'heap-node #f (list (-base 'comparator) N (-v a) (Un heap-node (-base 'heap-empty))) #f)) + (-base 'heap-empty)) + (Un (-mu heap-node (-struct 'heap-node #f (list (-base 'comparator) N (-pair N N) (Un heap-node (-base 'heap-empty))) #f)) + (-base 'heap-empty))])) + + + +(define-go + type-equal-tests) + + diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss new file mode 100644 index 00000000..21a62bda --- /dev/null +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -0,0 +1,606 @@ +#lang scheme/base + +(require "test-utils.ss" + (for-syntax scheme/base) + (for-template scheme/base)) +(require (private base-env)) + +(require (private planet-requires typechecker + type-rep type-effect-convenience type-env + prims type-environments tc-utils union + type-name-env init-envs mutated-vars + effect-rep type-annotation type-utils) + (for-syntax (private tc-utils typechecker base-env))) +(require (schemeunit)) + + + + +(provide typecheck-tests tc-expr/expand) + + +;; check that a literal typechecks correctly +(define-syntax tc-l + (syntax-rules () + [(_ lit ty) + (check-type-equal? (format "~a" 'lit) (tc-literal #'lit) ty)])) + +;; local-expand and then typecheck an expression +(define-syntax (tc-expr/expand stx) + (syntax-case stx () + [(_ e) + (with-syntax ([e* (local-expand #'e 'expression '())] + #; + [ienv initial-env]) + #'(begin + #;(initialize-type-name-env initial-env) + #;(initialize-type-env ienv) + (let ([ex #'e*]) + (find-mutated-vars ex) + (begin0 (tc-expr ex) + (report-all-errors)))))])) + +;; check that an expression typechecks correctly +(define-syntax (tc-e stx) + (syntax-case stx () + [(_ expr ty) #'(tc-e expr ty (list) (list))] + [(_ expr ty eff1 eff2) + #`(check-tc-result-equal? (format "~a" 'expr) + (tc-expr/expand expr) + #;(eval #'(tc-expr/expand expr)) + (ret ty eff1 eff2))])) + +(require (for-syntax syntax/kerncase)) + +;; duplication of the mzscheme toplevel expander, necessary for expanding the rhs of defines +;; note that this ability is never used +(define-for-syntax (local-expand/top-level form) + (let ([form* (local-expand form 'module (kernel-form-identifier-list #'here))]) + (kernel-syntax-case form* #f + [(define-syntaxes . _) (raise-syntax-error "don't use syntax defs here!" form)] + [(define-values vals body) + (quasisyntax/loc form (define-values vals #,(local-expand #'body 'expression '())))] + [e (local-expand #'e 'expression '())]))) + +;; check that typechecking this expression fails +(define-syntax (tc-err stx) + (syntax-case stx () + [(_ expr) + #'(test-exn (format "~a" 'expr) + exn:fail:syntax? + (lambda () (tc-expr/expand expr)))])) + + +(define (typecheck-tests) + (test-suite + "Typechecker tests" + #reader typed-scheme/typed-reader + (let ([-vet (lambda (x) (list (-vet x)))] + [-vef (lambda (x) (list (-vef x)))]) + (test-suite + "tc-expr tests" + + [tc-e + (let: ([x : (U Number (cons Number Number)) (cons 3 4)]) + (if (pair? x) + (+ 1 (car x)) + 5)) + N] + + (tc-e 3 -Integer) + (tc-e "foo" -String) + (tc-e (+ 3 4) N) + [tc-e (lambda: () 3) (-> -Integer)] + [tc-e (lambda: ([x : Number]) 3) (-> N -Integer)] + [tc-e (lambda: ([x : Number] [y : Boolean]) 3) (-> N B -Integer)] + [tc-e (lambda () 3) (-> -Integer)] + [tc-e (values 3 4) (-values (list -Integer -Integer))] + [tc-e (cons 3 4) (-pair -Integer -Integer)] + [tc-e (cons 3 #{'() : (Listof -Integer)}) (make-Listof -Integer)] + [tc-e (void) -Void] + [tc-e (void 3 4) -Void] + [tc-e (void #t #f '(1 2 3)) -Void] + [tc-e #(3 4 5) (make-Vector -Integer)] + [tc-e '(2 3 4) (-lst* -Integer -Integer -Integer)] + [tc-e '(2 3 #t) (-lst* -Integer -Integer (-val #t))] + [tc-e #(2 3 #t) (make-Vector (Un -Integer (-val #t)))] + [tc-e '(#t #f) (-lst* (-val #t) (-val #f))] + [tc-e (plambda: (a) ([l : (Listof a)]) (car l)) + (make-Poly '(a) (-> (make-Listof (-v a)) (-v a)))] + [tc-e #{(lambda: ([l : (list-of a)]) (car l)) PROP typechecker:plambda (a)} + (make-Poly '(a) (-> (make-Listof (-v a)) (-v a)))] + [tc-e (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (-> N N N)] + [tc-e (let: ([x : Number 5]) x) N (-vet #'x) (-vef #'x)] + [tc-e (let-values ([(x) 4]) (+ x 1)) N] + [tc-e (let-values ([(#{x : Number} #{y : boolean}) (values 3 #t)]) (and (= x 1) (not y))) + B (list (-rest (-val #f) #'y)) (list)] + [tc-e (values 3) -Integer] + [tc-e (values) (-values (list))] + [tc-e (values 3 #f) (-values (list -Integer (-val #f)))] + [tc-e (map #{values : (symbol -> symbol)} '(a b c)) (make-Listof Sym)] + [tc-e (letrec: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))]) + (fact 20)) + N] + [tc-e (let: fact : Number ([n : Number 20]) + (if (zero? n) 1 (* n (fact (- n 1))))) + N] + [tc-e (let: ([v : top 5]) + (if (number? v) (+ v 1) 3)) + N] + [tc-e (let: ([v : top #f]) + (if (number? v) (+ v 1) 3)) + N] + [tc-e (let: ([v : (Un Number boolean) #f]) + (if (boolean? v) 5 (+ v 1))) + N] + [tc-e (let: ([f : (Number Number -> Number) +]) (f 3 4)) N] + [tc-e (let: ([+ : (boolean -> Number) (lambda: ([x : boolean]) 3)]) (+ #f)) N] + [tc-e (when #f #t) (Un -Void)] + [tc-e (when (number? #f) (+ 4 5)) (Un N -Void)] + [tc-e (let: ([x : (Un #f Number) 7]) + (if x (+ x 1) 3)) + N] + [tc-e (let: ((x : Number 3)) (if (boolean? x) (not x) #t)) (-val #t)] + [tc-e (begin 3) -Integer] + [tc-e (begin #f 3) -Integer] + [tc-e (begin #t) (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] + [tc-e (begin0 #t) (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] + [tc-e (begin0 #t 3) (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] + [tc-e #t (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] + [tc-e #f (-val #f) (list (make-False-Effect)) (list (make-False-Effect))] + [tc-e '#t (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] + [tc-e '#f (-val #f) (list (make-False-Effect)) (list (make-False-Effect))] + [tc-e (if #f 'a 3) -Integer] + [tc-e (if #f #f #t) (Un (-val #t))] + [tc-e (when #f 3) -Void] + [tc-e '() (-val '())] + [tc-e (let: ([x : (Listof Number) '(1)]) + (cond [(pair? x) 1] + [(null? x) 1])) + -Integer] + [tc-e (lambda: ([x : Number] . [y : Number]) (car y)) (->* (list N) N N)] + [tc-e ((lambda: ([x : Number] . [y : Number]) (car y)) 3) N] + [tc-e ((lambda: ([x : Number] . [y : Number]) (car y)) 3 4 5) N] + [tc-e ((lambda: ([x : Number] . [y : Number]) (car y)) 3 4) N] + [tc-e (apply (lambda: ([x : Number] . [y : Number]) (car y)) 3 '(4)) N] + [tc-e (apply (lambda: ([x : Number] . [y : Number]) (car y)) 3 '(4 6 7)) N] + [tc-e (apply (lambda: ([x : Number] . [y : Number]) (car y)) 3 '()) N] + + [tc-e (lambda: ([x : Number] . [y : boolean]) (car y)) (->* (list N) B B)] + [tc-e ((lambda: ([x : Number] . [y : boolean]) (car y)) 3) B] + [tc-e (apply (lambda: ([x : Number] . [y : boolean]) (car y)) 3 '(#f)) B] + + [tc-e (let: ([x : Number 3]) + (when (number? x) #t)) + (-val #t)] + [tc-e (let: ([x : Number 3]) + (when (boolean? x) #t)) + -Void] + + [tc-e (let: ([x : Sexp 3]) + (if (list? x) + (begin (car x) 1) 2)) + N] + + + [tc-e (let: ([x : (U Number Boolean) 3]) + (if (not (boolean? x)) + (add1 x) + 3)) + N] + + [tc-e (let ([x 1]) x) -Integer (-vet #'x) (-vef #'x)] + [tc-e (let ([x 1]) (boolean? x)) B (list (-rest B #'x)) (list (-rem B #'x))] + [tc-e (boolean? number?) B (list (-rest B #'number?)) (list (-rem B #'number?))] + + [tc-e (let: ([x : (Option Number) #f]) x) (Un N (-val #f)) (-vet #'x) (-vef #'x)] + [tc-e (let: ([x : Any 12]) (not (not x))) + B (list (-rem (-val #f) #'x)) (list (-rest (-val #f) #'x))] + + [tc-e (let: ([x : (Option Number) #f]) + (if (let ([z 1]) x) + (add1 x) + 12)) + N] + [tc-err (5 4)] + [tc-err (apply 5 '(2))] + [tc-err (map (lambda: ([x : Any] [y : Any]) 1) '(1))] + [tc-e (map add1 '(1)) (-lst N)] + + [tc-e (let ([x 5]) + (if (eq? x 1) + 12 + 14)) + N] + + [tc-e (car (append (list 1 2) (list 3 4))) N] + + [tc-e + (let-syntax ([a + (syntax-rules () + [(_ e) (let ([v 1]) e)])]) + (let: ([v : String "a"]) + (string-append "foo" (a v)))) + -String] + + [tc-e (apply (plambda: (a) [x : a] x) '(5)) (-lst N)] + [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst N)] + + [tc-err ((case-lambda: [([x : Number]) x] + [([y : Number] [x : Number]) x]) + 1 2 3)] + [tc-err ((case-lambda: [([x : Number]) x] + [([y : Number] [x : Number]) x]) + 1 'foo)] + + [tc-err (apply + (case-lambda: [([x : Number]) x] + [([y : Number] [x : Number]) x]) + '(1 2 3))] + [tc-err (apply + (case-lambda: [([x : Number]) x] + [([y : Number] [x : Number]) x]) + '(1 foo))] + + [tc-e (let: ([x : Any #f]) + (if (number? (let ([z 1]) x)) + (add1 x) + 12)) + N] + + [tc-e (let: ([x : (Option Number) #f]) + (if x + (add1 x) + 12)) + N] + + + [tc-e null (-val null) (-vet #'null) (-vef #'null)] + + [tc-e (let* ([sym 'squarf] + [x (if (= 1 2) 3 sym)]) + x) + (Un (-val 'squarf) N) + (-vet #'x) (-vef #'x)] + + [tc-e (if #t 1 2) -Integer] + + + ;; eq? as predicate + [tc-e (let: ([x : (Un 'foo Number) 'foo]) + (if (eq? x 'foo) 3 x)) N] + [tc-e (let: ([x : (Un 'foo Number) 'foo]) + (if (eq? 'foo x) 3 x)) N] + + [tc-err (let: ([x : (U String 'foo) 'foo]) + (if (string=? x 'foo) + "foo" + x))] + #;[tc-e (let: ([x : (U String 5) 5]) + (if (eq? x 5) + "foo" + x)) + (Un -String (-val 5))] + + [tc-e (let* ([sym 'squarf] + [x (if (= 1 2) 3 sym)]) + (if (eq? x sym) 3 x)) + N] + [tc-e (let* ([sym 'squarf] + [x (if (= 1 2) 3 sym)]) + (if (eq? sym x) 3 x)) + N] + ;; equal? as predicate for symbols + [tc-e (let: ([x : (Un 'foo Number) 'foo]) + (if (equal? x 'foo) 3 x)) N] + [tc-e (let: ([x : (Un 'foo Number) 'foo]) + (if (equal? 'foo x) 3 x)) N] + + [tc-e (let* ([sym 'squarf] + [x (if (= 1 2) 3 sym)]) + (if (equal? x sym) 3 x)) + N] + [tc-e (let* ([sym 'squarf] + [x (if (= 1 2) 3 sym)]) + (if (equal? sym x) 3 x)) + N] + + [tc-e (let: ([x : (Listof Symbol)'(a b c)]) + (cond [(memq 'a x) => car] + [else 'foo])) + Sym] + + [tc-e (list 1 2 3) (-lst* -Integer -Integer -Integer)] + [tc-e (list 1 2 3 'a) (-lst* -Integer -Integer -Integer (-val 'a))] + #; + [tc-e `(1 2 ,(+ 3 4)) (-lst* N N N)] + + [tc-e (let: ([x : Any 1]) + (when (and (list? x) (not (null? x))) + (car x))) + Univ] + + [tc-err (let: ([x : Any 3]) + (car x))] + [tc-err (car #{3 : Any})] + [tc-err (map #{3 : Any} #{12 : Any})] + [tc-err (car 3)] + + [tc-e (let: ([x : Any 1]) + (if (and (list? x) (not (null? x))) + x + (error 'foo))) + (-pair Univ (-lst Univ))] + + ;[tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) N] + + + + ;;; tests for and + [tc-e (let: ([x : Any 1]) (and (number? x) (boolean? x))) B + (list (-rest N #'x) (-rest B #'x)) (list)] + [tc-e (let: ([x : Any 1]) (and (number? x) x)) (Un N (-val #f)) + (list (-rest N #'x) (make-Var-True-Effect #'x)) (list)] + [tc-e (let: ([x : Any 1]) (and x (boolean? x))) B + (list (-rem (-val #f) #'x) (-rest B #'x)) (list)] + + [tc-e (let: ([x : Sexp 3]) + (if (and (list? x) (not (null? x))) + (begin (car x) 1) 2)) + N] + + ;; set! tests + [tc-e (let: ([x : Any 3]) + (set! x '(1 2 3)) + (if (number? x) x 2)) + Univ] + + ;; or tests - doesn't do anything good yet + + #; + [tc-e (let: ([x : Any 3]) + (if (or (boolean? x) (number? x)) + (if (boolean? x) 12 x) + 47)) + Univ] + + ;; test for fake or + [tc-e (let: ([x : Any 1]) + (if (if (number? x) + #t + (boolean? x)) + (if (boolean? x) 1 x) + 4)) + N] + ;; these don't invoke the or rule + [tc-e (let: ([x : Any 1] + [y : Any 12]) + (if (if (number? x) + #t + (boolean? y)) + (if (boolean? x) 1 x) + 4)) + Univ] + [tc-e (let: ([x : Any 1]) + (if (if ((lambda: ([x : Any]) x) 12) + #t + (boolean? x)) + (if (boolean? x) 1 x) + 4)) + Univ] + + ;; T-AbsPred + [tc-e (let ([p? (lambda: ([x : Any]) (number? x))]) + (lambda: ([x : Any]) (if (p? x) (add1 x) 12))) + (-> Univ N)] + [tc-e (let ([p? (lambda: ([x : Any]) (not (number? x)))]) + (lambda: ([x : Any]) (if (p? x) 12 (add1 x)))) + (-> Univ N)] + [tc-e (let* ([z 1] + [p? (lambda: ([x : Any]) (number? z))]) + (lambda: ([x : Any]) (if (p? x) 11 12))) + (-> Univ N)] + [tc-e (let* ([z 1] + [p? (lambda: ([x : Any]) (number? z))]) + (lambda: ([x : Any]) (if (p? x) x 12))) + (-> Univ Univ)] + [tc-e (let* ([z 1] + [p? (lambda: ([x : Any]) (not (number? z)))]) + (lambda: ([x : Any]) (if (p? x) x 12))) + (-> Univ Univ)] + [tc-e (let* ([z 1] + [p? (lambda: ([x : Any]) z)]) + (lambda: ([x : Any]) (if (p? x) x 12))) + (-> Univ Univ)] + + [tc-e (not 1) B] + + [tc-err ((lambda () 1) 2)] + [tc-err (apply (lambda () 1) '(2))] + [tc-err ((lambda: ([x : Any] [y : Any]) 1) 2)] + [tc-err (map map '(2))] + [tc-err ((plambda: (a) ([x : (a -> a)] [y : a]) (x y)) 5)] + [tc-err ((plambda: (a) ([x : a] [y : a]) x) 5)] + [tc-err (ann 5 : String)] + [tc-e (letrec-syntaxes+values () ([(#{x : Number}) (values 1)]) (add1 x)) N] + + [tc-err (let ([x (add1 5)]) + (set! x "foo") + x)] + ;; w-c-m + [tc-e (with-continuation-mark 'key 'mark + 3) + -Integer] + [tc-err (with-continuation-mark (5 4) 1 + 3)] + [tc-err (with-continuation-mark 1 (5 4) + 3)] + [tc-err (with-continuation-mark 1 2 (5 4))] + + + + ;; call-with-values + + [tc-e (call-with-values (lambda () (values 1 2)) + (lambda: ([x : Number] [y : Number]) (+ x y))) + N] + [tc-e (call-with-values (lambda () 1) + (lambda: ([x : Number]) (+ x 1))) + N] + [tc-err (call-with-values (lambda () 1) + (lambda: () 2))] + + [tc-err (call-with-values (lambda () (values 2)) + (lambda: ([x : Number] [y : Number]) (+ x y)))] + [tc-err (call-with-values 5 + (lambda: ([x : Number] [y : Number]) (+ x y)))] + [tc-err (call-with-values (lambda () (values 2)) + 5)] + [tc-err (call-with-values (lambda () (values 2 1)) + (lambda: ([x : String] [y : Number]) (+ x y)))] + ;; quote-syntax + [tc-e #'3 Any-Syntax] + [tc-e #'(1 2 3) Any-Syntax] + + ;; testing some primitives + [tc-e (let ([app apply] + [f (lambda: [x : Number] 3)]) + (app f (list 1 2 3))) + N] + [tc-e ((lambda () (call/cc (lambda: ([k : (Number -> (U))]) (if (read) 5 (k 10)))))) + N] + + [tc-e (number->string 5) -String] + + [tc-e (let-values ([(a b) (quotient/remainder 5 12)] + [(a*) (quotient 5 12)] + [(b*) (remainder 5 12)]) + (+ a b a* b*)) + N] + + [tc-e (raise-type-error 'foo "bar" 5) (Un)] + [tc-e (raise-type-error 'foo "bar" 7 (list 5)) (Un)] + + #;[tc-e + (let ((x '(1 3 5 7 9))) + (do: : Number ((x : (list-of Number) x (cdr x)) + (sum : Number 0 (+ sum (car x)))) + ((null? x) sum))) + N] + + + ;; inference with internal define + [tc-e (let () + (define x 1) + (define y 2) + (define z (+ x y)) + (* x z)) + N] + + [tc-e (let () + (define: (f [x : Number]) : Number + (define: (g [y : Number]) : Number + (let*-values ([(#{z : Number} #{w : Number}) (values (g (f x)) 5)]) + (+ z w))) + (g 4)) + 5) + N] + + [tc-err (let () + (define x x) + 1)] + [tc-err (let () + (define (x) (y)) + (define (y) (x)) + 1)] + + [tc-err (let () + (define (x) (y)) + (define (y) 3) + 1)] + + [tc-e ((case-lambda: + [[x : Number] (+ 1 (car x))]) + 5) + N] + #; + [tc-e `(4 ,@'(3)) (-pair N (-lst N))] + + [tc-e + (let ((x '(1 3 5 7 9))) + (do: : Number ((x : (Listof Number) x (cdr x)) + (sum : Number 0 (+ sum (car x)))) + ((null? x) sum))) + N] + + [tc-e (if #f 1 'foo) (-val 'foo)] + + [tc-e (list* 1 2 3) (-pair -Integer (-pair -Integer -Integer))] + + ;; error tests + [tc-err (#%variable-reference number?)] + [tc-err (+ 3 #f)] + [tc-err (let: ([x : Number #f]) x)] + [tc-err (let: ([x : Number #f]) (+ 1 x))] + + [tc-err + (let: ([x : Sexp '(foo)]) + (if (null? x) 1 + (if (list? x) + (add1 x) + 12)))] + + [tc-err (let*: ([x : Any 1] + [f : (-> Void) (lambda () (set! x 'foo))]) + (if (number? x) + (begin (f) (add1 x)) + 12))] + + [tc-err (lambda: ([x : Any]) + (if (number? (not (not x))) + (add1 x) + 12))] + + #;[tc-err (let: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))]) + (fact 20))] + + #;[tc-err ] + )) + (test-suite + "check-type tests" + (test-exn "Fails correctly" exn:fail:syntax? (lambda () (check-type #'here N B))) + (test-not-exn "Doesn't fail on subtypes" (lambda () (check-type #'here N Univ))) + (test-not-exn "Doesn't fail on equal types" (lambda () (check-type #'here N N))) + ) + (test-suite + "tc-literal tests" + (tc-l 5 -Integer) + (tc-l 5# -Integer) + (tc-l 5.1 N) + (tc-l #t (-val #t)) + (tc-l "foo" -String) + (tc-l foo (-val 'foo)) + (tc-l #:foo -Keyword) + (tc-l #f (-val #f)) + (tc-l #"foo" -Bytes) + [tc-l () (-val null)] + ) + )) + + +;; these no longer work with the new scheme for top-level identifiers +;; could probably be revived +#;(define (tc-toplevel-tests) +#reader typed-scheme/typed-reader +(test-suite "Tests for tc-toplevel" + (tc-tl 3) + (tc-tl (define: x : Number 4)) + (tc-tl (define: (f [x : Number]) : Number x)) + [tc-tl (pdefine: (a) (f [x : a]) : Number 3)] + [tc-tl (pdefine: (a b) (mymap [f : (a -> b)] (l : (list-of a))) : (list-of b) + (if (null? l) #{'() : (list-of b)} + (cons (f (car l)) (map f (cdr l)))))])) + + +(define-go typecheck-tests #;tc-toplevel-tests) +