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

compiles again

Browse Source 
svn: r14625

original commit: 8cbdf3ee951ce80178ff79b135906cb3d56c5a7e
This commit is contained in:
Sam Tobin-Hochstadt 2009-04-27 16:06:54 +00:00
commit 8b96f98595
9 changed files with 72 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -0,0 +1,6 @@
#lang typed-scheme
(: f ((Listof Number) -> (Listof Number)))
(define (f x)
(for/lists (#{y : (Listof Number)}) ([e (in-list x)])
e))

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

@ -0,0 +1,9 @@
#lang typed-scheme
(require scheme/match)
(match "abc"
[(regexp "^abc") 1])
(match (list 1 1)
[(list x x) 1])

18
collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
View File

@ -87,7 +87,7 @@
(+ 1 (car x))
5))
N]
(tc-e (if (let ([y 12]) y) 3 4) -Integer)
(tc-e 3 -Integer)
(tc-e "foo" -String)
(tc-e (+ 3 4) -Integer)
@ -496,10 +496,10 @@
[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)))
(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]
@ -541,10 +541,10 @@
[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)))
(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)]

2
collects/typed-scheme/env/type-env.ss vendored
View File

@ -3,7 +3,7 @@
(require (except-in "../utils/utils.ss" extend))
(require syntax/boundmap
(utils tc-utils)
(types utils))
(types utils))
(provide register-type
finish-register-type

7
collects/typed-scheme/env/type-environments.ss vendored
View File

@ -19,9 +19,6 @@
env-keys+vals
with-dotted-env/extend)
(provide/contract [make-empty-env ((-> any/c any/c any/c) . -> . env?)]
[])
;; eq? has the type of equal?, and l is an alist (with conses!)
(define-struct env (eq? l))
@ -76,7 +73,7 @@
;; elements are not lists, or all at once, if the elements are lists
(define (extend/values kss vss env)
(foldr (lambda (ks vs env)
(cond [(and (list? ks) (list? vs))
(cond [(and (list? ks) (list? vs))
(extend-env ks vs env)]
[(or (list? ks) (list? vs))
(int-err "not both lists in extend/values: ~a ~a" ks vs)]
@ -87,3 +84,5 @@
(define-syntax with-dotted-env/extend
(syntax-rules ()
[(_ i t v . b) (parameterize ([dotted-env (extend/values (list i) (list (cons t v)) (dotted-env))]) . b)]))
(provide/contract [make-empty-env ((-> any/c any/c any/c) . -> . env?)])

2
collects/typed-scheme/private/parse-type.ss
View File

@ -300,7 +300,7 @@
(and (eq? (syntax-e #'Refinement) 'Refinement)
(identifier? #'p?))
(match (lookup-type/lexical #'p?)
[(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
[(and t (Function: (list (arr: (list dom) _ #f #f '()))))
(make-Refinement dom #'p? (syntax-local-certifier))]
[t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
[(Instance t)

9
collects/typed-scheme/typecheck/tc-toplevel.ss
View File

@ -10,9 +10,9 @@
(rep type-rep)
(types utils convenience)
(private parse-type type-annotation type-contract)
(env type-env init-envs type-name-env type-alias-env lexical-env)
(utils tc-utils mutated-vars)
"provide-handling.ss"
(env type-env init-envs type-name-env type-alias-env lexical-env)
(utils tc-utils mutated-vars)
"provide-handling.ss"
"def-binding.ss"
(for-template
"internal-forms.ss"
@ -41,9 +41,10 @@
(list)]
;; declare-refinement
;; FIXME - this sucks and should die
[(define-values () (begin (quote-syntax (declare-refinement-internal pred)) (#%plain-app values)))
(match (lookup-type/lexical #'pred)
[(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
[(and t (Function: (list (arr: (list dom) rng #f #f '()))))
(register-type #'pred
(make-pred-ty (list dom)
rng

4
collects/typed-scheme/typecheck/typechecker.ss
View File

@ -13,5 +13,5 @@
(provide-signature-elements typechecker^ tc-expr^)
(define-values/link-units/infer
tc-toplevel@ tc-new-if@ tc-lambda@ tc-dots@ tc-new-app@ tc-let@ tc-expr@ check-subforms@)
(define-values/invoke-unit/infer
(link tc-toplevel@ tc-new-if@ tc-lambda@ tc-dots@ tc-new-app@ tc-let@ tc-expr@ check-subforms@))

59
collects/typed-scheme/types/utils.ss
View File

@ -29,7 +29,8 @@
(struct-out DottedBoth)
just-Dotted?
tc-error/expr
lookup-fail)
lookup-fail
lookup-type-fail)
;; substitute : Type Name Type -> Type
@ -38,7 +39,7 @@
(if (hash-ref (free-vars* target) name #f)
(type-case (#:Type sb #:LatentFilter (sub-lf sb))
target
[#:Union tys (Un (map sb tys))]
[#:Union tys (Un (map sb tys))]
[#:F name* (if (eq? name* name) image target)]
[#:arr dom rng rest drest kws
(begin
@ -83,7 +84,7 @@
(map sb dom)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb (car drest))])
(map (lambda (img) (substitute img name expanded)) images)))
(map (lambda (img) (substitute img name expanded)) images)))
(sb rng)
rimage
#f
@ -190,25 +191,25 @@
;; convenience function for returning the result of typechecking an expression
(define ret
(case-lambda [(t)
(make-tc-results
(if (Type? t)
(list (make-tc-result t (make-FilterSet null null) (make-Empty)))
(for/list ([i t])
(make-tc-result i (make-FilterSet null null) (make-Empty))))
#f)]
[(t f)
(make-tc-results
(if (Type? t)
(list (make-tc-result t f (make-Empty)))
(for/list ([i t] [f f])
(make-tc-result i f (make-Empty))))
#f)]
[(t f o)
(make-tc-results
(if (and (list? t) (list? f) (list? o))
(map make-tc-result t f o)
(list (make-tc-result t f o)))
#f)]))
(make-tc-results
(if (Type? t)
(list (make-tc-result t (make-FilterSet null null) (make-Empty)))
(for/list ([i t])
(make-tc-result i (make-FilterSet null null) (make-Empty))))
#f)]
[(t f)
(make-tc-results
(if (Type? t)
(list (make-tc-result t f (make-Empty)))
(for/list ([i t] [f f])
(make-tc-result i f (make-Empty))))
#f)]
[(t f o)
(make-tc-results
(if (and (list? t) (list? f) (list? o))
(map make-tc-result t f o)
(list (make-tc-result t f o)))
#f)]))
(p/c
[ret
@ -254,4 +255,16 @@
return)
;; error for unbound variables
(define (lookup-fail e) (tc-error/expr "unbound identifier ~a" e))
(define (lookup-fail e)
(match (identifier-binding e)
['lexical (int-err "untyped lexical variable ~a" (syntax-e e))]
[#f (int-err "untyped top-level variable ~a" (syntax-e e))]
[(list _ _ nominal-source-mod nominal-source-id _ _ _)
(let-values ([(x y) (module-path-index-split nominal-source-mod)])
(cond [(and (not x) (not y))
(tc-error/expr "untyped identifier ~a" (syntax-e e))]
[else
(tc-error/expr "untyped identifier ~a imported from module <~a>" (syntax-e e) x)]))]))
(define (lookup-type-fail i)
(tc-error/expr "~a is not bound as a type" (syntax-e i)))