Mercurial > urweb
diff src/elaborate.sml @ 173:8221b95cc24c
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 |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Jul 31 10:31:30 2008 -0400 +++ b/src/elaborate.sml Thu Jul 31 10:44:52 2008 -0400 @@ -996,6 +996,8 @@ (((L'.PVar x, loc), t), (E.pushERel env x t, SS.add (bound, x))) end + | L.PPrim p => (((L'.PPrim p, loc), primType env p), + (env, bound)) | L.PCon ([], x, po) => (case E.lookupConstructor env x of NONE => (expError env (UnboundConstructor (loc, x)); @@ -1006,6 +1008,7 @@ datatype coverage = Wild + | None | Datatype of coverage IM.map fun exhaustive (env, denv, t, ps) = @@ -1019,12 +1022,16 @@ case p of L'.PWild => Wild | L'.PVar _ => Wild + | L'.PPrim _ => None | 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 + (None, _) => c2 + | (_, None) => c1 + + | (Wild, _) => Wild | (_, Wild) => Wild | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2)) @@ -1037,7 +1044,8 @@ fun isTotal (c, t) = case c of - Wild => (true, nil) + None => (false, []) + | Wild => (true, []) | Datatype cm => let val ((t, _), gs) = hnormCon (env, denv) t