Mercurial > urweb
diff src/elaborate.sml @ 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 |
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))