From e42ea5dbeb92bf49da6a73962c9f44a86fa989c2 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Thu, 28 Aug 2008 13:29:57 -0400
Subject: Shorthand for multi-binding con 'fn'

---
 src/lacweb.grm   | 50 ++++++++++++++++++++++++++++++++++++++++++++++++--
 tests/cargs.lac  |  7 +++++++
 tests/recBad.lac |  2 +-
 3 files changed, 56 insertions(+), 3 deletions(-)
 create mode 100644 tests/cargs.lac

diff --git a/src/lacweb.grm b/src/lacweb.grm
index df01558e..822cba8c 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -209,6 +209,10 @@ fun sql_relop (oper, sqlexp1, sqlexp2, loc) =
  | rcon of (con * con) list
  | rconn of (con * con) list
  | rcone of (con * con) list
+ | cargs of con * kind -> con * kind
+ | cargl of con * kind -> con * kind
+ | carg of con * kind -> con * kind
+ | cargp of con * kind -> con * kind
 
  | eexp of exp
  | eapps of exp
@@ -435,8 +439,7 @@ cexp   : capps                          (capps)
 
        | cexp PLUSPLUS cexp             (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))
 
-       | FN SYMBOL DARROW cexp          (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright))
-       | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright))
+       | FN cargs DARROW cexp           (#1 (cargs (cexp, (KWild, s (FNleft, cexpright)))))
        | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
        | cterm TWIDDLE cterm ARROW cexp (TDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
 
@@ -455,6 +458,49 @@ cexp   : capps                          (capps)
 kcolon : DCOLON                         (Explicit)
        | TCOLON                         (Implicit)
 
+cargs  : carg                           (carg)
+       | cargl                          (cargl)
+
+cargl  : cargp cargp                    (cargp1 o cargp2)
+       | cargp cargl                    (cargp o cargl)
+
+carg   : SYMBOL                         (fn (c, k) =>
+                                            let
+                                                val loc = s (SYMBOLleft, SYMBOLright)
+                                            in
+                                                ((CAbs (SYMBOL, NONE, c), loc),
+                                                 (KArrow ((KWild, loc), k), loc))
+                                            end)
+       | SYMBOL DCOLON kind             (fn (c, k) =>
+                                            let
+                                                val loc = s (SYMBOLleft, kindright)
+                                            in
+                                                ((CAbs (SYMBOL, SOME kind, c), loc),
+                                                 (KArrow (kind, k), loc))
+                                            end)
+       | LPAREN SYMBOL DCOLON kind RPAREN (fn (c, k) =>
+                                              let
+                                                  val loc = s (LPARENleft, RPARENright)
+                                              in
+                                                  ((CAbs (SYMBOL, SOME kind, c), loc),
+                                                   (KArrow (kind, k), loc))
+                                              end)
+
+cargp  : SYMBOL                         (fn (c, k) =>
+                                            let
+                                                val loc = s (SYMBOLleft, SYMBOLright)
+                                            in
+                                                ((CAbs (SYMBOL, NONE, c), loc),
+                                                 (KArrow ((KWild, loc), k), loc))
+                                            end)
+       | LPAREN SYMBOL DCOLON kind RPAREN (fn (c, k) =>
+                                              let
+                                                  val loc = s (LPARENleft, RPARENright)
+                                              in
+                                                  ((CAbs (SYMBOL, SOME kind, c), loc),
+                                                   (KArrow (kind, k), loc))
+                                              end)
+
 path   : SYMBOL                         ([], SYMBOL)
        | CSYMBOL DOT path               (let val (ms, x) = path in (CSYMBOL :: ms, x) end)
 
diff --git a/tests/cargs.lac b/tests/cargs.lac
new file mode 100644
index 00000000..4aba9860
--- /dev/null
+++ b/tests/cargs.lac
@@ -0,0 +1,7 @@
+con id = fn t :: Type => t
+con id2 = fn (t :: Type) => id t
+con id3 = fn t => id2 t
+
+con pair = fn (t :: Type) (u :: Type) => (t, u)
+con pair2 = fn t u => pair t u
+con pair3 = fn t (u :: Type) => pair2 t u
diff --git a/tests/recBad.lac b/tests/recBad.lac
index bfff8daf..8d844efb 100644
--- a/tests/recBad.lac
+++ b/tests/recBad.lac
@@ -6,4 +6,4 @@ val rec append : t ::: Type -> list t -> list t -> list t = fn t ::: Type => fn
           | Cons (h, t) => Cons (h, append t ls2)
 
 (*val rec ones : list int = Cons (1, ones)*)
-val rec ones : unit -> list int = fn () => Cons (1, ones ())
+val rec ones = fn () => Cons (1, ones ())
-- 
cgit v1.2.3