From d881d988c2d6189a9b32dd2725beaab156a455c8 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 30 Mar 2016 13:51:22 -0400
Subject: [PATCH] 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
---
 tapl/mlish.rkt                  |  79 ++++++++++++++++++-
 tapl/tests/mlish/match2.mlish   | 135 ++++++++++++++++++++++++++++----
 tapl/tests/run-mlish-tests1.rkt |   1 +
 3 files changed, 194 insertions(+), 21 deletions(-)

diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
index 4678584..8aafbb0 100644
--- 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
index 95b830c..bfd6398 100644
--- 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
index b06448d..c768ab2 100644
--- 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")