commit d881d988c2d6189a9b32dd2725beaab156a455c8
parent fca145bbd74db307a3d4f7334cc7a96dfb71e13c
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 30 Mar 2016 13:51:22 -0400
fix and enhance match2
- compiles to racket match patterns (but still typechecks)
- supports nested patterns
- no exhastiveness checking
- no parens required for root pattern
(except for comma tup stx)
- support _ else case
- always no parens for 0-arity constructors
- both user-defined and built-in (like nil)
- alternative :: cons stx
- alternative comma --- (x,y,z) --- tuple stx
- requires at least 1 comma to detect
- see examples in match2.mlish
Diffstat:
3 files changed, 194 insertions(+), 21 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -307,17 +307,50 @@
(unify-pat+ty (list pat ty)))
(define (unify-pat+ty pat+ty)
(syntax-parse pat+ty
+ [(pat ty) #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens)
+ (syntax-parse #'pat
+ [{(~datum _)} #'()]
+ [{(~literal stlc+cons:nil)} #'()]
+ [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
+ #:with ((~literal #%plain-lambda) (RecName)
+ ((~literal let-values) ()
+ ((~literal let-values) ()
+ . info-body)))
+ (get-extra-info #'ty)
+ #'()]
+ ;; comma tup syntax always has parens
+; [{(~and ps (p1 ((~literal unquote) p2) ((~literal unquote) p) ...))}
+ [{(~and ps (p1 (unq p) ...))}
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ (unify-pat+ty #'(ps ty))]
+ [{p ...}
+ (unify-pat+ty #'((p ...) ty))])] ; pair
[((~datum _) ty) #'()]
- [(~literal stlc+cons:nil) ; nil
+ [((~or (~literal stlc+cons:nil)) ty) #'()]
+ [(A:id ty) ; disambiguate 0-arity constructors (that don't need parens)
+ #:with ((~literal #%plain-lambda) (RecName)
+ ((~literal let-values) ()
+ ((~literal let-values) ()
+ . info-body)))
+ (get-extra-info #'ty)
#'()]
- [(x:id ty)
- #'((x ty))]
+ [(x:id ty) #'((x ty))]
+ [((p1 (unq p) ...) ty) ; comma tup stx
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ #:with (~× t ...) #'ty
+ #:with (pp ...) #'(p1 p ...)
+ (unifys #'([pp t] ...))]
[(((~literal stlc+tup:tup) p ...) ty) ; tup
#:with (~× t ...) #'ty
(unifys #'([p t] ...))]
[(((~literal stlc+cons:list) p ...) ty) ; known length list
#:with (~List t) #'ty
(unifys #'([p t] ...))]
+ [(((~seq p (~datum ::)) ... rst) ty) ; nicer cons stx
+ #:with (~List t) #'ty
+ (unifys #'([p t] ... [rst ty]))]
[(((~literal stlc+cons:cons) p ps) ty) ; arb length list
#:with (~List t) #'ty
(unifys #'([p t] [ps ty]))]
@@ -341,10 +374,42 @@
(define (compile-pat p ty)
(syntax-parse p
+ [pat #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens)
+ (syntax-parse #'pat
+ [{(~datum _)} #'_]
+ [{(~literal stlc+cons:nil)} #'(list)]
+ [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
+ #:with ((~literal #%plain-lambda) (RecName)
+ ((~literal let-values) ()
+ ((~literal let-values) ()
+ . info-body)))
+ (get-extra-info ty)
+ (compile-pat #'(A) ty)]
+ ;; comma tup stx always has parens
+ ;; comma tup syntax always has parens
+; [{(~and ps (p1 ((~literal unquote) p2) ((~literal unquote) p) ...))}
+ [{(~and ps (p1 (unq p) ...))}
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ (compile-pat #'ps ty)]
+ [{p ...} (compile-pat #'(p ...) ty)])]
[(~datum _) #'_]
[(~literal stlc+cons:nil) ; nil
#'(list)]
+ [A:id ; disambiguate 0-arity constructors (that don't need parens)
+ #:with ((~literal #%plain-lambda) (RecName)
+ ((~literal let-values) ()
+ ((~literal let-values) ()
+ . info-body)))
+ (get-extra-info ty)
+ (compile-pat #'(A) ty)]
[x:id p]
+ [(p1 (unq p) ...) ; comma tup stx
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ #: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 ...))
@@ -353,6 +418,11 @@
#: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 (~List t) ty
+ #:with (p- ...) (stx-map (lambda (pp) (compile-pat pp #'t)) #'(p ...))
+ #:with ps- (compile-pat #'rst ty)
+ #'(list-rest p- ... ps-)]
[((~literal stlc+cons:cons) p ps)
#:with (~List t) ty
#:with p- (compile-pat #'p #'t)
@@ -383,7 +453,8 @@
#:fail-when (null? (syntax->list #'clauses)) "no clauses"
#:with [e- τ_e] (infer+erase #'e)
(syntax-parse #'clauses #:datum-literals (->)
- [([pat -> e_body] ...)
+ [([(~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 ([(x- ...) e_body- ty_body] ...) (stx-map infer/ctx+erase #'(ctx ...) #'(e_body ...))
#:with (pat- ...) (stx-map (lambda (p) (compile-pat p #'τ_e)) #'(pat ...))
diff --git a/tapl/tests/mlish/match2.mlish b/tapl/tests/mlish/match2.mlish
@@ -10,32 +10,32 @@
(check-type
(match2 (B (tup 2 3)) with
- [(B x) -> x]) : (× Int Int) -> (list 2 3))
+ [B x -> x]) : (× Int Int) -> (list 2 3))
(check-type
(match2 (A (tup 2 3)) with
- [(A x) -> x]) : (× Int Int) -> (list 2 3))
+ [A x -> x]) : (× Int Int) -> (list 2 3))
(check-type
(match2 (A 1) with
- [(A x) -> x]) : Int -> 1)
+ [A x -> x]) : Int -> 1)
(typecheck-fail
(match2 (B 1) with
- [(B x) -> x])
+ [B x -> x])
#:with-msg "Could not infer instantiation of polymorphic function B")
(check-type
(match2 (B (tup 2 3)) with
- [(B (tup x y)) -> (+ x y)]) : Int -> 5)
+ [B (tup x y) -> (+ x y)]) : 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))]) : Int -> 9)
(check-type
(match2 (C (tup 2 (tup 3 4))) with
- [(A x) -> x]
+ [A x -> x]
[_ -> 100]) : Int -> 100)
@@ -44,28 +44,129 @@
(check-type
(match2 (list 1) with
- [(list x) -> x]) : Int -> 1)
+ [list x -> x]) : Int -> 1)
(check-type
(match2 (list 1 2) with
- [(list x y) -> (+ x y)]) : Int -> 3)
+ [list x y -> (+ x y)]) : Int -> 3)
(check-type
(match2 (list 1 2) with
- [(list) -> 0]
- [(list x y) -> (+ x y)]) : Int -> 3)
+ [list -> 0]
+ [list x y -> (+ x y)]) : 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 -> 0]
+ [list (list w x) (list y z) -> (+ (+ x y) (+ z w))]) : 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 -> 0]
+ [list (tup w x) (tup y z) -> (+ (+ x y) (+ z w))]) : Int -> 18)
-#;(check-type
+(check-type
(match2 (nil {Int}) with
[nil -> 0]
- [(list x y) -> (+ x y)]) : Int -> 0)
+ [list x y -> (+ x y)]) : Int -> 0)
+
+(check-type
+ (match2 (list 1 2) with
+ [nil -> 0]
+ [list x y -> (+ x y)]) : Int -> 3)
+
+;; falls off, results in run-time exception
+#;(check-type
+ (match2 (list 1 2 3) with
+ [nil -> 0]
+ [list x y -> (+ x y)]) : Int -> 3)
+
+;; 0-arity constructors
+(define-type (Test2 X)
+ AA
+ (BB X))
+
+(check-type
+ (match2 (BB 1) with
+ [AA -> 0]
+ [BB x -> x]) : Int -> 1)
+
+(check-type
+ (match2 (BB (AA {Int})) with
+ [AA -> 0]
+ [BB AA -> 1]
+ [_ -> 2]) : Int -> 1)
+
+;; drop parens around 0-arity constructors
+(check-type
+ (match2 (BB 1) with
+ [AA -> 0]
+ [BB x -> x]) : Int -> 1)
+
+(check-type
+ (match2 (BB (AA {Int})) with
+ [AA -> 0]
+ [BB AA -> 1]
+ [_ -> 2]) : Int -> 1)
+
+;; nicer cons pattern syntax (::)
+(check-type
+ (match2 (list 1 2) with
+ [nil -> -1]
+ [x :: xs -> x]) : Int -> 1)
+
+(check-type
+ (match2 (list 1 2) with
+ [nil -> -1]
+ [x :: y :: xs -> y]) : Int -> 2)
+
+(check-type
+ (match2 (list (tup 1 2) (tup 3 4)) with
+ [nil -> -1]
+ [(tup x y) :: (tup a b) :: xs -> (+ a b)]) : Int -> 7)
+
+(check-type
+ (match2 (list (list 2 3 4) (list 5 6 7) (list 9 10)) with
+ [nil -> -1]
+ [x :: (y :: z :: zs) :: xs -> z]) : Int -> 6)
+
+(check-type
+ (match2 (list (list 2 3 4) (list 5 6 7) (list 9 10)) with
+ [nil -> -1]
+ [x :: (list a b c) :: xs -> c]) : Int -> 7)
+
+(typecheck-fail
+ (match2 (list (list #t #f)) with
+ [nil -> -1]
+ [(list x y) :: tl -> (+ x y)])
+ #:with-msg "Type error applying function \\+")
+
+;; comma tup pattern syntax
+
+(check-type
+ (match2 (tup 1 2) with
+ [(x,y) -> (+ x y)]) : Int -> 3)
+
+(check-type
+ (match2 (tup 1 2 4) with
+ [(_,y,z) -> (+ z y)]) : Int -> 6)
+
+(check-type
+ (match2 (list (tup 1 2) (tup 3 4) (tup 5 6)) with
+ [(x,y) :: (a,b) :: rst -> (+ y a)]) : 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)
+
+(check-type
+ (match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with
+ [(((x,y),z),(a,(b,c))) -> (+ c y)]) : Int -> 9)
+
+(check-type
+ (match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with
+ [(((x,y),z),(_,(_,c))) -> (+ c y)]) : Int -> 9)
+
+(check-type
+ (match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with
+ [(((_,y),_),(_,(_,c))) -> (+ c y)]) : Int -> 9)
diff --git a/tapl/tests/run-mlish-tests1.rkt b/tapl/tests/run-mlish-tests1.rkt
@@ -2,6 +2,7 @@
(require "mlish-tests.rkt")
(require "mlish/queens.mlish")
(require "mlish/listpats.mlish")
+(require "mlish/match2.mlish")
;; (require "mlish/trees.mlish")
;; (require "mlish/chameneos.mlish")
