# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1213908204 14400
# Node ID d94c484337d06c165fed601f060e10768c16a708
# Parent  b3fbbc6cb1e59ff3f73f3f3ab46bd3f13a8f1c30
Subtyping for functor signatures

diff -r b3fbbc6cb1e5 -r d94c484337d0 src/elaborate.sml
--- 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))
 
diff -r b3fbbc6cb1e5 -r d94c484337d0 tests/functor.lac
--- 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*)