Mercurial > urweb
changeset 8:a455a9f85cc3
Parsing basic expressions
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 26 Jan 2008 17:10:26 -0500 |
| parents | 2ce5bf227d01 |
| children | 14b533dbe6cc |
| files | src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/stuff.lac |
| diffstat | 9 files changed, 137 insertions(+), 32 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Sat Jan 26 16:51:39 2008 -0500 +++ b/src/elab.sml Sat Jan 26 17:10:26 2008 -0500 @@ -52,7 +52,7 @@ | CRel of int | CNamed of int | CApp of con * con - | CAbs of explicitness * string * kind * con + | CAbs of string * kind * con | CName of string
--- a/src/elab_print.sml Sat Jan 26 16:51:39 2008 -0500 +++ b/src/elab_print.sml Sat Jan 26 17:10:26 2008 -0500 @@ -91,17 +91,17 @@ | CApp (c1, c2) => parenIf par (box [p_con env c1, space, p_con' true env c2]) - | CAbs (e, x, k, c) => parenIf par (box [string "fn", - space, - string x, - space, - p_explicitness e, - space, - p_kind k, - space, - string "=>", - space, - p_con (E.pushCRel env x k) c]) + | CAbs (x, k, c) => parenIf par (box [string "fn", + space, + string x, + space, + string "::", + space, + p_kind k, + space, + string "=>", + space, + p_con (E.pushCRel env x k) c]) | CName s => box [string "#", string s]
--- a/src/elab_util.sml Sat Jan 26 16:51:39 2008 -0500 +++ b/src/elab_util.sml Sat Jan 26 17:10:26 2008 -0500 @@ -111,12 +111,12 @@ S.map2 (mfc c2, fn c2' => (CApp (c1', c2'), loc))) - | CAbs (e, x, k, c) => + | CAbs (x, k, c) => S.bind2 (mfk k, fn k' => S.map2 (mfc c, fn c' => - (CAbs (e, x, k', c'), loc))) + (CAbs (x, k', c'), loc))) | CName _ => S.return2 cAll
--- a/src/elaborate.sml Sat Jan 26 16:51:39 2008 -0500 +++ b/src/elaborate.sml Sat Jan 26 17:10:26 2008 -0500 @@ -219,14 +219,13 @@ checkKind env c2' k2 dom; ((L'.CApp (c1', c2'), loc), ran) end - | L.CAbs (e, x, k, t) => + | L.CAbs (x, k, t) => let - val e' = elabExplicitness e val k' = elabKind k val env' = E.pushCRel env x k' val (t', tk) = elabCon env' t in - ((L'.CAbs (e', x, k', t'), loc), + ((L'.CAbs (x, k', t'), loc), (L'.KArrow (k', tk), loc)) end
--- a/src/lacweb.grm Sat Jan 26 16:51:39 2008 -0500 +++ b/src/lacweb.grm Sat Jan 26 17:10:26 2008 -0500 @@ -39,7 +39,7 @@ | SYMBOL of string | CSYMBOL of string | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH - | CON | LTYPE + | CON | LTYPE | VAL | TYPE | NAME | ARROW | LARROW | DARROW | FN | PLUSPLUS | DOLLAR @@ -59,6 +59,10 @@ | rcon of (con * con) list | rcone of (con * con) list + | eexp of exp + | eapps of exp + | eterm of exp + %verbose (* print summary of errors *) %pos int (* positions *) %start file @@ -88,6 +92,8 @@ | 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)) kind : TYPE (KType, s (TYPEleft, TYPEright)) | NAME (KName, s (NAMEleft, NAMEright)) @@ -104,9 +110,9 @@ | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) - | FN SYMBOL kcolon kind DARROW cexp (CAbs (kcolon, SYMBOL, kind, cexp), s (FNleft, cexpright)) + | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, kind, cexp), s (FNleft, cexpright)) - | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, RPARENright)) + | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) kcolon : DCOLON (Explicit) | TCOLON (Implicit) @@ -130,3 +136,18 @@ ident : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) | SYMBOL (CVar SYMBOL, s (SYMBOLleft, SYMBOLright)) + +eapps : eterm (eterm) + | eapps eterm (EApp (eapps, eterm), s (eappsleft, etermright)) + | eapps LBRACK cexp RBRACK (ECApp (eapps, cexp), s (eappsleft, RBRACKright)) + +eexp : eapps (eapps) + | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright)) + | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright)) + | FN SYMBOL DARROW eexp (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright)) + + | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright)) + +eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) + + | SYMBOL (EVar SYMBOL, s (SYMBOLleft, SYMBOLright))
--- a/src/lacweb.lex Sat Jan 26 16:51:39 2008 -0500 +++ b/src/lacweb.lex Sat Jan 26 17:10:26 2008 -0500 @@ -110,6 +110,7 @@ <INITIAL> "con" => (Tokens.CON (yypos, yypos + size yytext)); <INITIAL> "type" => (Tokens.LTYPE (yypos, yypos + size yytext)); +<INITIAL> "val" => (Tokens.VAL (yypos, yypos + size yytext)); <INITIAL> "fn" => (Tokens.FN (yypos, yypos + size yytext)); <INITIAL> "Type" => (Tokens.TYPE (yypos, yypos + size yytext));
--- a/src/source.sml Sat Jan 26 16:51:39 2008 -0500 +++ b/src/source.sml Sat Jan 26 17:10:26 2008 -0500 @@ -50,7 +50,7 @@ | CVar of string | CApp of con * con - | CAbs of explicitness * string * kind * con + | CAbs of string * kind * con | CName of string @@ -59,8 +59,20 @@ withtype con = con' located +datatype exp' = + EAnnot of exp * con + + | EVar of string + | EApp of exp * exp + | EAbs of string * con option * exp + | ECApp of exp * con + | ECAbs of explicitness * string * kind * exp + +withtype exp = exp' located + datatype decl' = DCon of string * kind option * con + | DVal of string * con option * exp withtype decl = decl' located
--- a/src/source_print.sml Sat Jan 26 16:51:39 2008 -0500 +++ b/src/source_print.sml Sat Jan 26 17:10:26 2008 -0500 @@ -91,17 +91,17 @@ | CApp (c1, c2) => parenIf par (box [p_con c1, space, p_con' true c2]) - | CAbs (e, x, k, c) => parenIf par (box [string "fn", - space, - string x, - space, - p_explicitness e, - space, - p_kind k, - space, - string "=>", - space, - p_con c]) + | CAbs (x, k, c) => parenIf par (box [string "fn", + space, + string x, + space, + string "::", + space, + p_kind k, + space, + string "=>", + space, + p_con c]) | CName s => box [string "#", string s] @@ -121,6 +121,57 @@ and p_con c = p_con' false c +fun p_exp' par (e, _) = + case e of + EAnnot (e, t) => box [string "(", + p_exp e, + space, + string ":", + space, + p_con t, + string ")"] + + | EVar s => string s + | EApp (e1, e2) => parenIf par (box [p_exp e1, + space, + p_exp' true e2]) + | EAbs (x, NONE, e) => parenIf par (box [string "fn", + space, + string x, + space, + string "=>", + space, + p_exp e]) + | EAbs (x, SOME t, e) => parenIf par (box [string "fn", + space, + string x, + space, + string ":", + space, + p_con t, + space, + string "=>", + space, + p_exp e]) + | ECApp (e, c) => parenIf par (box [p_exp e, + space, + string "[", + p_con c, + string "]"]) + | ECAbs (exp, x, k, e) => parenIf par (box [string "fn", + space, + string x, + space, + p_explicitness exp, + space, + p_kind k, + space, + string "=>", + space, + p_exp e]) + +and p_exp e = p_exp' false e + fun p_decl ((d, _) : decl) = case d of DCon (x, NONE, c) => box [string "con", @@ -141,6 +192,24 @@ 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] val p_file = p_list_sep newline p_decl