changeset 240:7036d29574f2

Shorthand for multi-binding con declaration
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 Aug 2008 13:39:20 -0400
parents fc6f04889bf2
children 052126db06e7
files src/lacweb.grm tests/cargs.lac
diffstat 2 files changed, 23 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/lacweb.grm	Thu Aug 28 13:29:57 2008 -0400
+++ b/src/lacweb.grm	Thu Aug 28 13:39:20 2008 -0400
@@ -193,6 +193,7 @@
  | kind of kind
  | ktuple of kind list
  | kcolon of explicitness
+ | kopt of kind option
 
  | path of string list * string
  | cpath of string list * string
@@ -211,6 +212,7 @@
  | rcone of (con * con) list
  | cargs of con * kind -> con * kind
  | cargl of con * kind -> con * kind
+ | cargl2 of con * kind -> con * kind
  | carg of con * kind -> con * kind
  | cargp of con * kind -> con * kind
 
@@ -295,8 +297,14 @@
 decls  :                                ([])
        | decl decls                     (decl :: decls)
 
-decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft, cexpright))
-       | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
+decl   : CON SYMBOL cargl2 kopt EQ cexp (let
+                                             val loc = s (CONleft, cexpright)
+
+                                             val k = Option.getOpt (kopt, (KWild, loc))
+                                             val (c, k) = cargl2 (cexp, k)
+                                         in
+                                             (DCon (SYMBOL, SOME k, c), loc)
+                                         end)
        | LTYPE SYMBOL EQ cexp           (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                          s (LTYPEleft, cexpright))
        | DATATYPE SYMBOL dargs EQ barOpt dcons(DDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))
@@ -337,6 +345,9 @@
                                              (DClass (SYMBOL1, c), s (CLASSleft, cexpright))
                                          end)
 
+kopt   :                                (NONE)
+       | DCOLON kind                    (SOME kind)
+
 dargs  :                                ([])
        | SYMBOL dargs                   (SYMBOL :: dargs)
 
@@ -464,6 +475,9 @@
 cargl  : cargp cargp                    (cargp1 o cargp2)
        | cargp cargl                    (cargp o cargl)
 
+cargl2 :                                (fn x => x)
+       | cargp cargl2                   (cargp o cargl2)
+
 carg   : SYMBOL                         (fn (c, k) =>
                                             let
                                                 val loc = s (SYMBOLleft, SYMBOLright)
--- a/tests/cargs.lac	Thu Aug 28 13:29:57 2008 -0400
+++ b/tests/cargs.lac	Thu Aug 28 13:39:20 2008 -0400
@@ -5,3 +5,10 @@
 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
+
+con id4 (t :: Type) = t
+con id5 (t :: Type) :: Type = id4 t
+con id6 t :: Type = id5 t
+
+con pair4 t (u :: Type) = pair3 t u
+con pair5 t (u :: Type) :: (Type * Type) = pair4 t u