Allow inexhaustive patterns for lefthand sides of top-level 'val' declarations

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>