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

Checkpoint.

Browse Source
This commit is contained in:
Sam Tobin-Hochstadt 2008-06-17 18:10:17 -04:00
parent c8a2810742
commit dfdfae95d7
9 changed files with 82 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/typed-scheme/private/lexical-env.ss
View File

@ -1,6 +1,6 @@
#lang scheme/base #lang scheme/base
(require "type-environments.ss" "tc-utils.ss" "type-env.ss" "mutated-vars.ss") (require "type-environments.ss" "tc-utils.ss" "type-env.ss" "mutated-vars.ss" "type-utils.ss")
(provide (all-defined-out)) (provide (all-defined-out))
@ -24,7 +24,7 @@
(lambda (i) (lookup-type (lambda (i) (lookup-type
i (lambda () i (lambda ()
(if (lookup (dotted-env) i (lambda _ #f)) (if (lookup (dotted-env) i (lambda _ #f))
(tc-error "Rest variable ~a with ... type used in an inappropriate context" (syntax-e i)) (tc-error/expr "Rest variable ~a with ... type used in an inappropriate context" (syntax-e i))
(lookup-fail (syntax-e i)))))))) (lookup-fail (syntax-e i))))))))
;; refine the type of i in the lexical env ;; refine the type of i in the lexical env

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

@ -73,7 +73,7 @@
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty)))] (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty)))]
[(dom ... rest ::: -> rng) [(dom ... rest ::: -> rng)
(and (eq? (syntax-e #'->) '->) (and (eq? (syntax-e #'->) '->)
(symbolic-identifier=? #'::: (quote-syntax *))) (eq? (syntax-e #':::) '*))
(begin (begin
(add-type-name-reference #'->) (add-type-name-reference #'->)
(->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng)))] (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng)))]
@ -106,17 +106,12 @@
(-values (map parse-type (syntax->list #'(tys ...))))] (-values (map parse-type (syntax->list #'(tys ...))))]
[(case-lambda tys ...) [(case-lambda tys ...)
(eq? (syntax-e #'case-lambda) 'case-lambda) (eq? (syntax-e #'case-lambda) 'case-lambda)
(make-Function (map (lambda (ty) (make-Function
(syntax-case* ty (->) symbolic-identifier=? (for/list ([ty (syntax->list #'(tys ...))])
[(dom ... -> rng) (let ([t (parse-type ty)])
(make-arr (match t
(map parse-type (syntax->list #'(dom ...))) [(Function: (list arr)) arr]
(parse-type #'rng))])) [_ (tc-error/stx ty "Component of case-lambda type was not a function clause")]))))]
(syntax->list #'(tys ...))))]
;; I wish I could write this
#;[(case-lambda ([dom ... -> rng] ...)) (make-funty (list (make-arr (list (parse-type #'dom) ...) (parse-type #'rng)) ...))]
#;[(list-of t) (make-lst (parse-type #'t))]
#;[(Listof t) (make-lst (parse-type #'t))]
[(Vectorof t) [(Vectorof t)
(eq? (syntax-e #'Vectorof) 'Vectorof) (eq? (syntax-e #'Vectorof) 'Vectorof)
(begin (begin

4
collects/typed-scheme/private/promote-demote.ss
View File

@ -30,7 +30,7 @@
(cond (cond
[(apply V-in? V (append thn els)) [(apply V-in? V (append thn els))
(make-arr null (Un) Univ #f null null)] (make-arr null (Un) Univ #f null null)]
[(and drest (V-in? V (cdr drest))) [(and drest (V-in? V (car drest)))
(make-arr (for/list ([d dom]) (var-demote d V)) (make-arr (for/list ([d dom]) (var-demote d V))
(vp rng) (vp rng)
(var-demote (car drest) V) (var-demote (car drest) V)
@ -66,7 +66,7 @@
(cond (cond
[(apply V-in? V (append thn els)) [(apply V-in? V (append thn els))
(make-arr null (Un) Univ #f null null)] (make-arr null (Un) Univ #f null null)]
[(and drest (V-in? V (cdr drest))) [(and drest (V-in? V (car drest)))
(make-arr (for/list ([d dom]) (var-promote d V)) (make-arr (for/list ([d dom]) (var-promote d V))
(vd rng) (vd rng)
(var-promote (car drest) V) (var-promote (car drest) V)

78
collects/typed-scheme/private/tc-app-unit.ss
View File

@ -204,17 +204,17 @@
(subtype tail-ty (car (car drests*)))))) (subtype tail-ty (car (car drests*))))))
(ret (car rngs*))] (ret (car rngs*))]
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1)))) [(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1))))
(let*-values ([(arg-tys) (map tc-expr/t fixed-args)] (let*-values ([(arg-tys) (map tc-expr/t fixed-args)]
[(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))]) [(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))])
(tc/dots tail))]) (tc/dots tail))])
(for-each (lambda (x) (unless (not (Poly? x)) (for-each (lambda (x) (unless (not (Poly? x))
(tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x))) (tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x)))
(cons tail-ty arg-tys)) (cons tail-ty arg-tys))
(let loop ([doms* doms] [rngs* rngs] [rests* rests]) (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
(cond [(null? doms*) (cond [(null? doms*)
(match f-ty (match f-ty
[(tc-result: (Poly-names: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1)))) [(tc-result: (Poly-names: vars (Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1))))
(cond (cond
[(null? doms) (int-err "how could doms be null: ~a ~a" doms f-ty)] [(null? doms) (int-err "how could doms be null: ~a ~a" doms f-ty)]
[(= 1 (length doms)) [(= 1 (length doms))
@ -250,6 +250,7 @@
(car rests*) (car rests*)
(car rngs*))) (car rngs*)))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg
[(and (car rests*) [(and (car rests*)
tail-bound tail-bound
(<= (length (car doms*)) (<= (length (car doms*))
@ -261,22 +262,32 @@
(car rests*) (car rests*)
(car rngs*))) (car rngs*)))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*))])))] ;; ... function, ... arg
[(and (car drests*)
tail-bound
(eq? tail-bound (cdr (car drests*)))
(= (length (car doms*))
(length arg-tys))
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*)))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (Poly: vars (Function: '()))) [(tc-result: (Poly: vars (Function: '())))
(tc-error/expr #:return (ret (Un)) (tc-error/expr #:return (ret (Un))
"Function has no cases")] "Function has no cases")]
[(tc-result: (PolyDots: (list fixed-vars ... dotted-var) [(tc-result: (PolyDots: (and vars (list fixed-vars ... dotted-var))
(Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1)))) (Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1))))
(let*-values ([(arg-tys tail-ty) (values (map tc-expr/t fixed-args) (let*-values ([(arg-tys) (map tc-expr/t fixed-args)]
(tc-expr/t tail))] [(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))])
[(arg-tys0) (append arg-tys (list tail-ty))]) (tc/dots tail))])
(for-each (lambda (x) (unless (not (Poly? x)) (for-each (lambda (x) (unless (not (Poly? x))
(tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x))) (tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x)))
(cons tail-ty arg-tys)) (cons tail-ty arg-tys))
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
(cond [(null? doms*) (cond [(null? doms*)
(match f-ty (match f-ty
[(tc-result: (PolyDots-names: vars (Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1)))) [(tc-result: (PolyDots-names: (list fixed-vars ... dotted-var)
(Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1))))
(cond (cond
[(null? doms) (int-err "how could doms be null: ~a ~a" doms f-ty)] [(null? doms) (int-err "how could doms be null: ~a ~a" doms f-ty)]
[(= 1 (length doms)) [(= 1 (length doms))
@ -284,11 +295,11 @@
(tc-error/expr (tc-error/expr
#:return (ret (Un)) #:return (ret (Un))
"polymorphic function domain did not match -~ndomain was: ~a~nrest argument was: ~a~narguments were ~a~n" "polymorphic function domain did not match -~ndomain was: ~a~nrest argument was: ~a~narguments were ~a~n"
(car doms) (car rests) (stringify arg-tys0)) (car doms) (car rests) (printable-h arg-tys tail-ty tail-bound))
(tc-error/expr (tc-error/expr
#:return (ret (Un)) #:return (ret (Un))
"polymorphic function domain did not match -~ndomain was: ~a~narguments were ~a~n" "polymorphic function domain did not match -~ndomain was: ~a~narguments were ~a~n"
(car doms) (stringify arg-tys0)))] (car doms) (printable-h arg-tys tail-ty tail-bound)))]
[else [else
(tc-error/expr (tc-error/expr
#:return (ret (Un)) #:return (ret (Un))
@ -299,22 +310,45 @@
(format "~a rest argument: " (stringify dom) rest) (format "~a rest argument: " (stringify dom) rest)
(stringify dom))) (stringify dom)))
"\n") "\n")
(stringify arg-tys0))])])] (printable-h arg-tys tail-ty tail-bound))])])]
[(and (= (length (car doms*)) ;; the actual work, when we have a * function and a list final argument
[(and (car rests*)
(not tail-bound)
(<= (length (car doms*))
(length arg-tys)) (length arg-tys))
(infer (append fixed-vars (list dotted-var)) (infer/vararg vars
arg-tys0 (append (car doms*) (list (make-Listof (car rests*)))) (car rngs*))) (cons tail-ty arg-tys)
=> (lambda (substitution) (cons (make-Listof (car rests*))
(let* ([s (lambda (t) (subst-all substitution t))] (car doms*))
[new-doms* (append (map s (car doms*)) (list (make-Listof (s (car rests*)))))]) (car rests*)
(unless (andmap subtype arg-tys0 new-doms*) (car rngs*)))
(int-err "Inconsistent substitution - arguments not subtypes: ~n~a~n~a~n" arg-tys0 new-doms*))) => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
(ret (subst-all substitution (car rngs*))))] ;; actual work, when we have a * function and ... final arg
[(and (car rests*)
tail-bound
(<= (length (car doms*))
(length arg-tys))
(infer/vararg vars
(cons (make-Listof tail-ty) arg-tys)
(cons (make-Listof (car rests*))
(car doms*))
(car rests*)
(car rngs*)))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg
[(and (car drests*)
tail-bound
(eq? tail-bound (cdr (car drests*)))
(= (length (car doms*))
(length arg-tys))
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*)))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (PolyDots: vars (Function: '()))) [(tc-result: (PolyDots: vars (Function: '())))
(tc-error/expr #:return (ret (Un)) (tc-error/expr #:return (ret (Un))
"Function has no cases")] "Function has no cases")]
[f-ty (tc-error/expr #:return (ret (Un)) [(tc-result: f-ty) (tc-error/expr #:return (ret (Un))
"Type of argument to apply is not a function type: ~n~a" f-ty)])) "Type of argument to apply is not a function type: ~n~a" f-ty)]))

5
collects/typed-scheme/private/tc-utils.ss
View File

@ -97,10 +97,6 @@
;; this is used only for printing type names ;; this is used only for printing type names
(define current-type-names (make-parameter (lambda () '()))) (define current-type-names (make-parameter (lambda () '())))
;; error for unbound variables
(define (lookup-fail e) (tc-error "unbound identifier ~a" e))
;; for reporting internal errors in the type checker ;; for reporting internal errors in the type checker
(define-struct (exn:fail:tc exn:fail) ()) (define-struct (exn:fail:tc exn:fail) ())
@ -125,3 +121,4 @@
(define (add-type-name-reference t) (define (add-type-name-reference t)
(type-name-references (cons t (type-name-references)))) (type-name-references (cons t (type-name-references))))

3
collects/typed-scheme/private/type-effect-convenience.ss
View File

@ -249,8 +249,5 @@
(exit t)))] (exit t)))]
[_ (exit t)])))) [_ (exit t)]))))
(define (tc-error/expr msg #:return [return (Un)] #:stx [stx (current-orig-stx)] . rest)
(tc-error/delayed #:stx stx (apply format msg rest))
return)

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

@ -1,7 +1,7 @@
#lang scheme/base #lang scheme/base
(require (lib "boundmap.ss" "syntax") (require (lib "boundmap.ss" "syntax")
"tc-utils.ss") "tc-utils.ss" "type-utils.ss")
(provide register-type (provide register-type
finish-register-type finish-register-type

3
collects/typed-scheme/private/type-name-env.ss
View File

@ -2,7 +2,8 @@
(require syntax/boundmap (require syntax/boundmap
mzlib/trace mzlib/trace
"tc-utils.ss") "tc-utils.ss"
"type-utils.ss")
(provide register-type-name (provide register-type-name
lookup-type-name lookup-type-name

11
collects/typed-scheme/private/type-utils.ss
View File

@ -23,7 +23,9 @@
unfold unfold
(struct-out Dotted) (struct-out Dotted)
(struct-out DottedBoth) (struct-out DottedBoth)
just-Dotted?) just-Dotted?
tc-error/expr
lookup-fail)
;; substitute : Type Name Type -> Type ;; substitute : Type Name Type -> Type
@ -140,3 +142,10 @@
(define (just-Dotted? S) (define (just-Dotted? S)
(and (Dotted? S) (and (Dotted? S)
(not (DottedBoth? S)))) (not (DottedBoth? S))))
(define (tc-error/expr msg #:return [return (make-Union null)] #:stx [stx (current-orig-stx)] . rest)
(tc-error/delayed #:stx stx (apply format msg rest))
return)
;; error for unbound variables
(define (lookup-fail e) (tc-error/expr "unbound identifier ~a" e))