Mercurial > urweb

comparison src/elaborate.sml @ 172:021f5beb6f8d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pattern match coverage checking
author Adam Chlipala <adamc@hcoop.net>
date Thu, 31 Jul 2008 10:31:30 -0400
parents c7a6e6dbc318
children 8221b95cc24c
comparison
equal deleted inserted replaced
171:c7a6e6dbc318 172:021f5beb6f8d
35 structure D = Disjoint 35 structure D = Disjoint
36 36
37 open Print 37 open Print
38 open ElabPrint 38 open ElabPrint
39 39
40 structure IM = IntBinaryMap
40 structure SS = BinarySetFn(struct 41 structure SS = BinarySetFn(struct
41 type ord_key = string 42 type ord_key = string
42 val compare = String.compare 43 val compare = String.compare
43 end) 44 end)
44 45
812 | DuplicatePatternVariable of ErrorMsg.span * string 813 | DuplicatePatternVariable of ErrorMsg.span * string
813 | PatUnify of L'.pat * L'.con * L'.con * cunify_error 814 | PatUnify of L'.pat * L'.con * L'.con * cunify_error
814 | UnboundConstructor of ErrorMsg.span * string 815 | UnboundConstructor of ErrorMsg.span * string
815 | PatHasArg of ErrorMsg.span 816 | PatHasArg of ErrorMsg.span
816 | PatHasNoArg of ErrorMsg.span 817 | PatHasNoArg of ErrorMsg.span
818 | Inexhaustive of ErrorMsg.span
817 819
818 fun expError env err = 820 fun expError env err =
819 case err of 821 case err of
820 UnboundExp (loc, s) => 822 UnboundExp (loc, s) =>
821 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) 823 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
850 ErrorMsg.errorAt loc ("Unbound constructor " ^ s ^ " in pattern") 852 ErrorMsg.errorAt loc ("Unbound constructor " ^ s ^ " in pattern")
851 | PatHasArg loc => 853 | PatHasArg loc =>
852 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument" 854 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
853 | PatHasNoArg loc => 855 | PatHasNoArg loc =>
854 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument" 856 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
857 | Inexhaustive loc =>
858 ErrorMsg.errorAt loc "Inexhaustive 'case'"
855 859
856 fun checkCon (env, denv) e c1 c2 = 860 fun checkCon (env, denv) e c1 c2 =
857 unifyCons (env, denv) c1 c2 861 unifyCons (env, denv) c1 c2
858 handle CUnify (c1, c2, err) => 862 handle CUnify (c1, c2, err) =>
859 (expError env (Unify (e, c1, c2, err)); 863 (expError env (Unify (e, c1, c2, err));
996 (case E.lookupConstructor env x of 1000 (case E.lookupConstructor env x of
997 NONE => (expError env (UnboundConstructor (loc, x)); 1001 NONE => (expError env (UnboundConstructor (loc, x));
998 rerror) 1002 rerror)
999 | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, dn)) 1003 | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, dn))
1000 | L.PCon _ => raise Fail "uhoh" 1004 | L.PCon _ => raise Fail "uhoh"
1005 end
1006
1007 datatype coverage =
1008 Wild
1009 | Datatype of coverage IM.map
1010
1011 fun exhaustive (env, denv, t, ps) =
1012 let
1013 fun pcCoverage pc =
1014 case pc of
1015 L'.PConVar n => n
1016 | _ => raise Fail "uh oh^2"
1017
1018 fun coverage (p, _) =
1019 case p of
1020 L'.PWild => Wild
1021 | L'.PVar _ => Wild
1022 | L'.PCon (pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
1023 | L'.PCon (pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
1024
1025 fun merge (c1, c2) =
1026 case (c1, c2) of
1027 (Wild, _) => Wild
1028 | (_, Wild) => Wild
1029
1030 | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2))
1031
1032 fun combinedCoverage ps =
1033 case ps of
1034 [] => raise Fail "Empty pattern list for coverage checking"
1035 | [p] => coverage p
1036 | p :: ps => merge (coverage p, combinedCoverage ps)
1037
1038 fun isTotal (c, t) =
1039 case c of
1040 Wild => (true, nil)
1041 | Datatype cm =>
1042 let
1043 val ((t, _), gs) = hnormCon (env, denv) t
1044 in
1045 case t of
1046 L'.CNamed n =>
1047 let
1048 val dt = E.lookupDatatype env n
1049 val cons = E.constructors dt
1050 in
1051 foldl (fn ((_, n, to), (total, gs)) =>
1052 case IM.find (cm, n) of
1053 NONE => (false, gs)
1054 | SOME c' =>
1055 case to of
1056 NONE => (total, gs)
1057 | SOME t' =>
1058 let
1059 val (total, gs') = isTotal (c', t')
1060 in
1061 (total, gs' @ gs)
1062 end)
1063 (true, gs) cons
1064 end
1065 | L'.CError => (true, gs)
1066 | _ => raise Fail "isTotal: Not a datatype"
1067 end
1068 in
1069 isTotal (combinedCoverage ps, t)
1001 end 1070 end
1002 1071
1003 fun elabExp (env, denv) (eAll as (e, loc)) = 1072 fun elabExp (env, denv) (eAll as (e, loc)) =
1004 let 1073 let
1005 1074
1225 val gs3 = checkCon (env, denv) e' et result 1294 val gs3 = checkCon (env, denv) e' et result
1226 in 1295 in
1227 ((p', e'), gs1 @ gs2 @ gs3 @ gs) 1296 ((p', e'), gs1 @ gs2 @ gs3 @ gs)
1228 end) 1297 end)
1229 gs1 pes 1298 gs1 pes
1299
1300 val (total, gs') = exhaustive (env, denv, et, map #1 pes')
1230 in 1301 in
1231 ((L'.ECase (e', pes', result), loc), result, gs) 1302 if total then
1303 ()
1304 else
1305 expError env (Inexhaustive loc);
1306
1307 ((L'.ECase (e', pes', result), loc), result, gs' @ gs)
1232 end 1308 end
1233 end 1309 end
1234 1310
1235 1311
1236 datatype decl_error = 1312 datatype decl_error =