Simple signature matching

18 files changed, 565 insertions, 98 deletions

diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index c7263e3b..c49d934e 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -186,9 +186,9 @@ fun p_decl env ((d, _) : decl) =
 
 fun p_file env file =
     let
-        val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
-                                             (E.declBinds env d,
-                                              p_decl env d))
+        val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+                                             (p_decl env d,
+                                              E.declBinds env d))
                              env file
     in
         p_list_sep newline (fn x => x) pds
diff --git a/src/compiler.sig b/src/compiler.sig
index 3c9eea8b..65254873 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -32,7 +32,7 @@ signature COMPILER = sig
     val compile : string -> unit
 
     val parse : string -> Source.file option
-    val elaborate : ElabEnv.env -> string -> (ElabEnv.env * Elab.file) option
+    val elaborate : ElabEnv.env -> string -> (Elab.file * ElabEnv.env) option
     val corify : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
     val reduce : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
     val shake : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
diff --git a/src/compiler.sml b/src/compiler.sml
index 4276ed46..9a213ab6 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -70,7 +70,7 @@ fun elaborate env filename =
 fun corify eenv cenv filename =
     case elaborate eenv filename of
         NONE => NONE
-      | SOME (_, file) =>
+      | SOME (file, _) =>
         if ErrorMsg.anyErrors () then
             NONE
         else
@@ -131,7 +131,7 @@ fun testParse filename =
 fun testElaborate filename =
     (case elaborate ElabEnv.basis filename of
          NONE => print "Failed\n"
-       | SOME (_, file) =>
+       | SOME (file, _) =>
          (Print.print (ElabPrint.p_file ElabEnv.basis file);
           print "\n"))
     handle ElabEnv.UnboundNamed n =>
diff --git a/src/core_print.sml b/src/core_print.sml
index a219ac4d..42cbbc7a 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -258,9 +258,9 @@ fun p_decl env ((d, _) : decl) =
 
 fun p_file env file =
     let
-        val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
-                                             (E.declBinds env d,
-                                              p_decl env d))
+        val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+                                             (p_decl env d,
+                                              E.declBinds env d))
                              env file
     in
         p_list_sep newline (fn x => x) pds
diff --git a/src/corify.sml b/src/corify.sml
index f9433cff..a5309dec 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -83,6 +83,9 @@ fun corifyDecl (d, loc : EM.span) =
         L.DCon (x, n, k, c) => (L'.DCon (x, n, corifyKind k, corifyCon c), loc)
       | L.DVal (x, n, t, e) => (L'.DVal (x, n, corifyCon t, corifyExp e), loc)
 
+      | L.DSgn _ => raise Fail "Not ready to corify signature"
+      | L.DStr _ => raise Fail "Not ready to corify structure"
+
 val corify = map corifyDecl
 
 end
diff --git a/src/elab.sml b/src/elab.sml
index ac1b4224..14664c0f 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -80,12 +80,34 @@ datatype exp' =
 
 withtype exp = exp' located
 
+datatype sgn_item' =
+         SgiConAbs of string * int * kind
+       | SgiCon of string * int * kind * con
+       | SgiVal of string * int * con
+       | SgiStr of string * int * sgn
+
+and sgn' =
+    SgnConst of sgn_item list
+  | SgnVar of int
+  | SgnError
+
+withtype sgn_item = sgn_item' located
+and sgn = sgn' located
+
 datatype decl' =
          DCon of string * int * kind * con
        | DVal of string * int * con * exp
+       | DSgn of string * int * sgn
+       | DStr of string * int * sgn * str
 
-withtype decl = decl' located
+     and str' =
+         StrConst of decl list
+       | StrVar of int
+       | StrError
 
+withtype decl = decl' located
+     and str = str' located
+               
 type file = decl list
 
 end
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 8fe1da71..05badecf 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -58,9 +58,22 @@ signature ELAB_ENV = sig
     val pushENamed : env -> string -> Elab.con -> env * int
     val pushENamedAs : env -> string -> int -> Elab.con -> env
     val lookupENamed : env -> int -> string * Elab.con
-                                                 
+
     val lookupE : env -> string -> Elab.con var
 
+    val pushSgnNamed : env -> string -> Elab.sgn -> env * int
+    val pushSgnNamedAs : env -> string -> int -> Elab.sgn -> env
+    val lookupSgnNamed : env -> int -> string * Elab.sgn
+
+    val lookupSgn : env -> string -> (int * Elab.sgn) option
+
+    val pushStrNamed : env -> string -> Elab.sgn -> env * int
+    val pushStrNamedAs : env -> string -> int -> Elab.sgn -> env
+    val lookupStrNamed : env -> int -> string * Elab.sgn
+
+    val lookupStr : env -> string -> (int * Elab.sgn) option
+
     val declBinds : env -> Elab.decl -> env
+    val sgiBinds : env -> Elab.sgn_item -> env
 
 end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 78fa3daa..fd078e05 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -80,7 +80,13 @@ type env = {
 
      renameE : con var' SM.map,
      relE : (string * con) list,
-     namedE : (string * con) IM.map
+     namedE : (string * con) IM.map,
+
+     renameSgn : (int * sgn) SM.map,
+     sgn : (string * sgn) IM.map,
+
+     renameStr : (int * sgn) SM.map,
+     str : (string * sgn) IM.map
 }
 
 val namedCounter = ref 0
@@ -92,7 +98,13 @@ val empty = {
 
     renameE = SM.empty,
     relE = [],
-    namedE = IM.empty
+    namedE = IM.empty,
+
+    renameSgn = SM.empty,
+    sgn = IM.empty,
+
+    renameStr = SM.empty,
+    str = IM.empty
 }
 
 fun pushCRel (env : env) x k =
@@ -106,7 +118,14 @@ fun pushCRel (env : env) x k =
 
          renameE = #renameE env,
          relE = map (fn (x, c) => (x, lift c)) (#relE env),
-         namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)}
+         namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
+
+         renameSgn = #renameSgn env,
+         sgn = #sgn env,
+
+         renameStr = #renameStr env,
+         str = #str env
+        }
     end
 
 fun lookupCRel (env : env) n =
@@ -120,7 +139,13 @@ fun pushCNamedAs (env : env) x n k co =
 
      renameE = #renameE env,
      relE = #relE env,
-     namedE = #namedE env}
+     namedE = #namedE env,
+
+     renameSgn = #renameSgn env,
+     sgn = #sgn env,
+     
+     renameStr = #renameStr env,
+     str = #str env}
 
 fun pushCNamed env x k co =
     let
@@ -152,7 +177,13 @@ fun pushERel (env : env) x t =
 
          renameE = SM.insert (renameE, x, Rel' (0, t)),
          relE = (x, t) :: #relE env,
-         namedE = #namedE env}
+         namedE = #namedE env,
+
+         renameSgn = #renameSgn env,
+         sgn = #sgn env,
+
+         renameStr = #renameStr env,
+         str = #str env}
     end
 
 fun lookupERel (env : env) n =
@@ -166,7 +197,13 @@ fun pushENamedAs (env : env) x n t =
 
      renameE = SM.insert (#renameE env, x, Named' (n, t)),
      relE = #relE env,
-     namedE = IM.insert (#namedE env, n, (x, t))}
+     namedE = IM.insert (#namedE env, n, (x, t)),
+
+     renameSgn = #renameSgn env,
+     sgn = #sgn env,
+     
+     renameStr = #renameStr env,
+     str = #str env}
 
 fun pushENamed env x t =
     let
@@ -187,10 +224,80 @@ fun lookupE (env : env) x =
       | SOME (Rel' x) => Rel x
       | SOME (Named' x) => Named x
 
+fun pushSgnNamedAs (env : env) x n sgis =
+    {renameC = #renameC env,
+     relC = #relC env,
+     namedC = #namedC env,
+
+     renameE = #renameE env,
+     relE = #relE env,
+     namedE = #namedE env,
+
+     renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
+     sgn = IM.insert (#sgn env, n, (x, sgis)),
+     
+     renameStr = #renameStr env,
+     str = #str env}
+
+fun pushSgnNamed env x sgis =
+    let
+        val n = !namedCounter
+    in
+        namedCounter := n + 1;
+        (pushSgnNamedAs env x n sgis, n)
+    end
+
+fun lookupSgnNamed (env : env) n =
+    case IM.find (#sgn env, n) of
+        NONE => raise UnboundNamed n
+      | SOME x => x
+
+fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
+
+fun pushStrNamedAs (env : env) x n sgis =
+    {renameC = #renameC env,
+     relC = #relC env,
+     namedC = #namedC env,
+
+     renameE = #renameE env,
+     relE = #relE env,
+     namedE = #namedE env,
+
+     renameSgn = #renameSgn env,
+     sgn = #sgn env,
+
+     renameStr = SM.insert (#renameStr env, x, (n, sgis)),
+     str = IM.insert (#str env, n, (x, sgis))}
+
+fun pushStrNamed env x sgis =
+    let
+        val n = !namedCounter
+    in
+        namedCounter := n + 1;
+        (pushStrNamedAs env x n sgis, n)
+    end
+
+fun lookupStrNamed (env : env) n =
+    case IM.find (#str env, n) of
+        NONE => raise UnboundNamed n
+      | SOME x => x
+
+fun lookupStr (env : env) x = SM.find (#renameStr env, x)
+
 fun declBinds env (d, _) =
     case d of
         DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
       | DVal (x, n, t, _) => pushENamedAs env x n t
+      | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
+      | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
+
+fun sgiBinds env (sgi, _) =
+    case sgi of
+        SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
+      | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
+      | SgiVal (x, n, t) => pushENamedAs env x n t
+      | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
+
 
 val ktype = (KType, ErrorMsg.dummySpan)
 
diff --git a/src/elab_print.sig b/src/elab_print.sig
index 66ae8d43..49af2ded 100644
--- a/src/elab_print.sig
+++ b/src/elab_print.sig
@@ -33,6 +33,7 @@ signature ELAB_PRINT = sig
     val p_con : ElabEnv.env -> Elab.con Print.printer
     val p_exp : ElabEnv.env -> Elab.exp Print.printer
     val p_decl : ElabEnv.env -> Elab.decl Print.printer
+    val p_sgn_item : ElabEnv.env -> Elab.sgn_item Print.printer
     val p_file : ElabEnv.env -> Elab.file Print.printer
 
     val debug : bool ref
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 37648068..c07631a0 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -228,57 +228,119 @@ fun p_exp' par env (e, _) =
 
 and p_exp env = p_exp' false env
 
+fun p_named x n =
+    if !debug then
+        box [string x,
+             string "__",
+             string (Int.toString n)]
+    else
+        string x
+
+fun p_sgn_item env (sgi, _) =
+    case sgi of
+        SgiConAbs (x, n, k) => box [string "con",
+                                    space,
+                                    p_named x n,
+                                    space,
+                                    string "::",
+                                    space,
+                                    p_kind k]
+      | SgiCon (x, n, k, c) => box [string "con",
+                                    space,
+                                    p_named x n,
+                                    space,
+                                    string "::",
+                                    space,
+                                    p_kind k,
+                                    space,
+                                    string "=",
+                                    space,
+                                    p_con env c]
+      | SgiVal (x, n, c) => box [string "val",
+                                 space,
+                                 p_named x n,
+                                 space,
+                                 string ":",
+                                 space,
+                                 p_con env c]
+      | SgiStr (x, n, sgn) => box [string "structure",
+                                   space,
+                                   p_named x n,
+                                   space,
+                                   string ":",
+                                   space,
+                                   p_sgn env sgn]
+
+and p_sgn env (sgn, _) =
+    case sgn of
+        SgnConst sgis => box [string "sig",
+                              newline,
+                              p_list_sep newline (p_sgn_item env) sgis,
+                              newline,
+                              string "end"]
+      | SgnVar n => string (#1 (E.lookupSgnNamed env n))
+      | SgnError => string "<ERROR>"
+
 fun p_decl env ((d, _) : decl) =
     case d of
-        DCon (x, n, k, c) =>
-        let
-            val xp = if !debug then
-                         box [string x,
-                              string "__",
-                              string (Int.toString n)]
-                     else
-                         string x
-        in
-            box [string "con",
-                 space,
-                 xp,
-                 space,
-                 string "::",
-                 space,
-                 p_kind k,
-                 space,
-                 string "=",
-                 space,
-                 p_con env c]
-        end
-      | DVal (x, n, t, e) =>
-        let
-            val xp = if !debug then
-                         box [string x,
-                              string "__",
-                              string (Int.toString n)]
-                     else
-                         string x        
-        in
-            box [string "val",
-                 space,
-                 xp,
-                 space,
-                 string ":",
-                 space,
-                 p_con env t,
-                 space,
-                 string "=",
-                 space,
-                 p_exp env e]
-        end
+        DCon (x, n, k, c) => box [string "con",
+                                  space,
+                                  p_named x n,
+                                  space,
+                                  string "::",
+                                  space,
+                                  p_kind k,
+                                  space,
+                                  string "=",
+                                  space,
+                                  p_con env c]
+      | DVal (x, n, t, e) => box [string "val",
+                                  space,
+                                  p_named x n,
+                                  space,
+                                  string ":",
+                                  space,
+                                  p_con env t,
+                                  space,
+                                  string "=",
+                                  space,
+                                  p_exp env e]
+                             
+      | DSgn (x, n, sgn) => box [string "signature",
+                                 space,
+                                 p_named x n,
+                                 space,
+                                 string "=",
+                                 space,
+                                 p_sgn env sgn]
+      | DStr (x, n, sgn, str) => box [string "structure",
+                                      space,
+                                      p_named x n,
+                                      space,
+                                      string ":",
+                                      space,
+                                      p_sgn env sgn,
+                                      space,
+                                      string "=",
+                                      space,
+                                      p_str env str]
+
+and p_str env (str, _) =
+    case str of
+        StrConst ds => box [string "struct",
+                            newline,
+                            p_list_sep newline (p_decl env) ds,
+                            newline,
+                            string "end"]
+      | StrVar n => string (#1 (E.lookupStrNamed env n))
+      | StrError => string "<ERROR>"
 
 fun p_file env file =
     let
-        val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
-                                             (E.declBinds env d,
-                                              p_decl env d))
-                             env file
+        val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+                                             (p_decl env d,
+                                              E.declBinds env d))
+                                         env file
     in
         p_list_sep newline (fn x => x) pds
     end
diff --git a/src/elaborate.sig b/src/elaborate.sig
index 655df86c..1d388122 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -27,6 +27,6 @@
 
 signature ELABORATE = sig
 
-    val elabFile : ElabEnv.env -> Source.file -> ElabEnv.env * Elab.file
+    val elabFile : ElabEnv.env -> Source.file -> Elab.file * ElabEnv.env
 
 end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9b25f5ca..3cdb2d9f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -135,6 +135,8 @@ val ktype_record = (L'.KRecord ktype, dummy)
 val cerror = (L'.CError, dummy)
 val kerror = (L'.KError, dummy)
 val eerror = (L'.EError, dummy)
+val sgnerror = (L'.SgnError, dummy)
+val strerror = (L'.StrError, dummy)
 
 local
     val count = ref 0
@@ -864,7 +866,220 @@ fun declError env err =
         (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression";
          eprefaces' [("Expression", p_exp env e)])
 
-fun elabDecl env (d, loc) =
+datatype sgn_error =
+         UnboundSgn of ErrorMsg.span * string
+       | UnmatchedSgi of L'.sgn_item
+       | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
+       | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
+
+fun sgnError env err =
+    case err of
+        UnboundSgn (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
+      | UnmatchedSgi (sgi as (_, loc)) =>
+        (ErrorMsg.errorAt loc "Unmatched signature item";
+         eprefaces' [("Item", p_sgn_item env sgi)])
+      | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
+        (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
+         eprefaces' [("Item 1", p_sgn_item env sgi1),
+                     ("Item 2", p_sgn_item env sgi2),
+                     ("Kind 1", p_kind k1),
+                     ("Kind 2", p_kind k2)];
+         kunifyError kerr)
+      | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
+        (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
+         eprefaces' [("Item 1", p_sgn_item env sgi1),
+                     ("Item 2", p_sgn_item env sgi2),
+                     ("Con 1", p_con env c1),
+                     ("Con 2", p_con env c2)];
+         cunifyError env cerr)
+
+datatype str_error =
+         UnboundStr of ErrorMsg.span * string
+
+fun strError env err =
+    case err of
+        UnboundStr (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
+
+
+fun elabSgn_item ((sgi, loc), env) =
+    let
+        
+    in
+        resetKunif ();
+        resetCunif ();
+        case sgi of
+            L.SgiConAbs (x, k) =>
+            let
+                val k' = elabKind k
+
+                val (env', n) = E.pushCNamed env x k' NONE
+            in
+                if ErrorMsg.anyErrors () then
+                    ()
+                else (
+                    if kunifsInKind k' then
+                        declError env (KunifsRemainKind (loc, k'))
+                    else
+                        ()
+                    );
+
+                ((L'.SgiConAbs (x, n, k'), loc), env')
+            end
+
+          | L.SgiCon (x, ko, c) =>
+            let
+                val k' = case ko of
+                             NONE => kunif ()
+                           | SOME k => elabKind k
+
+                val (c', ck) = elabCon env c
+                val (env', n) = E.pushCNamed env x k' (SOME c')
+            in
+                checkKind env c' ck k';
+
+                if ErrorMsg.anyErrors () then
+                    ()
+                else (
+                    if kunifsInKind k' then
+                        declError env (KunifsRemainKind (loc, k'))
+                    else
+                        ();
+
+                    if kunifsInCon c' then
+                        declError env (KunifsRemainCon (loc, c'))
+                    else
+                        ()
+                    );
+
+                ((L'.SgiCon (x, n, k', c'), loc), env')
+            end
+
+          | L.SgiVal (x, c) =>
+            let
+                val (c', ck) = elabCon env c
+
+                val (env', n) = E.pushENamed env x c'
+            in
+                unifyKinds ck ktype;
+
+                if ErrorMsg.anyErrors () then
+                    ()
+                else (
+                    if kunifsInCon c' then
+                        declError env (KunifsRemainCon (loc, c'))
+                    else
+                        ()
+                    );
+
+                ((L'.SgiVal (x, n, c'), loc), env')
+            end
+
+          | L.SgiStr (x, sgn) =>
+            let
+                val sgn' = elabSgn env sgn
+                val (env', n) = E.pushStrNamed env x sgn'
+            in
+                ((L'.SgiStr (x, n, sgn'), loc), env')
+            end
+            
+    end
+
+and elabSgn env (sgn, loc) =
+    case sgn of
+        L.SgnConst sgis =>
+        let
+            val (sgis', _) = ListUtil.foldlMap elabSgn_item env sgis
+        in
+            (L'.SgnConst sgis', loc)
+        end
+      | L.SgnVar x =>
+        (case E.lookupSgn env x of
+             NONE =>
+             (sgnError env (UnboundSgn (loc, x));
+              (L'.SgnError, loc))
+           | SOME (n, sgis) => (L'.SgnVar n, loc))
+
+fun sgiOfDecl (d, loc) =
+    case d of
+        L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
+      | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
+      | L'.DSgn _ => NONE
+      | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
+
+fun subSgn env (all1 as (sgn1, _)) (all2 as (sgn2, loc2)) =
+    case (sgn1, sgn2) of
+        (L'.SgnError, _) => ()
+      | (_, L'.SgnError) => ()
+
+      | (L'.SgnVar n, _) =>
+        subSgn env (#2 (E.lookupSgnNamed env n)) all2
+      | (_, L'.SgnVar n) =>
+        subSgn env all1 (#2 (E.lookupSgnNamed env n))
+
+      | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
+        let
+            fun folder (sgi2All as (sgi, _), env) =
+                let
+                    fun seek p =
+                        let
+                            fun seek env ls =
+                                case ls of
+                                    [] => (sgnError env (UnmatchedSgi sgi2All);
+                                           env)
+                                  | h :: t =>
+                                    case p h of
+                                        NONE => seek (E.sgiBinds env h) t
+                                      | SOME env => env
+                        in
+                            seek env sgis1
+                        end
+                in
+                    case sgi of
+                        L'.SgiConAbs (x, n2, k2) =>
+                        seek (fn sgi1All as (sgi1, _) =>
+                                 let
+                                     fun found (x, n1, k1, co1) =
+                                         let
+                                             val () = unifyKinds k1 k2
+                                                 handle KUnify (k1, k2, err) =>
+                                                        sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+                                             val env = E.pushCNamedAs env x n1 k1 co1
+                                         in
+                                             SOME (if n1 = n2 then
+                                                       env
+                                                   else
+                                                       E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)))
+                                         end
+                                 in
+                                     case sgi1 of
+                                         L'.SgiConAbs (x, n1, k1) => found (x, n1, k1, NONE)
+                                       | L'.SgiCon (x, n1, k1, c1) => found (x, n1, k1, SOME c1)
+                                       | _ => NONE
+                                 end)
+
+                      | L'.SgiCon (x, n2, k2, c2) =>
+                        seek (fn sgi1All as (sgi1, _) =>
+                                 case sgi1 of
+                                     L'.SgiCon (x, n1, k1, c1) =>
+                                     let
+                                         val () = unifyCons env c1 c2
+                                             handle CUnify (c1, c2, err) =>
+                                                    sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err))
+                                     in
+                                         SOME (E.pushCNamedAs env x n2 k2 (SOME c2))
+                                     end
+                                   | _ => NONE)
+
+                      | _ => raise Fail "Not ready for more sig matching"
+                end
+        in
+            ignore (foldl folder env sgis2)
+        end
+                                                               
+
+fun elabDecl ((d, loc), env) =
     let
         
     in
@@ -896,8 +1111,7 @@ fun elabDecl env (d, loc) =
                         ()
                     );
 
-                (env',
-                 (L'.DCon (x, n, k', c'), loc))
+                ((L'.DCon (x, n, k', c'), loc), env')
             end
           | L.DVal (x, co, e) =>
             let
@@ -933,15 +1147,50 @@ fun elabDecl env (d, loc) =
                     else
                         ());
 
-                (env',
-                 (L'.DVal (x, n, c', e'), loc))
+                ((L'.DVal (x, n, c', e'), loc), env')
             end
 
-          | L.DSgn _ => raise Fail "Not ready to elaborate signature"
-          | L.DStr _ => raise Fail "Not ready to elaborate structure"
+          | L.DSgn (x, sgn) =>
+            let
+                val sgn' = elabSgn env sgn
+                val (env', n) = E.pushSgnNamed env x sgn'
+            in
+                ((L'.DSgn (x, n, sgn'), loc), env')
+            end
+
+          | L.DStr (x, sgno, str) =>
+            let
+                val formal = Option.map (elabSgn env) sgno
+                val (str', actual) = elabStr env str
+
+                val sgn' = case formal of
+                               NONE => actual
+                             | SOME formal =>
+                               (subSgn env actual formal;
+                                formal)
+
+                val (env', n) = E.pushStrNamed env x sgn'
+            in
+                ((L'.DStr (x, n, sgn', str'), loc), env')
+            end
     end
 
-fun elabFile env ds =
-    ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds
+and elabStr env (str, loc) =
+    case str of
+        L.StrConst ds =>
+        let
+            val (ds', env') = ListUtil.foldlMap elabDecl env ds
+            val sgis = List.mapPartial sgiOfDecl ds'
+        in
+            ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
+        end
+      | L.StrVar x =>
+        (case E.lookupStr env x of
+             NONE =>
+             (strError env (UnboundStr (loc, x));
+              (strerror, sgnerror))
+           | SOME (n, sgn) => ((L'.StrVar n, loc), sgn))
+
+val elabFile = ListUtil.foldlMap elabDecl
 
 end
diff --git a/src/flat_print.sml b/src/flat_print.sml
index 612291c0..08008e9a 100644
--- a/src/flat_print.sml
+++ b/src/flat_print.sml
@@ -187,9 +187,9 @@ fun p_decl env ((d, _) : decl) =
 
 fun p_file env file =
     let
-        val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
-                                             (E.declBinds env d,
-                                              p_decl env d))
+        val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+                                             (p_decl env d,
+                                              E.declBinds env d))
                              env file
     in
         p_list_sep newline (fn x => x) pds
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 2170c1d5..c5ce7ae8 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -129,7 +129,7 @@ realconst = [0-9]+\.[0-9]*;
 <INITIAL> "fn"        => (Tokens.FN (yypos, yypos + size yytext));
 
 <INITIAL> "structure" => (Tokens.STRUCTURE (yypos, yypos + size yytext));
-<INITIAL> "signature" => (Tokens.STRUCTURE (yypos, yypos + size yytext));
+<INITIAL> "signature" => (Tokens.SIGNATURE (yypos, yypos + size yytext));
 <INITIAL> "struct"    => (Tokens.STRUCT (yypos, yypos + size yytext));
 <INITIAL> "sig"       => (Tokens.SIG (yypos, yypos + size yytext));
 <INITIAL> "end"       => (Tokens.END (yypos, yypos + size yytext));
diff --git a/src/list_util.sig b/src/list_util.sig
index 8185a28b..62013d25 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -27,9 +27,6 @@
 
 signature LIST_UTIL = sig
 
-    val mapfoldl : ('data1 * 'state -> 'state * 'data2) -> 'state -> 'data1 list
-                   -> 'state * 'data2 list
-
     val mapfold : ('data, 'state, 'abort) Search.mapfolder
                   -> ('data list, 'state, 'abort) Search.mapfolder
 
diff --git a/src/list_util.sml b/src/list_util.sml
index aed2cdf0..7d3f8333 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -27,21 +27,6 @@
 
 structure ListUtil :> LIST_UTIL = struct
 
-fun mapfoldl f i =
-    let
-        fun mf s ls' ls =
-            case ls of
-                nil => (s, rev ls')
-              | h :: t =>
-                let
-                    val (s, h') = f (h, s)
-                in
-                    mf s (h' :: ls') t
-                end
-    in
-        mf i []
-    end
-
 structure S = Search
 
 fun mapfold f =
diff --git a/src/mono_print.sml b/src/mono_print.sml
index 6b259b7c..885b2d34 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -130,9 +130,9 @@ fun p_decl env ((d, _) : decl) =
 
 fun p_file env file =
     let
-        val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
-                                             (E.declBinds env d,
-                                              p_decl env d))
+        val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+                                             (p_decl env d,
+                                              E.declBinds env d))
                              env file
     in
         p_list_sep newline (fn x => x) pds
diff --git a/tests/modules.lac b/tests/modules.lac
new file mode 100644
index 00000000..9d5fbc90
--- /dev/null
+++ b/tests/modules.lac
@@ -0,0 +1,28 @@
+signature A = sig end
+structure A = struct end
+structure Ao : A = A
+
+
+structure B = struct
+        type t = int
+end
+structure Bo0 : sig end = B
+structure BoA : A = B
+
+signature B1 = sig
+        type t
+end
+structure Bo1 : B1 = B
+(*structure AoB1 : B1 = A*)
+
+signature B2 = sig
+        type t = int
+end
+structure Bo2 : B2 = B
+
+
+structure C = struct
+        type t = float
+end
+structure CoB1 : B1 = C
+(*structure CoB2 : B2 = C*)