From 87314013187ad8c4a65d24ede5787c1581dfd70a Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 1 Apr 2016 17:08:48 -0400 Subject: [PATCH] start match2 exhaustiveness checking; nested checks not quite working --- tapl/mlish.rkt | 113 ++++++++++++++++++++---- tapl/stx-utils.rkt | 2 + tapl/tests/mlish/match2.mlish | 157 ++++++++++++++++++++++++++++++---- 3 files changed, 237 insertions(+), 35 deletions(-) diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt index dee74df..61fdcb8 100644 --- 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 index 6ac5b3a..c9f2aa0 100644 --- 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 index eba59c0..ead36dd 100644 --- 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 1) with - [A x -> x]) : Int -> 1) + (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] + [_ -> -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)