# HG changeset patch # User Adam Chlipala # Date 1213907740 14400 # Node ID b3fbbc6cb1e59ff3f73f3f3ab46bd3f13a8f1c30 # Parent 1405d8c2679021e9a7c78229a63fdce8d53e7a70 Elaborating 'where' diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/elab.sml --- a/src/elab.sml Thu Jun 19 16:04:28 2008 -0400 +++ b/src/elab.sml Thu Jun 19 16:35:40 2008 -0400 @@ -92,6 +92,7 @@ SgnConst of sgn_item list | SgnVar of int | SgnFun of string * int * sgn * sgn + | SgnWhere of sgn * string * con | SgnError withtype sgn_item = sgn_item' located diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/elab_env.sig --- a/src/elab_env.sig Thu Jun 19 16:04:28 2008 -0400 +++ b/src/elab_env.sig Thu Jun 19 16:35:40 2008 -0400 @@ -76,10 +76,10 @@ val declBinds : env -> Elab.decl -> env val sgiBinds : env -> Elab.sgn_item -> env + val hnormSgn : env -> Elab.sgn -> Elab.sgn + val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option - - end diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/elab_env.sml --- a/src/elab_env.sml Thu Jun 19 16:04:28 2008 -0400 +++ b/src/elab_env.sml Thu Jun 19 16:35:40 2008 -0400 @@ -361,52 +361,61 @@ sgn_item = id, sgn = id} -fun projectCon env {sgn = (sgn, _), str, field} = +fun hnormSgn env (all as (sgn, loc)) = case sgn of + SgnError => all + | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n)) + | SgnConst _ => all + | SgnFun _ => all + | SgnWhere (sgn, x, c) => + case #1 (hnormSgn env sgn) of + SgnError => (SgnError, loc) + | SgnConst sgis => + let + fun traverse (pre, post) = + case post of + [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]" + | (sgi as (SgiConAbs (x', n, k), loc)) :: rest => + if x = x' then + List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest) + else + traverse (sgi :: pre, rest) + | sgi :: rest => traverse (sgi :: pre, rest) + + val sgis = traverse ([], sgis) + in + (SgnConst sgis, loc) + end + | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" + +fun projectCon env {sgn, str, field} = + case #1 (hnormSgn env sgn) of SgnConst sgis => (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE | _ => NONE) sgis of NONE => NONE | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) - | SgnVar n => - let - val (_, sgn) = lookupSgnNamed env n - in - projectCon env {sgn = sgn, str = str, field = field} - end | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) - | SgnFun _ => NONE + | _ => NONE -fun projectVal env {sgn = (sgn, _), str, field} = - case sgn of +fun projectVal env {sgn, str, field} = + case #1 (hnormSgn env sgn) of SgnConst sgis => (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of NONE => NONE | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)) - | SgnVar n => - let - val (_, sgn) = lookupSgnNamed env n - in - projectVal env {sgn = sgn, str = str, field = field} - end | SgnError => SOME (CError, ErrorMsg.dummySpan) - | SgnFun _ => NONE + | _ => NONE -fun projectStr env {sgn = (sgn, _), str, field} = - case sgn of +fun projectStr env {sgn, str, field} = + case #1 (hnormSgn env sgn) of SgnConst sgis => (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of NONE => NONE | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) - | SgnVar n => - let - val (_, sgn) = lookupSgnNamed env n - in - projectStr env {sgn = sgn, str = str, field = field} - end | SgnError => SOME (SgnError, ErrorMsg.dummySpan) - | SgnFun _ => NONE + | _ => NONE val ktype = (KType, ErrorMsg.dummySpan) diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/elab_print.sml --- a/src/elab_print.sml Thu Jun 19 16:04:28 2008 -0400 +++ b/src/elab_print.sml Thu Jun 19 16:35:40 2008 -0400 @@ -323,6 +323,17 @@ string ":", space, p_sgn (E.pushStrNamedAs env x n sgn) sgn'] + | SgnWhere (sgn, x, c) => box [p_sgn env sgn, + space, + string "where", + space, + string "con", + space, + string x, + space, + string "=", + space, + p_con env c] | SgnError => string "" fun p_decl env ((d, _) : decl) = diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/elab_util.sml --- a/src/elab_util.sml Thu Jun 19 16:04:28 2008 -0400 +++ b/src/elab_util.sml Thu Jun 19 16:35:40 2008 -0400 @@ -370,6 +370,12 @@ S.map2 (sg (bind (ctx, Str (m, s1'))) s2, fn s2' => (SgnFun (m, n, s1', s2'), loc))) + | SgnWhere (sgn, x, c) => + S.bind2 (sg ctx sgn, + fn sgn' => + S.map2 (con ctx c, + fn c' => + (SgnWhere (sgn', x, c'), loc))) | SgnError => S.return2 sAll in sg diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/elaborate.sml --- a/src/elaborate.sml Thu Jun 19 16:04:28 2008 -0400 +++ b/src/elaborate.sml Thu Jun 19 16:35:40 2008 -0400 @@ -239,7 +239,7 @@ ((L'.CNamed n, loc), k)) | L.CVar (m1 :: ms, s) => (case E.lookupStr env m1 of - NONE => (conError env (UnboundStrInCon (loc, s)); + NONE => (conError env (UnboundStrInCon (loc, m1)); (cerror, kerror)) | SOME (n, sgn) => let @@ -824,7 +824,7 @@ | E.Named (n, t) => ((L'.ENamed n, loc), t)) | L.EVar (m1 :: ms, s) => (case E.lookupStr env m1 of - NONE => (expError env (UnboundStrInExp (loc, s)); + NONE => (expError env (UnboundStrInExp (loc, m1)); (eerror, cerror)) | SOME (n, sgn) => let @@ -969,6 +969,7 @@ | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error | SgnWrongForm of L'.sgn * L'.sgn + | UnWhereable of L'.sgn * string fun sgnError env err = case err of @@ -995,6 +996,10 @@ (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:"; eprefaces' [("Sig 1", p_sgn env sgn1), ("Sig 2", p_sgn env sgn2)]) + | UnWhereable (sgn, x) => + (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'"; + eprefaces' [("Signature", p_sgn env sgn), + ("Field", PD.string x)]) datatype str_error = UnboundStr of ErrorMsg.span * string @@ -1004,6 +1009,7 @@ UnboundStr (loc, s) => ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) +val hnormSgn = E.hnormSgn fun elabSgn_item ((sgi, loc), env) = let @@ -1110,6 +1116,25 @@ in (L'.SgnFun (m, n, dom', ran'), loc) end + | L.SgnWhere (sgn, x, c) => + let + val sgn' = elabSgn env sgn + val (c', ck) = elabCon env c + in + case #1 (hnormSgn env sgn') of + L'.SgnError => sgnerror + | L'.SgnConst sgis => + if List.exists (fn (L'.SgiConAbs (x, _, k), _) => + (unifyKinds k ck; + true) + | _ => false) sgis then + (L'.SgnWhere (sgn', x, c'), loc) + else + (sgnError env (UnWhereable (sgn', x)); + sgnerror) + | _ => (sgnError env (UnWhereable (sgn', x)); + sgnerror) + end fun sgiOfDecl (d, loc) = case d of @@ -1118,13 +1143,6 @@ | L'.DSgn _ => NONE | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc) -fun hnormSgn env (all as (sgn, _)) = - case sgn of - L'.SgnError => all - | L'.SgnVar n => hnormSgn env (#2 (E.lookupSgnNamed env n)) - | L'.SgnConst _ => all - | L'.SgnFun _ => all - fun subSgn env sgn1 (sgn2 as (_, loc2)) = case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of (L'.SgnError, _) => () @@ -1240,6 +1258,7 @@ (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) | x => x) sgis), #2 sgn) | L'.SgnFun _ => sgn + | L'.SgnWhere _ => sgn fun elabDecl ((d, loc), env) = let @@ -1384,7 +1403,7 @@ NONE => actual | SOME ran => let - val ran' = elabSgn env ran + val ran' = elabSgn env' ran in subSgn env' actual ran'; ran' diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/explify.sml --- a/src/explify.sml Thu Jun 19 16:04:28 2008 -0400 +++ b/src/explify.sml Thu Jun 19 16:35:40 2008 -0400 @@ -93,6 +93,7 @@ L.SgnConst sgis => (L'.SgnConst (map explifySgi sgis), loc) | L.SgnVar n => (L'.SgnVar n, loc) | L.SgnFun _ => raise Fail "Explify functor signature" + | L.SgnWhere _ => raise Fail "Explify where" | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) fun explifyDecl (d, loc : EM.span) = diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/lacweb.grm --- a/src/lacweb.grm Thu Jun 19 16:04:28 2008 -0400 +++ b/src/lacweb.grm Thu Jun 19 16:35:40 2008 -0400 @@ -44,7 +44,7 @@ | TYPE | NAME | ARROW | LARROW | DARROW | FN | PLUSPLUS | DOLLAR - | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR + | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE %nonterm file of decl list @@ -52,6 +52,7 @@ | decl of decl | sgn of sgn + | sgntm of sgn | sgi of sgn_item | sgis of sgn_item list @@ -110,12 +111,25 @@ | 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)) + | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN EQ str + (DStr (CSYMBOL1, NONE, + (StrFun (CSYMBOL2, sgn1, NONE, str), s (FUNCTORleft, strright))), + s (FUNCTORleft, strright)) + | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn EQ str + (DStr (CSYMBOL1, NONE, + (StrFun (CSYMBOL2, sgn1, SOME sgn2, str), s (FUNCTORleft, strright))), + s (FUNCTORleft, strright)) -sgn : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright)) - | CSYMBOL (SgnVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) +sgn : sgntm (sgntm) | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right)) +sgntm : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright)) + | CSYMBOL (SgnVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) + | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) + | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) + | LPAREN sgn RPAREN (sgn) + sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, kindright)) | LTYPE SYMBOL (SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))), s (LTYPEleft, SYMBOLright)) @@ -126,6 +140,10 @@ | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright)) | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)) + | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn + (SgiStr (CSYMBOL1, + (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))), + s (FUNCTORleft, sgn2right)) sgis : ([]) | sgi sgis (sgi :: sgis) diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/lacweb.lex --- a/src/lacweb.lex Thu Jun 19 16:04:28 2008 -0400 +++ b/src/lacweb.lex Thu Jun 19 16:35:40 2008 -0400 @@ -134,6 +134,7 @@ "sig" => (Tokens.SIG (yypos, yypos + size yytext)); "end" => (Tokens.END (yypos, yypos + size yytext)); "functor" => (Tokens.FUNCTOR (yypos, yypos + size yytext)); + "where" => (Tokens.WHERE (yypos, yypos + size yytext)); "Type" => (Tokens.TYPE (yypos, yypos + size yytext)); "Name" => (Tokens.NAME (yypos, yypos + size yytext)); diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/source.sml --- a/src/source.sml Thu Jun 19 16:04:28 2008 -0400 +++ b/src/source.sml Thu Jun 19 16:35:40 2008 -0400 @@ -72,6 +72,7 @@ SgnConst of sgn_item list | SgnVar of string | SgnFun of string * sgn * sgn + | SgnWhere of sgn * string * con withtype sgn_item = sgn_item' located and sgn = sgn' located diff -r 1405d8c26790 -r b3fbbc6cb1e5 src/source_print.sml --- a/src/source_print.sml Thu Jun 19 16:04:28 2008 -0400 +++ b/src/source_print.sml Thu Jun 19 16:35:40 2008 -0400 @@ -259,7 +259,18 @@ string ":", space, p_sgn sgn'] - + | SgnWhere (sgn, x, c) => box [p_sgn sgn, + space, + string "where", + space, + string "con", + space, + string x, + space, + string "=", + space, + p_con c] + fun p_decl ((d, _) : decl) = case d of DCon (x, NONE, c) => box [string "con", diff -r 1405d8c26790 -r b3fbbc6cb1e5 tests/functor.lac --- a/tests/functor.lac Thu Jun 19 16:04:28 2008 -0400 +++ b/tests/functor.lac Thu Jun 19 16:35:40 2008 -0400 @@ -9,11 +9,7 @@ val three : t end -signature F = functor (M : S) : T - -structure F = functor (M : S) : T => struct +functor F (M : S) : T where type t = M.t = struct type t = M.t val three = M.s (M.s (M.s M.z)) end - -structure F2 : F = F