summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-31 10:44:52 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-31 10:44:52 -0400
commitae494cac4389a07a6feef73a084e2db7ccb84e22 (patch)
tree86d47cf4bf1b2b404757efc6acf9b71797b69c83
parentaa799f3af3da1bb7925031dc4f4b65ccf4e3971d (diff)
Patterns for int and string constants
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_print.sml1
-rw-r--r--src/elaborate.sml12
-rw-r--r--src/lacweb.grm2
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml1
-rw-r--r--tests/pcase.lac9
7 files changed, 25 insertions, 2 deletions
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"