Mercurial > urweb
changeset 1574:644558d9c756
Extend and document 'con' syntax with arguments
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 15 Oct 2011 10:05:13 -0400 |
| parents | 34364e383bed |
| children | 287604b4a08d |
| files | doc/manual.tex src/urweb.grm tests/conargs.ur |
| diffstat | 3 files changed, 20 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/doc/manual.tex Sat Oct 15 09:04:41 2011 -0400 +++ b/doc/manual.tex Sat Oct 15 10:05:13 2011 -0400 @@ -380,7 +380,7 @@ &&& \{\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 @@ 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.
--- a/src/urweb.grm Sat Oct 15 09:04:41 2011 -0400 +++ b/src/urweb.grm Sat Oct 15 10:05:13 2011 -0400 @@ -706,8 +706,14 @@ 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)))