commit 87314013187ad8c4a65d24ede5787c1581dfd70a
parent d5435eb71bcab39d3b48aa6b12d8e37f4d5f5631
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 1 Apr 2016 17:08:48 -0400
start match2 exhaustiveness checking; nested checks not quite working
Diffstat:
3 files changed, 236 insertions(+), 34 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -381,7 +381,7 @@
[pat #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens)
(syntax-parse #'pat
[{(~datum _)} #'_]
- [{(~literal stlc+cons:nil)} #'(list)]
+ [{(~literal stlc+cons:nil)} (syntax/loc p (list))]
[{A:id} ; disambiguate 0-arity constructors (that don't need parens)
#:with ((~literal #%plain-lambda) (RecName)
((~literal let-values) ()
@@ -396,7 +396,7 @@
#:when (not (stx-null? #'(p ...)))
#:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
(compile-pat #'ps ty)]
- [{p ...} (compile-pat #'(p ...) ty)])]
+ [{pat ...} (compile-pat (syntax/loc p (pat ...)) ty)])]
[(~datum _) #'_]
[(~literal stlc+cons:nil) ; nil
#'(list)]
@@ -415,25 +415,25 @@
#:with (~× t ...) ty
#:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'(p1 p ...) #'(t ...))
#'(list p- ...)]
- [((~literal stlc+tup:tup) p ...)
- #:with (~× t ...) ty
- #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'(p ...) #'(t ...))
- #'(list p- ...)]
- [((~literal stlc+cons:list) p ...)
+ [((~literal stlc+tup:tup) . pats)
+ #:with (~× . tys) ty
+ #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'pats #'tys)
+ (syntax/loc p (list p- ...))]
+ [((~literal stlc+cons:list) . ps)
#:with (~List t) ty
- #:with (p- ...) (stx-map (lambda (p) (compile-pat p #'t)) #'(p ...))
- #'(list p- ...)]
- [((~seq p (~datum ::)) ... rst) ; nicer cons stx
+ #:with (p- ...) (stx-map (lambda (p) (compile-pat p #'t)) #'ps)
+ (syntax/loc p (list p- ...))]
+ [((~seq pat (~datum ::)) ... last) ; nicer cons stx
#:with (~List t) ty
- #:with (p- ...) (stx-map (lambda (pp) (compile-pat pp #'t)) #'(p ...))
- #:with ps- (compile-pat #'rst ty)
- #'(list-rest p- ... ps-)]
+ #:with (p- ...) (stx-map (lambda (pp) (compile-pat pp #'t)) #'(pat ...))
+ #:with last- (compile-pat #'last ty)
+ (syntax/loc p (list-rest p- ... last-))]
[((~literal stlc+cons:cons) p ps)
#:with (~List t) ty
#:with p- (compile-pat #'p #'t)
#:with ps- (compile-pat #'ps ty)
#'(cons p- ps-)]
- [(Name p ...)
+ [(Name . pats)
#:with ((~literal #%plain-lambda) (RecName)
((~literal let-values) ()
((~literal let-values) ()
@@ -447,8 +447,77 @@
[((~literal #%plain-app) 'C . rst)
(equal? (syntax->datum #'Name) (syntax->datum #'C))])
#'info-unfolded)
- #:with (p- ...) (stx-map compile-pat #'(p ...) #'(τ ...))
- #'(StructName p- ...)]))
+ #:with (p- ...) (stx-map compile-pat #'pats #'(τ ...))
+ (syntax/loc p (StructName p- ...))]))
+
+ (define (check-exhaust pats ty)
+ (define (else-pat? p)
+ (syntax-parse p [(~literal _) #t] [_ #f]))
+ (define (nil-pat? p)
+ (syntax-parse p
+ [((~literal list)) #t]
+ [_ #f]))
+ (define (non-nil-pat? p)
+ (syntax-parse p
+ [((~literal list-rest) . rst) #t]
+ [((~literal cons) . rst) #t]
+ [_ #f]))
+ (define (tup-pat? p)
+ (syntax-parse p
+ [((~literal list) . _) #t] [_ #f]))
+ (cond
+ [(or (stx-ormap else-pat? pats) (stx-ormap identifier? pats)) #t]
+ [(List? ty) ; lists
+ (unless (stx-ormap nil-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing nil clause for list expression"
+ (syntax-line last) (syntax-column last)))))
+ (unless (stx-ormap non-nil-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing clause for non-empty, arbitrary length list"
+ (syntax-line last) (syntax-column last)))))
+ #t]
+ [(×? ty) ; tuples
+ (unless (stx-ormap tup-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing pattern for tuple expression"
+ (syntax-line last) (syntax-column last)))))
+ (syntax-parse pats
+ [((_ p ...) ...)
+ (syntax-parse ty
+ [(~× t ...)
+ (apply stx-andmap
+ (lambda (t . ps) (check-exhaust ps t))
+ #'(t ...)
+ (syntax->list #'((p ...) ...)))])])]
+ [else ; algebraic datatypes
+ (syntax-parse (get-extra-info ty)
+ [((~literal #%plain-lambda) (RecName)
+ ((~literal let-values) ()
+ ((~literal let-values) ()
+ . (((~literal #%plain-app)
+ ((~literal quote) C)
+ ((~literal quote) Cstruct)
+ . rst) ...))))
+ (syntax-parse pats
+ [((Cpat _ ...) ...)
+ (define Cs (syntax->datum #'(C ...)))
+ (define Cstructs (syntax->datum #'(Cstruct ...)))
+ (define Cpats (syntax->datum #'(Cpat ...)))
+ (unless (set=? Cstructs Cpats)
+ (error 'match2
+ (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) clauses not exhaustive; missing: ~a"
+ (syntax-line last) (syntax-column last)
+ (string-join
+ (for/list ([C Cs][Cstr Cstructs] #:unless (member Cstr Cpats))
+ (symbol->string C))
+ ", ")))))
+ #t])]
+ [_ #t])]))
+
+ (define (compile-pats pats ty)
+ (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats))
)
(provide match2)
@@ -459,10 +528,16 @@
#:with [e- τ_e] (infer+erase #'e)
(syntax-parse #'clauses #:datum-literals (->)
[([(~seq p ...) -> e_body] ...)
- #:with (pat ...) #'({p ...} ...) ; use brace to indicate root pattern
- #:with ((~and ctx ([x ty] ...)) ...) (stx-map (lambda (p) (get-ctx p #'τ_e)) #'(pat ...))
+ #:with (pat ...) (stx-map (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
+ #'((p ...) ...)) ; use brace to indicate root pattern
+ #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)
+ ;; #:with ((~and ctx ([x ty] ...)) ...) (stx-map (lambda (p) (get-ctx p #'τ_e)) #'(pat ...))
#:with ([(x- ...) e_body- ty_body] ...) (stx-map infer/ctx+erase #'(ctx ...) #'(e_body ...))
- #:with (pat- ...) (stx-map (lambda (p) (compile-pat p #'τ_e)) #'(pat ...))
+ ;; #:with (pat- ...) (stx-map (lambda (p) (compile-pat p #'τ_e)) #'(pat ...))
+ #:fail-unless (same-types? #'(ty_body ...))
+ (string-append "branches have different types, given: "
+ (string-join (stx-map type->str #'(ty_body ...)) ", "))
+ #:when (check-exhaust #'(pat- ...) #'τ_e)
#:with τ_out (stx-car #'(ty_body ...))
(⊢ (match e- [pat- (let ([x- x] ...) e_body-)] ...) : τ_out)
])]))
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
@@ -11,6 +11,8 @@
(define (stx-cadr stx) (stx-car (stx-cdr stx)))
(define (stx-caddr stx) (stx-cadr (stx-cdr stx)))
+(define (stx-rev stx)
+ (reverse (syntax->list stx)))
(define (stx-andmap f . stx-lsts)
(apply andmap f (map syntax->list stx-lsts)))
(define (stx-ormap f . stx-lsts)
diff --git a/tapl/tests/mlish/match2.mlish b/tapl/tests/mlish/match2.mlish
@@ -8,18 +8,57 @@
(B (× X X))
(C (× X (× X X))))
+(typecheck-fail
+ (match2 (B (tup 2 3)) with
+ [B x -> x])
+ #:with-msg "clauses not exhaustive; missing: A, C")
+
+(typecheck-fail
+ (match2 (B (tup 2 3)) with
+ [A x -> x]
+ [C (x,y) -> y]
+ [B x -> x]) #:with-msg "branches have different types")
+
+(typecheck-fail
+ (match2 (B (tup 2 3)) with
+ [A x -> (tup x x)]
+ [C x -> x]
+ [B x -> x]) #:with-msg "branches have different types")
+
(check-type
(match2 (B (tup 2 3)) with
+ [A x -> (tup x x)]
+ [C (x,y) -> y]
[B x -> x]) : (× Int Int) -> (list 2 3))
+(typecheck-fail
+ (match2 (A (tup 2 3)) with
+ [A x -> x]) #:with-msg "clauses not exhaustive; missing: B, C")
+
(check-type
(match2 (A (tup 2 3)) with
+ [B (x,y) -> y]
+ [C (x,y) -> x]
[A x -> x]) : (× Int Int) -> (list 2 3))
(check-type
+ (match2 (A (tup 2 3)) with
+ [B (x,y) -> y]
+ [A x -> x]
+ [C (x,y) -> x]) : (× Int Int) -> (list 2 3))
+
+(typecheck-fail
+ (match2 (A (tup 2 3)) with
+ [B (x,y) -> y]
+ [A x -> x]
+ [C x -> x]) #:with-msg "branches have different types")
+
+(check-type
(match2 (A 1) with
- [A x -> x]) : Int -> 1)
+ [A x -> x]
+ [_ -> -1]) : Int -> 1)
+;; TODO: better err msg, is actually a type err
(typecheck-fail
(match2 (B 1) with
[B x -> x])
@@ -27,11 +66,13 @@
(check-type
(match2 (B (tup 2 3)) with
- [B (tup x y) -> (+ x y)]) : Int -> 5)
+ [B (tup x y) -> (+ x y)]
+ [_ -> -1]) : Int -> 5)
(check-type
(match2 (C (tup 2 (tup 3 4))) with
- [C (tup x (tup y z)) -> (+ x (+ y z))]) : Int -> 9)
+ [C (tup x (tup y z)) -> (+ x (+ y z))]
+ [_ -> -1]) : Int -> 9)
(check-type
(match2 (C (tup 2 (tup 3 4))) with
@@ -42,44 +83,104 @@
;; lists
+(typecheck-fail
+ (match2 (list 1) with
+ [list x -> x]) #:with-msg "missing nil clause")
+
+(typecheck-fail
+ (match2 (list 1) with
+ [nil -> 0]
+ [list x -> x])
+ #:with-msg "missing clause for non-empty, arbitrary length list")
+
(check-type
(match2 (list 1) with
- [list x -> x]) : Int -> 1)
+ [nil -> 0]
+ [x :: xs -> x]) : Int -> 1)
+
+(check-type
+ (match2 (list 1) with
+ [nil -> 0]
+ [list x -> x]
+ [x :: xs -> x]) : Int -> 1)
+
+(check-type
+ (match2 (list 1) with
+ [list -> 0]
+ [list x -> x]
+ [x :: xs -> x]) : Int -> 1)
+
+(check-type
+ (match2 (list 1) with
+ [list x -> x]
+ [_ -> 0]) : Int -> 1)
+
+(check-type
+ (match2 (list 1) with
+ [x :: xs -> x]
+ [nil -> 0]) : Int -> 1)
+
+(check-type
+ (match2 (list 1) with
+ [_ -> -1]
+ [list x -> x]
+ [nil -> 0]) : Int -> -1)
+
+(check-type
+ (match2 (list 1) with
+ [_ -> -1]
+ [list x -> x]
+ [list -> 0]) : Int -> -1)
+
+(check-type
+ (match2 (list 1) with
+ [_ -> 0]) : Int -> 0)
+
+(typecheck-fail
+ (match2 (list 1) with
+ [nil -> 0])
+ #:with-msg "missing clause for non-empty, arbitrary length list")
(check-type
(match2 (list 1 2) with
- [list x y -> (+ x y)]) : Int -> 3)
+ [list x y -> (+ x y)]
+ [_ -> 0]) : Int -> 3)
(check-type
(match2 (list 1 2) with
[list -> 0]
- [list x y -> (+ x y)]) : Int -> 3)
+ [list x y -> (+ x y)]
+ [_ -> -1]) : Int -> 3)
(check-type
(match2 (list (list 3 4) (list 5 6)) with
[list -> 0]
- [list (list w x) (list y z) -> (+ (+ x y) (+ z w))]) : Int -> 18)
+ [list (list w x) (list y z) -> (+ (+ x y) (+ z w))]
+ [_ -> -1]) : Int -> 18)
(check-type
(match2 (list (tup 3 4) (tup 5 6)) with
[list -> 0]
- [list (tup w x) (tup y z) -> (+ (+ x y) (+ z w))]) : Int -> 18)
+ [list (tup w x) (tup y z) -> (+ (+ x y) (+ z w))]
+ [_ -> -1]) : Int -> 18)
(check-type
(match2 (nil {Int}) with
[nil -> 0]
- [list x y -> (+ x y)]) : Int -> 0)
+ [list x y -> (+ x y)]
+ [_ -> -1]) : Int -> 0)
(check-type
(match2 (list 1 2) with
[nil -> 0]
- [list x y -> (+ x y)]) : Int -> 3)
+ [list x y -> (+ x y)]
+ [_ -> -1]) : Int -> 3)
-;; falls off, results in run-time exception
-#;(check-type
+(check-type
(match2 (list 1 2 3) with
[nil -> 0]
- [list x y -> (+ x y)]) : Int -> 3)
+ [list x y -> (+ x y)]
+ [_ -> -1]) : Int -> -1)
;; 0-arity constructors
(define-type (Test2 X)
@@ -154,11 +255,13 @@
(check-type
(match2 (list (tup 1 2) (tup 3 4) (tup 5 6)) with
- [(x,y) :: (a,b) :: rst -> (+ y a)]) : Int -> 5)
+ [(x,y) :: (a,b) :: rst -> (+ y a)]
+ [_ -> -1]) : Int -> 5)
(check-type
(match2 (list (tup (BB 1) (AA {Int})) (tup (BB 2) (AA {Int}))) with
- [((BB x),AA) :: ((BB y),AA) :: rst -> (+ y x)]) : Int -> 3)
+ [((BB x),AA) :: ((BB y),AA) :: rst -> (+ y x)]
+ [_ -> -1]) : Int -> 3)
(check-type
(match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with
@@ -171,3 +274,25 @@
(check-type
(match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with
[(((_,y),_),(_,(_,c))) -> (+ c y)]) : Int -> 9)
+
+(typecheck-fail
+ (match2 (tup (BB 1) (BB 2)) with
+ [((BB x),(BB y)) -> (+ x y)])
+ #:with-msg "clauses not exhaustive; missing: AA")
+
+;; TODO: should tail
+#;(typecheck-fail
+ (match2 (tup (BB 1) (BB 2)) with
+ [((BB x),(BB y)) -> (+ x y)]
+ [(AA,AA) -> 0])
+ #:with-msg "clauses not exhaustive; missing: AA")
+
+;; falls off; runtime match exception
+(match2 (tup (BB 2) (AA {Int})) with
+ [((BB x),(BB y)) -> (+ x y)]
+ [(AA,AA) -> 0])
+
+(check-type
+ (match2 (tup (BB 1) (BB 2)) with
+ [((BB x),(BB y)) -> (+ x y)]
+ [_ -> -1]) : Int -> 3)
