summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-19 16:43:24 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-19 16:43:24 -0400
commit9386a9382eda9bd19e99c80057398c593aaf812b (patch)
treef0e592614606c0b04edbb8c56bba0765bf05b872 /src/elaborate.sml
parente542e7ba2106c5763006e88d90b6834fe9221b85 (diff)
Subtyping for functor signatures
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml23
1 files changed, 21 insertions, 2 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9c96060d..5e0ba5fc 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -396,6 +396,17 @@ val subConInCon =
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 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
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))