diff src/urweb.grm @ 1001:1d456a06ea4e

Add tuple pattern-matching at the constructor level
author Adam Chlipala <adamc@hcoop.net>
date Tue, 20 Oct 2009 10:19:00 -0400
parents 10114d7b7477
children 36efaf119b85
line wrap: on
line diff
--- a/src/urweb.grm	Thu Oct 15 14:27:38 2009 -0400
+++ b/src/urweb.grm	Tue Oct 20 10:19:00 2009 -0400
@@ -242,6 +242,8 @@
  | csts of exp
  | cstopt of exp
 
+ | ckl of (string * kind option) list
+
  | pmode of prop_kind * exp
  | pkind of prop_kind
  | prule of exp
@@ -847,14 +849,35 @@
                                                 ((CAbs ("_", NONE, c), loc),
                                                  (KArrow ((KWild, loc), k), loc))
                                             end)
-       | LPAREN SYMBOL DCOLON kind RPAREN (fn (c, k) =>
+       | LPAREN SYMBOL kopt ckl RPAREN (fn (c, k) =>
                                               let
                                                   val loc = s (LPARENleft, RPARENright)
+                                                  val ckl = (SYMBOL, kopt) :: ckl
+                                                  val ckl = map (fn (x, ko) => (x, case ko of
+                                                                                       NONE => (KWild, loc)
+                                                                                     | SOME k => k)) ckl
                                               in
-                                                  ((CAbs (SYMBOL, SOME kind, c), loc),
-                                                   (KArrow (kind, k), loc))
+                                                  case ckl of
+                                                      [(x, k')] => ((CAbs (SYMBOL, SOME k', c), loc),
+                                                                    (KArrow (k', k), loc))
+                                                    | _ =>
+                                                      let
+                                                          val k' = (KTuple (map #2 ckl), loc)
+
+                                                          val c = foldr (fn ((x, k), c) =>
+                                                                            (CAbs (x, SOME k, c), loc)) c ckl
+                                                          val v = (CVar ([], "$x"), loc)
+                                                          val c = ListUtil.foldli (fn (i, _, c) =>
+                                                                                      (CApp (c, (CProj (v, i + 1), loc)),
+                                                                                       loc)) c ckl
+                                                      in
+                                                          ((CAbs ("$x", SOME k', c), loc),
+                                                           (KArrow (k', k), loc))
+                                                      end
                                               end)
 
+ckl    :                                ([])
+       | COMMA SYMBOL kopt ckl          ((SYMBOL, kopt) :: ckl)
 
 path   : SYMBOL                         ([], SYMBOL)
        | CSYMBOL DOT path               (let val (ms, x) = path in (CSYMBOL :: ms, x) end)