summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-26 09:03:38 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-26 09:03:38 -0400
commit276b6129962c7ed8d742b70e9f941db0ebd8a5fa (patch)
treef4b73fd3148b3be6ac6fb546d1fd5b84aff7ff78
parentaabe8dd88a80467442826e460e6b01f0dad2fb4d (diff)
Proper subsignaturing for sub-signatures
-rw-r--r--src/elaborate.sml15
-rw-r--r--tests/subs_sig.lac7
-rw-r--r--tests/subs_sig.lig5
3 files changed, 24 insertions, 3 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index d2d468db..b4d13f0c 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1353,9 +1353,18 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
case sgi1 of
L'.SgiSgn (x', n1, sgn1) =>
if x = x' then
- (subSgn env sgn1 sgn2;
- subSgn env sgn2 sgn1;
- SOME env)
+ let
+ val () = subSgn env sgn1 sgn2
+ val () = subSgn env sgn2 sgn1
+
+ val env = E.pushSgnNamedAs env x n2 sgn2
+ val env = if n1 = n2 then
+ env
+ else
+ E.pushSgnNamedAs env x n1 sgn2
+ in
+ SOME env
+ end
else
NONE
| _ => NONE)
diff --git a/tests/subs_sig.lac b/tests/subs_sig.lac
new file mode 100644
index 00000000..934f6042
--- /dev/null
+++ b/tests/subs_sig.lac
@@ -0,0 +1,7 @@
+signature S = sig
+ type t
+end
+
+structure S : S = struct
+ type t = int
+end
diff --git a/tests/subs_sig.lig b/tests/subs_sig.lig
new file mode 100644
index 00000000..7a6ab8fc
--- /dev/null
+++ b/tests/subs_sig.lig
@@ -0,0 +1,5 @@
+signature S = sig
+ type t
+end
+
+structure S : S