# HG changeset patch # User Adam Chlipala # Date 1217518135 14400 # Node ID 7ee424760d2fdfc54a3fd930ea27d1cf0dc96f73 # Parent 8221b95cc24c17e57e514bf779fbef58e089d15a Elaborating module constructor patterns; parsing record patterns diff -r 8221b95cc24c -r 7ee424760d2f src/elab_env.sig --- a/src/elab_env.sig Thu Jul 31 10:44:52 2008 -0400 +++ b/src/elab_env.sig Thu Jul 31 11:28:55 2008 -0400 @@ -88,6 +88,8 @@ val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (string * int * Elab.con option) list option + val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string } + -> (int * Elab.con option * Elab.con) option val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option diff -r 8221b95cc24c -r 7ee424760d2f src/elab_env.sml --- a/src/elab_env.sml Thu Jul 31 10:44:52 2008 -0400 +++ b/src/elab_env.sml Thu Jul 31 11:28:55 2008 -0400 @@ -570,6 +570,25 @@ | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs)) | _ => NONE +fun projectConstructor env {sgn, str, field} = + case #1 (hnormSgn env sgn) of + SgnConst sgis => + let + fun consider (n, xncs) = + ListUtil.search (fn (x, n', to) => + if x <> field then + NONE + else + SOME (n', to, (CNamed n, #2 str))) xncs + in + case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs) + | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs) + | _ => NONE) sgis of + NONE => NONE + | SOME ((n, to, t), subs) => SOME (n, Option.map (sgnSubCon (str, subs)) to, sgnSubCon (str, subs) t) + end + | _ => NONE + fun projectVal env {sgn, str, field} = case #1 (hnormSgn env sgn) of SgnConst sgis => diff -r 8221b95cc24c -r 7ee424760d2f src/elaborate.sml --- 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 diff -r 8221b95cc24c -r 7ee424760d2f src/lacweb.grm --- a/src/lacweb.grm Thu Jul 31 10:44:52 2008 -0400 +++ b/src/lacweb.grm Thu Jul 31 11:28:55 2008 -0400 @@ -43,7 +43,7 @@ | SYMBOL of string | CSYMBOL of string | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR - | DIVIDE | GT + | DIVIDE | GT | DOTDOTDOT | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT | DATATYPE | OF | TYPE | NAME @@ -104,6 +104,7 @@ | branchs of (pat * exp) list | pat of pat | pterm of pat + | rpat of (string * pat) list * bool | attrs of (con * exp) list | attr of con * exp @@ -351,6 +352,13 @@ | INT (PPrim (Prim.Int INT), s (INTleft, INTright)) | STRING (PPrim (Prim.String STRING), s (STRINGleft, STRINGright)) | LPAREN pat RPAREN (pat) + | LBRACE RBRACE (PRecord ([], false), s (LBRACEleft, RBRACEright)) + | UNIT (PRecord ([], false), s (UNITleft, UNITright)) + | LBRACE rpat RBRACE (PRecord rpat, s (LBRACEleft, RBRACEright)) + +rpat : STRING EQ pat ([(STRING, pat)], false) + | DOTDOTDOT ([], true) + | STRING EQ pat COMMA rpat ((STRING, pat) :: #1 rpat, #2 rpat) rexp : ([]) | ident EQ eexp ([(ident, eexp)]) diff -r 8221b95cc24c -r 7ee424760d2f src/lacweb.lex --- a/src/lacweb.lex Thu Jul 31 10:44:52 2008 -0400 +++ b/src/lacweb.lex Thu Jul 31 11:28:55 2008 -0400 @@ -242,6 +242,7 @@ ":::" => (Tokens.TCOLON (pos yypos, pos yypos + size yytext)); "::" => (Tokens.DCOLON (pos yypos, pos yypos + size yytext)); ":" => (Tokens.COLON (pos yypos, pos yypos + size yytext)); + "..." => (Tokens.DOTDOTDOT (pos yypos, pos yypos + size yytext)); "." => (Tokens.DOT (pos yypos, pos yypos + size yytext)); "$" => (Tokens.DOLLAR (pos yypos, pos yypos + size yytext)); "#" => (Tokens.HASH (pos yypos, pos yypos + size yytext)); diff -r 8221b95cc24c -r 7ee424760d2f src/source.sml --- a/src/source.sml Thu Jul 31 10:44:52 2008 -0400 +++ b/src/source.sml Thu Jul 31 11:28:55 2008 -0400 @@ -94,6 +94,7 @@ | PVar of string | PPrim of Prim.t | PCon of string list * string * pat option + | PRecord of (string * pat) list * bool withtype pat = pat' located diff -r 8221b95cc24c -r 7ee424760d2f src/source_print.sml --- a/src/source_print.sml Thu Jul 31 10:44:52 2008 -0400 +++ b/src/source_print.sml Thu Jul 31 11:28:55 2008 -0400 @@ -171,8 +171,20 @@ | PCon (ms, x, SOME p) => parenIf par (box [p_list_sep (string ".") string (ms @ [x]), space, p_pat' true p]) + | PRecord (xps, flex) => + let + val pps = map (fn (x, p) => box [string "x", space, string "=", space, p_pat p]) xps + in + box [string "{", + p_list_sep (box [string ",", space]) (fn x => x) + (if flex then + pps + else + pps @ [string "..."]), + string "}"] + end -val p_pat = p_pat' false +and p_pat x = p_pat' false x fun p_exp' par (e, _) = case e of diff -r 8221b95cc24c -r 7ee424760d2f tests/caseMod.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/caseMod.lac Thu Jul 31 11:28:55 2008 -0400 @@ -0,0 +1,19 @@ +structure M = struct + datatype t = A | B +end + +val f = fn x : M.t => case x of M.A => M.B | M.B => M.A + +datatype t = datatype M.t + +val g = fn x : t => case x of M.A => B | B => M.A + +structure N = struct + datatype t = C of t | D +end + +val h = fn x : N.t => case x of N.C x => x | N.D => M.A + +datatype u = datatype N.t + +val i = fn x : u => case x of N.C x => x | D => M.A