From 40047b604b23d8342f9f3d499bacff2d78b88749 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 15 Oct 2011 10:05:13 -0400
Subject: Extend and document 'con' syntax with arguments

---
 doc/manual.tex   |  4 +++-
 src/urweb.grm    | 10 ++++++++--
 tests/conargs.ur |  9 +++++++++
 3 files changed, 20 insertions(+), 3 deletions(-)
 create mode 100644 tests/conargs.ur

diff --git a/doc/manual.tex b/doc/manual.tex
index 2c1cecc2..541dd96b 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -380,7 +380,7 @@ $$\begin{array}{rrcll}
   &&& \{\kappa\} & \textrm{type-level records} \\
   &&& (\kappa\times^+) & \textrm{type-level tuples} \\
   &&& X & \textrm{variable} \\
-  &&& X \longrightarrow k & \textrm{kind-polymorphic type-level function} \\
+  &&& X \longrightarrow \kappa & \textrm{kind-polymorphic type-level function} \\
   &&& \_\_ & \textrm{wildcard} \\
   &&& (\kappa) & \textrm{explicit precedence} \\
 \end{array}$$
@@ -549,6 +549,8 @@ A tuple type $\tau_1 \times \ldots \times \tau_n$ expands to a record type $\{1
 
 In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards.  More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid X$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$.
 
+Further, the signature item or declaration syntax $\mt{con} \; x \; b^+ = c$ is shorthand for wrapping of the appropriate $\lambda$s around the righthand side $c$.  The $b$ elements may not include $X$, and there may also be an optional $:: \kappa$ before the $=$.
+
 In some contexts, the parser isn't happy with token sequences like $x :: \_$, to indicate a constructor variable of wildcard kind.  In such cases, write the second two tokens as $::\hspace{-.05in}\_$, with no intervening spaces.  Analogous syntax $:::\hspace{-.05in}\_$ is available for implicit constructor arguments.
 
 For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard.
diff --git a/src/urweb.grm b/src/urweb.grm
index d39fbe55..65264cdf 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -706,8 +706,14 @@ sgntm  : SIG sgis END                   (SgnConst sgis, s (SIGleft, ENDright))
 sgi    : CON SYMBOL DCOLON kind         ((SgiConAbs (SYMBOL, kind), s (CONleft, kindright)))
        | LTYPE SYMBOL                   ((SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))),
                                           s (LTYPEleft, SYMBOLright)))
-       | CON SYMBOL EQ cexp             ((SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright)))
-       | CON SYMBOL DCOLON kind EQ cexp ((SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)))
+       | 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
+                                             (SgiCon (SYMBOL, SOME k, c), loc)
+                                         end)
        | LTYPE SYMBOL EQ cexp           ((SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                           s (LTYPEleft, cexpright)))
        | DATATYPE dtypes                ((SgiDatatype dtypes, s (DATATYPEleft, dtypesright)))
diff --git a/tests/conargs.ur b/tests/conargs.ur
new file mode 100644
index 00000000..310e1246
--- /dev/null
+++ b/tests/conargs.ur
@@ -0,0 +1,9 @@
+con func a b = a -> b
+
+signature S = sig
+    con funcy a b = a -> b
+end
+
+structure M : S = struct
+    con funcy = func
+end
-- 
cgit v1.2.3