From 230753c968d4615b8e875940c4147d79d04d1ad3 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 12 Jun 2008 14:04:22 -0400 Subject: Parsing and printing basic module system --- src/elaborate.sml | 143 +++++++++++++++++++++++++++------------------------ src/lacweb.grm | 33 +++++++++++- src/lacweb.lex | 6 +++ src/source.sml | 20 +++++++ src/source_print.sml | 86 +++++++++++++++++++++++++++++++ 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]*; "val" => (Tokens.VAL (yypos, yypos + size yytext)); "fn" => (Tokens.FN (yypos, yypos + size yytext)); + "structure" => (Tokens.STRUCTURE (yypos, yypos + size yytext)); + "signature" => (Tokens.STRUCTURE (yypos, yypos + size yytext)); + "struct" => (Tokens.STRUCT (yypos, yypos + size yytext)); + "sig" => (Tokens.SIG (yypos, yypos + size yytext)); + "end" => (Tokens.END (yypos, yypos + size yytext)); + "Type" => (Tokens.TYPE (yypos, yypos + size yytext)); "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 -- cgit v1.2.3