Fix normalization of signatures that project signatures from other modules with multi-element paths (fixes #72)

4 files changed, 69 insertions, 41 deletions

diff --git a/src/elab_env.sig b/src/elab_env.sig
index cbc85cdd..47b31c08 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -96,6 +96,7 @@ signature ELAB_ENV = sig
 
     val pushStrNamed : env -> string -> Elab.sgn -> env * int
     val pushStrNamedAs : env -> string -> int -> Elab.sgn -> env
+    val pushStrNamedAs' : bool (* also enrich typeclass instances? *) -> env -> string -> int -> Elab.sgn -> env
     val lookupStrNamed : env -> int -> string * Elab.sgn
 
     val lookupStr : env -> string -> (int * Elab.sgn) option
@@ -123,6 +124,4 @@ signature ELAB_ENV = sig
     val patBinds : env -> Elab.pat -> env
     val patBindsN : Elab.pat -> int
 
-    exception Bad of Elab.con * Elab.con
-
 end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index cb08f348..8402bcba 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1097,14 +1097,21 @@ fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
              end)
       | _ => sgn
 
-fun sgnSubSgn x =
+fun projectStr env {sgn, str, field} =
+    case #1 (hnormSgn env sgn) of
+        SgnConst sgis =>
+        (case sgnSeek (fn SgiStr (_, x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
+             NONE => NONE
+           | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
+      | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
+      | _ => NONE
+
+and sgnSubSgn x =
     ElabUtil.Sgn.map {kind = id,
                       con = sgnS_con x,
                       sgn_item = id,
                       sgn = sgnS_sgn x}
 
-
-
 and projectSgn env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
@@ -1123,12 +1130,23 @@ and hnormSgn env (all as (sgn, loc)) =
       | SgnProj (m, ms, x) =>
         let
             val (_, sgn) = lookupStrNamed env m
+
+            fun doProjection (m1, NONE) = NONE
+              | doProjection (m1, SOME (str, sgn)) =
+                case projectStr env {str = str,
+                                     sgn = sgn,
+                                     field = m1} of
+                    NONE => NONE
+                  | SOME sgn' => SOME ((StrProj (str, m1), loc), sgn')
         in
-            case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms,
-                                 sgn = sgn,
-                                 field = x} of
-                NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
-              | SOME sgn => hnormSgn env sgn
+            case foldl doProjection (SOME ((StrVar m, loc), sgn)) ms of
+                NONE => raise Fail "ElabEnv.hnormSgn: pre-projectSgn failed"
+              | SOME (str, sgn) =>
+                case projectSgn env {str = str,
+                                     sgn = sgn,
+                                     field = x} of
+                    NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
+                  | SOME sgn => hnormSgn env sgn
         end
       | SgnWhere (sgn, ms, x, c) =>
 	let
@@ -1281,28 +1299,40 @@ fun enrichClasses env classes (m1, ms) sgn =
         end
       | _ => classes
 
-fun pushStrNamedAs (env : env) x n sgn =
-    {renameK = #renameK env,
-     relK = #relK env,
+and pushStrNamedAs' enrich (env : env) x n sgn =
+    let
+        val renameStr = SM.insert (#renameStr env, x, (n, sgn))
+        val str = IM.insert (#str env, n, (x, sgn))
+        fun newEnv classes =
+            {renameK = #renameK env,
+             relK = #relK env,
 
-     renameC = #renameC env,
-     relC = #relC env,
-     namedC = #namedC env,
+             renameC = #renameC env,
+             relC = #relC env,
+             namedC = #namedC env,
 
-     datatypes = #datatypes env,
-     constructors = #constructors env,
+             datatypes = #datatypes env,
+             constructors = #constructors env,
 
-     classes = enrichClasses env (#classes env) (n, []) sgn,
+             classes = classes,
 
-     renameE = #renameE env,
-     relE = #relE env,
-     namedE = #namedE env,
+             renameE = #renameE env,
+             relE = #relE env,
+             namedE = #namedE env,
 
-     renameSgn = #renameSgn env,
-     sgn = #sgn env,
+             renameSgn = #renameSgn env,
+             sgn = #sgn env,
+
+             renameStr = renameStr,
+             str = str}
+    in
+        if enrich then
+            newEnv (enrichClasses (newEnv (#classes env)) (#classes env) (n, []) sgn)
+        else
+            newEnv (#classes env)
+    end
 
-     renameStr = SM.insert (#renameStr env, x, (n, sgn)),
-     str = IM.insert (#str env, n, (x, sgn))}
+and pushStrNamedAs env = pushStrNamedAs' true env
 
 fun pushStrNamed env x sgn =
     let
@@ -1364,7 +1394,7 @@ fun sgiBinds env (sgi, loc) =
             env xncs
         end
       | SgiVal (x, n, t) => pushENamedAs env x n t
-      | SgiStr (_, x, n, sgn) => pushStrNamedAs env x n sgn
+      | SgiStr (_, x, n, sgn) => pushStrNamedAs' false env x n sgn
       | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
       | SgiConstraint _ => env
 
@@ -1375,15 +1405,6 @@ fun sgnSubCon x =
     ElabUtil.Con.map {kind = id,
                       con = sgnS_con x}
 
-fun projectStr env {sgn, str, field} =
-    case #1 (hnormSgn env sgn) of
-        SgnConst sgis =>
-        (case sgnSeek (fn SgiStr (_, x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
-             NONE => NONE
-           | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
-      | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
-      | _ => NONE
-
 fun chaseMpath env (n, ms) =
     let
         val (_, sgn) = lookupStrNamed env n
@@ -1642,8 +1663,8 @@ fun declBinds env (d, loc) =
       | DVal (x, n, t, _) => pushENamedAs env x n t
       | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
       | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
-      | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
-      | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
+      | DStr (x, n, sgn, _) => pushStrNamedAs' false env x n sgn
+      | DFfiStr (x, n, sgn) => pushStrNamedAs' false env x n sgn
       | DConstraint _ => env
       | DExport _ => env
       | DTable (tn, x, n, c, _, pc, _, cc) =>
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 06ea097f..8a6a651a 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -678,7 +678,7 @@ and p_sgn env (sgn, _) =
                                          space,
                                          string ":",
                                          space,
-                                         p_sgn (E.pushStrNamedAs env x n sgn) sgn']
+                                         p_sgn (E.pushStrNamedAs' false env x n sgn) sgn']
       | SgnWhere (sgn, ms, x, c) => box [p_sgn env sgn,
 					 space,
 					 string "where",
@@ -695,7 +695,7 @@ and p_sgn env (sgn, _) =
             val m1x = #1 (E.lookupStrNamed env m1)
                 handle E.UnboundNamed _ => "UNBOUND_SGN_" ^ Int.toString m1
                    
-            val m1s = if !debug then
+            val m1x = if !debug then
                           m1x ^ "__" ^ Int.toString m1
                       else
                           m1x
@@ -867,7 +867,7 @@ and p_str env (str, _) =
                                  string s]
       | StrFun (x, n, sgn, sgn', str) =>
         let
-            val env' = E.pushStrNamedAs env x n sgn
+            val env' = E.pushStrNamedAs' false env x n sgn
         in
             box [string "functor",
                  space,
diff --git a/tests/sigInModule.ur b/tests/sigInModule.ur
new file mode 100644
index 00000000..efb7b0fc
--- /dev/null
+++ b/tests/sigInModule.ur
@@ -0,0 +1,8 @@
+structure A = struct
+    signature S = sig
+        val x : int
+    end 
+end
+structure B : A.S = struct
+    val x = 42
+end