diff --git a/tapl/tests/tlb-mlish-tests.rkt b/tapl/tests/tlb-mlish-tests.rkt index 964168b..2290a92 100644 --- a/tapl/tests/tlb-mlish-tests.rkt +++ b/tapl/tests/tlb-mlish-tests.rkt @@ -12,7 +12,7 @@ ;; top-level defines (define (f [x : Int] → Int) x) -(typecheck-fail (f 1 2) #:with-msg "Wrong number of arguments") +(typecheck-fail (f 1 2) #:with-msg "f: wrong number of arguments: expected 1, given 2") (check-type f : (→ Int Int)) (check-type (f 1) : Int ⇒ 1) (typecheck-fail (f (λ ([x : Int]) x))) @@ -32,7 +32,7 @@ (Cons X (List X))) ;; arity err -(typecheck-fail (Cons 1) #:with-msg "Cons: Wrong number of arguments") +(typecheck-fail (Cons 1) #:with-msg "Cons: wrong number of arguments: expected 2, given 1") ;; type err (typecheck-fail (Cons 1 1) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 223556e..af93b6d 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -399,6 +399,41 @@ (define (expand/df e) (local-expand e 'expression null)) + ;; typecheck-fail-msg/1 : Type Type Stx -> String + (define (typecheck-fail-msg/1 τ_expected τ_given expression) + (format "type mismatch: expected ~a, given ~a\n expression: ~s" + (type->str τ_expected) + (type->str τ_given) + (syntax->datum (get-orig expression)))) + + ;; typecheck-fail-msg/1/no-expr : Type Type Stx -> String + (define (typecheck-fail-msg/1/no-expr τ_expected τ_given) + (format "type mismatch: expected ~a, given ~a" + (type->str τ_expected) + (type->str τ_given))) + + ;; typecheck-fail-msg/multi/no-exprs : (Stx-Listof Type) (Stx-Listof Type) -> String + (define (typecheck-fail-msg/multi/no-exprs τs_expected τs_given) + (format (string-append "type mismatch\n" + " expected: ~a\n" + " given: ~a") + (string-join (stx-map type->str τs_expected) ", ") + (string-join (stx-map type->str τs_given) ", "))) + + ;; no-expected-type-fail-msg : -> String + (define (no-expected-type-fail-msg) + "no expected type, add annotations") + + ;; num-args-fail-msg : Stx (Stx-Listof Type) (Stx-Listof Stx) -> String + (define (num-args-fail-msg fn τs_expected arguments) + (format (string-append "~s: wrong number of arguments: expected ~a, given ~a\n" + " expected: ~a\n" + " arguments: ~a") + (syntax->datum (get-orig fn)) + (stx-length τs_expected) (stx-length arguments) + (string-join (stx-map type->str τs_expected) ", ") + (string-join (map ~s (map syntax->datum (stx-map get-orig arguments))) ", "))) + (struct exn:fail:type:check exn:fail:user ()) (struct exn:fail:type:infer exn:fail:user ()) @@ -434,7 +469,7 @@ [(stx-pair? τ) (string-join (stx-map type->str τ) #:before-first "(" #:after-last ")")] - [else (format "~a" (syntax->datum τ))]))) + [else (format "~s" (syntax->datum τ))]))) (begin-for-syntax (define (mk-? id) (format-id id "~a?" id)) diff --git a/tapl/typed-lang-builder/fomega.rkt b/tapl/typed-lang-builder/fomega.rkt index 021b4ff..5bf58c8 100644 --- a/tapl/typed-lang-builder/fomega.rkt +++ b/tapl/typed-lang-builder/fomega.rkt @@ -110,8 +110,7 @@ [(tyapp τ_fn τ_arg ...) ▶ [⊢ [[τ_fn ≫ τ_fn-] ⇒ : (~⇒ k_in ... k_out)]] [#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...]) - (format "wrong number of arguments: expected ~a, given ~a" - (stx-length #'[k_in ...]) (stx-length #'[τ_arg ...]))] + (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])] [⊢ [[τ_arg ≫ τ_arg-] ⇐ : k_in] ...] -------- [⊢ [[_ ≫ (#%app- τ_fn- τ_arg- ...)] ⇒ : k_out]]]) diff --git a/tapl/typed-lang-builder/mlish-core.rkt b/tapl/typed-lang-builder/mlish-core.rkt index abbf7d2..12e777b 100644 --- a/tapl/typed-lang-builder/mlish-core.rkt +++ b/tapl/typed-lang-builder/mlish-core.rkt @@ -865,7 +865,7 @@ [#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)] ;; arity check [#:fail-unless (stx-length=? #'(τ_in ...) #'e_args) - (format "~s: Wrong number of arguments." (syntax->datum (get-orig #'e_fn)))] + (num-args-fail-msg #'e_fn #'[τ_in ...] #'e_args)] ;; compute argument types [#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))] ;; typecheck args diff --git a/tapl/typed-lang-builder/stlc+effect.rkt b/tapl/typed-lang-builder/stlc+effect.rkt index 51e6d60..5bb2ba0 100644 --- a/tapl/typed-lang-builder/stlc+effect.rkt +++ b/tapl/typed-lang-builder/stlc+effect.rkt @@ -66,8 +66,7 @@ (⇒ := (~locs fas ...)) (⇒ ! (~locs fds ...))]] [#:fail-unless (stx-length=? #'[e ...] #'[τ_in ...]) - (format "wrong number of arguments: expected ~a, given ~a" - (stx-length #'[τ_in ...] #'[e ...]))] + (num-args-fail-msg #'efn #'[τ_in ...] #'[e ...])] [⊢ [[e ≫ e_arg-] (⇐ : τ_in) (⇒ ν (~locs ns ...)) diff --git a/tapl/typed-lang-builder/stlc.rkt b/tapl/typed-lang-builder/stlc.rkt index bc1c92a..2e05ab9 100644 --- a/tapl/typed-lang-builder/stlc.rkt +++ b/tapl/typed-lang-builder/stlc.rkt @@ -41,8 +41,7 @@ [(_ e_fn e_arg ...) ▶ [⊢ [[e_fn ≫ e_fn-] ⇒ : (~→ τ_in ... τ_out)]] [#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) - (format "wrong number of arguments: expected ~a, given ~a" - (stx-length #'[τ_in ...]) (stx-length #'[e_arg ...]))] + (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])] [⊢ [[e_arg ≫ e_arg-] ⇐ : τ_in] ...] -------- [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ : τ_out]]]) diff --git a/tapl/typed-lang-builder/typed-lang-builder.rkt b/tapl/typed-lang-builder/typed-lang-builder.rkt index 4a83dad..6a525a1 100644 --- a/tapl/typed-lang-builder/typed-lang-builder.rkt +++ b/tapl/typed-lang-builder/typed-lang-builder.rkt @@ -59,10 +59,7 @@ (~post (~fail #:when (and (not (typecheck? #'τ-tmp #'τ-exp)) (get-orig #'e-tmp)) - (format "type mismatch: expected ~a, given ~a\n expression: ~s" - (type->str #'τ-exp) - (type->str #'τ-tmp) - (syntax->datum (get-orig #'e-tmp))))) + (typecheck-fail-msg/1 #'τ-exp #'τ-tmp #'e-tmp))) (get-orig #'e-tmp)))]) (define-splicing-syntax-class ⇒-props #:attributes (e-pat) @@ -147,18 +144,12 @@ #:with [pat ...] #'[(~post (~fail #:unless (typecheck? #'a #'b) - (format "type mismatch: expected ~a, given ~a" - (type->str #'b) - (type->str #'a))))]] + (typecheck-fail-msg/1/no-expr #'b #'a)))]] [pattern (~seq [a τ⊑ b] ooo:elipsis) #:with [pat ...] #'[(~post (~fail #:unless (typechecks? #'[a ooo] #'[b ooo]) - (format (string-append "type mismatch\n" - " expected: ~a\n" - " given: ~a") - (string-join (stx-map type->str #'[b ooo]) ", ") - (string-join (stx-map type->str #'[a ooo]) ", "))))]] + (typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))]] [pattern [#:when condition:expr] #:with [pat ...] #'[(~fail #:unless condition)]] @@ -189,7 +180,7 @@ pat* (~parse τ (get-expected-type #'stx)) (~post (~post (~fail #:unless (syntax-e #'τ) - "no expected type, add annotations"))) + (no-expected-type-fail-msg)))) (~parse τ-pat #'τ)) #:with [stuff ...] #'[] #:with body:expr @@ -216,7 +207,7 @@ pat* (~parse τ (get-expected-type #'stx)) (~post (~post (~fail #:unless (syntax-e #'τ) - "no expected type, add annotations"))) + (no-expected-type-fail-msg)))) (~parse τ-pat #'τ)) #:attr transform-body (lambda (body)