Parsing and elaborating (non-mutual) 'val rec'

10 files changed, 123 insertions, 48 deletions

diff --git a/src/elab.sml b/src/elab.sml
index d9d59d98..653539a6 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -111,6 +111,7 @@ and sgn = sgn' located
 datatype decl' =
          DCon of string * int * kind * con
        | DVal of string * int * con * exp
+       | DValRec of (string * int * con * exp) list
        | DSgn of string * int * sgn
        | DStr of string * int * sgn * str
        | DFfiStr of string * int * sgn
diff --git a/src/elab_env.sml b/src/elab_env.sml
index b0550299..e16296ad 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -296,6 +296,7 @@ fun declBinds env (d, _) =
     case d of
         DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
       | DVal (x, n, t, _) => pushENamedAs env x n t
+      | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
       | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
       | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
       | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
diff --git a/src/elab_print.sml b/src/elab_print.sml
index a95b2952..1da98c7a 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -391,7 +391,17 @@ and p_sgn env (sgn, _) =
         end
       | SgnError => string "<ERROR>"
 
-fun p_decl env ((d, _) : decl) =
+fun p_vali env (x, n, t, e) = box [p_named x n,
+                                   space,
+                                   string ":",
+                                   space,
+                                   p_con env t,
+                                   space,
+                                   string "=",
+                                   space,
+                                   p_exp env e]
+
+fun p_decl env (dAll as (d, _) : decl) =
     case d of
         DCon (x, n, k, c) => box [string "con",
                                   space,
@@ -404,17 +414,19 @@ fun p_decl env ((d, _) : decl) =
                                   string "=",
                                   space,
                                   p_con env c]
-      | DVal (x, n, t, e) => box [string "val",
-                                  space,
-                                  p_named x n,
-                                  space,
-                                  string ":",
-                                  space,
-                                  p_con env t,
-                                  space,
-                                  string "=",
-                                  space,
-                                  p_exp env e]
+      | DVal vi => box [string "val",
+                        space,
+                        p_vali env vi]
+      | DValRec vis =>
+        let
+            val env = E.declBinds env dAll
+        in
+            box [string "val",
+                 space,
+                 string "rec",
+                 space,
+                 p_list_sep (box [newline, string "and", space]) (p_vali env) vis]
+        end
                              
       | DSgn (x, n, sgn) => box [string "signature",
                                  space,
diff --git a/src/elab_util.sml b/src/elab_util.sml
index c14b2c60..35f4cfcd 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -504,6 +504,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                    bind (ctx, NamedC (x, k))
                                                  | DVal (x, _, c, _) =>
                                                    bind (ctx, NamedE (x, c))
+                                                 | DValRec vis =>
+                                                   foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
                                                  | DSgn (x, _, sgn) =>
                                                    bind (ctx, Sgn (x, sgn))
                                                  | DStr (x, _, sgn, _) =>
@@ -546,12 +548,14 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                             S.map2 (mfc ctx c,
                                     fn c' =>
                                        (DCon (x, n, k', c'), loc)))
-              | DVal (x, n, c, e) =>
-                S.bind2 (mfc ctx c,
-                         fn c' =>
-                            S.map2 (mfe ctx e,
-                                    fn e' =>
-                                       (DVal (x, n, c', e'), loc)))
+              | DVal vi =>
+                S.map2 (mfvi ctx vi,
+                     fn vi' =>
+                        (DVal vi', loc))
+              | DValRec vis =>
+                S.map2 (ListUtil.mapfold (mfvi ctx) vis,
+                     fn vis' =>
+                        (DValRec vis', loc))
               | DSgn (x, n, sgn) =>
                 S.map2 (mfsg ctx sgn,
                         fn sgn' =>
@@ -578,6 +582,13 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                             S.map2 (mfst ctx str,
                                     fn str' =>
                                        (DExport (en, sgn', str'), loc)))
+
+        and mfvi ctx (x, n, c, e) =
+            S.bind2 (mfc ctx c,
+                  fn c' =>
+                     S.map2 (mfe ctx e,
+                          fn e' =>
+                             (x, n, c', e')))
     in
         mfd
     end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index af5c6c95..eca00e54 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1593,13 +1593,14 @@ fun dopenConstraints (loc, env, denv) {str, strs} =
 
 fun sgiOfDecl (d, loc) =
     case d of
-        L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
-      | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
-      | L'.DSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, sgn), loc)
-      | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
-      | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc)
-      | L'.DConstraint cs => SOME (L'.SgiConstraint cs, loc)
-      | L'.DExport _ => NONE
+        L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
+      | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
+      | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis
+      | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
+      | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
+      | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
+      | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
+      | L'.DExport _ => []
 
 fun sgiBindsD (env, denv) (sgi, _) =
     case sgi of
@@ -1789,7 +1790,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
         end
       | L.DVal (x, co, e) =>
         let
-            val (c', ck, gs1) = case co of
+            val (c', _, gs1) = case co of
                                     NONE => (cunif (loc, ktype), ktype, [])
                                   | SOME c => elabCon (env, denv) c
 
@@ -1800,6 +1801,36 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
         in
             ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs))
         end
+      | L.DValRec vis =>
+        let
+            val (vis, gs) = ListUtil.foldlMap
+                                (fn ((x, co, e), gs) =>
+                                    let
+                                        val (c', _, gs1) = case co of
+                                                               NONE => (cunif (loc, ktype), ktype, [])
+                                                             | SOME c => elabCon (env, denv) c
+                                    in
+                                        ((x, c', e), gs1 @ gs)
+                                    end) [] vis
+
+            val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
+                                                   let
+                                                       val (env, n) = E.pushENamed env x c'
+                                                   in
+                                                       ((x, n, c', e), env)
+                                                   end) env vis
+
+            val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
+                                                  let
+                                                      val (e', et, gs1) = elabExp (env, denv) e
+                                                                          
+                                                      val gs2 = checkCon (env, denv) e' et c'
+                                                  in
+                                                      ((x, n, c', e'), gs1 @ gs2 @ gs)
+                                                  end) gs vis
+        in
+            ([(L'.DValRec vis, loc)], (env, denv, gs))
+        end
 
       | L.DSgn (x, sgn) =>
         let
@@ -1970,7 +2001,7 @@ and elabStr (env, denv) (str, loc) =
         L.StrConst ds =>
         let
             val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
-            val sgis = List.mapPartial sgiOfDecl ds'
+            val sgis = ListUtil.mapConcat sgiOfDecl ds'
 
             val (sgis, _, _, _, _) =
                 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
diff --git a/src/explify.sml b/src/explify.sml
index ecca21f8..2bab60df 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -111,6 +111,7 @@ fun explifyDecl (d, loc : EM.span) =
     case d of
         L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
       | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc)
+      | L.DValRec _ => raise Fail "Expliofy DValRec"
 
       | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc)
       | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc)
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 2cc23e78..f04c93dd 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -44,7 +44,7 @@ fun uppercaseFirst "" = ""
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
  | DIVIDE | GT
- | CON | LTYPE | VAL | FOLD | UNIT | KUNIT
+ | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT
  | TYPE | NAME
  | ARROW | LARROW | DARROW
  | FN | PLUSPLUS | DOLLAR | TWIDDLE
@@ -59,6 +59,8 @@ fun uppercaseFirst "" = ""
    file of decl list
  | decls of decl list
  | decl of decl
+ | vali of string * con option * exp
+ | valis of (string * con option * exp) list
 
  | sgn of sgn
  | sgntm of sgn
@@ -125,8 +127,8 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
        | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
        | LTYPE SYMBOL EQ cexp           (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                          s (LTYPEleft, cexpright))
-       | VAL SYMBOL EQ eexp             (DVal (SYMBOL, NONE, eexp), s (VALleft, eexpright))
-       | VAL SYMBOL COLON cexp EQ eexp  (DVal (SYMBOL, SOME cexp, eexp), s (VALleft, eexpright))
+       | VAL vali                       (DVal vali, s (VALleft, valiright))
+       | VAL REC valis                  (DValRec valis, s (VALleft, valisright))
 
        | SIGNATURE CSYMBOL EQ sgn       (DSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
        | STRUCTURE CSYMBOL EQ str       (DStr (CSYMBOL, NONE, str), s (STRUCTUREleft, strright))
@@ -149,6 +151,12 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
        | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
        | EXPORT spath                   (DExport spath, s (EXPORTleft, spathright))
 
+vali   : SYMBOL EQ eexp                 (SYMBOL, NONE, eexp)
+       | SYMBOL COLON cexp EQ eexp      (SYMBOL, SOME cexp, eexp)
+
+valis  : vali                           ([vali])
+       | vali AND valis                 (vali :: valis)
+
 sgn    : sgntm                          (sgntm)
        | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
                                         (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right))
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 9e261d9f..f6aeedf3 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -251,6 +251,8 @@ notags = [^<{\n]+;
 <INITIAL> "con"       => (Tokens.CON (pos yypos, pos yypos + size yytext));
 <INITIAL> "type"      => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));
 <INITIAL> "val"       => (Tokens.VAL (pos yypos, pos yypos + size yytext));
+<INITIAL> "rec"       => (Tokens.REC (pos yypos, pos yypos + size yytext));
+<INITIAL> "and"       => (Tokens.AND (pos yypos, pos yypos + size yytext));
 <INITIAL> "fn"        => (Tokens.FN (pos yypos, pos yypos + size yytext));
 <INITIAL> "fold"      => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
 
diff --git a/src/source.sml b/src/source.sml
index d5aa137e..a04836bb 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -107,6 +107,7 @@ withtype exp = exp' located
 datatype decl' =
          DCon of string * kind option * con
        | DVal of string * con option * exp
+       | DValRec of (string * con option * exp) list
        | DSgn of string * sgn
        | DStr of string * sgn option * str
        | DFfiStr of string * sgn
diff --git a/src/source_print.sml b/src/source_print.sml
index 760f46bf..245ee79e 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -329,6 +329,23 @@ and p_sgn (sgn, _) =
       | SgnProj (m, ms, x) => p_list_sep (string ".") string (m :: ms @ [x])
                                    
 
+fun p_vali (x, co, e) =
+    case co of
+        NONE => box [string x,
+                     space,
+                     string "=",
+                     space,
+                     p_exp e]
+      | SOME t => box [string x,
+                       space,
+                       string ":",
+                       space,
+                       p_con t,
+                       space,
+                       string "=",
+                       space,
+                       p_exp e]
+
 fun p_decl ((d, _) : decl) =
     case d of
         DCon (x, NONE, c) => box [string "con",
@@ -349,24 +366,14 @@ fun p_decl ((d, _) : decl) =
                                     string "=",
                                     space,
                                     p_con c]
-      | DVal (x, NONE, e) => box [string "val",
-                                  space,
-                                  string x,
-                                  space,
-                                  string "=",
-                                  space,
-                                  p_exp e]
-      | DVal (x, SOME t, e) => box [string "val",
-                                    space,
-                                    string x,
-                                    space,
-                                    string ":",
-                                    space,
-                                    p_con t,
-                                    space,
-                                    string "=",
-                                    space,
-                                    p_exp e]
+      | DVal vi => box [string "val",
+                        space,
+                        p_vali vi]
+      | DValRec vis => box [string "val",
+                            space,
+                            string "rec",
+                            space,
+                            p_list_sep (box [newline, string "and", space]) p_vali vis]
 
       | DSgn (x, sgn) => box [string "signature",
                               space,