New error handling for type parsing errors.

New error type that is both top/bot.
Fix provide handling if identifier is provided twice.
Note that require/typed is really a definition.
Fix require of #%kernel.

svn: r12083

original commit: 3a9928474523b042f83a7a707346daa01ef63899
This commit is contained in:
Sam Tobin-Hochstadt 2008-10-21 18:01:03 +00:00
parent a8185f5048
commit 6db06c53cd
9 changed files with 91 additions and 71 deletions

View File

@ -4,7 +4,7 @@
scheme/list
(only-in rnrs/lists-6 fold-left)
'#%paramz
(rename-in '#%kernel [apply kernel:apply])
(only-in '#%kernel [apply kernel:apply])
scheme/promise
(only-in scheme/match/runtime match:error))

View File

@ -213,10 +213,10 @@
(make-Name #'id)]
[(eq? '-> (syntax-e #'id))
(tc-error/delayed "Incorrect use of -> type constructor")
Univ]
Err]
[else
(tc-error/delayed "Unbound type name ~a" (syntax-e #'id))
Univ])]
Err])]
[(All . rest) (eq? (syntax-e #'All) 'All) (tc-error "All: bad syntax")]
[(Opaque . rest) (eq? (syntax-e #'Opaque) 'Opqaue) (tc-error "Opaque: bad syntax")]
@ -239,8 +239,9 @@
(tc-error "Wrong number of arguments to type ~a, expected ~a but got ~a" rator (length ns) (length args)))
(instantiate-poly rator args)]
[(Mu: _ _) (loop (unfold rator) args)]
[(Error:) Err]
[_ (tc-error/delayed "Type ~a cannot be applied, arguments were: ~a" rator args)
Univ]))
Err]))
#;
(let ([ty (parse-type #'id)])
#;(printf "ty is ~a" ty)

View File

@ -52,14 +52,13 @@ This file defines two sorts of primitives. All of them are provided into any mod
(define-syntax (require/typed stx)
(define-syntax (require/typed stx)
(syntax-case* stx (rename) (lambda (x y) (eq? (syntax-e x) (syntax-e y)))
[(_ lib [nm ty] ...)
#'(begin (require/typed nm ty lib) ...)]
[(_ nm ty lib)
(identifier? #'nm)
(with-syntax ([(cnt*) (syntax->datum #'(nm))])
(with-syntax ([(cnt*) (generate-temporaries #'(nm))])
(quasisyntax/loc stx (begin
#,(syntax-property (syntax-property #'(define cnt* #f)
'typechecker:contract-def #'ty)

View File

@ -168,6 +168,9 @@
[(list t t) A0]
;; univ is top
[(list _ (Univ:)) A0]
;; error is top and bot
[(list _ (Error:)) A0]
[(list (Error:) _) A0]
;; (Un) is bot
[(list _ (Union: (list))) (fail! s t)]
[(list (Union: (list)) _) A0]

View File

@ -139,6 +139,7 @@
(define -Promise make-promise-ty)
(define Univ (make-Univ))
(define Err (make-Error))
(define-syntax -v
(syntax-rules ()

View File

@ -15,6 +15,9 @@
;; t must be a Type
(dt Scope (t))
;; this is ONLY used when a type error ocurrs
(dt Error () [#:frees #f] [#:fold-rhs #:base])
;; i is an nat
(dt B (i)
[#:frees empty-hash-table (make-immutable-hasheq (list (cons i Covariant)))]

View File

@ -2,7 +2,7 @@
(require (except-in "../utils/utils.ss" extend))
(require (only-in srfi/1/list s:member)
syntax/kerncase
syntax/kerncase syntax/boundmap
mzlib/trace
(private type-contract)
(rep type-rep)
@ -23,68 +23,77 @@
(define (remove-provides forms)
(filter (lambda (e) (not (provide? e))) (syntax->list forms)))
(define ((generate-prov stx-defs val-defs) form)
(define (mem? i vd)
(cond [(s:member i vd (lambda (i j) (free-identifier=? i (binding-name j)))) => car]
[else #f]))
(define (lookup-id i vd)
(def-binding-ty (mem? i vd)))
(define (mk internal-id external-id)
(cond
[(mem? internal-id val-defs)
=>
(lambda (b)
(with-syntax ([id internal-id]
[out-id external-id])
(cond [(type->contract (def-binding-ty b) (lambda () #f))
=>
(lambda (cnt)
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
#`(begin
(define/contract cnt-id #,cnt id)
(define (generate-prov stx-defs val-defs)
(define mapping (make-free-identifier-mapping))
(lambda (form)
(define (mem? i vd)
(cond [(s:member i vd (lambda (i j) (free-identifier=? i (binding-name j)))) => car]
[else #f]))
(define (lookup-id i vd)
(def-binding-ty (mem? i vd)))
(define (mk internal-id external-id)
(cond
;; if it's already done, do nothing
[(free-identifier-mapping-get mapping internal-id
;; if it wasn't there, put it in, and skip this case
(lambda ()
(free-identifier-mapping-put! mapping internal-id #t)
#f))
#'(begin)]
[(mem? internal-id val-defs)
=>
(lambda (b)
(with-syntax ([id internal-id]
[out-id external-id])
(cond [(type->contract (def-binding-ty b) (lambda () #f))
=>
(lambda (cnt)
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
#`(begin
(define/contract cnt-id #,cnt id)
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(make-rename-transformer #'cnt-id)))
(#%provide (rename export-id out-id)))))]
[else
(with-syntax ([(export-id) (generate-temporaries #'(id))])
#`(begin
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(make-rename-transformer #'cnt-id)))
(#%provide (rename export-id out-id)))))]
[else
(with-syntax ([(export-id) (generate-temporaries #'(id))])
#`(begin
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
(provide (rename-out [export-id out-id]))))])))]
[(mem? internal-id stx-defs)
=>
(lambda (b)
(with-syntax ([id internal-id]
[out-id external-id])
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
#`(begin
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(lambda (stx)
(tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
(provide (rename-out [export-id out-id]))))))]
[(eq? (syntax-e internal-id) (syntax-e external-id))
#`(provide #,internal-id)]
[else #`(provide (rename-out [#,internal-id #,external-id]))]))
(kernel-syntax-case form #f
[(#%provide form ...)
(map
(lambda (f)
(parameterize ([current-orig-stx f])
(syntax-case* f (struct rename all-defined protect all-defined-except all-from all-from-except)
(lambda (a b) (eq? (syntax-e a) (syntax-e b)))
[id
(identifier? #'id)
(mk #'id #'id)]
[(rename in out)
(mk #'in #'out)]
[(protect . _)
(tc-error "provide: protect not supported by Typed Scheme")]
[_ (int-err "unknown provide form")])))
(syntax->list #'(form ...)))]
[_ (int-err "non-provide form! ~a" (syntax->datum form))]))
(lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
(provide (rename-out [export-id out-id]))))])))]
[(mem? internal-id stx-defs)
=>
(lambda (b)
(with-syntax ([id internal-id]
[out-id external-id])
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
#`(begin
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(lambda (stx)
(tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
(provide (rename-out [export-id out-id]))))))]
[(eq? (syntax-e internal-id) (syntax-e external-id))
#`(provide #,internal-id)]
[else #`(provide (rename-out [#,internal-id #,external-id]))]))
(kernel-syntax-case form #f
[(#%provide form ...)
(map
(lambda (f)
(parameterize ([current-orig-stx f])
(syntax-case* f (struct rename all-defined protect all-defined-except all-from all-from-except)
(lambda (a b) (eq? (syntax-e a) (syntax-e b)))
[id
(identifier? #'id)
(mk #'id #'id)]
[(rename in out)
(mk #'in #'out)]
[(protect . _)
(tc-error "provide: protect not supported by Typed Scheme")]
[_ (int-err "unknown provide form")])))
(syntax->list #'(form ...)))]
[_ (int-err "non-provide form! ~a" (syntax->datum form))])))

View File

@ -484,6 +484,8 @@
(match-let ([(list (tc-result: ts) ...) (map (lambda (f) (outer-loop
(ret f e1 e2) argtypes arg-thn-effs arg-els-effs args)) fs)])
(ret (apply Un ts)))]
;; error type is a perfectly good fcn type
[(tc-result: (Error:)) (ret (make-Error))]
[(tc-result: f-ty _ _) (tc-error/expr #:return (ret (Un))
"Cannot apply expression of type ~a, since it is not a function type" f-ty)]))))

View File

@ -40,7 +40,9 @@
;; require/typed
[(define-values () (begin (quote-syntax (require/typed-internal nm ty)) (#%plain-app values)))
(register-type #'nm (parse-type #'ty))]
(let ([t (parse-type #'ty)])
(register-type #'nm t)
(list (make-def-binding #'nm t)))]
;; define-typed-struct
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...))) (#%plain-app values)))