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>