Mercurial > urweb
diff src/elaborate.sml @ 174:7ee424760d2f
Elaborating module constructor patterns; parsing record patterns
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 31 Jul 2008 11:28:55 -0400 |
parents | 8221b95cc24c |
children | b2d752455182 |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Jul 31 10:44:52 2008 -0400 +++ b/src/elaborate.sml Thu Jul 31 11:28:55 2008 -0400 @@ -812,7 +812,7 @@ | IncompatibleCons of L'.con * L'.con | DuplicatePatternVariable of ErrorMsg.span * string | PatUnify of L'.pat * L'.con * L'.con * cunify_error - | UnboundConstructor of ErrorMsg.span * string + | UnboundConstructor of ErrorMsg.span * string list * string | PatHasArg of ErrorMsg.span | PatHasNoArg of ErrorMsg.span | Inexhaustive of ErrorMsg.span @@ -848,8 +848,8 @@ ("Have con", p_con env c1), ("Need con", p_con env c2)]; cunifyError env uerr) - | UnboundConstructor (loc, s) => - ErrorMsg.errorAt loc ("Unbound constructor " ^ s ^ " in pattern") + | UnboundConstructor (loc, ms, s) => + ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern") | PatHasArg loc => ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument" | PatHasNoArg loc => @@ -958,7 +958,7 @@ unravel (t, e) end -fun elabPat (pAll as (p, loc), (env, bound)) = +fun elabPat (pAll as (p, loc), (env, denv, bound)) = let val perror = (L'.PWild, loc) val terror = (L'.CError, loc) @@ -972,13 +972,13 @@ rerror) | (SOME _, NONE) => (expError env (PatHasArg loc); rerror) - | (NONE, NONE) => (((L'.PCon (pc, NONE), loc), (L'.CNamed dn, loc)), + | (NONE, NONE) => (((L'.PCon (pc, NONE), loc), dn), (env, bound)) | (SOME p, SOME t) => let - val ((p', pt), (env, bound)) = elabPat (p, (env, bound)) + val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound)) in - (((L'.PCon (pc, SOME p'), loc), (L'.CNamed dn, loc)), + (((L'.PCon (pc, SOME p'), loc), dn), (env, bound)) end in @@ -1000,10 +1000,28 @@ (env, bound)) | L.PCon ([], x, po) => (case E.lookupConstructor env x of - NONE => (expError env (UnboundConstructor (loc, x)); + NONE => (expError env (UnboundConstructor (loc, [], x)); rerror) - | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, dn)) - | L.PCon _ => raise Fail "uhoh" + | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc))) + | L.PCon (m1 :: ms, x, po) => + (case E.lookupStr env m1 of + NONE => (expError env (UnboundStrInExp (loc, m1)); + rerror) + | SOME (n, sgn) => + let + val (str, sgn) = foldl (fn (m, (str, sgn)) => + case E.projectStr env {sgn = sgn, str = str, field = m} of + NONE => raise Fail "typeof: Unknown substructure" + | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) + ((L'.StrVar n, loc), sgn) ms + in + case E.projectConstructor env {str = str, sgn = sgn, field = x} of + NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x)); + rerror) + | SOME (_, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn) + end) + + | L.PRecord _ => raise Fail "Elaborate PRecord" end datatype coverage = @@ -1016,7 +1034,14 @@ fun pcCoverage pc = case pc of L'.PConVar n => n - | _ => raise Fail "uh oh^2" + | 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 constructor" + | SOME (n, _, _) => n + end fun coverage (p, _) = case p of @@ -1049,6 +1074,21 @@ | Datatype cm => let val ((t, _), gs) = hnormCon (env, denv) t + + fun dtype cons = + foldl (fn ((_, n, to), (total, gs)) => + case IM.find (cm, n) of + NONE => (false, gs) + | SOME c' => + case to of + NONE => (total, gs) + | SOME t' => + let + val (total, gs') = isTotal (c', t') + in + (total, gs' @ gs) + end) + (true, gs) cons in case t of L'.CNamed n => @@ -1056,19 +1096,15 @@ val dt = E.lookupDatatype env n val cons = E.constructors dt in - foldl (fn ((_, n, to), (total, gs)) => - case IM.find (cm, n) of - NONE => (false, gs) - | SOME c' => - case to of - NONE => (total, gs) - | SOME t' => - let - val (total, gs') = isTotal (c', t') - in - (total, gs' @ gs) - end) - (true, gs) cons + dtype 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 => raise Fail "isTotal: Can't project datatype" + | SOME cons => dtype cons end | L'.CError => (true, gs) | _ => raise Fail "isTotal: Not a datatype" @@ -1295,7 +1331,7 @@ val (pes', gs) = ListUtil.foldlMap (fn ((p, e), gs) => let - val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty)) + val ((p', pt), (env, _)) = elabPat (p, (env, denv, SS.empty)) val gs1 = checkPatCon (env, denv) p' pt et val (e', et, gs2) = elabExp (env, denv) e