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

fix mlish tests to use new app err msg abstractions

Browse Source
This commit is contained in:
Stephen Chang 2016-02-27 16:26:15 -05:00
parent d880b9d668
commit 9000e126ff
3 changed files with 58 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
tapl/mlish.rkt
View File

@ -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

49
tapl/tests/mlish-tests.rkt
View File

@ -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)

19
tapl/tests/rackunit-typechecking.rkt
View File

@ -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