From 6d9522c001574db729262073cadb96c75f0f7c44 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 12 Jul 2017 16:23:51 -0400 Subject: Allow inexhaustive patterns for lefthand sides of top-level 'val' declarations --- src/elaborate.sml | 69 ++++++++++++++++++++++++++++++++++++++++++---------- src/settings.sml | 2 +- src/source.sml | 2 +- src/source_print.sml | 10 +++++--- src/urweb.grm | 40 ++++++++++++++++++++++++++---- 5 files changed, 100 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/elaborate.sml b/src/elaborate.sml index 6965adfd..4a04d4bf 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2489,6 +2489,15 @@ fun queryOf () = (L'.CModProj (!basis_r, [], "sql_query"), ErrorMsg.dummySpan) fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan) fun styleOf () = (L'.CModProj (!basis_r, [], "css_class"), ErrorMsg.dummySpan) +fun patVarsOf (p : L.pat) = + case #1 p of + L.PVar x => [x] + | L.PPrim _ => [] + | L.PCon (_, _, NONE) => [] + | L.PCon (_, _, SOME p) => patVarsOf p + | L.PRecord (xps, _) => ListUtil.mapConcat (fn (_, p) => patVarsOf p) xps + | L.PAnnot (p', _) => patVarsOf p' + fun dopenConstraints (loc, env, denv) {str, strs} = case E.lookupStr env str of NONE => (strError env (UnboundStr (loc, str)); @@ -3807,7 +3816,8 @@ and wildifyStr env (str, sgn) = foldl (fn ((d, _), nd) => case d of L.DCon (x, _, _) => ndelCon (nd, x) - | L.DVal (x, _, _) => ndelVal (nd, x) + | L.DVal (p, _) => + foldl (fn (x, nd) => ndelVal (nd, x)) nd (patVarsOf p) | L.DOpen _ => nempty | L.DStr (x, _, _, (L.StrConst ds', _), _) => (case SM.find (nmods nd, x) of @@ -3855,7 +3865,7 @@ and wildifyStr env (str, sgn) = | xs => let val ewild = (L.EWild, #2 str) - val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs + val ds'' = map (fn x => (L.DVal ((L.PVar x, #2 str), ewild), #2 str)) xs in ds'' @ ds' end @@ -4022,22 +4032,55 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = ([], (env, denv, []))) end) - | L.DVal (x, co, e) => + | L.DVal (p, e) => let - val (c', _, gs1) = case co of - NONE => (cunif env (loc, ktype), ktype, []) - | SOME c => elabCon (env, denv) c + val ((p', pt), (env', bound)) = elabPat (p, (env, SS.empty)) - val (e', et, gs2) = elabExp (env, denv) e + val (e', et, gs1) = elabExp (env, denv) e - val () = checkCon env e' et c' + val c' = normClassConstraint env et - val c' = normClassConstraint env c' - val (env', n) = E.pushENamed env x c' + fun singleVar (p : L.pat) = + case #1 p of + L.PVar x => SOME x + | L.PAnnot (p', _) => singleVar p' + | _ => NONE in - (*prefaces "DVal" [("x", Print.PD.string x), - ("c'", p_con env c')];*) - ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs)) + unifyCons env loc et pt; + + (case exhaustive (env, et, [p'], loc) of + NONE => () + | SOME p => if !mayDelay then + delayedExhaustives := (env, et, [p'], loc) :: !delayedExhaustives + else + expError env (Inexhaustive (loc, p))); + + case singleVar p of + SOME x => + let + val (env', n) = E.pushENamed env x et + in + ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs)) + end + | NONE => + let + val (env', n) = E.pushENamed env "$tmp" et + val vars = SS.listItems bound + val (decls, env') = + ListUtil.foldlMap (fn (x, env') => + let + val e = (L.ECase ((L.EVar ([], "$tmp", L.Infer), loc), + [(p, (L.EVar ([], x, L.Infer), loc))]), loc) + val (e', t, _) = elabExp (env', denv) e + val (env', n) = E.pushENamed env' x t + in + ((L'.DVal (x, n, t, e'), loc), + env') + end) env' vars + in + ((L'.DVal ("$tmp", n, c', e'), loc) :: decls, + (env', denv, gs1 @ gs)) + end end | L.DValRec vis => let diff --git a/src/settings.sml b/src/settings.sml index 7ae4bf85..a3263c06 100644 --- a/src/settings.sml +++ b/src/settings.sml @@ -395,7 +395,7 @@ val jsFuncsBase = basisM [("alert", "alert"), ("htmlifySpecialChar", "htmlifySpecialChar"), ("chr", "chr")] val jsFuncs = ref jsFuncsBase -val jsModule = ref NONE +val jsModule = ref (NONE : string option) fun setJsModule m = jsModule := m fun jsFuncName f = case !jsModule of diff --git a/src/source.sml b/src/source.sml index 9971ca93..2d8c1ed3 100644 --- a/src/source.sml +++ b/src/source.sml @@ -157,7 +157,7 @@ datatype decl' = DCon of string * kind option * con | DDatatype of (string * string list * (string * con option) list) list | DDatatypeImp of string * string list * string - | DVal of string * con option * exp + | DVal of pat * exp | DValRec of (string * con option * exp) list | DSgn of string * sgn | DStr of string * sgn option * Time.time option * str * bool (* did this module come from the '-root' directive? *) diff --git a/src/source_print.sml b/src/source_print.sml index 7b657422..e18a82f9 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -560,9 +560,13 @@ fun p_decl ((d, _) : decl) = string "datatype", space, p_list_sep (string ".") string (ms @ [x'])] - | DVal vi => box [string "val", - space, - p_vali vi] + | DVal (p, e) => box [string "val", + space, + p_pat p, + space, + string "=", + space, + p_exp e] | DValRec vis => box [string "val", space, string "rec", diff --git a/src/urweb.grm b/src/urweb.grm index db5473a6..2a3fe283 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -490,7 +490,7 @@ fun patternOut (e : exp) = | earga of exp * con -> exp * con | eargs of exp * con -> exp * con | eargl of exp * con -> exp * con - | eargl2 of exp * con -> exp * con + | eargl2 of bool * (exp * con -> exp * con) | branch of pat * exp | branchs of (pat * exp) list @@ -622,7 +622,37 @@ decl : CON SYMBOL cargl2 kopt EQ cexp (let (case dargs of [] => [(DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))] | _ => raise Fail "Arguments specified for imported datatype") - | VAL vali ([(DVal vali, s (VALleft, valiright))]) + | VAL pat eargl2 copt EQ eexp (let + fun justVar (p : pat) = + case #1 p of + PVar x => SOME x + | PAnnot (p', _) => justVar p' + | _ => NONE + + val loc = s (VALleft, eexpright) + in + case justVar pat of + SOME x => + let + val t = Option.getOpt (copt, (CWild (KType, loc), loc)) + val (e, t) = #2 eargl2 (eexp, t) + in + [(DVal (pat, e), loc)] + end + | NONE => + let + val pat = + case copt of + SOME t => (PAnnot (pat, t), loc) + | _ => pat + in + (if #1 eargl2 then + ErrorMsg.errorAt loc "Additional arguments not allowed after pattern" + else + ()); + [(DVal (pat, eexp), loc)] + end + end) | VAL REC valis ([(DValRec valis, s (VALleft, valisright))]) | FUN valis ([(DValRec valis, s (FUNleft, valisright))]) @@ -695,7 +725,7 @@ vali : SYMBOL eargl2 copt EQ eexp (let val loc = s (SYMBOLleft, eexpright) val t = Option.getOpt (copt, (CWild (KType, loc), loc)) - val (e, t) = eargl2 (eexp, t) + val (e, t) = #2 eargl2 (eexp, t) in (SYMBOL, SOME t, e) end) @@ -1279,8 +1309,8 @@ eargs : earg (earg) eargl : eargp eargp (eargp1 o eargp2) | eargp eargl (eargp o eargl) -eargl2 : (fn x => x) - | eargp eargl2 (eargp o eargl2) +eargl2 : (false, fn x => x) + | eargp eargl2 (true, eargp o #2 eargl2) earg : patS (fn (e, t) => let -- cgit v1.2.3