Mercurial > urweb
changeset 75:88ffb3d61817
Folding through a functor
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 26 Jun 2008 12:35:26 -0400 |
parents | 144d082b47ae |
children | 522f4bd3955e |
files | src/elaborate.sml tests/foldm.lac |
diffstat | 2 files changed, 45 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Jun 26 12:12:06 2008 -0400 +++ b/src/elaborate.sml Thu Jun 26 12:35:26 2008 -0400 @@ -1082,6 +1082,7 @@ | 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 + | WhereWrongKind of L'.kind * L'.kind * kunify_error | NotIncludable of L'.sgn | DuplicateCon of ErrorMsg.span * string | DuplicateVal of ErrorMsg.span * string @@ -1117,6 +1118,11 @@ (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'"; eprefaces' [("Signature", p_sgn env sgn), ("Field", PD.string x)]) + | WhereWrongKind (k1, k2, kerr) => + (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'"; + eprefaces' [("Have", p_kind k1), + ("Need", p_kind k2)]; + kunifyError kerr) | NotIncludable sgn => (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'"; eprefaces' [("Signature", p_sgn env sgn)]) @@ -1134,6 +1140,7 @@ | NotFunctor of L'.sgn | FunctorRebind of ErrorMsg.span | UnOpenable of L'.sgn + | NotType of L'.kind * (L'.kind * L'.kind * kunify_error) fun strError env err = case err of @@ -1147,6 +1154,12 @@ | UnOpenable sgn => (ErrorMsg.errorAt (#2 sgn) "Un-openable structure"; eprefaces' [("Signature", p_sgn env sgn)]) + | NotType (k, (k1, k2, ue)) => + (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'"; + eprefaces' [("Kind", p_kind k), + ("Subkind 1", p_kind k1), + ("Subkind 2", p_kind k2)]; + kunifyError ue) val hnormSgn = E.hnormSgn @@ -1209,7 +1222,8 @@ val (env', n) = E.pushENamed env x c' in - unifyKinds ck ktype; + (unifyKinds ck ktype + handle KUnify ue => strError env (NotType (ck, ue))); if ErrorMsg.anyErrors () then () @@ -1316,8 +1330,10 @@ case #1 (hnormSgn env sgn') of L'.SgnError => sgnerror | L'.SgnConst sgis => - if List.exists (fn (L'.SgiConAbs (x, _, k), _) => - (unifyKinds k ck; + if List.exists (fn (L'.SgiConAbs (x', _, k), _) => + x' = x andalso + (unifyKinds k ck + handle KUnify x => sgnError env (WhereWrongKind x); true) | _ => false) sgis then (L'.SgnWhere (sgn', x, c'), loc)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/foldm.lac Thu Jun 26 12:35:26 2008 -0400 @@ -0,0 +1,26 @@ +con currier = fold (fn nm => fn t => fn acc => t -> acc) {} + +signature S = sig + type t + val x : t + + con rs :: {Type} + val create : currier rs -> t +end + +functor Currier (M : sig con rs :: {Type} end) : S where con rs = M.rs = struct + val currier : rs :: {Type} -> currier rs = + fold [currier] (fn nm :: Name => fn t :: Type => fn rest :: {Type} => fn acc => fn x : t => acc) {} + + type t = currier M.rs + val x = currier [M.rs] + + con rs = M.rs + val create : t -> t = fn x => x +end + +structure ChefsSpecial = Currier(struct + con rs = [A = int, B = float] +end) + +val main = ChefsSpecial.x