Mercurial > urweb
changeset 1306:3a845f2ce9e9
:::_ notation; switch to TooDeep error message
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 10 Oct 2010 20:33:10 -0400 (2010-10-11) |
parents | a6fc03d28170 |
children | d2ad997ca157 |
files | doc/manual.tex src/elab_err.sig src/elab_err.sml src/elaborate.sml src/urweb.grm src/urweb.lex |
diffstat | 6 files changed, 17 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/doc/manual.tex Sun Oct 10 15:54:51 2010 -0400 +++ b/doc/manual.tex Sun Oct 10 20:33:10 2010 -0400 @@ -495,7 +495,7 @@ 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^+$. -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. +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/elab_err.sig Sun Oct 10 15:54:51 2010 -0400 +++ b/src/elab_err.sig Sun Oct 10 20:33:10 2010 -0400 @@ -58,6 +58,7 @@ | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con) option | TooLifty of ErrorMsg.span * ErrorMsg.span | TooUnify of Elab.con * Elab.con + | TooDeep val cunifyError : ElabEnv.env -> cunify_error -> unit
--- a/src/elab_err.sml Sun Oct 10 15:54:51 2010 -0400 +++ b/src/elab_err.sml Sun Oct 10 20:33:10 2010 -0400 @@ -121,6 +121,7 @@ | CRecordFailure of con * con * (con * con * con) option | TooLifty of ErrorMsg.span * ErrorMsg.span | TooUnify of con * con + | TooDeep fun cunifyError env err = case err of @@ -162,6 +163,7 @@ (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable"; eprefaces' [("Replacement", p_con env c1), ("Body", p_con env c2)]) + | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting" datatype exp_error = UnboundExp of ErrorMsg.span * string
--- a/src/elaborate.sml Sun Oct 10 15:54:51 2010 -0400 +++ b/src/elaborate.sml Sun Oct 10 20:33:10 2010 -0400 @@ -1079,13 +1079,13 @@ err COccursCheckFailed else (r := SOME (squish nl c2All) - handle CantSquish => err CIncompatible) + handle CantSquish => err (fn _ => TooDeep)) | (_, L'.CUnif (nl, _, _, _, r)) => if occursCon r c1All then err COccursCheckFailed else (r := SOME (squish nl c1All) - handle CantSquish => err CIncompatible) + handle CantSquish => err (fn _ => TooDeep)) | (L'.CUnit, L'.CUnit) => ()
--- a/src/urweb.grm Sun Oct 10 15:54:51 2010 -0400 +++ b/src/urweb.grm Sun Oct 10 20:33:10 2010 -0400 @@ -212,7 +212,7 @@ | STRING of string | INT of Int64.int | FLOAT of Real64.real | CHAR of char | SYMBOL of string | CSYMBOL of string | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE - | EQ | COMMA | COLON | DCOLON | DCOLONWILD | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR + | EQ | COMMA | COLON | DCOLON | DCOLONWILD | TCOLON | TCOLONWILD | DOT | HASH | UNDER | UNDERUNDER | BAR | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS | DATATYPE | OF @@ -394,7 +394,7 @@ %left ANDALSO %left ORELSE %nonassoc COLON -%nonassoc DCOLON TCOLON +%nonassoc DCOLON TCOLON DCOLONWILD TCOLONWILD %left UNION INTERSECT EXCEPT %right COMMA %right JOIN INNER CROSS OUTER LEFT RIGHT FULL @@ -1111,6 +1111,14 @@ ((ECAbs (kcolon, SYMBOL, kind, e), loc), (TCFun (kcolon, SYMBOL, kind, t), loc)) end) + | LBRACK SYMBOL TCOLONWILD RBRACK (fn (e, t) => + let + val loc = s (LBRACKleft, RBRACKright) + val kind = (KWild, loc) + in + ((ECAbs (Implicit, SYMBOL, kind, e), loc), + (TCFun (Implicit, SYMBOL, kind, t), loc)) + end) | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) => let val loc = s (LBRACKleft, RBRACKright)
--- a/src/urweb.lex Sun Oct 10 15:54:51 2010 -0400 +++ b/src/urweb.lex Sun Oct 10 20:33:10 2010 -0400 @@ -371,6 +371,7 @@ <INITIAL> "<=" => (Tokens.LE (pos yypos, pos yypos + size yytext)); <INITIAL> ">=" => (Tokens.GE (pos yypos, pos yypos + size yytext)); <INITIAL> "," => (Tokens.COMMA (pos yypos, pos yypos + size yytext)); +<INITIAL> ":::_" => (Tokens.TCOLONWILD (pos yypos, pos yypos + size yytext)); <INITIAL> ":::" => (Tokens.TCOLON (pos yypos, pos yypos + size yytext)); <INITIAL> "::_" => (Tokens.DCOLONWILD (pos yypos, pos yypos + size yytext)); <INITIAL> "::" => (Tokens.DCOLON (pos yypos, pos yypos + size yytext));