summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sml78
1 files changed, 77 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index e59cb9d2..a123d626 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -37,6 +37,7 @@ structure D = Disjoint
open Print
open ElabPrint
+structure IM = IntBinaryMap
structure SS = BinarySetFn(struct
type ord_key = string
val compare = String.compare
@@ -814,6 +815,7 @@ datatype exp_error =
| UnboundConstructor of ErrorMsg.span * string
| PatHasArg of ErrorMsg.span
| PatHasNoArg of ErrorMsg.span
+ | Inexhaustive of ErrorMsg.span
fun expError env err =
case err of
@@ -852,6 +854,8 @@ fun expError env err =
ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
| PatHasNoArg loc =>
ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
+ | Inexhaustive loc =>
+ ErrorMsg.errorAt loc "Inexhaustive 'case'"
fun checkCon (env, denv) e c1 c2 =
unifyCons (env, denv) c1 c2
@@ -1000,6 +1004,71 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
| L.PCon _ => raise Fail "uhoh"
end
+datatype coverage =
+ Wild
+ | Datatype of coverage IM.map
+
+fun exhaustive (env, denv, t, ps) =
+ let
+ fun pcCoverage pc =
+ case pc of
+ L'.PConVar n => n
+ | _ => raise Fail "uh oh^2"
+
+ fun coverage (p, _) =
+ case p of
+ L'.PWild => Wild
+ | L'.PVar _ => Wild
+ | 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
+ | (_, Wild) => Wild
+
+ | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2))
+
+ fun combinedCoverage ps =
+ case ps of
+ [] => raise Fail "Empty pattern list for coverage checking"
+ | [p] => coverage p
+ | p :: ps => merge (coverage p, combinedCoverage ps)
+
+ fun isTotal (c, t) =
+ case c of
+ Wild => (true, nil)
+ | Datatype cm =>
+ let
+ val ((t, _), gs) = hnormCon (env, denv) t
+ in
+ case t of
+ L'.CNamed n =>
+ let
+ val dt = E.lookupDatatype env n
+ val cons = E.constructors dt
+ in
+ foldl (fn ((_, n, to), (total, gs)) =>
+ case IM.find (cm, n) of
+ NONE => (false, gs)
+ | SOME c' =>
+ case to of
+ NONE => (total, gs)
+ | SOME t' =>
+ let
+ val (total, gs') = isTotal (c', t')
+ in
+ (total, gs' @ gs)
+ end)
+ (true, gs) cons
+ end
+ | L'.CError => (true, gs)
+ | _ => raise Fail "isTotal: Not a datatype"
+ end
+ in
+ isTotal (combinedCoverage ps, t)
+ end
+
fun elabExp (env, denv) (eAll as (e, loc)) =
let
@@ -1227,8 +1296,15 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((p', e'), gs1 @ gs2 @ gs3 @ gs)
end)
gs1 pes
+
+ val (total, gs') = exhaustive (env, denv, et, map #1 pes')
in
- ((L'.ECase (e', pes', result), loc), result, gs)
+ if total then
+ ()
+ else
+ expError env (Inexhaustive loc);
+
+ ((L'.ECase (e', pes', result), loc), result, gs' @ gs)
end
end