From bef69954307005832dca731aff9a7b008c88c8d8 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 26 Jun 2008 09:48:54 -0400 Subject: Elaborating cfold --- src/elab.sml | 1 + src/elab_print.sml | 1 + src/elab_util.sml | 6 ++++++ src/elaborate.sml | 50 +++++++++++++++++++++++++++++++++++++++++++++----- src/explify.sml | 1 + src/lacweb.grm | 6 ++++-- src/lacweb.lex | 1 + src/source.sml | 3 ++- src/source_print.sml | 30 +++++++++++++++++++----------- 9 files changed, 80 insertions(+), 19 deletions(-) (limited to 'src') diff --git a/src/elab.sml b/src/elab.sml index 43837413..ea00d199 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -59,6 +59,7 @@ datatype con' = | CRecord of kind * (con * con) list | CConcat of con * con + | CFold of kind * kind | CError | CUnif of kind * string * con option ref diff --git a/src/elab_print.sml b/src/elab_print.sml index 4c02c495..2b515a03 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -152,6 +152,7 @@ fun p_con' par env (c, _) = string "++", space, p_con env c2]) + | CFold _ => string "fold" | CError => string "" | CUnif (_, _, ref (SOME c)) => p_con' par env c diff --git a/src/elab_util.sml b/src/elab_util.sml index 2d075fb4..7892211c 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -143,6 +143,12 @@ fun mapfoldB {kind = fk, con = fc, bind} = 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 --git a/src/elaborate.sml b/src/elaborate.sml index cc9c2f80..d6e3085d 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -115,6 +115,7 @@ datatype con_error = 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 @@ fun conError env err = ("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 @@ fun elabKind (k, loc) = | 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 @@ fun elabCon env (c, loc) = 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 @@ fun elabCon env (c, loc) = 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 @@ fun elabCon env (c, loc) = 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 @@ fun kindof env (c, loc) = | 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 @@ and hnormCon env (cAll as (c, loc)) = 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 --git a/src/explify.sml b/src/explify.sml index 0c3f5f1f..79e3b07f 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -59,6 +59,7 @@ fun explifyCon (c, loc) = | 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 --git a/src/lacweb.grm b/src/lacweb.grm index e36630ae..c1cf6712 100644 --- a/src/lacweb.grm +++ b/src/lacweb.grm @@ -40,7 +40,7 @@ val s = ErrorMsg.spanOf | 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 : capps (capps) | 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 @@ cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) | 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 --git a/src/lacweb.lex b/src/lacweb.lex index a821cc9e..038e591f 100644 --- a/src/lacweb.lex +++ b/src/lacweb.lex @@ -146,6 +146,7 @@ realconst = [0-9]+\.[0-9]*; "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 --git a/src/source.sml b/src/source.sml index 9ea1ea20..2246399b 100644 --- a/src/source.sml +++ b/src/source.sml @@ -51,12 +51,13 @@ datatype con' = | 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 --git a/src/source_print.sml b/src/source_print.sml index ca72c014..b4496a7a 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -92,17 +92,24 @@ fun p_con' par (c, _) = | 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 @@ fun p_con' par (c, _) = string "++", space, p_con c2]) + | CFold => string "fold" | CWild k => box [string "(_", space, string "::", -- cgit v1.2.3