comparison src/urweb.grm @ 1302:d008c4c43a0a

Flex kinds for type-level tuples; ::_ notation
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 13:07:38 -0400
parents e8d68fd8ed4b
children 3a845f2ce9e9
comparison
equal deleted inserted replaced
1301:4359e185d3af 1302:d008c4c43a0a
210 %term 210 %term
211 EOF 211 EOF
212 | STRING of string | INT of Int64.int | FLOAT of Real64.real | CHAR of char 212 | STRING of string | INT of Int64.int | FLOAT of Real64.real | CHAR of char
213 | SYMBOL of string | CSYMBOL of string 213 | SYMBOL of string | CSYMBOL of string
214 | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE 214 | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
215 | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR 215 | EQ | COMMA | COLON | DCOLON | DCOLONWILD | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
216 | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT 216 | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT
217 | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS 217 | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS
218 | DATATYPE | OF 218 | DATATYPE | OF
219 | TYPE | NAME 219 | TYPE | NAME
220 | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW | BANG 220 | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW | BANG
508 dtypes : dtype ([dtype]) 508 dtypes : dtype ([dtype])
509 | dtype AND dtypes (dtype :: dtypes) 509 | dtype AND dtypes (dtype :: dtypes)
510 510
511 kopt : (NONE) 511 kopt : (NONE)
512 | DCOLON kind (SOME kind) 512 | DCOLON kind (SOME kind)
513 | DCOLONWILD (SOME (KWild, s (DCOLONWILDleft, DCOLONWILDright)))
513 514
514 dargs : ([]) 515 dargs : ([])
515 | SYMBOL dargs (SYMBOL :: dargs) 516 | SYMBOL dargs (SYMBOL :: dargs)
516 517
517 barOpt : () 518 barOpt : ()
849 | UNDER DCOLON kind (fn (c, k) => 850 | UNDER DCOLON kind (fn (c, k) =>
850 let 851 let
851 val loc = s (UNDERleft, kindright) 852 val loc = s (UNDERleft, kindright)
852 in 853 in
853 ((CAbs ("_", SOME kind, c), loc), 854 ((CAbs ("_", SOME kind, c), loc),
855 (KArrow (kind, k), loc))
856 end)
857 | SYMBOL DCOLONWILD (fn (c, k) =>
858 let
859 val loc = s (SYMBOLleft, DCOLONWILDright)
860 val kind = (KWild, loc)
861 in
862 ((CAbs (SYMBOL, NONE, c), loc),
863 (KArrow (kind, k), loc))
864 end)
865 | UNDER DCOLONWILD (fn (c, k) =>
866 let
867 val loc = s (UNDERleft, DCOLONWILDright)
868 val kind = (KWild, loc)
869 in
870 ((CAbs ("_", NONE, c), loc),
854 (KArrow (kind, k), loc)) 871 (KArrow (kind, k), loc))
855 end) 872 end)
856 | cargp (cargp) 873 | cargp (cargp)
857 874
858 cargp : SYMBOL (fn (c, k) => 875 cargp : SYMBOL (fn (c, k) =>
1077 val kind = (KWild, loc) 1094 val kind = (KWild, loc)
1078 in 1095 in
1079 ((ECAbs (Implicit, SYMBOL, kind, e), loc), 1096 ((ECAbs (Implicit, SYMBOL, kind, e), loc),
1080 (TCFun (Implicit, SYMBOL, kind, t), loc)) 1097 (TCFun (Implicit, SYMBOL, kind, t), loc))
1081 end) 1098 end)
1099 | LBRACK SYMBOL DCOLONWILD RBRACK (fn (e, t) =>
1100 let
1101 val loc = s (LBRACKleft, RBRACKright)
1102 val kind = (KWild, loc)
1103 in
1104 ((ECAbs (Explicit, SYMBOL, kind, e), loc),
1105 (TCFun (Explicit, SYMBOL, kind, t), loc))
1106 end)
1082 | LBRACK SYMBOL kcolon kind RBRACK(fn (e, t) => 1107 | LBRACK SYMBOL kcolon kind RBRACK(fn (e, t) =>
1083 let 1108 let
1084 val loc = s (LBRACKleft, RBRACKright) 1109 val loc = s (LBRACKleft, RBRACKright)
1085 in 1110 in
1086 ((ECAbs (kcolon, SYMBOL, kind, e), loc), 1111 ((ECAbs (kcolon, SYMBOL, kind, e), loc),