diff options
| -rw-r--r-- | src/elab.sml | 2 | ||||
| -rw-r--r-- | src/elab_print.sml | 22 | ||||
| -rw-r--r-- | src/elab_util.sml | 4 | ||||
| -rw-r--r-- | src/elaborate.sml | 5 | ||||
| -rw-r--r-- | src/lacweb.grm | 27 | ||||
| -rw-r--r-- | src/lacweb.lex | 1 | ||||
| -rw-r--r-- | src/source.sml | 14 | ||||
| -rw-r--r-- | src/source_print.sml | 91 | ||||
| -rw-r--r-- | tests/stuff.lac | 3 |
9 files changed, 137 insertions, 32 deletions
diff --git a/src/elab.sml b/src/elab.sml index 89febb0b..5e1a3a9b 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -52,7 +52,7 @@ datatype con' = | CRel of int | CNamed of int | CApp of con * con - | CAbs of explicitness * string * kind * con + | CAbs of string * kind * con | CName of string diff --git a/src/elab_print.sml b/src/elab_print.sml index 2ac8f6fc..98d9e196 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -91,17 +91,17 @@ fun p_con' par env (c, _) = | 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] diff --git a/src/elab_util.sml b/src/elab_util.sml index 37d58fcc..3b608710 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -111,12 +111,12 @@ fun mapfold {kind = fk, con = fc} = 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 diff --git a/src/elaborate.sml b/src/elaborate.sml index b3250190..3e2cac1b 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -219,14 +219,13 @@ fun elabCon env (c, loc) = 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 diff --git a/src/lacweb.grm b/src/lacweb.grm index 5d88c3ad..9d7079e4 100644 --- a/src/lacweb.grm +++ b/src/lacweb.grm @@ -39,7 +39,7 @@ val s = ErrorMsg.spanOf | 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 @@ val s = ErrorMsg.spanOf | 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 @@ 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)) kind : TYPE (KType, s (TYPEleft, TYPEright)) | NAME (KName, s (NAMEleft, NAMEright)) @@ -104,9 +110,9 @@ cexp : capps (capps) | 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 @@ rcone : ([]) 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)) diff --git a/src/lacweb.lex b/src/lacweb.lex index 88410f2a..5234db3d 100644 --- a/src/lacweb.lex +++ b/src/lacweb.lex @@ -110,6 +110,7 @@ ws = [\ \t\012]; <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)); diff --git a/src/source.sml b/src/source.sml index c42e8bab..d574141c 100644 --- a/src/source.sml +++ b/src/source.sml @@ -50,7 +50,7 @@ datatype con' = | 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 @@ datatype con' = 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 diff --git a/src/source_print.sml b/src/source_print.sml index 704d07ec..b81a82df 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -91,17 +91,17 @@ fun p_con' par (c, _) = | 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 @@ fun p_con' par (c, _) = 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 @@ 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] val p_file = p_list_sep newline p_decl diff --git a/tests/stuff.lac b/tests/stuff.lac index d58c1573..db29d5db 100644 --- a/tests/stuff.lac +++ b/tests/stuff.lac @@ -13,3 +13,6 @@ con c8 = fn t :: Type => t con c9 = {} con c10 = ([]) :: {Type} + +val v1 = fn t :: Type => fn x : t => x +val v2 = v1 [c1] (fn y => y) |