summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab_err.sig2
-rw-r--r--src/elab_err.sml7
-rw-r--r--src/elaborate.sml260
3 files changed, 252 insertions, 17 deletions
diff --git a/src/elab_err.sig b/src/elab_err.sig
index c0a90e19..10cda7d3 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -71,7 +71,7 @@ signature ELAB_ERR = sig
| UnboundConstructor of ErrorMsg.span * string list * string
| PatHasArg of ErrorMsg.span
| PatHasNoArg of ErrorMsg.span
- | Inexhaustive of ErrorMsg.span
+ | Inexhaustive of ErrorMsg.span * Elab.pat
| DuplicatePatField of ErrorMsg.span * string
| Unresolvable of ErrorMsg.span * Elab.con
| OutOfContext of ErrorMsg.span * (Elab.exp * Elab.con) option
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 9eafa7df..dc34560b 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -161,7 +161,7 @@ datatype exp_error =
| 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 @@ 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'"
+ | 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) =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 8b23d91e..fb376df2 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -38,6 +38,7 @@
open ElabPrint
open ElabErr
+ structure IS = IntBinarySet
structure IM = IntBinaryMap
structure SK = struct
@@ -1291,7 +1292,238 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
end
-datatype coverage =
+(* This exhaustiveness checking follows Luc Maranget's paper "Warnings for pattern matching." *)
+fun exhaustive (env, t, ps, loc) =
+ let
+ fun fail n = raise Fail ("Elaborate.exhaustive: Impossible " ^ Int.toString n)
+
+ fun patConNum pc =
+ case pc of
+ L'.PConVar n => n
+ | L'.PConProj (m1, ms, x) =>
+ let
+ val (str, sgn) = E.chaseMpath env (m1, ms)
+ in
+ case E.projectConstructor env {str = str, sgn = sgn, field = x} of
+ NONE => raise Fail "exhaustive: Can't project datatype"
+ | SOME (_, n, _, _, _) => n
+ end
+
+ fun nameOfNum (t, n) =
+ case t of
+ L'.CModProj (m1, ms, x) =>
+ let
+ val (str, sgn) = E.chaseMpath env (m1, ms)
+ in
+ case E.projectDatatype env {str = str, sgn = sgn, field = x} of
+ NONE => raise Fail "exhaustive: Can't project datatype"
+ | SOME (_, cons) =>
+ case ListUtil.search (fn (name, n', _) =>
+ if n' = n then
+ SOME name
+ else
+ NONE) cons of
+ NONE => fail 9
+ | SOME name => L'.PConProj (m1, ms, name)
+ end
+ | _ => L'.PConVar n
+
+ fun S (args, c, P) =
+ List.mapPartial
+ (fn [] => fail 1
+ | p1 :: ps =>
+ let
+ val loc = #2 p1
+
+ fun wild () =
+ SOME (map (fn _ => (L'.PWild, loc)) args @ ps)
+ in
+ case #1 p1 of
+ L'.PPrim _ => NONE
+ | L'.PCon (_, c', _, NONE) =>
+ if patConNum c' = c then
+ SOME ps
+ else
+ NONE
+ | L'.PCon (_, c', _, SOME p) =>
+ if patConNum c' = c then
+ SOME (p :: ps)
+ else
+ NONE
+ | L'.PRecord xpts =>
+ SOME (map (fn x =>
+ case ListUtil.search (fn (x', p, _) =>
+ if x = x' then
+ SOME p
+ else
+ NONE) xpts of
+ NONE => (L'.PWild, loc)
+ | SOME p => p) args @ ps)
+ | L'.PWild => wild ()
+ | L'.PVar _ => wild ()
+ end)
+ P
+
+ fun D P =
+ List.mapPartial
+ (fn [] => fail 2
+ | (p1, _) :: ps =>
+ case p1 of
+ L'.PWild => SOME ps
+ | L'.PVar _ => SOME ps
+ | L'.PPrim _ => NONE
+ | L'.PCon _ => NONE
+ | L'.PRecord _ => NONE)
+ P
+
+ fun I (P, q) =
+ (*(prefaces "I" [("P", p_list (fn P' => box [PD.string "[", p_list (p_pat env) P', PD.string "]"]) P),
+ ("q", p_list (p_con env) q)];*)
+ case q of
+ [] => (case P of
+ [] => SOME []
+ | _ => NONE)
+ | q1 :: qs =>
+ let
+ val loc = #2 q1
+
+ fun unapp (t, acc) =
+ case t of
+ L'.CApp ((t, _), arg) => unapp (t, arg :: acc)
+ | _ => (t, rev acc)
+
+ val (t1, args) = unapp (#1 (hnormCon env q1), [])
+ fun doSub t = foldl (fn (arg, t) => subConInCon (0, arg) t) t args
+
+ fun dtype (dtO, names) =
+ let
+ val nameSet = IS.addList (IS.empty, names)
+ val nameSet = foldl (fn (ps, nameSet) =>
+ case ps of
+ [] => fail 4
+ | (L'.PCon (_, pc, _, _), _) :: _ =>
+ (IS.delete (nameSet, patConNum pc)
+ handle NotFound => nameSet)
+ | _ => nameSet)
+ nameSet P
+ in
+ nameSet
+ end
+
+ fun default () = (NONE, IS.singleton 0, [])
+
+ val (dtO, unused, cons) =
+ case t1 of
+ L'.CNamed n =>
+ let
+ val dt = E.lookupDatatype env n
+ val cons = E.constructors dt
+ in
+ (SOME dt,
+ dtype (SOME dt, map #2 cons),
+ map (fn (_, n, co) =>
+ (n,
+ case co of
+ NONE => []
+ | SOME t => [("", doSub t)])) cons)
+ end
+ | L'.CModProj (m1, ms, x) =>
+ let
+ val (str, sgn) = E.chaseMpath env (m1, ms)
+ in
+ case E.projectDatatype env {str = str, sgn = sgn, field = x} of
+ NONE => default ()
+ | SOME (_, cons) =>
+ (NONE,
+ dtype (NONE, map #2 cons),
+ map (fn (s, _, co) =>
+ (patConNum (L'.PConProj (m1, ms, s)),
+ case co of
+ NONE => []
+ | SOME t => [("", doSub t)])) cons)
+ end
+ | L'.TRecord (L'.CRecord (_, xts), _) =>
+ let
+ val xts = map (fn ((L'.CName x, _), co) => SOME (x, co)
+ | _ => NONE) xts
+ in
+ if List.all Option.isSome xts then
+ let
+ val xts = List.mapPartial (fn x => x) xts
+ val xts = ListMergeSort.sort (fn ((x1, _), (x2, _)) =>
+ String.compare (x1, x2) = GREATER) xts
+ in
+ (NONE, IS.empty, [(0, xts)])
+ end
+ else
+ default ()
+ end
+ | _ => default ()
+ in
+ if IS.isEmpty unused then
+ let
+ fun recurse cons =
+ case cons of
+ [] => NONE
+ | (name, args) :: cons =>
+ case I (S (map #1 args, name, P),
+ map #2 args @ qs) of
+ NONE => recurse cons
+ | SOME ps =>
+ let
+ val nargs = length args
+ val argPs = List.take (ps, nargs)
+ val restPs = List.drop (ps, nargs)
+
+ val p = case name of
+ 0 => L'.PRecord (ListPair.map
+ (fn ((name, t), p) => (name, p, t))
+ (args, argPs))
+ | _ => L'.PCon (L'.Default, nameOfNum (t1, name), [],
+ case argPs of
+ [] => NONE
+ | [p] => SOME p
+ | _ => fail 3)
+ in
+ SOME ((p, loc) :: restPs)
+ end
+ in
+ recurse cons
+ end
+ else
+ case I (D P, qs) of
+ NONE => NONE
+ | SOME ps =>
+ let
+ val p = case cons of
+ [] => L'.PWild
+ | (0, _) :: _ => L'.PWild
+ | _ =>
+ case IS.find (fn _ => true) unused of
+ NONE => fail 6
+ | SOME name =>
+ case ListUtil.search (fn (name', args) =>
+ if name = name' then
+ SOME (name', args)
+ else
+ NONE) cons of
+ SOME (n, []) =>
+ L'.PCon (L'.Default, nameOfNum (t1, n), [], NONE)
+ | SOME (n, [_]) =>
+ L'.PCon (L'.Default, nameOfNum (t1, n), [], SOME (L'.PWild, loc))
+ | _ => fail 7
+ in
+ SOME ((p, loc) :: ps)
+ end
+ end
+ in
+ case I (map (fn x => [x]) ps, [t]) of
+ NONE => NONE
+ | SOME [p] => SOME p
+ | _ => fail 7
+ end
+
+(*datatype coverage =
Wild
| None
| Datatype of coverage IM.map
@@ -1360,16 +1592,16 @@ fun exhaustive (env, t, ps, loc) =
| p :: ps => merge (coverage p, combinedCoverage ps)
fun enumerateCases depth t =
- if depth = 0 then
+ (TextIO.print "enum'\n"; if depth <= 0 then
[Wild]
else
let
- fun dtype cons =
+ val dtype =
ListUtil.mapConcat (fn (_, n, to) =>
case to of
NONE => [Datatype (IM.insert (IM.empty, n, Wild))]
| SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c)))
- (enumerateCases (depth-1) t)) cons
+ (enumerateCases (depth-1) t))
in
case #1 (hnormCon env t) of
L'.CNamed n =>
@@ -1393,8 +1625,11 @@ fun exhaustive (env, t, ps, loc) =
val this = enumerateCases depth t
val rest = exponentiate rest
in
+ TextIO.print ("Before (" ^ Int.toString (length this)
+ ^ ", " ^ Int.toString (length rest) ^ ")\n");
ListUtil.mapConcat (fn fmap =>
map (fn c => SM.insert (fmap, x, c)) this) rest
+ before TextIO.print "After\n"
end
| _ => raise Fail "exponentiate: Not CName"
in
@@ -1406,7 +1641,7 @@ fun exhaustive (env, t, ps, loc) =
end
| _ => [Wild])
| _ => [Wild]
- end
+ end before TextIO.print "/enum'\n")
fun coverageImp (c1, c2) =
let
@@ -1487,10 +1722,11 @@ fun exhaustive (env, t, ps, loc) =
("c", p_con env (c, ErrorMsg.dummySpan))];
raise Fail "isTotal: Not a datatype")
end
- | Record _ => List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t)
+ | Record _ => List.all (fn c2 => coverageImp (c, c2))
+ (TextIO.print "enum\n"; enumerateCases depth t before TextIO.print "/enum\n")
in
isTotal (combinedCoverage ps, t)
- end
+ end*)
fun unmodCon env (c, loc) =
case c of
@@ -1835,10 +2071,9 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
end)
gs1 pes
in
- if exhaustive (env, et, map #1 pes', loc) then
- ()
- else
- expError env (Inexhaustive loc);
+ case exhaustive (env, et, map #1 pes', loc) of
+ NONE => ()
+ | SOME p => expError env (Inexhaustive (loc, p));
((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs)
end
@@ -1851,8 +2086,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((L'.ELet (eds, e), loc), t, gs1 @ gs2)
end
in
- (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll),
- ("t", PD.string (LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))))];*)
+ (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*)
r
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 15:13:07 +0000