# HG changeset patch # User Adam Chlipala # Date 1214488134 14400 # Node ID 9f89f0b00b842d0fb3458699f24b8b619f3b1bc4 # Parent 1ec5703c09c43278958cd6caa987cebc2b454e56 Elaborating cfold diff -r 1ec5703c09c4 -r 9f89f0b00b84 src/elab.sml --- a/src/elab.sml Thu Jun 26 09:09:30 2008 -0400 +++ b/src/elab.sml Thu Jun 26 09:48:54 2008 -0400 @@ -59,6 +59,7 @@ | CRecord of kind * (con * con) list | CConcat of con * con + | CFold of kind * kind | CError | CUnif of kind * string * con option ref diff -r 1ec5703c09c4 -r 9f89f0b00b84 src/elab_print.sml --- a/src/elab_print.sml Thu Jun 26 09:09:30 2008 -0400 +++ b/src/elab_print.sml Thu Jun 26 09:48:54 2008 -0400 @@ -152,6 +152,7 @@ string "++", space, p_con env c2]) + | CFold _ => string "fold" | CError => string "" | CUnif (_, _, ref (SOME c)) => p_con' par env c diff -r 1ec5703c09c4 -r 9f89f0b00b84 src/elab_util.sml --- a/src/elab_util.sml Thu Jun 26 09:09:30 2008 -0400 +++ b/src/elab_util.sml Thu Jun 26 09:48:54 2008 -0400 @@ -143,6 +143,12 @@ S.map2 (mfc ctx c2, fn c2' => (CConcat (c1', c2'), loc))) + | CFold (k1, k2) => + S.bind2 (mfk k1, + fn k1' => + S.map2 (mfk k2, + fn k2' => + (CFold (k1', k2'), loc))) | CError => S.return2 cAll | CUnif (_, _, ref (SOME c)) => mfc' ctx c diff -r 1ec5703c09c4 -r 9f89f0b00b84 src/elaborate.sml --- a/src/elaborate.sml Thu Jun 26 09:09:30 2008 -0400 +++ b/src/elaborate.sml Thu Jun 26 09:48:54 2008 -0400 @@ -115,6 +115,7 @@ UnboundCon of ErrorMsg.span * string | UnboundStrInCon of ErrorMsg.span * string | WrongKind of L'.con * L'.kind * L'.kind * kunify_error + | DuplicateField of ErrorMsg.span * string fun conError env err = case err of @@ -128,6 +129,8 @@ ("Have kind", p_kind k1), ("Need kind", p_kind k2)]; kunifyError kerr) + | DuplicateField (loc, s) => + ErrorMsg.errorAt loc ("Duplicate record field " ^ s) fun checkKind env c k1 k2 = unifyKinds k1 k2 @@ -198,6 +201,14 @@ | L.KRecord k => (L'.KRecord (elabKind k), loc) | L.KWild => kunif () +fun foldKind (dom, ran, loc)= + (L'.KArrow ((L'.KArrow ((L'.KName, loc), + (L'.KArrow (dom, + (L'.KArrow (ran, ran), loc)), loc)), loc), + (L'.KArrow (ran, + (L'.KArrow ((L'.KRecord dom, loc), + ran), loc)), loc)), loc) + fun elabCon env (c, loc) = case c of L.CAnnot (c, k) => @@ -278,9 +289,11 @@ checkKind env c2' k2 dom; ((L'.CApp (c1', c2'), loc), ran) end - | L.CAbs (x, k, t) => + | L.CAbs (x, ko, t) => let - val k' = elabKind k + val k' = case ko of + NONE => kunif () + | SOME k => elabKind k val env' = E.pushCRel env x k' val (t', tk) = elabCon env' t in @@ -304,8 +317,11 @@ checkKind env c' ck k; (x', c') end) xcs + + val rc = (L'.CRecord (k, xcs'), loc) + (* Add duplicate field checking later. *) in - ((L'.CRecord (k, xcs'), loc), (L'.KRecord k, loc)) + (rc, (L'.KRecord k, loc)) end | L.CConcat (c1, c2) => let @@ -318,6 +334,14 @@ checkKind env c2' k2 k; ((L'.CConcat (c1', c2'), loc), k) end + | L.CFold => + let + val dom = kunif () + val ran = kunif () + in + ((L'.CFold (dom, ran), loc), + foldKind (dom, ran, loc)) + end | L.CWild k => let @@ -473,6 +497,7 @@ | L'.CRecord (k, _) => (L'.KRecord k, loc) | L'.CConcat (c, _) => kindof env c + | L'.CFold (dom, ran) => foldKind (dom, ran, loc) | L'.CError => kerror | L'.CUnif (k, _, _) => k @@ -624,10 +649,25 @@ end | L'.CApp (c1, c2) => - (case hnormCon env c1 of - (L'.CAbs (_, _, cb), _) => + (case #1 (hnormCon env c1) of + L'.CAbs (_, _, cb) => ((hnormCon env (subConInCon (0, c2) cb)) handle SynUnif => cAll) + | L'.CApp (c', i) => + (case #1 (hnormCon env c') of + L'.CApp (c', f) => + (case #1 (hnormCon env c') of + L'.CFold ks => + (case #1 (hnormCon env c2) of + L'.CRecord (_, []) => hnormCon env i + | L'.CRecord (k, (x, c) :: rest) => + hnormCon env + (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), + (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), + (L'.CRecord (k, rest), loc)), loc)), loc) + | _ => cAll) + | _ => cAll) + | _ => cAll) | _ => cAll) | L'.CConcat (c1, c2) => diff -r 1ec5703c09c4 -r 9f89f0b00b84 src/explify.sml --- a/src/explify.sml Thu Jun 26 09:09:30 2008 -0400 +++ b/src/explify.sml Thu Jun 26 09:48:54 2008 -0400 @@ -59,6 +59,7 @@ | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc) | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc) + | L.CFold _ => raise Fail "Explify CFold" | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) | L.CUnif (_, _, ref (SOME c)) => explifyCon c diff -r 1ec5703c09c4 -r 9f89f0b00b84 src/lacweb.grm --- a/src/lacweb.grm Thu Jun 26 09:09:30 2008 -0400 +++ b/src/lacweb.grm Thu Jun 26 09:48:54 2008 -0400 @@ -40,7 +40,7 @@ | SYMBOL of string | CSYMBOL of string | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER - | CON | LTYPE | VAL + | CON | LTYPE | VAL | FOLD | TYPE | NAME | ARROW | LARROW | DARROW | FN | PLUSPLUS | DOLLAR @@ -190,7 +190,8 @@ | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) - | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, kind, cexp), s (FNleft, cexpright)) + | FN SYMBOL DARROW cexp (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright)) + | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) @@ -214,6 +215,7 @@ | path (CVar path, s (pathleft, pathright)) | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright)) + | FOLD (CFold, s (FOLDleft, FOLDright)) rcon : ([]) | ident EQ cexp ([(ident, cexp)]) diff -r 1ec5703c09c4 -r 9f89f0b00b84 src/lacweb.lex --- a/src/lacweb.lex Thu Jun 26 09:09:30 2008 -0400 +++ b/src/lacweb.lex Thu Jun 26 09:48:54 2008 -0400 @@ -146,6 +146,7 @@ "type" => (Tokens.LTYPE (pos yypos, pos yypos + size yytext)); "val" => (Tokens.VAL (pos yypos, pos yypos + size yytext)); "fn" => (Tokens.FN (pos yypos, pos yypos + size yytext)); + "fold" => (Tokens.FOLD (pos yypos, pos yypos + size yytext)); "structure" => (Tokens.STRUCTURE (pos yypos, pos yypos + size yytext)); "signature" => (Tokens.SIGNATURE (pos yypos, pos yypos + size yytext)); diff -r 1ec5703c09c4 -r 9f89f0b00b84 src/source.sml --- a/src/source.sml Thu Jun 26 09:09:30 2008 -0400 +++ b/src/source.sml Thu Jun 26 09:48:54 2008 -0400 @@ -51,12 +51,13 @@ | CVar of string list * string | CApp of con * con - | CAbs of string * kind * con + | CAbs of string * kind option * con | CName of string | CRecord of (con * con) list | CConcat of con * con + | CFold | CWild of kind diff -r 1ec5703c09c4 -r 9f89f0b00b84 src/source_print.sml --- a/src/source_print.sml Thu Jun 26 09:09:30 2008 -0400 +++ b/src/source_print.sml Thu Jun 26 09:48:54 2008 -0400 @@ -92,17 +92,24 @@ | CApp (c1, c2) => parenIf par (box [p_con c1, space, p_con' true c2]) - | CAbs (x, k, c) => parenIf par (box [string "fn", - space, - string x, - space, - string "::", - space, - p_kind k, - space, - string "=>", - space, - p_con c]) + | CAbs (x, NONE, c) => parenIf par (box [string "fn", + space, + string x, + space, + string "=>", + space, + p_con c]) + | CAbs (x, SOME 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] @@ -119,6 +126,7 @@ string "++", space, p_con c2]) + | CFold => string "fold" | CWild k => box [string "(_", space, string "::", diff -r 1ec5703c09c4 -r 9f89f0b00b84 tests/cfold.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/cfold.lac Thu Jun 26 09:48:54 2008 -0400 @@ -0,0 +1,10 @@ +con currier = fold (fn nm => fn t => fn acc => t -> acc) {} + +con greenCurry = currier [] +val greenCurry : greenCurry = {} + +con redCurry = currier [A = int, B = string] +val redCurry : redCurry = fn x : int => fn y : string => {} + +con yellowCurry = currier [A = string, B = int, C = float] +val yellowCurry : yellowCurry = fn x => fn y => fn z => {}