changeset 173:8221b95cc24c

Patterns for int and string constants
author Adam Chlipala <adamc@hcoop.net>
date Thu, 31 Jul 2008 10:44:52 -0400
parents 021f5beb6f8d
children 7ee424760d2f
files src/elab.sml src/elab_print.sml src/elaborate.sml src/lacweb.grm src/source.sml src/source_print.sml tests/pcase.lac
diffstat 7 files changed, 25 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Thu Jul 31 10:31:30 2008 -0400
+++ b/src/elab.sml	Thu Jul 31 10:44:52 2008 -0400
@@ -78,6 +78,7 @@
 datatype pat' =
          PWild
        | PVar of string
+       | PPrim of Prim.t
        | PCon of patCon * pat option
 
 withtype pat = pat' located
--- a/src/elab_print.sml	Thu Jul 31 10:31:30 2008 -0400
+++ b/src/elab_print.sml	Thu Jul 31 10:44:52 2008 -0400
@@ -215,6 +215,7 @@
     case p of
         PWild => string "_"
       | PVar s => string s
+      | PPrim p => Prim.p_t p
       | PCon (pc, NONE) => p_patCon env pc
       | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
                                                space,
--- a/src/elaborate.sml	Thu Jul 31 10:31:30 2008 -0400
+++ b/src/elaborate.sml	Thu Jul 31 10:44:52 2008 -0400
@@ -996,6 +996,8 @@
                 (((L'.PVar x, loc), t),
                  (E.pushERel env x t, SS.add (bound, x)))
             end
+          | L.PPrim p => (((L'.PPrim p, loc), primType env p),
+                          (env, bound))
           | L.PCon ([], x, po) =>
             (case E.lookupConstructor env x of
                  NONE => (expError env (UnboundConstructor (loc, x));
@@ -1006,6 +1008,7 @@
 
 datatype coverage =
          Wild
+       | None
        | Datatype of coverage IM.map
 
 fun exhaustive (env, denv, t, ps) =
@@ -1019,12 +1022,16 @@
             case p of
                 L'.PWild => Wild
               | L'.PVar _ => Wild
+              | L'.PPrim _ => None
               | L'.PCon (pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
               | L'.PCon (pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
 
         fun merge (c1, c2) =
             case (c1, c2) of
-                (Wild, _) => Wild
+                (None, _) => c2
+              | (_, None) => c1
+                
+              | (Wild, _) => Wild
               | (_, Wild) => Wild
 
               | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2))
@@ -1037,7 +1044,8 @@
 
         fun isTotal (c, t) =
             case c of
-                Wild => (true, nil)
+                None => (false, [])
+              | Wild => (true, [])
               | Datatype cm =>
                 let
                     val ((t, _), gs) = hnormCon (env, denv) t
--- a/src/lacweb.grm	Thu Jul 31 10:31:30 2008 -0400
+++ b/src/lacweb.grm	Thu Jul 31 10:44:52 2008 -0400
@@ -348,6 +348,8 @@
 pterm  : SYMBOL                         (PVar SYMBOL, s (SYMBOLleft, SYMBOLright))
        | cpath                          (PCon (#1 cpath, #2 cpath, NONE), s (cpathleft, cpathright))
        | UNDER                          (PWild, s (UNDERleft, UNDERright))
+       | INT                            (PPrim (Prim.Int INT), s (INTleft, INTright))
+       | STRING                         (PPrim (Prim.String STRING), s (STRINGleft, STRINGright))
        | LPAREN pat RPAREN              (pat)
 
 rexp   :                                ([])
--- a/src/source.sml	Thu Jul 31 10:31:30 2008 -0400
+++ b/src/source.sml	Thu Jul 31 10:44:52 2008 -0400
@@ -92,6 +92,7 @@
 datatype pat' =
          PWild
        | PVar of string
+       | PPrim of Prim.t
        | PCon of string list * string * pat option
 
 withtype pat = pat' located
--- a/src/source_print.sml	Thu Jul 31 10:31:30 2008 -0400
+++ b/src/source_print.sml	Thu Jul 31 10:44:52 2008 -0400
@@ -166,6 +166,7 @@
     case p of
         PWild => string "_"
       | PVar s => string s
+      | PPrim p => Prim.p_t p
       | PCon (ms, x, NONE) => p_list_sep (string ".") string (ms @ [x])
       | PCon (ms, x, SOME p) => parenIf par (box [p_list_sep (string ".") string (ms @ [x]),
                                                   space,
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/pcase.lac	Thu Jul 31 10:44:52 2008 -0400
@@ -0,0 +1,9 @@
+val flip = fn x : int => case x of 0 => 1 | _ => 0
+
+val zero = flip 1
+val one = flip 0
+
+val flipS = fn x : string => case x of "" => "Hello world!" | _ => ""
+
+val s1 = flipS ""
+val s2 = flipS "Boop"