Mercurial > urweb

comparison src/elaborate.sml @ 173:8221b95cc24c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Patterns for int and string constants
author Adam Chlipala <adamc@hcoop.net>
date Thu, 31 Jul 2008 10:44:52 -0400
parents 021f5beb6f8d
children 7ee424760d2f
comparison
equal deleted inserted replaced
172:021f5beb6f8d 173:8221b95cc24c
994 cunif (loc, (L'.KType, loc)) 994 cunif (loc, (L'.KType, loc))
995 in 995 in
996 (((L'.PVar x, loc), t), 996 (((L'.PVar x, loc), t),
997 (E.pushERel env x t, SS.add (bound, x))) 997 (E.pushERel env x t, SS.add (bound, x)))
998 end 998 end
999 | L.PPrim p => (((L'.PPrim p, loc), primType env p),
1000 (env, bound))
999 | L.PCon ([], x, po) => 1001 | L.PCon ([], x, po) =>
1000 (case E.lookupConstructor env x of 1002 (case E.lookupConstructor env x of
1001 NONE => (expError env (UnboundConstructor (loc, x)); 1003 NONE => (expError env (UnboundConstructor (loc, x));
1002 rerror) 1004 rerror)
1003 | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, dn)) 1005 | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, dn))
1004 | L.PCon _ => raise Fail "uhoh" 1006 | L.PCon _ => raise Fail "uhoh"
1005 end 1007 end
1006 1008
1007 datatype coverage = 1009 datatype coverage =
1008 Wild 1010 Wild
1011 | None
1009 | Datatype of coverage IM.map 1012 | Datatype of coverage IM.map
1010 1013
1011 fun exhaustive (env, denv, t, ps) = 1014 fun exhaustive (env, denv, t, ps) =
1012 let 1015 let
1013 fun pcCoverage pc = 1016 fun pcCoverage pc =
1017 1020
1018 fun coverage (p, _) = 1021 fun coverage (p, _) =
1019 case p of 1022 case p of
1020 L'.PWild => Wild 1023 L'.PWild => Wild
1021 | L'.PVar _ => Wild 1024 | L'.PVar _ => Wild
1025 | L'.PPrim _ => None
1022 | L'.PCon (pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild)) 1026 | 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)) 1027 | L'.PCon (pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
1024 1028
1025 fun merge (c1, c2) = 1029 fun merge (c1, c2) =
1026 case (c1, c2) of 1030 case (c1, c2) of
1027 (Wild, _) => Wild 1031 (None, _) => c2
1032 | (_, None) => c1
1033
1034 | (Wild, _) => Wild
1028 | (_, Wild) => Wild 1035 | (_, Wild) => Wild
1029 1036
1030 | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2)) 1037 | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2))
1031 1038
1032 fun combinedCoverage ps = 1039 fun combinedCoverage ps =
1035 | [p] => coverage p 1042 | [p] => coverage p
1036 | p :: ps => merge (coverage p, combinedCoverage ps) 1043 | p :: ps => merge (coverage p, combinedCoverage ps)
1037 1044
1038 fun isTotal (c, t) = 1045 fun isTotal (c, t) =
1039 case c of 1046 case c of
1040 Wild => (true, nil) 1047 None => (false, [])
1048 | Wild => (true, [])
1041 | Datatype cm => 1049 | Datatype cm =>
1042 let 1050 let
1043 val ((t, _), gs) = hnormCon (env, denv) t 1051 val ((t, _), gs) = hnormCon (env, denv) t
1044 in 1052 in
1045 case t of 1053 case t of