From 8656e1469d7821ad9939ca88500b15055a7d8b8b Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 30 Jun 2015 12:43:03 -0400 Subject: [PATCH] report errors in terms of surface, not expanded, type --- tapl/fomega.rkt | 44 ++++++++++++++++++++++++++++++++++++-------- tapl/fomega2.rkt | 21 ++++++++++++++++++--- tapl/stlc.rkt | 24 ++++++++++++++++++++---- tapl/stx-utils.rkt | 3 +++ tapl/typecheck.rkt | 7 +++++++ 5 files changed, 84 insertions(+), 15 deletions(-) diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt index b886340..b24d245 100644 --- a/tapl/fomega.rkt +++ b/tapl/fomega.rkt @@ -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)])) diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt index f6bcc08..1cd68ea 100644 --- a/tapl/fomega2.rkt +++ b/tapl/fomega2.rkt @@ -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)])) diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index a1fa55c..fecea95 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -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)])) diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt index aa812c6..b0fd6f7 100644 --- a/tapl/stx-utils.rkt +++ b/tapl/stx-utils.rkt @@ -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))) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 6303b13..c9715c6 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -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)