Mercurial > urweb
changeset 762:9021d44ba6b2
List notations
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 30 Apr 2009 15:10:13 -0400 |
| parents | 16b34dc2e29c |
| children | af41ec2f302a |
| files | src/urweb.grm tests/list.ur |
| diffstat | 2 files changed, 28 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/src/urweb.grm Thu Apr 30 14:48:23 2009 -0400 +++ b/src/urweb.grm Thu Apr 30 15:10:13 2009 -0400 @@ -933,6 +933,16 @@ | eexp CARET eexp (native_op ("strcat", eexp1, eexp2, s (eexp1left, eexp2right))) + | eterm DCOLON eexp (let + val loc = s (etermleft, eexpright) + in + (EApp ((EVar (["Basis"], "Cons", Infer), loc), + (ERecord [((CName "1", loc), + eterm), + ((CName "2", loc), + eexp)], loc)), loc) + end) + bind : SYMBOL LARROW eapps (SYMBOL, NONE, eapps) | UNIT LARROW eapps (let val loc = s (UNITleft, eappsright) @@ -1161,6 +1171,8 @@ | LET edecls IN eexp END (ELet (edecls, eexp), s (LETleft, ENDright)) + | LBRACK RBRACK (EVar (["Basis"], "Nil", Infer), s (LBRACKleft, RBRACKright)) + edecls : ([]) | edecl edecls (edecl :: edecls) @@ -1196,6 +1208,13 @@ pat : pterm (pterm) | cpath pterm (PCon (#1 cpath, #2 cpath, SOME pterm), s (cpathleft, ptermright)) + | pterm DCOLON pat (let + val loc = s (ptermleft, patright) + in + (PCon (["Basis"], "Cons", SOME (PRecord ([("1", pterm), + ("2", pat)], false), loc)), + loc) + end) pterm : SYMBOL (PVar SYMBOL, s (SYMBOLleft, SYMBOLright)) | cpath (PCon (#1 cpath, #2 cpath, NONE), s (cpathleft, cpathright)) @@ -1209,6 +1228,7 @@ | LPAREN ptuple RPAREN (PRecord (ListUtil.mapi (fn (i, p) => (Int.toString (i + 1), p)) ptuple, false), s (LPARENleft, RPARENright)) + | LBRACK RBRACK (PCon (["Basis"], "Nil", NONE), s (LBRACKleft, RBRACKright)) rpat : CSYMBOL EQ pat ([(CSYMBOL, pat)], false) | INT EQ pat ([(Int64.toString INT, pat)], false)
--- a/tests/list.ur Thu Apr 30 14:48:23 2009 -0400 +++ b/tests/list.ur Thu Apr 30 15:10:13 2009 -0400 @@ -1,22 +1,22 @@ fun isNil (t ::: Type) (ls : list t) = case ls of - Nil => True + [] => True | _ => False fun delist (ls : list string) : xbody = case ls of - Nil => <xml>Nil</xml> - | Cons (h, t) => <xml>{[h]} :: {delist t}</xml> + [] => <xml>Nil</xml> + | h :: t => <xml>{[h]} :: {delist t}</xml> fun callback ls = return <xml><body> {delist ls} </body></xml> fun main () = return <xml><body> - {[isNil (Nil : list bool)]}, - {[isNil (Cons (1, Nil))]}, - {[isNil (Cons ("A", Cons ("B", Nil)))]} + {[isNil ([] : list bool)]}, + {[isNil (1 :: [])]}, + {[isNil ("A" :: "B" :: [])]} - <p>{delist (Cons ("X", Cons ("Y", Cons ("Z", Nil))))}</p> - <a link={callback (Cons ("A", Cons ("B", Nil)))}>Go!</a> + <p>{delist ("X" :: "Y" :: "Z" :: [])}</p> + <a link={callback ("A" :: "B" :: [])}>Go!</a> </body></xml>