summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@csail.mit.edu>2017-07-12 16:23:51 -0400
committerGravatar Adam Chlipala <adamc@csail.mit.edu>2017-07-12 16:23:51 -0400
commit6d9522c001574db729262073cadb96c75f0f7c44 (patch)
tree2f3cb126d919b552b7cabefbc88be1abcbd45689
parent979ad6b8246e50d5c1f685afd0bd41ec0298696b (diff)
Allow inexhaustive patterns for lefthand sides of top-level 'val' declarations
-rw-r--r--doc/manual.tex4
-rw-r--r--src/elaborate.sml69
-rw-r--r--src/settings.sml2
-rw-r--r--src/source.sml2
-rw-r--r--src/source_print.sml10
-rw-r--r--src/urweb.grm40
-rw-r--r--tests/topLevelPattern.ur5
7 files changed, 107 insertions, 25 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 3d73b948..eaf7aab5 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -555,7 +555,7 @@ $$\begin{array}{rrcll}
&&& \_ & \textrm{wildcard} \\
&&& (e) & \textrm{explicit precedence} \\
\\
- \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
+ \textrm{Local declarations} & ed &::=& \cd{val} \; p = e & \textrm{non-recursive value} \\
&&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually recursive values} \\
\end{array}$$
@@ -566,7 +566,7 @@ $$\begin{array}{rrcll}
\textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
&&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
&&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
- &&& \mt{val} \; x : \tau = e & \textrm{value} \\
+ &&& \mt{val} \; p = e & \textrm{value} \\
&&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually recursive values} \\
&&& \mt{structure} \; X : S = M & \textrm{module definition} \\
&&& \mt{signature} \; X = S & \textrm{signature definition} \\
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
diff --git a/tests/topLevelPattern.ur b/tests/topLevelPattern.ur
new file mode 100644
index 00000000..e272c30c
--- /dev/null
+++ b/tests/topLevelPattern.ur
@@ -0,0 +1,5 @@
+val (x, y) = (1, 2)
+
+fun main () : transaction page = return <xml>
+ {[x]} + {[y]} = {[x + y]}
+</xml>