summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elaborate.sml143
-rw-r--r--src/lacweb.grm33
-rw-r--r--src/lacweb.lex6
-rw-r--r--src/source.sml20
-rw-r--r--src/source_print.sml86
5 files changed, 219 insertions, 69 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index d6e1f287..9b25f5ca 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -865,74 +865,81 @@ fun declError env err =
eprefaces' [("Expression", p_exp env e)])
fun elabDecl env (d, loc) =
- (resetKunif ();
- resetCunif ();
- case d of
- L.DCon (x, ko, c) =>
- let
- val k' = case ko of
- NONE => kunif ()
- | SOME k => elabKind k
-
- val (c', ck) = elabCon env c
- val (env', n) = E.pushCNamed env x k' (SOME c')
- in
- checkKind env c' ck k';
-
- if ErrorMsg.anyErrors () then
- ()
- else (
- if kunifsInKind k' then
- declError env (KunifsRemainKind (loc, k'))
- else
- ();
-
- if kunifsInCon c' then
- declError env (KunifsRemainCon (loc, c'))
- else
- ()
- );
-
- (env',
- (L'.DCon (x, n, k', c'), loc))
- end
- | L.DVal (x, co, e) =>
- let
- val (c', ck) = case co of
- NONE => (cunif ktype, ktype)
- | SOME c => elabCon env c
-
- val (e', et) = elabExp env e
- val (env', n) = E.pushENamed env x c'
- in
- checkCon env e' et c';
-
- if ErrorMsg.anyErrors () then
- ()
- else (
- if kunifsInCon c' then
- declError env (KunifsRemainCon (loc, c'))
- else
- ();
-
- if cunifsInCon c' then
- declError env (CunifsRemainCon (loc, c'))
- else
- ();
-
- if kunifsInExp e' then
- declError env (KunifsRemainExp (loc, e'))
- else
- ();
-
- if cunifsInExp e' then
- declError env (CunifsRemainExp (loc, e'))
- else
- ());
-
- (env',
- (L'.DVal (x, n, c', e'), loc))
- end)
+ let
+
+ in
+ resetKunif ();
+ resetCunif ();
+ case d of
+ L.DCon (x, ko, c) =>
+ let
+ val k' = case ko of
+ NONE => kunif ()
+ | SOME k => elabKind k
+
+ val (c', ck) = elabCon env c
+ val (env', n) = E.pushCNamed env x k' (SOME c')
+ in
+ checkKind env c' ck k';
+
+ if ErrorMsg.anyErrors () then
+ ()
+ else (
+ if kunifsInKind k' then
+ declError env (KunifsRemainKind (loc, k'))
+ else
+ ();
+
+ if kunifsInCon c' then
+ declError env (KunifsRemainCon (loc, c'))
+ else
+ ()
+ );
+
+ (env',
+ (L'.DCon (x, n, k', c'), loc))
+ end
+ | L.DVal (x, co, e) =>
+ let
+ val (c', ck) = case co of
+ NONE => (cunif ktype, ktype)
+ | SOME c => elabCon env c
+
+ val (e', et) = elabExp env e
+ val (env', n) = E.pushENamed env x c'
+ in
+ checkCon env e' et c';
+
+ if ErrorMsg.anyErrors () then
+ ()
+ else (
+ if kunifsInCon c' then
+ declError env (KunifsRemainCon (loc, c'))
+ else
+ ();
+
+ if cunifsInCon c' then
+ declError env (CunifsRemainCon (loc, c'))
+ else
+ ();
+
+ if kunifsInExp e' then
+ declError env (KunifsRemainExp (loc, e'))
+ else
+ ();
+
+ if cunifsInExp e' then
+ declError env (CunifsRemainExp (loc, e'))
+ else
+ ());
+
+ (env',
+ (L'.DVal (x, n, c', e'), loc))
+ end
+
+ | L.DSgn _ => raise Fail "Not ready to elaborate signature"
+ | L.DStr _ => raise Fail "Not ready to elaborate structure"
+ end
fun elabFile env ds =
ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 0c491bc3..0c708699 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -44,12 +44,19 @@ val s = ErrorMsg.spanOf
| TYPE | NAME
| ARROW | LARROW | DARROW
| FN | PLUSPLUS | DOLLAR
+ | STRUCTURE | SIGNATURE | STRUCT | SIG | END
-%nonterm
+%nonterm
file of decl list
| decls of decl list
| decl of decl
+ | sgn of sgn
+ | sgi of sgn_item
+ | sgis of sgn_item list
+
+ | str of str
+
| kind of kind
| kcolon of explicitness
@@ -97,6 +104,30 @@ decl : CON SYMBOL EQ cexp (DCon (SYMBOL, NONE, cexp), s (CONleft,
| 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))
+ | SIGNATURE CSYMBOL EQ sgn (DSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
+ | STRUCTURE CSYMBOL EQ str (DStr (CSYMBOL, NONE, str), s (STRUCTUREleft, strright))
+ | STRUCTURE CSYMBOL COLON sgn EQ str (DStr (CSYMBOL, SOME sgn, str), s (STRUCTUREleft, strright))
+
+sgn : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright))
+ | CSYMBOL (SgnVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+
+sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, kindright))
+ | LTYPE SYMBOL (SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))),
+ s (LTYPEleft, SYMBOLright))
+ | CON SYMBOL EQ cexp (SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright))
+ | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
+ | LTYPE SYMBOL EQ cexp (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
+ s (LTYPEleft, cexpright))
+ | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright))
+
+ | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright))
+
+sgis : ([])
+ | sgi sgis (sgi :: sgis)
+
+str : STRUCT decls END (StrConst decls, s (STRUCTleft, ENDright))
+ | CSYMBOL (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+
kind : TYPE (KType, s (TYPEleft, TYPEright))
| NAME (KName, s (NAMEleft, NAMEright))
| LBRACE kind RBRACE (KRecord kind, s (LBRACEleft, RBRACEright))
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 3fb3d95e..2170c1d5 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -128,6 +128,12 @@ realconst = [0-9]+\.[0-9]*;
<INITIAL> "val" => (Tokens.VAL (yypos, yypos + size yytext));
<INITIAL> "fn" => (Tokens.FN (yypos, yypos + size yytext));
+<INITIAL> "structure" => (Tokens.STRUCTURE (yypos, yypos + size yytext));
+<INITIAL> "signature" => (Tokens.STRUCTURE (yypos, yypos + size yytext));
+<INITIAL> "struct" => (Tokens.STRUCT (yypos, yypos + size yytext));
+<INITIAL> "sig" => (Tokens.SIG (yypos, yypos + size yytext));
+<INITIAL> "end" => (Tokens.END (yypos, yypos + size yytext));
+
<INITIAL> "Type" => (Tokens.TYPE (yypos, yypos + size yytext));
<INITIAL> "Name" => (Tokens.NAME (yypos, yypos + size yytext));
diff --git a/src/source.sml b/src/source.sml
index c76ebf0b..6fe07255 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -77,11 +77,31 @@ datatype exp' =
withtype exp = exp' located
+datatype sgn_item' =
+ SgiConAbs of string * kind
+ | SgiCon of string * kind option * con
+ | SgiVal of string * con
+ | SgiStr of string * sgn
+
+and sgn' =
+ SgnConst of sgn_item list
+ | SgnVar of string
+
+withtype sgn_item = sgn_item' located
+and sgn = sgn' located
+
datatype decl' =
DCon of string * kind option * con
| DVal of string * con option * exp
+ | DSgn of string * sgn
+ | DStr of string * sgn option * str
+
+ and str' =
+ StrConst of decl list
+ | StrVar of string
withtype decl = decl' located
+ and str = str' located
type file = decl list
diff --git a/src/source_print.sml b/src/source_print.sml
index 28146f1f..5a2412a9 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -197,6 +197,57 @@ fun p_exp' par (e, _) =
and p_exp e = p_exp' false e
+fun p_sgn_item (sgi, _) =
+ case sgi of
+ SgiConAbs (x, k) => box [string "con",
+ space,
+ string x,
+ space,
+ string "::",
+ space,
+ p_kind k]
+ | SgiCon (x, NONE, c) => box [string "con",
+ space,
+ string x,
+ space,
+ string "=",
+ space,
+ p_con c]
+ | SgiCon (x, SOME k, c) => box [string "con",
+ space,
+ string x,
+ space,
+ string "::",
+ space,
+ p_kind k,
+ space,
+ string "=",
+ space,
+ p_con c]
+ | SgiVal (x, c) => box [string "val",
+ space,
+ string x,
+ space,
+ string ":",
+ space,
+ p_con c]
+ | SgiStr (x, sgn) => box [string "structure",
+ space,
+ string x,
+ space,
+ string ":",
+ space,
+ p_sgn sgn]
+
+and p_sgn (sgn, _) =
+ case sgn of
+ SgnConst sgis => box [string "sig",
+ newline,
+ p_list_sep newline p_sgn_item sgis,
+ newline,
+ string "end"]
+ | SgnVar x => string x
+
fun p_decl ((d, _) : decl) =
case d of
DCon (x, NONE, c) => box [string "con",
@@ -236,6 +287,41 @@ fun p_decl ((d, _) : decl) =
space,
p_exp e]
+ | DSgn (x, sgn) => box [string "signature",
+ space,
+ string x,
+ space,
+ string "=",
+ space,
+ p_sgn sgn]
+ | DStr (x, NONE, str) => box [string "structure",
+ space,
+ string x,
+ space,
+ string "=",
+ space,
+ p_str str]
+ | DStr (x, SOME sgn, str) => box [string "structure",
+ space,
+ string x,
+ space,
+ string ":",
+ space,
+ p_sgn sgn,
+ space,
+ string "=",
+ space,
+ p_str str]
+
+and p_str (str, _) =
+ case str of
+ StrConst ds => box [string "struct",
+ newline,
+ p_list_sep newline p_decl ds,
+ newline,
+ string "end"]
+ | StrVar x => string x
+
val p_file = p_list_sep newline p_decl
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 14:00:39 +0000