suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add typed scheme tests.

Browse Source 
svn: r9404

original commit: fca36c126c2f26e8e930ad66220b4dccd6c86028
This commit is contained in:
Sam Tobin-Hochstadt 2008-04-22 21:58:10 +00:00
parent 9936e61c9a
commit 9fd128f7e5
47 changed files with 3122 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
collects/tests/typed-scheme/fail/back-and-forth.ss Normal file
View File

@ -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)

28
collects/tests/typed-scheme/fail/cnt-err1.ss Normal file
View File

@ -0,0 +1,28 @@
#;
(exn-pred exn:fail:contract? ".*expected <T.*" #rx".*contract \\(->.*")
#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)

22
collects/tests/typed-scheme/fail/gadt.ss Normal file
View File

@ -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})]))

14
collects/tests/typed-scheme/fail/set-struct.ss Normal file
View File

@ -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)))

9
collects/tests/typed-scheme/fail/set-tests.ss Normal file
View File

@ -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))

81
collects/tests/typed-scheme/main.ss Normal file
View File

@ -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))

12
collects/tests/typed-scheme/succeed/annotation-test.ss Normal file
View File

@ -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}

11
collects/tests/typed-scheme/succeed/area.ss Normal file
View File

@ -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))]))

5
collects/tests/typed-scheme/succeed/bad-map-infer.ss Normal file
View File

@ -0,0 +1,5 @@
#lang typed-scheme
(: cross1 ((Listof Number) -> (Listof Number)))
(define (cross1 m)
(map (lambda: ([m1 : Number]) #{(error 'bad) :: Number}) m))

29
collects/tests/typed-scheme/succeed/barland.ss Normal file
View File

@ -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

100
collects/tests/typed-scheme/succeed/basic-tests.ss Normal file
View File

@ -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)}))))

86
collects/tests/typed-scheme/succeed/batched-queue.scm Normal file
View File

@ -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)))

8
collects/tests/typed-scheme/succeed/broken-let-syntax.ss Normal file
View File

@ -0,0 +1,8 @@
#lang typed-scheme
(let: ([x : Number 1])
(let-syntax ([m (syntax-rules ()
[(_) x])])
(m)))

35
collects/tests/typed-scheme/succeed/cl-tests.ss Normal file
View File

@ -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*)

8
collects/tests/typed-scheme/succeed/cl.ss Normal file
View File

@ -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)]))

17
collects/tests/typed-scheme/succeed/do.ss Normal file
View File

@ -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)))

15
collects/tests/typed-scheme/succeed/fix.ss Normal file
View File

@ -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))))))))

48
collects/tests/typed-scheme/succeed/foo.scm Normal file
View File

@ -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)))
)

111
collects/tests/typed-scheme/succeed/hw01.scm Normal file
View File

@ -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))))

13
collects/tests/typed-scheme/succeed/if-splitting-test.ss Normal file
View File

@ -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]))

302
collects/tests/typed-scheme/succeed/leftist-heap.ss Normal file
View File

@ -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 =? <?)
#;"typed-list.ss"
#;(lib "42.ss" "srfi")
#;(only (lib "list.ss") foldl))
#;(provide (all-defined))
(provide comparator Heap elements empty fold heap-node? find-min empty? insert insert* delete-min size union)
#;(define-type-alias top top)
(define-type-alias comparator (top top -> 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 <? ((top top -> 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-compare h) x (heap-node-elm h))
(f)]
[else
(let ([cmp (heap-compare h)])
(let ([y (heap-node-elm h)]
[l (heap-node-left h)]
[r (heap-node-right h)])
(delete/sf x l
(lambda: ([h1 : (Heap a)]) (s (make y h1 r)))
(lambda () (delete/sf x r
(lambda: ([h1 : (Heap a)]) (s (make y l h1)))
(lambda () (f)))))))]))
(delete/sf x h
(lambda: ([h1 : (Heap a)]) h1)
(lambda () h)))
;; annotated w/ no errors
(pdefine: (a) (delete-all [x : a] [h : (Heap a)]) : (Heap a)
(define: (delete-all/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 (delete-all x (heap-node-left h))
(delete-all x (heap-node-right h))))]
[(<? (heap-compare h) x (heap-node-elm h))
(f)]
[else
(let ([cmp (heap-compare h)])
(let ([y (heap-node-elm h)]
[l (heap-node-left h)]
[r (heap-node-right h)])
(delete-all/sf x l
(lambda: ([l1 : (Heap a)]) (s (delete-all/sf x r
(lambda: ([r1 : (Heap a)]) (make y l1 r1))
(lambda () (make y l1 r)))))
(lambda () (delete-all/sf x r
(lambda: ([r1 : (Heap a)]) (s (make y l r1)))
(lambda () (f)))))))]))
(delete-all/sf x h
(lambda: ([h1 : (Heap a)]) h1)
(lambda () h)))
(pdefine: (a) (find-min [h : (heap-node a)]) : a
(heap-node-elm h))
(pdefine: (a) (delete-min [h : (heap-node a)]) : (Heap a)
(union (heap-node-left h) (heap-node-right h)))
(pdefine: (a) (get [x : a] [h : (Heap a)]) : (Un #f a)
(let ([cmp (heap-compare h)])
(define: (inner-get [h : (Heap a)] [s : (a -> 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))
|#

26
collects/tests/typed-scheme/succeed/let-values-tests.ss Normal file
View File

@ -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))

453
collects/tests/typed-scheme/succeed/little-schemer.ss Normal file
View File

@ -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))

74
collects/tests/typed-scheme/succeed/manual-examples.ss Normal file
View File

@ -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))])))

20
collects/tests/typed-scheme/succeed/match-expander-problem.ss Normal file
View File

@ -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]))

9
collects/tests/typed-scheme/succeed/mu-rec.ss Normal file
View File

@ -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))))

8
collects/tests/typed-scheme/succeed/pair-test.ss Normal file
View File

@ -0,0 +1,8 @@
#lang typed-scheme
(define: x : (Number . Boolean) (cons 3 #f))
(define: y : Number (car x))
(define: z : Boolean (cdr x))

9
collects/tests/typed-scheme/succeed/poly-struct.ss Normal file
View File

@ -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)))

27
collects/tests/typed-scheme/succeed/poly-tests.ss Normal file
View File

@ -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)

103
collects/tests/typed-scheme/succeed/priority-queue.scm Normal file
View File

@ -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 =? <?)
(only-in "leftist-heap.ss" comparator))
(require/typed number-compare (number number -> 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 <? ((top top -> number) top top -> boolean) (lib "67.ss" "srfi"))
; a priority-queue is a heap of (cons <priority> <element>)
(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)

5
collects/tests/typed-scheme/succeed/provide-syntax.ss Normal file
View File

@ -0,0 +1,5 @@
#lang typed-scheme
(define-syntax-rule (foo) 1)
(provide foo)

40
collects/tests/typed-scheme/succeed/rec-types.ss Normal file
View File

@ -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))))]))

11
collects/tests/typed-scheme/succeed/require-tests.ss Normal file
View File

@ -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))

6
collects/tests/typed-scheme/succeed/scratch.ss Normal file
View File

@ -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)))

106
collects/tests/typed-scheme/succeed/seasoned-schemer.ss Normal file
View File

@ -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)]))

4
collects/tests/typed-scheme/succeed/struct-exec.ss Normal file
View File

@ -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))

7
collects/tests/typed-scheme/succeed/typed-list.ss Normal file
View File

@ -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))))

48
collects/tests/typed-scheme/succeed/varargs-tests.ss Normal file
View File

@ -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))

4
collects/tests/typed-scheme/succeed/vec-tests.ss Normal file
View File

@ -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))

85
collects/tests/typed-scheme/unit-tests/all-tests.ss Normal file
View File

@ -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)

122
collects/tests/typed-scheme/unit-tests/infer-tests.ss Normal file
View File

@ -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) (string<? (symbol->string (car a)) (symbol->string (car b))))))
(define-go fv-tests i2-tests combine-tests)

78
collects/tests/typed-scheme/unit-tests/parse-type-tests.ss Normal file
View File

@ -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))

69
collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss Normal file
View File

@ -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)

126
collects/tests/typed-scheme/unit-tests/subtype-tests.ss Normal file
View File

@ -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)

58
collects/tests/typed-scheme/unit-tests/test-utils.ss Normal file
View File

@ -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)]))

46
collects/tests/typed-scheme/unit-tests/type-equal-tests.ss Normal file
View File

@ -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)

606
collects/tests/typed-scheme/unit-tests/typecheck-tests.ss Normal file
View File

@ -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)