From 9000e126ffec62c785042f139dcc10f730614d4b Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Sat, 27 Feb 2016 16:26:15 -0500 Subject: [PATCH] fix mlish tests to use new app err msg abstractions --- tapl/mlish.rkt | 32 +++++++++--------- tapl/tests/mlish-tests.rkt | 49 +++++++++++++++------------- tapl/tests/rackunit-typechecking.rkt | 19 +++++++++-- 3 files changed, 58 insertions(+), 42 deletions(-) diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt index 1a34877..cf91be9 100644 --- a/tapl/mlish.rkt +++ b/tapl/mlish.rkt @@ -10,7 +10,7 @@ ;(reuse tup × proj #:from "stlc+tup.rkt") ;(reuse define-type-alias #:from "stlc+reco+var.rkt") ;(provide hd tl nil?) -(provide (rename-out [lifted→ →])) +(provide →) (provide define-type match) (provide (rename-out [ext-stlc:let let])) @@ -91,10 +91,11 @@ (define-syntax (define-type stx) (syntax-parse stx [(_ Name:id . rst) - #:with Name2 (generate-temporary #'Name) + #:with NewName (generate-temporary #'Name) + #:with Name2 (add-orig #'(NewName) #'Name) #`(begin - (define-type (Name2) . #,(subst (add-orig #'(Name2) #'Name) #'Name #'rst)) - (define-type-alias Name (Name2)))] + (define-type Name2 . #,(subst #'Name2 #'Name #'rst)) + (define-type-alias Name Name2))] [(_ (Name:id X:id ...) ;; constructors must have the form (Cons τ ...) ;; but the first ~or clause accepts 0-arg constructors as ids @@ -206,7 +207,7 @@ #;(define-syntax lifted→ ; wrap → with ∀ (syntax-parser [(_ . rst) #'(∀ () (ext-stlc:→ . rst))])) -(define-syntax lifted→ ; wrapping → +(define-syntax → ; wrapping → (syntax-parser #;[(_ (~and Xs {X:id ...}) . rst) #:when (brace? #'Xs) @@ -222,18 +223,17 @@ (define Y (datum->syntax #'rst (syntax->datum X))) (L (cons Y Xs)))]) ((current-type-eval) #`(∀ #,Xs (ext-stlc:→ . rst)))))])) - ;#'(∀ () (ext-stlc:→ . rst)) -; redefine these to use lifted→ -(define-primop + : (lifted→ Int Int Int)) -(define-primop - : (lifted→ Int Int Int)) -(define-primop void : (lifted→ Unit)) -(define-primop = : (lifted→ Int Int Bool)) -(define-primop zero? : (lifted→ Int Bool)) -(define-primop sub1 : (lifted→ Int Int)) -(define-primop add1 : (lifted→ Int Int)) -(define-primop not : (lifted→ Bool Bool)) -(define-primop abs : (lifted→ Int Int)) +; redefine these to use lifted → +(define-primop + : (→ Int Int Int)) +(define-primop - : (→ Int Int Int)) +(define-primop void : (→ Unit)) +(define-primop = : (→ Int Int Bool)) +(define-primop zero? : (→ Int Bool)) +(define-primop sub1 : (→ Int Int)) +(define-primop add1 : (→ Int Int)) +(define-primop not : (→ Bool Bool)) +(define-primop abs : (→ Int Int)) ; all λs have type (∀ (X ...) (→ τ_in ... τ_out)), even monomorphic fns diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt index e28379a..acbf831 100644 --- a/tapl/tests/mlish-tests.rkt +++ b/tapl/tests/mlish-tests.rkt @@ -27,11 +27,10 @@ (define (g2 [lst : (List X)] → (List X)) lst) (check-type g2 : (→ (List X) (List X))) -(typecheck-fail (g2 1) - #:with-msg - (string-append - "Could not infer instantiation of polymorphic function.*" - "Expected.+argument\\(s\\) with type\\(s\\).+\\(List X\\)")) +(typecheck-fail (g2 1) + #:with-msg + (expected "(List X)" #:given "Int" + #:note "Could not infer instantiation of polymorphic function")) ;(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int})) ;(check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool})) @@ -82,7 +81,9 @@ (typecheck-fail (match 1 with [INil -> 1])) (typecheck-fail (ConsI #f INil) - #:with-msg "Type error applying constructor ConsI.*Expected.*Int, IntList") + #:with-msg + (expected "Int, IntList" #:given "Bool, IntList" + #:note "Type error applying constructor ConsI")) ;; annotated (check-type (Nil {Int}) : (List Int)) @@ -106,11 +107,17 @@ (typecheck-fail Nil #:with-msg "add annotations") (typecheck-fail (Cons 1 (Nil {Bool})) - #:with-msg "Type error applying constructor Cons.*Expected.*argument.*with type.*Int, \\(List Int\\)") + #:with-msg + (expected "Int, (List Int)" #:given "Int, (List Bool)" + #:note "Type error applying constructor Cons")) (typecheck-fail (Cons {Bool} 1 (Nil {Int})) - #:with-msg "Type error applying constructor Cons.*Expected.*argument.*with type.*Bool, \\(List Bool\\)") + #:with-msg + (expected "Bool, (List Bool)" #:given "Int, (List Int)" + #:note "Type error applying constructor Cons")) (typecheck-fail (Cons {Bool} 1 Nil) - #:with-msg "Type error applying constructor Cons.*Expected.*argument.*with type.*Bool, \\(List Bool\\)") + #:with-msg + (expected "Bool, (List Bool)" #:given "Int, (List Bool)" + #:note "Type error applying constructor Cons")) (typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1]) #:with-msg "add annotations") @@ -154,12 +161,12 @@ (typecheck-fail ((λ ([x : Unit]) x) 2) - #:with-msg - "Type error applying function.*Expected.*argument.*with type.* Unit.*Given.*Int") + #:with-msg + (expected "Unit" #:given "Int" #:note "Type error applying function")) (typecheck-fail ((λ ([x : Unit]) x) void) #:with-msg - "Type error applying function.*Expected.*argument.*with type.* Unit.*Given.*\\(→ Unit\\)") + (expected "Unit" #:given "(→ Unit)" #:note "Type error applying function")) (check-type ((λ ([x : Unit]) x) (void)) : Unit) @@ -194,16 +201,14 @@ (check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) (typecheck-fail (let ([x #f]) (+ x 1)) - #:with-msg - "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int") + #:with-msg (expected "Int, Int" #:given "Bool, Int")) (typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y)) #:with-msg "x: unbound identifier") (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) (typecheck-fail (let* ([x #t] [y (+ x 1)]) 1) - #:with-msg - "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int") + #:with-msg (expected "Int, Int" #:given "Bool, Int")) ; letrec (typecheck-fail @@ -277,8 +282,7 @@ (typecheck-fail ((λ ([x : Bool]) x) 1) - #:with-msg - "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Bool") + #:with-msg (expected "Bool" #:given "Int")) ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type (typecheck-fail (λ ([f : Int]) (f 1 2)) @@ -292,15 +296,14 @@ (typecheck-fail (+ 1 (λ ([x : Int]) x)) - #:with-msg - "Arguments to function \\+ have wrong type.+Given:\n 1 : Int.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int") + #:with-msg (expected "Int, Int" #:given "Int, (→ Int Int)")) (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x)) - #:with-msg - "Arguments to function \\+ have wrong type.+Given:.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int") + #:with-msg (expected "Int, Int" #:given "(→ Int Int), (→ Int Int)")) (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1) - #:with-msg "Wrong number of arguments given to function") + #:with-msg (expected "Int, Int" #:given "Int" + #:note "Wrong number of arguments")) (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt index 488affa..9aeb024 100644 --- a/tapl/tests/rackunit-typechecking.rkt +++ b/tapl/tests/rackunit-typechecking.rkt @@ -2,6 +2,17 @@ (require (for-syntax rackunit) rackunit "../typecheck.rkt") (provide (all-defined-out)) +(begin-for-syntax + (define (add-esc s) (string-append "\\" s)) + (define escs (map add-esc '("(" ")"))) + (define (add-escs str) + (foldl (lambda (c s) (regexp-replace c s (add-esc c))) str escs)) + (define (expected tys #:given [givens ""] #:note [note ""]) + (string-append + note ".*Expected.+argument\\(s\\) with type\\(s\\).+" + (add-escs tys) ".*Given:.*" + (string-join (map add-escs (string-split givens ", ")) ".*")))) + (define-syntax (check-type stx) (syntax-parse stx #:datum-literals (: ⇒) [(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)] @@ -29,7 +40,9 @@ (define-syntax (typecheck-fail stx) (syntax-parse stx #:datum-literals (:) - [(_ e (~optional (~seq #:with-msg msg-pat) #:defaults ([msg-pat ""]))) + [(_ e (~optional (~seq #:with-msg msg-pat) #:defaults ([msg-pat #'""]))) + #:with msg:str + (eval-syntax (datum->syntax #'here (syntax->datum #'msg-pat))) #:when (check-exn (λ (ex) (or (exn:fail? ex) (exn:test:check? ex))) (λ () @@ -37,12 +50,12 @@ ; check err msg matches ([exn:fail? (λ (ex) - (unless (regexp-match? (syntax-e #'msg-pat) (exn-message ex)) + (unless (regexp-match? (syntax-e #'msg) (exn-message ex)) (printf (string-append "ERROR-MSG ERROR: wrong err msg produced by expression ~v:\n" "EXPECTED:\nmsg matching pattern ~v,\nGOT:\n~v\n") - (syntax->datum #'e) (syntax-e #'msg-pat) (exn-message ex))) + (syntax->datum #'e) (syntax-e #'msg) (exn-message ex))) (raise ex))]) (expand/df #'e))) (format