diff src/elab_err.sml @ 819:cb30dd2ba353

Switch to Maranget's pattern exhaustiveness algorithm
author Adam Chlipala <adamc@hcoop.net>
date Sat, 23 May 2009 09:45:02 -0400
parents d20d6afc1206
children e571fb150a9f
line wrap: on
line diff
--- a/src/elab_err.sml	Thu May 21 11:45:04 2009 -0400
+++ b/src/elab_err.sml	Sat May 23 09:45:02 2009 -0400
@@ -161,7 +161,7 @@
      | UnboundConstructor of ErrorMsg.span * string list * string
      | PatHasArg of ErrorMsg.span
      | PatHasNoArg of ErrorMsg.span
-     | Inexhaustive of ErrorMsg.span
+     | Inexhaustive of ErrorMsg.span * pat
      | DuplicatePatField of ErrorMsg.span * string
      | Unresolvable of ErrorMsg.span * con
      | OutOfContext of ErrorMsg.span * (exp * con) option
@@ -207,8 +207,9 @@
         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'"
+      | Inexhaustive (loc, p) =>
+        (ErrorMsg.errorAt loc "Inexhaustive 'case'";
+         eprefaces' [("Missed case", p_pat env p)])
       | DuplicatePatField (loc, s) =>
         ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
       | OutOfContext (loc, co) =>