# HG changeset patch # User Adam Chlipala # Date 1213293862 14400 # Node ID e6ccf961d8a34db451714730dd3e4b5f80f02004 # Parent 537db4ee89f41e563661d1f44505873320b9e5e3 Parsing and printing basic module system diff -r 537db4ee89f4 -r e6ccf961d8a3 src/elaborate.sml --- a/src/elaborate.sml Tue Jun 10 18:28:43 2008 -0400 +++ b/src/elaborate.sml Thu Jun 12 14:04:22 2008 -0400 @@ -865,74 +865,81 @@ 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 + 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'; + 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 ErrorMsg.anyErrors () then + () + else ( + if kunifsInKind k' then + declError env (KunifsRemainKind (loc, k')) + else + (); - if kunifsInCon c' then - declError env (KunifsRemainCon (loc, c')) - 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 + (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'; + 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 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 cunifsInCon c' then + declError env (CunifsRemainCon (loc, c')) + else + (); - if kunifsInExp e' then - declError env (KunifsRemainExp (loc, e')) - else - (); + if kunifsInExp e' then + declError env (KunifsRemainExp (loc, e')) + else + (); - if cunifsInExp e' then - declError env (CunifsRemainExp (loc, e')) - else - ()); + if cunifsInExp e' then + declError env (CunifsRemainExp (loc, e')) + else + ()); - (env', - (L'.DVal (x, n, c', e'), loc)) - end) + (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 -r 537db4ee89f4 -r e6ccf961d8a3 src/lacweb.grm --- a/src/lacweb.grm Tue Jun 10 18:28:43 2008 -0400 +++ b/src/lacweb.grm Thu Jun 12 14:04:22 2008 -0400 @@ -44,12 +44,19 @@ | 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 @@ | 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 -r 537db4ee89f4 -r e6ccf961d8a3 src/lacweb.lex --- a/src/lacweb.lex Tue Jun 10 18:28:43 2008 -0400 +++ b/src/lacweb.lex Thu Jun 12 14:04:22 2008 -0400 @@ -128,6 +128,12 @@ "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 -r 537db4ee89f4 -r e6ccf961d8a3 src/source.sml --- a/src/source.sml Tue Jun 10 18:28:43 2008 -0400 +++ b/src/source.sml Thu Jun 12 14:04:22 2008 -0400 @@ -77,11 +77,31 @@ 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 -r 537db4ee89f4 -r e6ccf961d8a3 src/source_print.sml --- a/src/source_print.sml Tue Jun 10 18:28:43 2008 -0400 +++ b/src/source_print.sml Thu Jun 12 14:04:22 2008 -0400 @@ -197,6 +197,57 @@ 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 @@ 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