summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_env.sml1
-rw-r--r--src/elab_print.sml36
-rw-r--r--src/elab_util.sml23
-rw-r--r--src/elaborate.sml49
-rw-r--r--src/explify.sml1
-rw-r--r--src/lacweb.grm14
-rw-r--r--src/lacweb.lex2
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml43
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,
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-15 15:50:15 +0000