Add typed scheme tests.
svn: r9404
This commit is contained in:
Sam Tobin-Hochstadt
parent
c40da0feb8
commit
fca36c126c
|
|
@ -20,5 +20,6 @@
|
|||
"srpersist"
|
||||
"stepper"
|
||||
"syntax-color"
|
||||
"typed-scheme"
|
||||
"units"
|
||||
"web-server"))
|
||||
|
|
|
|||
238
collects/tests/typed-scheme/660-examples/hw02.scm
Normal file
238
collects/tests/typed-scheme/660-examples/hw02.scm
Normal file
|
|
@ -0,0 +1,238 @@
|
|||
#reader (planet "typed-reader.ss" ("plt" "typed-scheme.plt"))
|
||||
(module hw02 "../../typed-scheme.ss"
|
||||
(require "support.ss")
|
||||
;;; --------------------------------------------------------------------
|
||||
;;; Question 1
|
||||
|
||||
;; list-product : (list-of number) (list-of number) -> number
|
||||
;; computes the dot-product of two lists (as vector representations)
|
||||
;; (Assumes the two inputs are of equal length)
|
||||
(define: (list-product [l1 : (Listof number)] [l2 : (Listof number)]) : number
|
||||
(foldl #{+ :: (number number -> number)} 0 (map #{* :: (number number -> number)} l1 l2)))
|
||||
|
||||
;; tests
|
||||
(test (list-product '(1 2 3) '(4 5 6)) => 32)
|
||||
(test (list-product '() '()) => 0)
|
||||
|
||||
|
||||
;;; --------------------------------------------------------------------
|
||||
;;; Question 2
|
||||
|
||||
#|
|
||||
|
||||
<AE> ::= <AE> + <fac>
|
||||
| <AE> - <fac>
|
||||
| <fac>
|
||||
|
||||
<fac> ::= <fac> * <atom>
|
||||
| <fac> / <atom>
|
||||
| <atom>
|
||||
|
||||
<atom> ::= <number>
|
||||
| + <atom>
|
||||
| - <atom>
|
||||
| ( <AE> )
|
||||
|
||||
In the rules for <atom>, note that any number of unary +/-
|
||||
operators can be used, and that the resulting grammar is not
|
||||
ambiguous since they are put in yet another level below <fac> (they
|
||||
have higher precedence than the binary operators).
|
||||
|
||||
|#
|
||||
|
||||
|
||||
;;; --------------------------------------------------------------------
|
||||
;;; Question 3
|
||||
|
||||
;; [3a]
|
||||
(define-type BINTREE
|
||||
[Node (l BINTREE) (r BINTREE)]
|
||||
[Leaf (n number)])
|
||||
|
||||
;; used for tests:
|
||||
(define: 1234-tree : BINTREE
|
||||
(Node (Node (Leaf 1) (Leaf 2))
|
||||
(Node (Leaf 3) (Leaf 4))))
|
||||
(define: 528-tree : BINTREE (Node (Leaf 5) (Node (Leaf 2) (Leaf 8))))
|
||||
#;(provide (all-defined))
|
||||
#| [3b] BNF:
|
||||
|
||||
<BINTREE> ::= <Node> | <Leaf>
|
||||
|
||||
<Node> ::= (Node <BINTREE> <BINTREE>)
|
||||
|
||||
<Leaf> ::= (Leaf <num>)
|
||||
|
||||
|#
|
||||
|
||||
;; [3c]
|
||||
|
||||
;; tree-reduce : BINTREE (num num -> num) -> num
|
||||
;; Reduces a BINTREE to a number by descending recursively and combining
|
||||
;; results with `op'.
|
||||
(define: (tree-reduce [tree : BINTREE] [op : (number number -> number)]) : number
|
||||
(cases tree
|
||||
[(Node l r) (op (tree-reduce l op) (tree-reduce r op))]
|
||||
[(Leaf n) n]))
|
||||
;; tests:
|
||||
(test 10 <= (tree-reduce 1234-tree +))
|
||||
(test 10 <= (tree-reduce (Leaf 10) +))
|
||||
(test 24 <= (tree-reduce 1234-tree *))
|
||||
|
||||
;; tree-min : BINTREE -> num
|
||||
;; Finds the minimum number in a BINTREE.
|
||||
(define: (tree-min [tree : BINTREE]) : number
|
||||
(tree-reduce tree min))
|
||||
;; tests:
|
||||
(test 1 <= (tree-min 1234-tree))
|
||||
(test 1 <= (tree-min (Leaf 1)))
|
||||
|
||||
;; tree-min : BINTREE -> num
|
||||
;; Finds the maximum number in a BINTREE.
|
||||
(define: (tree-max [tree : BINTREE]) : number
|
||||
(tree-reduce tree max))
|
||||
;; tests:
|
||||
(test 4 <= (tree-max 1234-tree))
|
||||
(test 1 <= (tree-max (Leaf 1)))
|
||||
|
||||
;; tree-sorted? : BINTREE -> bool
|
||||
;; Tests whether the tree is sorted or not.
|
||||
(define: (tree-sorted? [tree : BINTREE]) : boolean
|
||||
(cases tree
|
||||
[(Node l r) (and (tree-sorted? l)
|
||||
(tree-sorted? r)
|
||||
(<= (tree-max l) (tree-min r)))]
|
||||
[(Leaf n) #t]))
|
||||
;; tests:
|
||||
(test (tree-sorted? 1234-tree))
|
||||
(test (tree-sorted? (Leaf 1)))
|
||||
(test (not (tree-sorted? 528-tree)))
|
||||
#|
|
||||
#| [3d]
|
||||
|
||||
Say that the cost function is cost(n) for a tree with n leaves, and
|
||||
that we're given a balanced tree of 32 leaves. We have:
|
||||
|
||||
cost(32) = 16 ; for finding the max the left side
|
||||
+ 16 ; for finding the min the right side
|
||||
+ cost(16) ; for the recursive call on the left
|
||||
+ cost(16) ; for the recursive call on the right
|
||||
+ 1 ; some constant for the `and' and the `<'
|
||||
|
||||
In general, we can drop the last one since it doesn't matter and get:
|
||||
|
||||
cost(n) = 2*(n/2) + 2*cost(n/2) = n + 2*cost(n/2)
|
||||
|
||||
and
|
||||
|
||||
cost(1) = 1
|
||||
|
||||
Continueing with the case of 32:
|
||||
|
||||
cost(32) = 32 + 2*cost(16)
|
||||
= 32 + 2*(16 + 2*cost(8))
|
||||
= 32 + 32 + 4*cost(8)
|
||||
= 32 + 32 + 32 + 8*cost(4)
|
||||
= 32 + 32 + 32 + 32 + 16*cost(2)
|
||||
= 32 + 32 + 32 + 32 + 32 + 32*cost(1)
|
||||
= 32 + 32 + 32 + 32 + 32 + 32
|
||||
|
||||
So the total cost for n leaves is n*log2(n).
|
||||
|
||||
|#
|
||||
|
||||
;; 3e
|
||||
|
||||
;; tree-sorted*? : BINTREE -> bool
|
||||
;; Tests whether the tree is sorted or not in linear time.
|
||||
;; -- The trick is to check for sortedness by recursively walking the
|
||||
;; tree and remembering the last value we have seen and making sure
|
||||
;; that new leaves are always bigger. The return value of the helper
|
||||
;; is either the right-most value if it is sorted, or #f if not.
|
||||
(define (tree-sorted*? tree)
|
||||
;; `and' is used to turn the result into a proper boolean
|
||||
(and (sorted*?-helper
|
||||
tree
|
||||
(- (left-most-value tree) 1)) ; initialize a last value
|
||||
#t))
|
||||
|
||||
;; left-most-value : BINTREE -> num
|
||||
;; Finds the left-most value in a BINTREE.
|
||||
(define (left-most-value tree)
|
||||
(cases tree
|
||||
[(Leaf n) n]
|
||||
[(Node l r) (left-most-value l)]))
|
||||
|
||||
;; sorted*?-helper : BINTREE num -> bool-or-num
|
||||
;; Helper for the above -- checks that the given tree is sorted and
|
||||
;; bigger than the given number, and returns the right-most number if it
|
||||
;; is sorted.
|
||||
(define (sorted*?-helper tree last)
|
||||
(cases tree
|
||||
[(Leaf n)
|
||||
(and (< last n) n)]
|
||||
[(Node l r)
|
||||
(let ([left-last (sorted*?-helper l last)])
|
||||
(and left-last (sorted*?-helper r left-last)))]))
|
||||
|
||||
;; tests:
|
||||
(test (tree-sorted*? 1234-tree))
|
||||
(test (tree-sorted*? (Leaf 1)))
|
||||
(test (not (tree-sorted*? 528-tree)))
|
||||
|
||||
|
||||
;;; --------------------------------------------------------------------
|
||||
;;; Question 4
|
||||
|
||||
;; tree-map : (num -> num) BINTREE -> BINTREE
|
||||
;; Maps the given function recursively over the given tree, returning a
|
||||
;; tree of the results with the same shape.
|
||||
(define (tree-map f tree)
|
||||
(cases tree
|
||||
[(Leaf n) (Leaf (f n))]
|
||||
[(Node l r) (Node (tree-map f l) (tree-map f r))]))
|
||||
|
||||
;; tests
|
||||
(test (tree-map add1 (Node (Leaf 1) (Node (Leaf 2) (Leaf 3))))
|
||||
=> (Node (Leaf 2) (Node (Leaf 3) (Leaf 4))))
|
||||
(test (tree-map add1 1234-tree)
|
||||
=> (Node (Node (Leaf 2) (Leaf 3)) (Node (Leaf 4) (Leaf 5))))
|
||||
(test (tree-map add1 (Leaf 1))
|
||||
=> (Leaf 2))
|
||||
|
||||
|
||||
;;; --------------------------------------------------------------------
|
||||
;;; Question 5
|
||||
|
||||
;; tree-insert : BINTREE num -> BINTREE
|
||||
(define (tree-insert tree n)
|
||||
(cases tree
|
||||
[(Leaf m) (if (< n m)
|
||||
(Node (Leaf n) tree)
|
||||
(Node tree (Leaf n)))]
|
||||
[(Node l r) (if (< n (tree-max l))
|
||||
(Node (tree-insert l n) r)
|
||||
(Node l (tree-insert r n)))]))
|
||||
|
||||
;; tests:
|
||||
(test (tree-sorted?
|
||||
(tree-insert (Node (Leaf 2) (Node (Leaf 4) (Leaf 6)))
|
||||
3)))
|
||||
(test (tree-sorted? (tree-insert 1234-tree 0)))
|
||||
(test (tree-sorted? (tree-insert 1234-tree 5)))
|
||||
|
||||
|
||||
;;; --------------------------------------------------------------------
|
||||
;;; Question 6
|
||||
|
||||
#|
|
||||
|
||||
The problem is that we need to keep both flattened copies in memory
|
||||
for the comparison. This means that if we have two big trees, say
|
||||
200MB each, then during the comparison we will need to have 800MB of
|
||||
RAM! The solution for this is very hard for now, but later in the
|
||||
course we will see one easy way to solve it.
|
||||
|
||||
|#|#
|
||||
|
||||
)
|
||||
275
collects/tests/typed-scheme/660-examples/hw03.scm
Normal file
275
collects/tests/typed-scheme/660-examples/hw03.scm
Normal file
|
|
@ -0,0 +1,275 @@
|
|||
#reader (planet "typed-reader.ss" ("plt" "typed-scheme.plt"))
|
||||
(module hw03 "../../typed-scheme.ss"
|
||||
|
||||
(require "support.ss")
|
||||
|
||||
#| This is the updated Algae BNF definition:
|
||||
<ALGAE> ::= <num>
|
||||
| { + <ALGAE> ... }
|
||||
| { - <ALGAE> <ALGAE> ... }
|
||||
| { * <ALGAE> ... }
|
||||
| { / <ALGAE> <ALGAE> ... }
|
||||
| { = <ALGAE> <ALGAE> }
|
||||
| { < <ALGAE> <ALGAE> }
|
||||
| { <= <ALGAE> <ALGAE> }
|
||||
| { if <ALGAE> <ALGAE> <ALGAE> }
|
||||
| { with { <id> <ALGAE> } <ALGAE>}
|
||||
| <id>
|
||||
|#
|
||||
|
||||
(define-type ALGAE
|
||||
[Num (n number)]
|
||||
[Add (args (list-of ALGAE))]
|
||||
;; note how Sub & Div match the corresponding BNF derivation
|
||||
[Sub (fst ALGAE) (args (list-of ALGAE))]
|
||||
[Mul (args (list-of ALGAE))]
|
||||
[Div (fst ALGAE) (args (list-of ALGAE))]
|
||||
[Eql (lhs ALGAE) (rhs ALGAE)]
|
||||
[Less (lhs ALGAE) (rhs ALGAE)]
|
||||
[LessEql (lhs ALGAE) (rhs ALGAE)]
|
||||
[If (cond-expr ALGAE) (then-expr ALGAE) (else-expr ALGAE)]
|
||||
[Id (name symbol)]
|
||||
[With (name symbol) (named ALGAE) (body ALGAE)])
|
||||
|
||||
|
||||
;; parse-sexpr : s-expr -> ALGAE
|
||||
#;(define: (parse-sexpr [sexpr : Sexp]) : ALGAE
|
||||
(cond
|
||||
[(number? sexpr) (Num sexpr)]
|
||||
[(symbol? sexpr) (Id sexpr)]
|
||||
;; new code (needed because not doesn't work)
|
||||
[(null? sexpr) (error 'parse-sexpr "bad syntax in ~s" sexpr)]
|
||||
;; end new code
|
||||
;; these next two have the horrid and trick.
|
||||
[(and (list? sexpr) (not (null? sexpr))
|
||||
(eq? 'with (first sexpr))
|
||||
(let ([s (second sexpr)])
|
||||
(if (list? s)
|
||||
(if (= 2 (length s))
|
||||
(let ([sym (first s)])
|
||||
(if (symbol? sym)
|
||||
(With sym
|
||||
(parse-sexpr (second s))
|
||||
(parse-sexpr (third sexpr)))
|
||||
(error 'parse-sexpr "bad `with' syntax")))
|
||||
(error 'parse-sexpr "bad `with' syntax"))
|
||||
(error 'parse-sexpr "bad `with' syntax"))))]
|
||||
[(and (list? sexpr) (not (null? sexpr))
|
||||
(let ([subs (map parse-sexpr (rest sexpr))])
|
||||
(case (first sexpr)
|
||||
[(+) (Add subs)]
|
||||
[(-) (if (null? subs)
|
||||
(error 'parse-sexpr "need at least one arg for `-'")
|
||||
(Sub (first subs) (rest subs)))]
|
||||
[(*) (Mul subs)]
|
||||
[(/) (if (null? subs)
|
||||
(error 'parse-sexpr "need at least one arg for `/'")
|
||||
(Div (first subs) (rest subs)))]
|
||||
[(=) (if (= 2 (length subs))
|
||||
(Eql (first subs) (second subs))
|
||||
(error 'parse-sexpr "need two args for `='"))]
|
||||
[(<) (if (= 2 (length subs))
|
||||
(Less (first subs) (second subs))
|
||||
(error 'parse-sexpr "need two args for `<'"))]
|
||||
[(<=) (if (= 2 (length subs))
|
||||
(LessEql (first subs) (second subs))
|
||||
(error 'parse-sexpr "need two args for `<='"))]
|
||||
[(if) (if (= 3 (length subs))
|
||||
(If (first subs) (second subs) (third subs))
|
||||
(error 'parse-sexpr "need three exprs for `if'"))]
|
||||
[else (error 'parse-sexpr "don't know about ~s"
|
||||
(first sexpr))])))]
|
||||
[else (error 'parse-sexpr "bad syntax in ~s" sexpr)]))
|
||||
|
||||
;; parse : string -> ALGAE
|
||||
;; parses a string containing an ALGAE expression to an ALGAE AST
|
||||
#;(define: (parse [str : String]) : ALGAE
|
||||
(parse-sexpr (string->sexpr str)))
|
||||
|
||||
#| Formal specs for `subst':
|
||||
(`N' is a <num>, `E1', `E2' are <ALGAE>s, `x' is some <id>, `y' is a
|
||||
*different* <id>)
|
||||
N[v/x] = N
|
||||
{+ E ...}[v/x] = {+ E[v/x] ...}
|
||||
{- E1 E ...}[v/x] = {- E1[v/x] E[v/x] ...}
|
||||
{* E ...}[v/x] = {* E[v/x] ...}
|
||||
{/ E1 E ...}[v/x] = {/ E1[v/x] E[v/x] ...}
|
||||
{= E1 E2}[v/x] = {= E1[v/x] E2[v/x]}
|
||||
{< E1 E2}[v/x] = {< E1[v/x] E2[v/x]}
|
||||
{<= E1 E2}[v/x] = {<= E1[v/x] E2[v/x]}
|
||||
{if E1 E2 E3}[v/x] = {if E1[v/x] E2[v/x] E3[v/x]}
|
||||
y[v/x] = y
|
||||
x[v/x] = v
|
||||
{with {y E1} E2}[v/x] = {with {y E1[v/x]} E2[v/x]}
|
||||
{with {x E1} E2}[v/x] = {with {x E1[v/x]} E2}
|
||||
|#
|
||||
|
||||
;; subst : ALGAE symbol ALGAE -> ALGAE
|
||||
;; substitutes the second argument with the third argument in the
|
||||
;; first argument, as per the rules of substitution; the resulting
|
||||
;; expression contains no free instances of the second argument
|
||||
(define: (subst [expr : ALGAE] [from : Symbol] [to : ALGAE]) : ALGAE
|
||||
(let ([subst-list (lambda: ([exprs : (Listof ALGAE)])
|
||||
(map (lambda: ([x : ALGAE]) (subst x from to)) exprs))])
|
||||
(cases expr
|
||||
[(Num n) expr]
|
||||
[(Add args) (Add (subst-list args))]
|
||||
[(Mul args) (Mul (subst-list args))]
|
||||
[(Sub fst args) (Sub (subst fst from to) (subst-list args))]
|
||||
[(Div fst args) (Div (subst fst from to) (subst-list args))]
|
||||
[(Eql l r) (Eql (subst l from to) (subst r from to))]
|
||||
[(Less l r) (Less (subst l from to) (subst r from to))]
|
||||
[(LessEql l r) (LessEql (subst l from to) (subst r from to))]
|
||||
[(If c t e) (If (subst c from to)
|
||||
(subst t from to)
|
||||
(subst e from to))]
|
||||
[(Id id) (if (eq? id from) to expr)]
|
||||
[(With bound-id named-expr bound-body)
|
||||
(With bound-id
|
||||
(subst named-expr from to)
|
||||
(if (eq? bound-id from)
|
||||
bound-body
|
||||
(subst bound-body from to)))])))
|
||||
|
||||
(define: (subst2 [expr : ALGAE] [from : Symbol] [to : ALGAE]) : ALGAE
|
||||
(let ([subst-list (lambda: ([exprs : (Listof ALGAE)])
|
||||
(map (lambda: ([x : ALGAE]) (subst2 x from to)) exprs))])
|
||||
(cond
|
||||
[(Num? expr) expr]
|
||||
[(Add? expr) (Add (subst-list (Add-args expr)))]
|
||||
[(Mul? expr) (Mul (subst-list (Mul-args expr)))]
|
||||
[(Sub? expr) (Sub (subst2 (Sub-fst expr) from to) (subst-list (Sub-args expr)))]
|
||||
[(Div? expr) (Div (subst2 (Div-fst expr) from to) (subst-list (Div-args expr)))]
|
||||
[(Eql? expr) (Eql (subst2 (Eql-lhs expr) from to) (subst2 (Eql-rhs expr) from to))]
|
||||
[(Less? expr) (Less (subst2 (Less-lhs expr) from to) (subst2 (Less-rhs expr) from to))]
|
||||
[(LessEql? expr) (LessEql (subst2 (LessEql-lhs expr) from to) (subst2 (LessEql-rhs expr) from to))]
|
||||
[(If? expr) (If (subst2 (If-cond-expr expr) from to)
|
||||
(subst2 (If-then-expr expr) from to)
|
||||
(subst2 (If-else-expr expr) from to))]
|
||||
[(Id? expr) (if (eq? (Id-name expr) from) to expr)]
|
||||
[(With? expr)
|
||||
(With (With-name expr)
|
||||
(subst2 (With-named expr) from to)
|
||||
(if (eq? (With-name expr) from)
|
||||
(With-body expr)
|
||||
(subst2 (With-body expr) from to)))])))
|
||||
|
||||
#| Formal specs for `eval':
|
||||
eval(N) = N
|
||||
eval({+ E ...}) = eval(E) + ...
|
||||
eval({- E1}) = -eval(E1)
|
||||
eval({- E1 E ...}) = eval(E1) - (eval(E) + ...)
|
||||
eval({* E ...}) = eval(E1) * ...
|
||||
eval({/ E1}) = 1/eval(E1)
|
||||
eval({/ E1 E ...}) = eval(E1) / (eval(E) * ...)
|
||||
eval({= E1 E2}) = 1 if eval(E1)=eval(E2), 0 otherwise
|
||||
eval({< E1 E2}) = 1 if eval(E1)<eval(E2), 0 otherwise
|
||||
eval({<= E1 E2}) = 1 if eval(E1)<=eval(E2), 0 otherwise
|
||||
eval({if E1 E2 E3}) = eval(E3) if eval(E1)=0, eval(E2) otherwise
|
||||
eval(id) = error!
|
||||
eval({with {x E1} E2}) = eval(E2[eval(E1)/x])
|
||||
|#
|
||||
|
||||
;; -eval : ALGAE -> number
|
||||
;; evaluates ALGAE expressions by reducing them to numbers
|
||||
(define: (-eval [expr : ALGAE]) : Number
|
||||
(cases expr
|
||||
[(Num n) n]
|
||||
[(Add args) (foldl #{+ : (Number Number -> Number)} 0 (map -eval args))]
|
||||
[(Mul args) (foldl #{* : (Number Number -> Number)} 1 (map -eval args))]
|
||||
[(Sub fst args) (if (null? args)
|
||||
(- (-eval fst))
|
||||
(- (-eval fst) (foldl #{+ : (Number Number -> Number)} 0 (map -eval args))))]
|
||||
[(Div fst args) (if (null? args)
|
||||
(/ (-eval fst))
|
||||
(/ (-eval fst) (foldl #{* : (Number Number -> Number)} 1 (map -eval args))))]
|
||||
[(Eql l r) (if (= (-eval l) (-eval r)) 1 0)]
|
||||
[(Less l r) (if (< (-eval l) (-eval r)) 1 0)]
|
||||
[(LessEql l r) (if (<= (-eval l) (-eval r)) 1 0)]
|
||||
[(If cond then else) (-eval (if (= 0 (-eval cond)) else then))]
|
||||
[(With bound-id named-expr bound-body)
|
||||
(-eval (subst bound-body bound-id (Num (-eval named-expr))))]
|
||||
[(Id id) (error '-eval "free identifier: ~s" id)]))
|
||||
|
||||
;; run : string -> number
|
||||
;; evaluate an ALGAE program contained in a string
|
||||
#;(define: (run [str : String]) : Number
|
||||
(-eval (parse str)))
|
||||
|
||||
;; previous tests
|
||||
(test 5 <= (run "5"))
|
||||
(test 10 <= (run "{+ 5 5}"))
|
||||
(test 20 <= (run "{with {x {+ 5 5}} {+ x x}}"))
|
||||
(test 10 <= (run "{with {x 5} {+ x x}}"))
|
||||
(test 14 <= (run "{with {x {+ 5 5}} {with {y {- x 3}} {+ y y}}}"))
|
||||
(test 4 <= (run "{with {x 5} {with {y {- x 3}} {+ y y}}}"))
|
||||
(test 15 <= (run "{with {x 5} {+ x {with {x 3} 10}}}"))
|
||||
(test 8 <= (run "{with {x 5} {+ x {with {x 3} x}}}"))
|
||||
(test 10 <= (run "{with {x 5} {+ x {with {y 3} x}}}"))
|
||||
(test 5 <= (run "{with {x 5} {with {y x} y}}"))
|
||||
(test 5 <= (run "{with {x 5} {with {x x} x}}"))
|
||||
;; new tests
|
||||
(test 0 <= (run "{+}"))
|
||||
(test 1 <= (run "{*}"))
|
||||
(test -2 <= (run "{- 2}"))
|
||||
(test 1/2 <= (run "{/ 2}"))
|
||||
(test 1/2 <= (run "{/ 1 2}"))
|
||||
(test 10 <= (run "{+ 1 2 3 4}"))
|
||||
(test 2 <= (run "{if {< 2 3} 2 3}"))
|
||||
(test 2 <= (run "{if {<= 3 3} 2 3}"))
|
||||
(test 3 <= (run "{if {= 2 3} {/ 2 0} 3}"))
|
||||
(test 1 <= (run "{+ {= 3 3} {< 3 2} {<= 3 2}}"))
|
||||
(test 1 <= (run "{with {x 2} {= 1/8 {/ {* x 4}}}}"))
|
||||
(test 1 <= (run "{with {x 2} {if {< 1 2} {<= 1 2} 3}}"))
|
||||
;; test errors
|
||||
(test (run "{-}") =error> "need at least")
|
||||
(test (run "{/}") =error> "need at least")
|
||||
(test (run "{= 1 2 3}") =error> "need two args")
|
||||
(test (run "{< 1}") =error> "need two args")
|
||||
(test (run "{<=}") =error> "need two args")
|
||||
(test (run "{with 1}") =error> "bad * syntax")
|
||||
(test (run "{with {x 1} y}") =error> "free identifier")
|
||||
(test (run "{if 1}") =error> "need three")
|
||||
(test (run "{foo 1}") =error> "don't know")
|
||||
(test (run "{}") =error> "bad syntax in")
|
||||
|
||||
#| Dessert answer:
|
||||
|
||||
Adding `...' (or Kleene star) to our BNF language does not make it
|
||||
more expressive. An informal proof: say that you have a BNF with
|
||||
some use of `...' ("?" indicates unknown parts):
|
||||
|
||||
<FOO> ::= ? | ? <BAR> ... ? | ?
|
||||
|
||||
we can translate that to a BNF that does not use `...' by inventing a
|
||||
fresh non-terminal (say that `<FOO1>' is not used elsewhere) and
|
||||
rewriting the above derivation as follows:
|
||||
|
||||
<FOO> ::= ? | ? <FOO1> ? | ?
|
||||
<FOO1> ::= <BAR> <FOO1>
|
||||
| <-- an empty derivation
|
||||
|
||||
This can be systematically repeated, and the result will be an
|
||||
ellipsis-free BNF that is equivalent to the original.
|
||||
|
||||
|#
|
||||
|
||||
#| Bonus answer
|
||||
|
||||
Yes, we could simulate `and' and `or' using arithmetics:
|
||||
|
||||
* use {* x y} instead of {and x y}
|
||||
|
||||
* use {+ {* x x} {* y y}} instead of {or x y}
|
||||
|
||||
... but that wouldn't be enough to do short circuiting and simulating
|
||||
Scheme's `and' and `or', because these forms will evaluate *all* of
|
||||
their subexpressions. To do that properly, we need more than
|
||||
arithmetics: we need conditionals. For example:
|
||||
|
||||
* use {if x y 0} instead of {and x y}
|
||||
|
||||
* use {if x 1 y} instead of {or x y}
|
||||
|
||||
|#
|
||||
)
|
||||
349
collects/tests/typed-scheme/660-examples/hw04.scm
Normal file
349
collects/tests/typed-scheme/660-examples/hw04.scm
Normal file
|
|
@ -0,0 +1,349 @@
|
|||
#reader (planet "typed-reader.ss" ("plt" "typed-scheme.plt"))
|
||||
(module hw04 "../../typed-scheme.ss"
|
||||
|
||||
(require "support.ss")
|
||||
|
||||
#| This is the updated Algae BNF definition:
|
||||
<PROGRAM> ::= { program <FUN> ... }
|
||||
<FUN> ::= { fun <id> { <id> } <ALGAE> }
|
||||
<ALGAE> ::= <num>
|
||||
| { + <ALGAE> ... }
|
||||
| { - <ALGAE> <ALGAE> ... }
|
||||
| { * <ALGAE> ... }
|
||||
| { / <ALGAE> <ALGAE> ... }
|
||||
| { = <ALGAE> <ALGAE> }
|
||||
| { < <ALGAE> <ALGAE> }
|
||||
| { <= <ALGAE> <ALGAE> }
|
||||
| { if <ALGAE> <ALGAE> <ALGAE> }
|
||||
| { with { <id> <ALGAE> } <ALGAE>}
|
||||
| <id>
|
||||
| { call <id> <ALGAE> }
|
||||
|#
|
||||
|
||||
|
||||
(define-type ALGAE
|
||||
[Num (n number)]
|
||||
[Add (args (list-of ALGAE))]
|
||||
;; note how Sub & Div match the corresponding BNF derivation
|
||||
[Sub (fst ALGAE) (args (list-of ALGAE))]
|
||||
[Mul (args (list-of ALGAE))]
|
||||
[Div (fst ALGAE) (args (list-of ALGAE))]
|
||||
[Eql (lhs ALGAE) (rhs ALGAE)]
|
||||
[Less (lhs ALGAE) (rhs ALGAE)]
|
||||
[LessEql (lhs ALGAE) (rhs ALGAE)]
|
||||
[If (cond-expr ALGAE) (then-expr ALGAE) (else-expr ALGAE)]
|
||||
[Id (name symbol)]
|
||||
[With (name symbol) (named ALGAE) (body ALGAE)]
|
||||
[Call (fun symbol) (arg ALGAE)])
|
||||
|
||||
(define-type FUN
|
||||
[Fun (name symbol) (arg symbol) (body ALGAE)])
|
||||
|
||||
(define-type PROGRAM
|
||||
[Funs (funs (list-of FUN))])
|
||||
|
||||
|
||||
;; parse-program : s-expr -> PROGRAM
|
||||
;; parses a whole program s-expression into a PROGRAM
|
||||
#;(define: (parse-program [sexpr : Sexp]) : PROGRAM
|
||||
(if (and (list? sexpr)
|
||||
(not (null? sexpr))
|
||||
(eq? 'program (first sexpr)))
|
||||
(Funs (map parse-fun (rest sexpr)))
|
||||
(error 'parse-program "bad program syntax: ~s" sexpr)))
|
||||
|
||||
;; parse-fun : s-expr -> FUN
|
||||
;; parses a function s-expression syntax to an instance of FUN
|
||||
#;(define: (parse-fun [sexpr : Sexp]) : FUN
|
||||
(if (and ;; check overall structure
|
||||
(list? sexpr)
|
||||
(= 4 (length sexpr))
|
||||
(eq? 'fun (first sexpr))
|
||||
;; check function name
|
||||
(symbol? (second sexpr))
|
||||
;; check argument in a sublist
|
||||
(list? (third sexpr))
|
||||
(= 1 (length (third sexpr)))
|
||||
(symbol? (first (third sexpr))))
|
||||
;; assemble the needed Fun parts
|
||||
(Fun (second sexpr)
|
||||
(first (third sexpr))
|
||||
(parse-expr (fourth sexpr)))
|
||||
(error 'parse-program "bad function syntax: ~s" sexpr)))
|
||||
|
||||
;; parse-expr : s-expr -> ALGAE
|
||||
;; parses an s-expression into an ALGAE abstract syntax tree
|
||||
#;(define: (parse-expr [sexpr : Sexp]) : ALGAE
|
||||
(cond
|
||||
[(number? sexpr) (Num sexpr)]
|
||||
[(symbol? sexpr) (Id sexpr)]
|
||||
[(and (list? sexpr) (not (null? sexpr))
|
||||
(eq? 'with (first sexpr)))
|
||||
(if (and (list? (second sexpr))
|
||||
(= 2 (length (second sexpr)))
|
||||
(symbol? (first (second sexpr))))
|
||||
(With (first (second sexpr))
|
||||
(parse-expr (second (second sexpr)))
|
||||
(parse-expr (third sexpr)))
|
||||
(error 'parse-expr "bad `with' syntax"))]
|
||||
;; and trick
|
||||
[(and (list? sexpr) (not (null? sexpr))
|
||||
(eq? 'call (first sexpr)))
|
||||
(if (and (= 3 (length sexpr)) (symbol? (second sexpr)))
|
||||
(Call (second sexpr)
|
||||
(parse-expr (third sexpr)))
|
||||
(error 'parse-expr "bad `call' syntax"))]
|
||||
;; and trick
|
||||
[(and (list? sexpr) (not (null? sexpr)))
|
||||
(let ([subs (map parse-expr (rest sexpr))])
|
||||
(case (first sexpr)
|
||||
[(+) (Add subs)]
|
||||
[(-) (if (null? subs)
|
||||
(error 'parse-expr "need at least one arg for `-'")
|
||||
(Sub (first subs) (rest subs)))]
|
||||
[(*) (Mul subs)]
|
||||
[(/) (if (null? subs)
|
||||
(error 'parse-expr "need at least one arg for `/'")
|
||||
(Div (first subs) (rest subs)))]
|
||||
[(=) (if (= 2 (length subs))
|
||||
(Eql (first subs) (second subs))
|
||||
(error 'parse-expr "need two args for `='"))]
|
||||
[(<) (if (= 2 (length subs))
|
||||
(Less (first subs) (second subs))
|
||||
(error 'parse-expr "need two args for `<'"))]
|
||||
[(<=) (if (= 2 (length subs))
|
||||
(LessEql (first subs) (second subs))
|
||||
(error 'parse-expr "need two args for `<='"))]
|
||||
[(if) (if (= 3 (length subs))
|
||||
(If (first subs) (second subs) (third subs))
|
||||
(error 'parse-expr "need three exprs for `if'"))]
|
||||
[else (error 'parse-expr "don't know about ~s"
|
||||
(first sexpr))]))]
|
||||
[else (error 'parse-expr "bad syntax in ~s" sexpr)]))
|
||||
|
||||
;; Bonus:
|
||||
;; verify-functions : PROGRAM -> void
|
||||
;; this function verifies the list of functions, and doesn't return any
|
||||
;; useful value.
|
||||
(define: (verify-functions [prog : PROGRAM]) : Any
|
||||
;; this will fail if there is no `main' definition
|
||||
(lookup-fun 'main prog)
|
||||
;; check for repeating names, see helper below
|
||||
(check-duplicates (map Fun-name (Funs-funs prog)) '())
|
||||
;; finally, scan `Call' syntaxes
|
||||
(check-calls-list (map Fun-body (Funs-funs prog)) prog))
|
||||
|
||||
;; check-duplicates : (list-of symbol) (list-of symbol) -> void
|
||||
;; helper for `verify-functions'
|
||||
(define: (check-duplicates [symbols : (Listof Symbol)] [seen : (Listof Symbol)]) : Any
|
||||
;; `symbols' is what we check, `seen' is names we've already seen
|
||||
(cond [(null? symbols) 'ok]
|
||||
[(member (first symbols) seen)
|
||||
(error 'verify-functions
|
||||
"duplicate definition: ~s" (first symbols))]
|
||||
[else (check-duplicates (rest symbols) ;; CHANGE
|
||||
(cons (first symbols) seen))]))
|
||||
|
||||
;; helper for `verify-functions'
|
||||
(define: (check-calls-list [funs : (Listof ALGAE)] [prog : PROGRAM]) : Any
|
||||
(if (null? funs)
|
||||
'ok
|
||||
;; note that `and' is not really needed below, we just want to use
|
||||
;; both expressions so everything is checked. Also in
|
||||
;; `check-calls-expr'.
|
||||
(and (check-calls-expr (first funs) prog)
|
||||
(check-calls-list (rest funs) prog))))
|
||||
|
||||
(define: (check-calls-expr [expr : ALGAE] [prog : PROGRAM]) : Any
|
||||
(cases expr
|
||||
[(Num n) 'ok]
|
||||
[(Add args) (check-calls-list args prog)]
|
||||
[(Mul args) (check-calls-list args prog)]
|
||||
[(Sub fst args) (check-calls-list (cons fst args) prog)]
|
||||
[(Div fst args) (check-calls-list (cons fst args) prog)]
|
||||
[(Eql l r) (and (check-calls-expr l prog)
|
||||
(check-calls-expr r prog))]
|
||||
[(Less l r) (and (check-calls-expr l prog)
|
||||
(check-calls-expr r prog))]
|
||||
[(LessEql l r) (and (check-calls-expr l prog)
|
||||
(check-calls-expr r prog))]
|
||||
[(If c t e) (and (check-calls-expr c prog)
|
||||
(check-calls-expr t prog)
|
||||
(check-calls-expr e prog))]
|
||||
[(Id id) 'ok]
|
||||
[(With bound-id named-expr bound-body)
|
||||
(and (check-calls-expr named-expr prog)
|
||||
(check-calls-expr bound-body prog))]
|
||||
[(Call fun-name arg)
|
||||
(and (lookup-fun fun-name prog)
|
||||
(check-calls-expr arg prog))]))
|
||||
|
||||
;; parse : string -> PROGRAM
|
||||
;; parses a string containing an ALGAE program to a PROGRAM instance
|
||||
#;(define (parse str)
|
||||
(let ([prog (parse-program (string->sexpr str))])
|
||||
;; Bonus answer: the reason we use two expressions is that
|
||||
;; `verify-functions' can only signal errors, so it is used only for
|
||||
;; its side effect.
|
||||
(verify-functions prog)
|
||||
prog))
|
||||
|
||||
;; subst : ALGAE symbol ALGAE -> ALGAE
|
||||
;; substitutes the second argument with the third argument in the
|
||||
;; first argument, as per the rules of substitution; the resulting
|
||||
;; expression contains no free instances of the second argument
|
||||
(define: (subst [expr : ALGAE] [from : symbol] [to : ALGAE]) : ALGAE
|
||||
(let ([subst-list (lambda: ([exprs : (Listof ALGAE)])
|
||||
(map (lambda: ([x : ALGAE]) (subst x from to)) exprs))])
|
||||
(cases expr
|
||||
[(Num n) expr]
|
||||
[(Add args) (Add (subst-list args))]
|
||||
[(Mul args) (Mul (subst-list args))]
|
||||
[(Sub fst args) (Sub (subst fst from to) (subst-list args))]
|
||||
[(Div fst args) (Div (subst fst from to) (subst-list args))]
|
||||
[(Eql l r) (Eql (subst l from to) (subst r from to))]
|
||||
[(Less l r) (Less (subst l from to) (subst r from to))]
|
||||
[(LessEql l r) (LessEql (subst l from to) (subst r from to))]
|
||||
[(If c t e) (If (subst c from to)
|
||||
(subst t from to)
|
||||
(subst e from to))]
|
||||
[(Id id) (if (eq? id from) to expr)]
|
||||
[(With bound-id named-expr bound-body)
|
||||
(With bound-id
|
||||
(subst named-expr from to)
|
||||
(if (eq? bound-id from)
|
||||
bound-body
|
||||
(subst bound-body from to)))]
|
||||
[(Call fun-name arg) (Call fun-name (subst arg from to))])))
|
||||
|
||||
;; lookup-fun : symbol PROGRAM -> FUN
|
||||
;; looks up a FUN instance in a PROGRAM given its name
|
||||
(define: (lookup-fun [name : Symbol] [prog : PROGRAM]) : FUN
|
||||
(cases prog
|
||||
[(Funs funs)
|
||||
(or (ormap (lambda: ([fun : FUN])
|
||||
;; `ormap' will return the first true (= non-#f)
|
||||
;; result, so this is both a predicate and returning
|
||||
;; the value that is used
|
||||
(cases fun
|
||||
[(Fun fname arg expr) (and (eq? fname name) fun)]))
|
||||
funs)
|
||||
(error 'lookup-fun
|
||||
"missing function definition for: ~s" name))]))
|
||||
|
||||
;; eval : ALGAE PROGRAM -> number
|
||||
;; evaluates ALGAE expressions by reducing them to numbers
|
||||
;; `prog' is provided for function lookup
|
||||
(define: (-eval [expr : ALGAE] [prog : PROGRAM]) : Number
|
||||
;; note the scoping rules: the following function will call the real
|
||||
;; eval, but it expects a single argument, and always uses `prog'
|
||||
(let ([-eval (lambda: ([expr : ALGAE]) (-eval expr prog))])
|
||||
(cases expr
|
||||
[(Num n) n]
|
||||
[(Add args) (foldl #{+ :: (Number Number -> Number)} 0 (map -eval args))]
|
||||
[(Mul args) (foldl #{* :: (Number Number -> Number)} 1 (map -eval args))]
|
||||
[(Sub fst args) (if (null? args)
|
||||
(- (-eval fst))
|
||||
(- (-eval fst) (foldl #{+ :: (Number Number -> Number)} 0 (map -eval args))))]
|
||||
[(Div fst args) (if (null? args)
|
||||
(/ (-eval fst))
|
||||
(/ (-eval fst) (foldl #{* :: (Number Number -> Number)} 1 (map -eval args))))]
|
||||
[(Eql l r) (if (= (-eval l) (-eval r)) 1 0)]
|
||||
[(Less l r) (if (< (-eval l) (-eval r)) 1 0)]
|
||||
[(LessEql l r) (if (<= (-eval l) (-eval r)) 1 0)]
|
||||
[(If cond then else) (-eval (if (= 0 (-eval cond)) else then))]
|
||||
[(With bound-id named-expr bound-body)
|
||||
(-eval (subst bound-body bound-id (Num (-eval named-expr))))]
|
||||
[(Id id) (error '-eval "free identifier: ~s" id)]
|
||||
[(Call fun-name arg)
|
||||
(cases (lookup-fun fun-name prog)
|
||||
[(Fun name bound-id body)
|
||||
(-eval (subst body bound-id (Num (-eval arg))))])])))
|
||||
|
||||
;; run : string number -> number
|
||||
;; evaluate an ALGAE complete program contained in a string using a
|
||||
;; given value
|
||||
#;(define: (run [str : String] [arg : Number]) : Number
|
||||
(let ([prog (parse str)])
|
||||
(-eval (Call 'main (Num arg)) prog)))
|
||||
|
||||
;; big test
|
||||
(test (run "{program
|
||||
{fun even? {n}
|
||||
{if {= 0 n} 1 {call odd? {- n 1}}}}
|
||||
{fun odd? {n}
|
||||
{if {= 0 n} 0 {call even? {- n 1}}}}
|
||||
{fun main {n}
|
||||
{if {= n 1}
|
||||
1
|
||||
{+ 1 {call main
|
||||
{if {call even? n}
|
||||
{/ n 2}
|
||||
{+ 1 {* n 3}}}}}}}}"
|
||||
3)
|
||||
=> 8)
|
||||
;; test cases for full coverage
|
||||
(test (run "1" 1)
|
||||
=error> "bad program syntax")
|
||||
(test (run "{program 1}" 1)
|
||||
=error> "bad function syntax")
|
||||
(test (run "{program {fun main {x} {with {y 1} {+ x y}}}}" 1)
|
||||
=> 2)
|
||||
(test (run "{program {fun main {x} {with {foo 1} {call foo foo}}}
|
||||
{fun foo {x} {- x -1}}}"
|
||||
1)
|
||||
=> 2)
|
||||
(test (run "{program {fun main {x} {with y {+ x y}}}}" 1)
|
||||
=error> "bad `with' syntax")
|
||||
(test (run "{program {fun main {x} {call 1 2}}}" 1)
|
||||
=error> "bad `call' syntax")
|
||||
(test (run "{program {fun main {x} {-}}}" 1)
|
||||
=error> "need at least one")
|
||||
(test (run "{program {fun main {x} {/}}}" 1)
|
||||
=error> "need at least one")
|
||||
(test (run "{program {fun main {x} {=}}}" 1)
|
||||
=error> "need two args")
|
||||
(test (run "{program {fun main {x} {< 1}}}" 1)
|
||||
=error> "need two args")
|
||||
(test (run "{program {fun main {x} {<=}}}" 1)
|
||||
=error> "need two args")
|
||||
(test (run "{program {fun main {x} {if 1 2 3 4}}}" 1)
|
||||
=error> "need three exprs")
|
||||
(test (run "{program {fun main {x} {main 1}}}" 1)
|
||||
=error> "don't know about")
|
||||
(test (run "{program {fun main {x} {}}}" 1)
|
||||
=error> "bad syntax in")
|
||||
(test (run "{program {fun main {x} x} {fun main {x} x}}" 1)
|
||||
=error> "duplicate definition")
|
||||
(test (run "{program {fun main {x} {call foo x}}}" 1)
|
||||
=error> "missing function definition")
|
||||
(test (run "{program {fun main {x} y}}" 1)
|
||||
=error> "free identifier")
|
||||
(test (run "{program
|
||||
{fun main {x}
|
||||
{*{+{*{+{*}{*}}{+{*}{*}{*}{*}}{+{*}{*}{*}{*}}}{*}}
|
||||
{+{*}{*}{*}{*}{*}}
|
||||
{+{*}{*}{*}{*}}}}}" 1)
|
||||
=> 660)
|
||||
(test (run "{program {fun main {x} {+ {< x 3} {<= x 3} {= x 3}}}}" 1)
|
||||
=> 2)
|
||||
(test (run "{program {fun main {x} {+ {< x 3} {<= x 3} {= x 3}}}}" 3)
|
||||
=> 2)
|
||||
(test (run "{program {fun main {x} {+ {< x 3} {<= x 3} {= x 3}}}}" 4)
|
||||
=> 0)
|
||||
(test (run "{program {fun main {x} {* {- x} {/ x}}}}" 2)
|
||||
=> -1)
|
||||
(test (run "{program {fun main {x} {with {x 2} x}}}" 1)
|
||||
=> 2)
|
||||
;; can't check `run' since we won't check that the error happend when
|
||||
;; parsing
|
||||
(test (parse "{program {fun foo {x} x}}")
|
||||
=error> "missing function definition for: main")
|
||||
(test (parse "{program {fun main {x} {call bar x}} {fun foo {x} x}}")
|
||||
=error> "missing function definition for: bar")
|
||||
;; test that the language is not higher order
|
||||
(test 1 <= (run "{program {fun foo {foo} foo}
|
||||
{fun main {foo} {call foo foo}}}"
|
||||
1))
|
||||
|
||||
)
|
||||
222
collects/tests/typed-scheme/660-examples/hw05.scm
Normal file
222
collects/tests/typed-scheme/660-examples/hw05.scm
Normal file
|
|
@ -0,0 +1,222 @@
|
|||
#reader(planet "typed-reader.ss" ("plt" "typed-scheme.plt"))
|
||||
(module hw05 "../../typed-scheme.ss"
|
||||
|
||||
(require "support.ss")
|
||||
|
||||
#|
|
||||
The grammar:
|
||||
<BRANG> ::= <num>
|
||||
| { + <BRANG> <BRANG> }
|
||||
| { - <BRANG> <BRANG> }
|
||||
| { * <BRANG> <BRANG> }
|
||||
| { / <BRANG> <BRANG> }
|
||||
| { with { <id> <BRANG> } <BRANG> }
|
||||
| <id>
|
||||
| { fun { <id> } <BRANG> }
|
||||
| { call <BRANG> <BRANG> }
|
||||
|
||||
Evaluation rules:
|
||||
eval(N,env) = N
|
||||
eval({+ E1 E2},env) = eval(E1,env) + eval(E2,env)
|
||||
eval({- E1 E2},env) = eval(E1,env) - eval(E2,env)
|
||||
eval({* E1 E2},env) = eval(E1,env) * eval(E2,env)
|
||||
eval({/ E1 E2},env) = eval(E1,env) / eval(E2,env)
|
||||
eval(Ref(N),env) = list-ref(env,N)
|
||||
eval({with {x E1} E2},env) = eval(E2,cons(eval(E1,env),env))
|
||||
eval({fun {x} E},env) = <{fun {x} E},env>
|
||||
eval({call E1 E2},env1) = eval(Ef,cons(eval(E2,env1),env2))
|
||||
if eval(E1,env1)=<{fun {x} Ef},env2>
|
||||
= error! otherwise
|
||||
|#
|
||||
|
||||
;; input syntax
|
||||
(define-type BRANG
|
||||
[Num (n number)]
|
||||
[Add (lhs BRANG) (rhs BRANG)]
|
||||
[Sub (lhs BRANG) (rhs BRANG)]
|
||||
[Mul (lhs BRANG) (rhs BRANG)]
|
||||
[Div (lhs BRANG) (rhs BRANG)]
|
||||
[Id (name symbol)]
|
||||
[With (name symbol) (named BRANG) (body BRANG)]
|
||||
[Fun (name symbol) (body BRANG)]
|
||||
[Call (fun-expr BRANG) (arg-expr BRANG)])
|
||||
|
||||
;; preprocessed syntax
|
||||
(define-type BRANG*
|
||||
[Num* (n number)]
|
||||
[Add* (lhs BRANG*) (rhs BRANG*)]
|
||||
[Sub* (lhs BRANG*) (rhs BRANG*)]
|
||||
[Mul* (lhs BRANG*) (rhs BRANG*)]
|
||||
[Div* (lhs BRANG*) (rhs BRANG*)]
|
||||
[Ref* (idx Number)]
|
||||
[With* (named BRANG*) (body BRANG*)]
|
||||
[Fun* (body BRANG*)]
|
||||
[Call* (fun-expr BRANG*) (arg-expr BRANG*)])
|
||||
|
||||
;; parse-sexpr : s-expr -> BRANG
|
||||
#;(define (parse-sexpr sexpr)
|
||||
(cond [(number? sexpr) (Num sexpr)]
|
||||
[(symbol? sexpr) (Id sexpr)]
|
||||
[(and (list? sexpr)
|
||||
(not (null? sexpr))
|
||||
(eq? 'with (first sexpr)))
|
||||
(if (and (= 3 (length sexpr))
|
||||
(list? (second sexpr))
|
||||
(= 2 (length (second sexpr)))
|
||||
(symbol? (first (second sexpr))))
|
||||
(With (first (second sexpr))
|
||||
(parse-sexpr (second (second sexpr)))
|
||||
(parse-sexpr (third sexpr)))
|
||||
(error 'parse-sexpr "bad `with' syntax"))]
|
||||
[(and (list? sexpr)
|
||||
(not (null? sexpr))
|
||||
(eq? 'fun (first sexpr)))
|
||||
(if (and (= 3 (length sexpr))
|
||||
(list? (second sexpr))
|
||||
(= 1 (length (second sexpr)))
|
||||
(symbol? (first (second sexpr))))
|
||||
(Fun (first (second sexpr))
|
||||
(parse-sexpr (third sexpr)))
|
||||
(error 'parse-sexpr "bad `fun' syntax"))]
|
||||
[(and (list? sexpr) (= 3 (length sexpr)))
|
||||
(let ([make-node
|
||||
(case (first sexpr)
|
||||
[(+) Add]
|
||||
[(-) Sub]
|
||||
[(*) Mul]
|
||||
[(/) Div]
|
||||
[(call) Call]
|
||||
[else (error 'parse-sexpr "don't know about ~s"
|
||||
(first sexpr))])])
|
||||
(make-node (parse-sexpr (second sexpr))
|
||||
(parse-sexpr (third sexpr))))]
|
||||
[else (error 'parse-sexpr "bad syntax in ~s" sexpr)]))
|
||||
|
||||
;; parse : string -> BRANG
|
||||
;; parses a string containing an BRANG expression to a BRANG AST
|
||||
#;(define (parse str)
|
||||
(parse-sexpr (string->sexpr str)))
|
||||
|
||||
|
||||
;; These are the values of our language
|
||||
(define-type VAL
|
||||
[NumV (n number)]
|
||||
[FunV (body BRANG*) (env ENV)])
|
||||
|
||||
;; NEW
|
||||
(define-type-alias ENV (Listof VAL))
|
||||
|
||||
;; An environment is a simple list of values
|
||||
;(define ENV? (list-of VAL?))
|
||||
|
||||
;; Syntactic environments for the de-Bruijn preprocessing:
|
||||
;; define a type and an empty environment
|
||||
|
||||
;; this is represented by procedures, but the type should be:
|
||||
;; DE-ENV := symbol -> integer
|
||||
;; NEW
|
||||
(define-type-alias DE-ENV (Symbol -> Number))
|
||||
|
||||
;; de-empty-env : DE-ENV
|
||||
;; the empty syntactic environment, always throws an error
|
||||
(define: (de-empty-env [id : Symbol]) : Number
|
||||
(error 'de-env "Free identifier: ~s" id))
|
||||
|
||||
;; de-extend : DE-ENV symbol -> DE-ENV
|
||||
;; extends a given de-env for a new identifier
|
||||
(define: (de-extend [env : DE-ENV] [id : Symbol]) : DE-ENV
|
||||
(lambda: ([name : Symbol])
|
||||
(if (eq? id name)
|
||||
0
|
||||
(+ 1 (env name)))))
|
||||
;; test
|
||||
#;(test (let ([e (de-extend (de-extend de-empty-env 'b) 'a)])
|
||||
(map (lambda (id) (e id))
|
||||
'(a b)))
|
||||
=> '(0 1))
|
||||
|
||||
;; preprocess : BRANG DE-ENV -> BRANG*
|
||||
;; replaces identifier expressions into Ref AST values
|
||||
(define: (preprocess [expr : BRANG] [de-env : DE-ENV]) : BRANG*
|
||||
(let ([sub (lambda: ([expr : BRANG]) (preprocess expr de-env))])
|
||||
(cases expr
|
||||
[(Num n) (Num* n)]
|
||||
[(Add l r) (Add* (sub l) (sub r))]
|
||||
[(Sub l r) (Sub* (sub l) (sub r))]
|
||||
[(Mul l r) (Mul* (sub l) (sub r))]
|
||||
[(Div l r) (Div* (sub l) (sub r))]
|
||||
[(With bound-id named-expr bound-body)
|
||||
(With* (sub named-expr)
|
||||
(preprocess bound-body (de-extend de-env bound-id)))]
|
||||
[(Id id) (Ref* (de-env id))]
|
||||
[(Fun bound-id bound-body)
|
||||
(Fun* (preprocess bound-body (de-extend de-env bound-id)))]
|
||||
[(Call fun-expr arg-expr)
|
||||
(Call* (sub fun-expr) (sub arg-expr))])))
|
||||
|
||||
;; arith-op : (num num -> num) VAL VAL -> VAL
|
||||
;; gets a Scheme numeric binary operator, and uses it within a NumV
|
||||
;; wrapper
|
||||
(define: (arith-op [op : (Number Number -> Number)] [val1 : VAL] [val2 : VAL]) : VAL
|
||||
(define: (NumV->number [v : VAL]) : Number
|
||||
(cases v
|
||||
[(NumV n) n]
|
||||
[else (error 'arith-op "expects a number, got: ~s" v)]))
|
||||
(NumV (op (NumV->number val1) (NumV->number val2))))
|
||||
|
||||
;; eval : BRANG* env -> VAL
|
||||
;; evaluates BRANG* expressions by reducing them to values
|
||||
(define: (-eval [expr : BRANG*] [env : ENV]) : VAL
|
||||
(cases expr
|
||||
[(Num* n) (NumV n)]
|
||||
[(Add* l r) (arith-op + (-eval l env) (-eval r env))]
|
||||
[(Sub* l r) (arith-op - (-eval l env) (-eval r env))]
|
||||
[(Mul* l r) (arith-op * (-eval l env) (-eval r env))]
|
||||
[(Div* l r) (arith-op / (-eval l env) (-eval r env))]
|
||||
[(With* named-expr bound-body)
|
||||
(-eval bound-body (cons (-eval named-expr env) env))]
|
||||
[(Ref* n) (list-ref env n)]
|
||||
[(Fun* bound-body) (FunV bound-body env)]
|
||||
[(Call* fun-expr arg-expr)
|
||||
(let ([fval (-eval fun-expr env)])
|
||||
(cases fval
|
||||
[(FunV bound-body f-env)
|
||||
(-eval bound-body (cons (-eval arg-expr env) f-env))]
|
||||
[else (error '-eval "`call' expects a function, got: ~s"
|
||||
fval)]))]))
|
||||
#|
|
||||
;; run : string -> number
|
||||
;; evaluate a BRANG program contained in a string
|
||||
(define (run str)
|
||||
(let ([result (-eval (preprocess (parse str) de-empty-env) null)])
|
||||
(cases result
|
||||
[(NumV n) n]
|
||||
[else (error 'run
|
||||
"evaluation returned a non-number: ~s" result)])))
|
||||
|
||||
;; tests
|
||||
|
||||
(test (run "{call {fun {x} {+ x 1}} 4}")
|
||||
=> 5)
|
||||
(test (run "{with {add3 {fun {x} {+ x 3}}}
|
||||
{call add3 1}}")
|
||||
=> 4)
|
||||
(test (run "{with {add3 {fun {x} {+ x 3}}}
|
||||
{with {add1 {fun {x} {+ x 1}}}
|
||||
{with {x 3}
|
||||
{call add1 {call add3 x}}}}}")
|
||||
=> 7)
|
||||
(test (run "{with {identity {fun {x} x}}
|
||||
{with {foo {fun {x} {+ x 1}}}
|
||||
{call {call identity foo} 123}}}")
|
||||
=> 124)
|
||||
(test (run "{with {x 3}
|
||||
{with {f {fun {y} {+ x y}}}
|
||||
{with {x 5}
|
||||
{call f 4}}}}")
|
||||
=> 7)
|
||||
(test (run "{call {call {fun {x} {call x 1}}
|
||||
{fun {x} {fun {y} {+ x y}}}}
|
||||
123}")
|
||||
=> 124)
|
||||
|#)
|
||||
25
collects/tests/typed-scheme/660-examples/slow.ss
Normal file
25
collects/tests/typed-scheme/660-examples/slow.ss
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
(module slow "../../typed-scheme.ss"
|
||||
(require "../../CSU660/datatype.ss")
|
||||
|
||||
(define-type BINTREE
|
||||
[Node (l BINTREE) (r BINTREE)]
|
||||
[Leaf (n number)]
|
||||
[Q ]
|
||||
[Q1 ]
|
||||
[Q2 ]
|
||||
[Q3 ]
|
||||
[Q4 ]
|
||||
[Q5 ]
|
||||
|
||||
)
|
||||
|
||||
(cases (Leaf 1)
|
||||
[(Node (Node (Node (Node (Node zz z) x) a) e) b) a]
|
||||
[(Node a b) a]
|
||||
[(Q) 1]
|
||||
[(Q1) 1]
|
||||
[(Q2) 1]
|
||||
[(Q3) 1]
|
||||
[(Q4) 1]
|
||||
[(Q5) 1]
|
||||
[(Leaf l) l]))
|
||||
21
collects/tests/typed-scheme/660-examples/support.ss
Normal file
21
collects/tests/typed-scheme/660-examples/support.ss
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
(module support "../../typed-scheme.ss"
|
||||
(require (for-syntax scheme/base))
|
||||
(provide sqr test first second third fourth string->sexpr rest foldl)
|
||||
|
||||
(define: (sqr [a : number]) : number (* a a))
|
||||
|
||||
(define-type-alias SExp (mu s (Un Number Boolean String Symbol (Listof s))))
|
||||
|
||||
(define-syntax (test stx) #'#f)
|
||||
(pdefine: (a) (first [x : (Listof a)]) : a (car x))
|
||||
(pdefine: (a) (second [x : (Listof a)]) : a (car (cdr x)))
|
||||
(pdefine: (a) (third [x : (Listof a)]) : a (car (cdr (cdr x))))
|
||||
(pdefine: (a) (fourth [x : (Listof a)]) : a (car (cdr (cdr (cdr x)))))
|
||||
(pdefine: (a) (rest [x : (Listof a)]) : (Listof a) (cdr x))
|
||||
(define: (string->sexpr [s : String]) : Sexp
|
||||
(read (open-input-string s)))
|
||||
|
||||
#;(define: (list-of [f : (Any -> Any)]) : Any
|
||||
(lambda: ([l : List]) (andmap f l)))
|
||||
|
||||
)
|
||||
18
collects/tests/typed-scheme/fail/back-and-forth.ss
Normal file
18
collects/tests/typed-scheme/fail/back-and-forth.ss
Normal 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
28
collects/tests/typed-scheme/fail/cnt-err1.ss
Normal 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
22
collects/tests/typed-scheme/fail/gadt.ss
Normal 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
14
collects/tests/typed-scheme/fail/set-struct.ss
Normal 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
9
collects/tests/typed-scheme/fail/set-tests.ss
Normal 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
81
collects/tests/typed-scheme/main.ss
Normal 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))
|
||||
|
||||
|
||||
52
collects/tests/typed-scheme/stress.ss
Normal file
52
collects/tests/typed-scheme/stress.ss
Normal file
|
|
@ -0,0 +1,52 @@
|
|||
(define files
|
||||
(list "basic-tests.ss"
|
||||
"area.ss"
|
||||
"barland.ss"
|
||||
"batched-queue.scm"
|
||||
"annotation-test.ss"
|
||||
"cl.ss"
|
||||
"do.ss"
|
||||
"foo.scm"
|
||||
"if-splitting-test.ss"
|
||||
"leftist-heap.ss"
|
||||
"let-values-tests.ss"
|
||||
"little-schemer.ss"
|
||||
"seasoned-schemer.ss"
|
||||
"manual-examples.ss"
|
||||
"mu-rec.ss"
|
||||
"struct-exec.ss"
|
||||
"pair-test.ss"
|
||||
"poly-struct.ss"
|
||||
"poly-tests.ss"
|
||||
"priority-queue.scm"
|
||||
"rec-types.ss"
|
||||
"require-tests.ss"
|
||||
#;"set-struct.ss"
|
||||
"typed-list.ss"
|
||||
"varargs-tests.ss"
|
||||
"vec-tests.ss"))
|
||||
|
||||
(define eli-files
|
||||
(map (lambda (s) (string-append "660-examples/" s))
|
||||
(list "slow.ss"
|
||||
"hw01.scm"
|
||||
"hw02.scm"
|
||||
"hw03.scm"
|
||||
"hw04.scm"
|
||||
"hw05.scm")))
|
||||
|
||||
(define (loader f) (with-handlers ([exn:fail? (lambda _ (printf "FAILED: ~a~n" f))])
|
||||
(load f)))
|
||||
|
||||
(require (planet "io.ss" ("dherman" "io.plt" 1)))
|
||||
|
||||
(define (count-lines f)
|
||||
(length (read-lines (open-input-file f))))
|
||||
|
||||
(define (go)
|
||||
(for-each loader files)
|
||||
(for-each loader eli-files))
|
||||
|
||||
(apply + (map count-lines (append files eli-files)))
|
||||
|
||||
(time (go))
|
||||
12
collects/tests/typed-scheme/succeed/annotation-test.ss
Normal file
12
collects/tests/typed-scheme/succeed/annotation-test.ss
Normal 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
11
collects/tests/typed-scheme/succeed/area.ss
Normal 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
5
collects/tests/typed-scheme/succeed/bad-map-infer.ss
Normal 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
29
collects/tests/typed-scheme/succeed/barland.ss
Normal 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
100
collects/tests/typed-scheme/succeed/basic-tests.ss
Normal 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
86
collects/tests/typed-scheme/succeed/batched-queue.scm
Normal 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
8
collects/tests/typed-scheme/succeed/broken-let-syntax.ss
Normal 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
35
collects/tests/typed-scheme/succeed/cl-tests.ss
Normal 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
8
collects/tests/typed-scheme/succeed/cl.ss
Normal 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
17
collects/tests/typed-scheme/succeed/do.ss
Normal 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
15
collects/tests/typed-scheme/succeed/fix.ss
Normal 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
48
collects/tests/typed-scheme/succeed/foo.scm
Normal 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
111
collects/tests/typed-scheme/succeed/hw01.scm
Normal 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
13
collects/tests/typed-scheme/succeed/if-splitting-test.ss
Normal 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
302
collects/tests/typed-scheme/succeed/leftist-heap.ss
Normal 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
26
collects/tests/typed-scheme/succeed/let-values-tests.ss
Normal 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
453
collects/tests/typed-scheme/succeed/little-schemer.ss
Normal 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
74
collects/tests/typed-scheme/succeed/manual-examples.ss
Normal 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))])))
|
||||
|
||||
|
|
@ -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
9
collects/tests/typed-scheme/succeed/mu-rec.ss
Normal 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
8
collects/tests/typed-scheme/succeed/pair-test.ss
Normal 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
9
collects/tests/typed-scheme/succeed/poly-struct.ss
Normal 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
27
collects/tests/typed-scheme/succeed/poly-tests.ss
Normal 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
103
collects/tests/typed-scheme/succeed/priority-queue.scm
Normal 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
5
collects/tests/typed-scheme/succeed/provide-syntax.ss
Normal 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
40
collects/tests/typed-scheme/succeed/rec-types.ss
Normal 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
11
collects/tests/typed-scheme/succeed/require-tests.ss
Normal 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
6
collects/tests/typed-scheme/succeed/scratch.ss
Normal 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
106
collects/tests/typed-scheme/succeed/seasoned-schemer.ss
Normal 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
4
collects/tests/typed-scheme/succeed/struct-exec.ss
Normal 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
7
collects/tests/typed-scheme/succeed/typed-list.ss
Normal 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
48
collects/tests/typed-scheme/succeed/varargs-tests.ss
Normal 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
4
collects/tests/typed-scheme/succeed/vec-tests.ss
Normal 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
85
collects/tests/typed-scheme/unit-tests/all-tests.ss
Normal 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
122
collects/tests/typed-scheme/unit-tests/infer-tests.ss
Normal 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)
|
||||
16
collects/tests/typed-scheme/unit-tests/module-tests.ss
Normal file
16
collects/tests/typed-scheme/unit-tests/module-tests.ss
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
#lang scheme
|
||||
(require "test-utils.ss")
|
||||
(require (private planet-requires))
|
||||
(require (schemeunit))
|
||||
|
||||
(provide module-tests)
|
||||
|
||||
(define (module-tests)
|
||||
(test-suite "Tests for whole modules"
|
||||
#;(test-not-exn "name" (lambda () (expand #'(module m (planet "typed-scheme.ss" ("plt" "typed-scheme.plt"))
|
||||
(define: x : number 3)))))
|
||||
))
|
||||
|
||||
|
||||
(define-go module-tests)
|
||||
|
||||
102
collects/tests/typed-scheme/unit-tests/new-fv-tests.ss
Normal file
102
collects/tests/typed-scheme/unit-tests/new-fv-tests.ss
Normal file
|
|
@ -0,0 +1,102 @@
|
|||
(module new-fv-tests mzscheme
|
||||
(require "test-utils.ss")
|
||||
(require/private type-rep rep-utils planet-requires type-effect-convenience meet-join subtype union)
|
||||
(require-schemeunit)
|
||||
|
||||
(define variance-gen (random-uniform Covariant Contravariant Invariant Constant))
|
||||
|
||||
(define alpha-string (random-string (random-char (random-int-between 65 90)) (random-size 1)))
|
||||
|
||||
(define (free-gen var) (random-apply make-immutable-hash-table (random-list-of (random-apply cons var variance-gen) (random-size 1))))
|
||||
(define free-var-gen (free-gen (random-symbol alpha-string)))
|
||||
(define free-idx-gen (free-gen (random-size)))
|
||||
|
||||
(define free-vars-gen (free-gen free-var-gen))
|
||||
(define free-idxs-gen (free-gen free-idx-gen))
|
||||
|
||||
(define type-gen
|
||||
(random-recursive
|
||||
t
|
||||
[10 Univ]
|
||||
[10 N]
|
||||
[10 B]
|
||||
[2 (random-apply make-Pair t t)]
|
||||
[2 (random-apply make-Vector t)]
|
||||
[2 (random-apply -lst t)]
|
||||
[2 (random-apply -Promise t)]
|
||||
[1 (random-apply apply Un (random-list-of t))]))
|
||||
|
||||
(define values-gen
|
||||
(random-weighted 1 type-gen 6 (random-apply -values (random-list-of type-gen (random-weighted 1 0 3 (random-size 2))))))
|
||||
|
||||
|
||||
(define (fvars frees) (hash-table-map frees (lambda (k v) k)))
|
||||
(define (subset a b) (andmap (lambda (e) (memq e b)) a))
|
||||
|
||||
(define (var-below v w)
|
||||
(or (eq? v w) (eq? v Invariant) (eq? w Constant)))
|
||||
|
||||
(define (free-var-from frees)
|
||||
(let ([keys (map car (generate (random-apply hash-table-map frees list)))])
|
||||
(apply choose-uniform keys)))
|
||||
|
||||
(define (fv-tests)
|
||||
(test-suite "random tests"
|
||||
(test-randomly "combine includes all the elements"
|
||||
100
|
||||
([A free-vars-gen]
|
||||
[B free-vars-gen]
|
||||
[C free-idxs-gen]
|
||||
[D free-idxs-gen])
|
||||
(let ([C1 (combine-frees (list A B))]
|
||||
[C2 (combine-frees (list C D))])
|
||||
(check-not-false (subset (fvars A) (fvars C1)))
|
||||
(check-not-false (subset (fvars B) (fvars C1)))
|
||||
(check-not-false (subset (fvars C) (fvars C2)))
|
||||
(check-not-false (subset (fvars D) (fvars C2)))))
|
||||
(test-randomly "combine produces lower variance"
|
||||
100
|
||||
([A free-vars-gen]
|
||||
[B free-vars-gen]
|
||||
[key (free-var-from A)])
|
||||
(let* ([comb (combine-frees (list A B))]
|
||||
[var1 (hash-table-get A key)]
|
||||
[var2 (hash-table-get comb key)])
|
||||
(check-not-false (var-below var2 var1))))))
|
||||
|
||||
|
||||
(define (meet-join-tests)
|
||||
(test-suite
|
||||
"meet join"
|
||||
(test-randomly "join of two types is above them"
|
||||
10
|
||||
([A type-gen]
|
||||
[B type-gen]
|
||||
[A+B (join A B)])
|
||||
(check-not-false (subtype A A+B))
|
||||
(check-not-false (subtype B A+B)))
|
||||
(test-randomly "meet of two types is below them"
|
||||
10
|
||||
([A type-gen]
|
||||
[B type-gen]
|
||||
[A+B (meet A B)])
|
||||
(check-not-false (subtype A+B A))
|
||||
(check-not-false (subtype A+B B)))
|
||||
(test-randomly "promote/demote"
|
||||
10
|
||||
([t type-gen]
|
||||
[V (random-list-of (random-symbol alpha-string))]
|
||||
[p (promote t V)]
|
||||
[d (demote t V)]
|
||||
[fv-p (fv p)]
|
||||
[fv-d (fv d)])
|
||||
(check-false (ormap (lambda (e) (memq e V)) fv-p))
|
||||
(check-false (ormap (lambda (e) (memq e V)) fv-d))
|
||||
(check-not-false (subtype t p))
|
||||
(check-not-false (subtype p d)))))
|
||||
|
||||
(define-go fv-tests meet-join-tests)
|
||||
|
||||
|
||||
|
||||
)
|
||||
78
collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
Normal file
78
collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
Normal 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))
|
||||
|
||||
|
||||
|
||||
|
|
@ -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
126
collects/tests/typed-scheme/unit-tests/subtype-tests.ss
Normal 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
58
collects/tests/typed-scheme/unit-tests/test-utils.ss
Normal 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)]))
|
||||
|
||||
|
|
@ -0,0 +1,29 @@
|
|||
#lang scheme/base
|
||||
(require "test-utils.ss"
|
||||
(for-syntax scheme/base))
|
||||
(require (private planet-requires type-annotation tc-utils type-rep type-effect-convenience type-environments
|
||||
parse-type init-envs type-name-env))
|
||||
|
||||
(require (schemeunit))
|
||||
|
||||
(provide type-annotation-tests)
|
||||
|
||||
(define-syntax (tat stx)
|
||||
(syntax-case stx ()
|
||||
[(_ ann-stx ty)
|
||||
#`(check-type-equal? #,(format "~a" (syntax->datum #'ann-stx))
|
||||
(type-annotation #'ann-stx)
|
||||
ty)]))
|
||||
|
||||
#reader typed-scheme/typed-reader
|
||||
(define (type-annotation-tests)
|
||||
(test-suite
|
||||
"Type Annotation tests"
|
||||
|
||||
(tat #{foo : Number} N)
|
||||
(tat foo #f)
|
||||
(tat #{foo : 3} (-val 3))))
|
||||
|
||||
(define-go
|
||||
type-annotation-tests)
|
||||
|
||||
46
collects/tests/typed-scheme/unit-tests/type-equal-tests.ss
Normal file
46
collects/tests/typed-scheme/unit-tests/type-equal-tests.ss
Normal 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
606
collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
Normal 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)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user