summaryrefslogtreecommitdiff
path: root/src/urweb.grm
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-10-20 10:19:00 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-10-20 10:19:00 -0400
commiteafb2bfc151efd5fe9a18dd5bba14141a1b832cf (patch)
tree800ab89ca52c3ef6e7df0f9420292131459f0e47 /src/urweb.grm
parent64783736b3c002c095640c0bf16b48994a44869c (diff)
Add tuple pattern-matching at the constructor level
Diffstat (limited to 'src/urweb.grm')
-rw-r--r--src/urweb.grm29
1 files changed, 26 insertions, 3 deletions
diff --git a/src/urweb.grm b/src/urweb.grm
index edd93d96..38d7d60d 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -242,6 +242,8 @@ fun patType loc (p : pat) =
| 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 @@ cargp : SYMBOL (fn (c, k) =>
((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)