Fix opening and corifying of functors

3 files changed, 80 insertions, 56 deletions

diff --git a/src/corify.sml b/src/corify.sml
index d1b44384..0b0e9787 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -58,6 +58,8 @@ structure St : sig
 
     val empty : t
 
+    val debug : t -> unit
+
     val enter : t -> t
     val leave : t -> {outer : t, inner : t}
     val ffi : string -> L'.con SM.map -> t
@@ -80,16 +82,16 @@ structure St : sig
     val lookupStrById : t -> int -> t
     val lookupStrByName : string * t -> t
 
-    val bindFunctor : t -> string -> int -> int -> L.str -> t
-    val lookupFunctorById : t -> int -> int * L.str
-    val lookupFunctorByName : string * t -> int * L.str
+    val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
+    val lookupFunctorById : t -> int -> string * int * L.str
+    val lookupFunctorByName : string * t -> string * int * L.str
 end = struct
 
 datatype flattening =
          FNormal of {cons : int SM.map,
                      vals : int SM.map,
                      strs : flattening SM.map,
-                     funs : (int * L.str) SM.map}
+                     funs : (string * int * L.str) SM.map}
        | FFfi of {mod : string,
                   vals : L'.con SM.map}
                            
@@ -97,7 +99,7 @@ type t = {
      cons : int IM.map,
      vals : int IM.map,
      strs : flattening IM.map,
-     funs : (int * L.str) IM.map,
+     funs : (string * int * L.str) IM.map,
      current : flattening,
      nested : flattening list
 }
@@ -111,6 +113,13 @@ val empty = {
     nested = []
 }
 
+fun debug ({current = FNormal {cons, vals, strs, funs}, ...} : t) =
+    print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
+           ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
+           ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
+           ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
+  | debug _ = print "Not normal!\n"
+
 datatype core_con =
          CNormal of int
        | CFfi of string
@@ -243,17 +252,17 @@ fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) =
 
 fun bindFunctor ({cons, vals, strs, funs,
                   current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
-                x n na str =
+                x n xa na str =
     {cons = cons,
      vals = vals,
      strs = strs,
-     funs = IM.insert (funs, n, (na, str)),
+     funs = IM.insert (funs, n, (xa, na, str)),
      current = FNormal {cons = mcons,
                         vals = mvals,
                         strs = mstrs,
-                        funs = SM.insert (mfuns, x, (na, str))},
+                        funs = SM.insert (mfuns, x, (xa, na, str))},
      nested = nested}
-  | bindFunctor _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
+  | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
 
 fun lookupFunctorById ({funs, ...} : t) n =
     case IM.find (funs, n) of
@@ -412,8 +421,8 @@ fun corifyDecl ((d, loc : EM.span), st) =
         end
       | L.DSgn _ => ([], st)
 
-      | L.DStr (x, n, _, (L.StrFun (_, na, _, _, str), _)) =>
-        ([], St.bindFunctor st x n na str)
+      | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
+        ([], St.bindFunctor st x n xa na str)
 
       | L.DStr (x, n, _, str) =>
         let
@@ -514,7 +523,6 @@ fun corifyDecl ((d, loc : EM.span), st) =
                      end
              end
            | _ => raise Fail "Non-const signature for 'export'")
-                 
 
 and corifyStr ((str, _), st) =
     case str of
@@ -547,12 +555,12 @@ and corifyStr ((str, _), st) =
                   | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
                   | _ => raise Fail "Corify of fancy functor application [2]"
 
-            val (na, body) = unwind str1
+            val (xa, na, body) = unwind str1
 
-            val (ds1, {inner, outer}) = corifyStr (str2, st)
-            val (ds2, sts) = corifyStr (body, St.bindStr outer "ARG" na inner)
+            val (ds1, {inner = inner', outer}) = corifyStr (str2, st)
+            val (ds2, {inner, outer}) = corifyStr (body, St.bindStr outer xa na inner')
         in
-            (ds1 @ ds2, sts)
+            (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer})
         end
 
 fun maxName ds = foldl (fn ((d, _), n) =>
@@ -577,6 +585,7 @@ and maxNameStr (str, _) =
 fun corify ds =
     let
         val () = reset (maxName ds + 1)
+
         val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds
     in
         ds
diff --git a/src/elaborate.sml b/src/elaborate.sml
index a36a0224..b5794ecd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1988,41 +1988,42 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
                 case #1 (hnormSgn env sgn) of
                     L'.SgnConst sgis =>
                     let
-                        fun doOne (all as (sgi, _)) =
-                            case sgi of
-                                L'.SgiVal (x, n, t) =>
-                                (case hnormCon (env, denv) t of
-                                     ((L'.TFun (dom, ran), _), []) =>
-                                     (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
-                                          (((L'.TRecord domR, _), []),
-                                           ((L'.CApp (tf, arg3), _), [])) =>
-                                          (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
-                                               (((L'.CApp (tf, arg2), _), []),
-                                                (((L'.CRecord (_, []), _), []))) =>
-                                               (case (hnormCon (env, denv) tf) of
-                                                    ((L'.CApp (tf, arg1), _), []) =>
-                                                    (case (hnormCon (env, denv) tf,
-                                                           hnormCon (env, denv) domR,
-                                                           hnormCon (env, denv) arg2) of
-                                                         ((tf, []), (domR, []),
-                                                          ((L'.CRecord (_, []), _), [])) =>
-                                                         let
-                                                             val t = (L'.CApp (tf, arg1), loc)
-                                                             val t = (L'.CApp (t, arg2), loc)
-                                                             val t = (L'.CApp (t, arg3), loc)
-                                                         in
-                                                             (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
-                                                                                         t),
-                                                                                loc)), loc)
-                                                         end
-                                                       | _ => all)
-                                                  | _ => all)
-                                             | _ => all)
-                                        | _ => all)
-                                   | _ => all)
-                              | _ => all
+                        fun doOne (all as (sgi, _), env) =
+                            (case sgi of
+                                 L'.SgiVal (x, n, t) =>
+                                 (case hnormCon (env, denv) t of
+                                      ((L'.TFun (dom, ran), _), []) =>
+                                      (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
+                                           (((L'.TRecord domR, _), []),
+                                            ((L'.CApp (tf, arg3), _), [])) =>
+                                           (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
+                                                (((L'.CApp (tf, arg2), _), []),
+                                                 (((L'.CRecord (_, []), _), []))) =>
+                                                (case (hnormCon (env, denv) tf) of
+                                                     ((L'.CApp (tf, arg1), _), []) =>
+                                                     (case (hnormCon (env, denv) tf,
+                                                            hnormCon (env, denv) domR,
+                                                            hnormCon (env, denv) arg2) of
+                                                          ((tf, []), (domR, []),
+                                                           ((L'.CRecord (_, []), _), [])) =>
+                                                          let
+                                                              val t = (L'.CApp (tf, arg1), loc)
+                                                              val t = (L'.CApp (t, arg2), loc)
+                                                              val t = (L'.CApp (t, arg3), loc)
+                                                          in
+                                                              (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
+                                                                                          t),
+                                                                                 loc)), loc)
+                                                          end
+                                                        | _ => all)
+                                                   | _ => all)
+                                              | _ => all)
+                                         | _ => all)
+                                    | _ => all)
+                               | _ => all,
+                             E.sgiBinds env all)
                     in
-                        (L'.SgnConst (map doOne sgis), loc)
+                        (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
                     end
                   | _ => sgn
         in
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 095a6e24..2c4e7c89 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -100,7 +100,7 @@ fun p_con' par env (c, _) =
                       else
                           m1x
         in
-            p_list_sep (string ".") string (m1x :: ms @ [x])
+            p_list_sep (string ".") string (m1s :: ms @ [x])
         end
 
       | CApp (c1, c2) => parenIf par (box [p_con env c1,
@@ -155,7 +155,7 @@ and p_name env (all as (c, _)) =
         CName s => string s
       | _ => p_con env all
 
-fun p_exp' par env (e, _) =
+fun p_exp' par env (e, loc) =
     case e of
         EPrim p => Prim.p_t p
       | ERel n =>
@@ -171,13 +171,14 @@ fun p_exp' par env (e, _) =
       | EModProj (m1, ms, x) =>
         let
             val (m1x, sgn) = E.lookupStrNamed env m1
+                handle E.UnboundNamed _ => ("UNBOUND", (SgnConst [], loc))
 
             val m1s = if !debug then
                           m1x ^ "__" ^ Int.toString m1
                       else
                           m1x
         in
-            p_list_sep (string ".") string (m1x :: ms @ [x])
+            p_list_sep (string ".") string (m1s :: ms @ [x])
         end
                                          
       | EApp (e1, e2) => parenIf par (box [p_exp env e1,
@@ -294,7 +295,7 @@ fun p_sgn_item env (sgi, _) =
                                    space,
                                    p_sgn env sgn]
 
-and p_sgn env (sgn, _) =
+and p_sgn env (sgn, loc) =
     case sgn of
         SgnConst sgis => box [string "sig",
                               newline,
@@ -308,7 +309,8 @@ and p_sgn env (sgn, _) =
                               end,
                               newline,
                               string "end"]
-      | SgnVar n => string (#1 (E.lookupSgnNamed env n))
+      | SgnVar n => string ((#1 (E.lookupSgnNamed env n))
+                            handle E.UnboundNamed _ => "UNBOUND")
       | SgnFun (x, n, sgn, sgn') => box [string "functor",
                                          space,
                                          string "(",
@@ -336,6 +338,7 @@ and p_sgn env (sgn, _) =
       | SgnProj (m1, ms, x) =>
         let
             val (m1x, sgn) = E.lookupStrNamed env m1
+                handle E.UnboundNamed _ => ("UNBOUND", (SgnConst [], loc))
                              
             val m1s = if !debug then
                           m1x ^ "__" ^ Int.toString m1
@@ -424,7 +427,18 @@ and p_str env (str, _) =
                             p_file env ds,
                             newline,
                             string "end"]
-      | StrVar n => string (#1 (E.lookupStrNamed env n))
+      | StrVar n =>
+        let
+            val x = #1 (E.lookupStrNamed env n)
+                    handle E.UnboundNamed _ => "UNBOUND"
+
+            val s = if !debug then
+                        x ^ "__" ^ Int.toString n
+                    else
+                        x
+        in
+            string s
+        end
       | StrProj (str, s) => box [p_str env str,
                                  string ".",
                                  string s]