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

report errors in terms of surface, not expanded, type

Browse Source
This commit is contained in:
Stephen Chang 2015-06-30 12:43:03 -04:00
parent d69a16ffcb
commit 8656e1469d
5 changed files with 84 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
tapl/fomega.rkt
View File

@ -110,19 +110,32 @@
(syntax->datum #'τ_fn) (syntax->datum #'k_fn))
#:with ((~literal #%plain-app) _ k ... k_res) #'k_fn
#:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
#:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
#:fail-unless (stx-length=? #'(k_arg ...) #'(k ...))
(string-append
(format
"Wrong number of args given to tyλ ~a, or args have wrong kind:\ngiven: "
"Wrong number of args given to tyλ ~a:\ngiven: "
(syntax->datum #'τ_fn))
(string-join
(map
(λ (τ+k) (format "~a : ~a" (car τ+k) (cadr τ+k)))
(syntax->datum #'([τ_arg k_arg] ...)))
(λ (t k) (format "~a : ~a" t k))
(syntax->datum #'(τ_arg ...))
(syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
", ")
(format "\nexpected: ~a argument(s)." (stx-length #'(k ...))))
#:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
(string-append
(format
"Arguments to tyλ ~a have wrong type:\ngiven: "
(syntax->datum #'τ_fn))
(string-join
(map
(λ (t k) (format "~a : ~a" t k))
(syntax->datum #'(τ_arg ...))
(syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
", ")
"\nexpected arguments with type: "
(string-join
(map (λ (x) (format "~a" x)) (syntax->datum #'(k ...)))
(map ~a (syntax->datum #`#,(stx-map get-orig #'(k ...))))
", "))
;; cant do type-subst here bc τ_fn might be a (forall) tyvar
;#:with τ_res ((current-type-eval) #'(tyapply τ_fn- τ_arg- ...))
@ -150,17 +163,32 @@
(syntax->datum #'e_fn) (syntax->datum #'τ_fn))
#:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
(string-append
(format
"Wrong number of args given to function ~a:\ngiven: "
(syntax->datum #'e_fn))
(string-join
(map
(λ (e t) (format "~a : ~a" e t))
(syntax->datum #'(e_arg ...))
(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
", ")
(format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
(string-append
(format
"Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
"Arguments to function ~a have wrong type:\ngiven: "
(syntax->datum #'e_fn))
(string-join
(map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
(map
(λ (e t) (format "~a : ~a" e t))
(syntax->datum #'(e_arg ...))
(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
", ")
"\nexpected arguments with type: "
(string-join
(map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
(map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
", "))
(⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))

21
tapl/fomega2.rkt
View File

@ -165,17 +165,32 @@
(syntax->datum #'e_fn) (syntax->datum #'τ_fn))
#:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
(string-append
(format
"Wrong number of args given to function ~a:\ngiven: "
(syntax->datum #'e_fn))
(string-join
(map
(λ (e t) (format "~a : ~a" e t))
(syntax->datum #'(e_arg ...))
(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
", ")
(format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
(string-append
(format
"Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
"Arguments to function ~a have wrong type:\ngiven: "
(syntax->datum #'e_fn))
(string-join
(map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
(map
(λ (e t) (format "~a : ~a" e t))
(syntax->datum #'(e_arg ...))
(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
", ")
"\nexpected arguments with type: "
(string-join
(map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
(map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
", "))
(⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))

24
tapl/stlc.rkt
View File

@ -17,7 +17,8 @@
;; - for now, type-eval = full expansion
;; - must expand because:
;; - checks for unbound identifiers (ie, undefined types)
(define (type-eval τ) (expand/df τ))
(define (type-eval τ)
(add-orig (expand/df τ) τ))
(current-type-eval type-eval))
(begin-for-syntax
@ -60,16 +61,31 @@
(syntax->datum #'e_fn) (syntax->datum #'τ_fn))
#:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
#:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
#:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
(string-append
(format
"Wrong number of args given to function ~a:\ngiven: "
(syntax->datum #'e_fn))
(string-join
(map
(λ (e t) (format "~a : ~a" e t))
(syntax->datum #'(e_arg ...))
(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
", ")
(format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
(string-append
(format
"Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
"Arguments to function ~a have wrong type:\ngiven: "
(syntax->datum #'e_fn))
(string-join
(map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
(map
(λ (e t) (format "~a : ~a" e t))
(syntax->datum #'(e_arg ...))
(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
", ")
"\nexpected arguments with type: "
(string-join
(map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
(map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
", "))
(⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))

3
tapl/stx-utils.rkt
View File

@ -23,7 +23,10 @@
(member (datum->syntax v) (map datum->syntax (syntax->list stx)) string=?))
(define (str-stx-assoc v stx)
(assoc v (map syntax->list (syntax->list stx)) stx-str=?))
(define (stx-length stx) (length (syntax->list stx)))
(define (stx-length=? stx1 stx2)
(= (stx-length stx1) (stx-length stx2)))
(define (stx-last stx) (last (syntax->list stx)))

7
tapl/typecheck.rkt
View File

@ -33,6 +33,13 @@
(struct exn:fail:type:runtime exn:fail:user ())
(begin-for-syntax
(define (add-orig stx orig)
(define origs (or (syntax-property orig 'orig) null))
(syntax-property stx 'orig (cons orig origs)))
(define (get-orig τ)
(car (reverse (or (syntax-property τ 'orig) (list τ))))))
;; TODO: refine this to enable specifying arity information
;; type constructors currently must have 1+ arguments
(define-syntax (define-type-constructor stx)