Mercurial > urweb
changeset 43:d94c484337d0
Subtyping for functor signatures
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 19 Jun 2008 16:43:24 -0400 |
| parents | b3fbbc6cb1e5 |
| children | a9f3ce2d1b9b |
| files | src/elaborate.sml tests/functor.lac |
| diffstat | 2 files changed, 26 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Jun 19 16:35:40 2008 -0400 +++ b/src/elaborate.sml Thu Jun 19 16:43:24 2008 -0400 @@ -396,6 +396,17 @@ bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) | (ctx, _) => ctx} +fun subStrInSgn (m1, m2) = + U.Sgn.map {kind = fn k => k, + con = fn c as L'.CModProj (m1', ms, x) => + if m1 = m1' then + L'.CModProj (m2, ms, x) + else + c + | c => c, + sgn_item = fn sgi => sgi, + sgn = fn sgn => sgn} + type record_summary = { fields : (L'.con * L'.con) list, unifs : (L'.con * L'.con option ref) list, @@ -1241,8 +1252,16 @@ end | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => - (subSgn env dom2 dom1; - subSgn env ran1 ran2) + let + val ran1 = + if n1 = n2 then + ran1 + else + subStrInSgn (n1, n2) ran1 + in + subSgn env dom2 dom1; + subSgn (E.pushStrNamedAs env m2 n2 dom2) ran1 ran2 + end | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
--- a/tests/functor.lac Thu Jun 19 16:35:40 2008 -0400 +++ b/tests/functor.lac Thu Jun 19 16:43:24 2008 -0400 @@ -13,3 +13,8 @@ type t = M.t val three = M.s (M.s (M.s M.z)) end + +structure F2 : functor (M : S) : T where type t = M.t = F +structure F3 : functor (M : S) : T = F +(*structure F4 : functor (M : S) : sig type q end = F*) +(*structure F5 : functor (M : S) : T where type t = int = F*)