From ae494cac4389a07a6feef73a084e2db7ccb84e22 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Thu, 31 Jul 2008 10:44:52 -0400
Subject: Patterns for int and string constants

---
 src/elab.sml         |  1 +
 src/elab_print.sml   |  1 +
 src/elaborate.sml    | 12 ++++++++++--
 src/lacweb.grm       |  2 ++
 src/source.sml       |  1 +
 src/source_print.sml |  1 +
 tests/pcase.lac      |  9 +++++++++
 7 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 tests/pcase.lac

diff --git a/src/elab.sml b/src/elab.sml
index 48790a15..34e0c91c 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -78,6 +78,7 @@ datatype patCon =
 datatype pat' =
          PWild
        | PVar of string
+       | PPrim of Prim.t
        | PCon of patCon * pat option
 
 withtype pat = pat' located
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 7e13c116..0e7fe7d7 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -215,6 +215,7 @@ fun p_pat' par env (p, _) =
     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,
diff --git a/src/elaborate.sml b/src/elaborate.sml
index a123d626..e15ef185 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -996,6 +996,8 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
                 (((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 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
 
 datatype coverage =
          Wild
+       | None
        | Datatype of coverage IM.map
 
 fun exhaustive (env, denv, t, ps) =
@@ -1019,12 +1022,16 @@ fun exhaustive (env, denv, t, ps) =
             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 exhaustive (env, denv, t, ps) =
 
         fun isTotal (c, t) =
             case c of
-                Wild => (true, nil)
+                None => (false, [])
+              | Wild => (true, [])
               | Datatype cm =>
                 let
                     val ((t, _), gs) = hnormCon (env, denv) t
diff --git a/src/lacweb.grm b/src/lacweb.grm
index a5a4f745..817171a6 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -348,6 +348,8 @@ pat    : pterm                          (pterm)
 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   :                                ([])
diff --git a/src/source.sml b/src/source.sml
index b11828f0..3dbada25 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -92,6 +92,7 @@ and sgn = sgn' located
 datatype pat' =
          PWild
        | PVar of string
+       | PPrim of Prim.t
        | PCon of string list * string * pat option
 
 withtype pat = pat' located
diff --git a/src/source_print.sml b/src/source_print.sml
index 4bd7e28e..68ef3508 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -166,6 +166,7 @@ fun p_pat' par (p, _) =
     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,
diff --git a/tests/pcase.lac b/tests/pcase.lac
new file mode 100644
index 00000000..581d94c3
--- /dev/null
+++ b/tests/pcase.lac
@@ -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"
-- 
cgit v1.2.3