Elaborating module projection

14 files changed, 451 insertions, 29 deletions

diff --git a/src/corify.sml b/src/corify.sml
index a5309dec..61634a5d 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -50,6 +50,8 @@ fun corifyCon (c, loc) =
 
       | L.CRel n => (L'.CRel n, loc)
       | L.CNamed n => (L'.CNamed n, loc)
+      | L.CModProj _ => raise Fail "Corify CModProj"
+
       | L.CApp (c1, c2) => (L'.CApp (corifyCon c1, corifyCon c2), loc)
       | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon c), loc)
 
@@ -67,6 +69,7 @@ fun corifyExp (e, loc) =
         L.EPrim p => (L'.EPrim p, loc)
       | L.ERel n => (L'.ERel n, loc)
       | L.ENamed n => (L'.ENamed n, loc)
+      | L.EModProj _ => raise Fail "Corify EModProj"
       | L.EApp (e1, e2) => (L'.EApp (corifyExp e1, corifyExp e2), loc)
       | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon dom, corifyCon ran, corifyExp e1), loc)
       | L.ECApp (e1, c) => (L'.ECApp (corifyExp e1, corifyCon c), loc)
diff --git a/src/elab.sml b/src/elab.sml
index 14664c0f..da64febf 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -51,6 +51,7 @@ datatype con' =
 
        | CRel of int
        | CNamed of int
+       | CModProj of int * string list * string
        | CApp of con * con
        | CAbs of string * kind * con
 
@@ -68,6 +69,7 @@ datatype exp' =
          EPrim of Prim.t
        | ERel of int
        | ENamed of int
+       | EModProj of int * string list * string
        | EApp of exp * exp
        | EAbs of string * con * con * exp
        | ECApp of exp * con
@@ -103,6 +105,7 @@ datatype decl' =
      and str' =
          StrConst of decl list
        | StrVar of int
+       | StrProj of str * string
        | StrError
 
 withtype decl = decl' located
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 05badecf..89d5fb60 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -76,4 +76,8 @@ signature ELAB_ENV = sig
     val declBinds : env -> Elab.decl -> env
     val sgiBinds : env -> Elab.sgn_item -> env
 
+    val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option
+    val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option
+    val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
+
 end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index fd078e05..b10882a7 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -298,6 +298,113 @@ fun sgiBinds env (sgi, _) =
       | SgiVal (x, n, t) => pushENamedAs env x n t
       | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
 
+fun sgnSeek f sgis =
+    let
+        fun seek (sgis, strs, cons) =
+            case sgis of
+                [] => NONE
+              | (sgi, _) :: sgis =>
+                case f sgi of
+                    SOME v => SOME (v, (strs, cons))
+                    | NONE =>
+                      case sgi of
+                          SgiConAbs (x, n, _) => seek (sgis, strs, IM.insert (cons, n, x))
+                        | SgiCon (x, n, _, _) => seek (sgis, strs, IM.insert (cons, n, x))
+                        | SgiVal _ => seek (sgis, strs, cons)
+                        | SgiStr (x, n, _) => seek (sgis, IM.insert (strs, n, x), cons)
+    in
+        seek (sgis, IM.empty, IM.empty)
+    end
+
+fun id x = x
+
+fun unravelStr (str, _) =
+    case str of
+        StrVar x => (x, [])
+      | StrProj (str, m) =>
+        let
+            val (x, ms) = unravelStr str
+        in
+            (x, ms @ [m])
+        end
+      | _ => raise Fail "unravelStr"
+
+fun sgnS_con (str, (strs, cons)) c =
+    case c of
+        CModProj (m1, ms, x) =>
+        (case IM.find (strs, m1) of
+             NONE => c
+           | SOME m1x =>
+             let
+                 val (m1, ms') = unravelStr str
+             in
+                 CModProj (m1, ms' @ m1x :: ms, x)
+             end)
+      | CNamed n =>
+        (case IM.find (cons, n) of
+             NONE => c
+           | SOME nx =>
+             let
+                 val (m1, ms) = unravelStr str
+             in
+                 CModProj (m1, ms, nx)
+             end)
+      | _ => c
+
+fun sgnSubCon (str, (strs, cons)) =
+    ElabUtil.Con.map {kind = id,
+                      con = sgnS_con (str, (strs, cons))}
+
+fun sgnSubSgn (str, (strs, cons)) =
+    ElabUtil.Sgn.map {kind = id,
+                      con = sgnS_con (str, (strs, cons)),
+                      sgn_item = id,
+                      sgn = id}
+
+fun projectCon env {sgn = (sgn, _), str, field} =
+    case sgn of
+        SgnConst sgis =>
+        (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
+                        | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
+                        | _ => NONE) sgis of
+             NONE => NONE
+           | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
+      | SgnVar n =>
+        let
+            val (_, sgn) = lookupSgnNamed env n
+        in
+            projectCon env {sgn = sgn, str = str, field = field}
+        end
+      | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
+
+fun projectVal env {sgn = (sgn, _), str, field} =
+    case sgn of
+        SgnConst sgis =>
+        (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of
+             NONE => NONE
+           | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
+      | SgnVar n =>
+        let
+            val (_, sgn) = lookupSgnNamed env n
+        in
+            projectVal env {sgn = sgn, str = str, field = field}
+        end
+      | SgnError => SOME (CError, ErrorMsg.dummySpan)
+
+fun projectStr env {sgn = (sgn, _), str, field} =
+    case 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))
+      | SgnVar n =>
+        let
+            val (_, sgn) = lookupSgnNamed env n
+        in
+            projectStr env {sgn = sgn, str = str, field = field}
+        end
+      | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
+
 
 val ktype = (KType, ErrorMsg.dummySpan)
 
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 435ea13d..b214d5d4 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -93,10 +93,22 @@ fun p_con' par env (c, _) =
         else
             string (#1 (E.lookupCRel env n))
       | CNamed n =>
-        if !debug then
-            string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
-        else
-            string (#1 (E.lookupCNamed env n))
+        ((if !debug then
+              string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
+          else
+              string (#1 (E.lookupCNamed env n)))
+         handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
+      | CModProj (m1, ms, x) =>
+        let
+            val (m1x, sgn) = E.lookupStrNamed env m1
+
+            val m1s = if !debug then
+                          m1x ^ "__" ^ Int.toString m1
+                      else
+                          m1x
+        in
+            p_list_sep (string ".") string (m1x :: ms @ [x])
+        end
 
       | CApp (c1, c2) => parenIf par (box [p_con env c1,
                                            space,
@@ -167,6 +179,18 @@ fun p_exp' par env (e, _) =
             string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
         else
             string (#1 (E.lookupENamed env n))
+      | EModProj (m1, ms, x) =>
+        let
+            val (m1x, sgn) = E.lookupStrNamed env m1
+
+            val m1s = if !debug then
+                          m1x ^ "__" ^ Int.toString m1
+                      else
+                          m1x
+        in
+            p_list_sep (string ".") string (m1x :: ms @ [x])
+        end
+                                         
       | EApp (e1, e2) => parenIf par (box [p_exp env e1,
                                            space,
                                            p_exp' true env e2])
@@ -340,6 +364,9 @@ and p_str env (str, _) =
                             newline,
                             string "end"]
       | StrVar n => string (#1 (E.lookupStrNamed env n))
+      | StrProj (str, s) => box [p_str env str,
+                                 string ".",
+                                 string s]
       | StrError => string "<ERROR>"
 
 and p_file env file =
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 80d04465..0917d126 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -50,6 +50,9 @@ structure Con : sig
                 con : 'context -> Elab.con' -> Elab.con',
                 bind : 'context * binder -> 'context}
                -> 'context -> (Elab.con -> Elab.con)
+    val map : {kind : Elab.kind' -> Elab.kind',
+               con : Elab.con' -> Elab.con'}
+              -> Elab.con -> Elab.con
     val exists : {kind : Elab.kind' -> bool,
                   con : Elab.con' -> bool} -> Elab.con -> bool
 end
@@ -75,4 +78,32 @@ structure Exp : sig
                   exp : Elab.exp' -> bool} -> Elab.exp -> bool
 end
 
+structure Sgn : sig
+    datatype binder =
+             RelC of string * Elab.kind
+           | NamedC of string * Elab.kind
+           | Str of string * Elab.sgn
+
+    val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+                    con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
+                    sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
+                    sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
+                    bind : 'context * binder -> 'context}
+                   -> ('context, Elab.sgn, 'state, 'abort) Search.mapfolderB
+
+
+    val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+                   con : (Elab.con', 'state, 'abort) Search.mapfolder,
+                   sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder,
+                   sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder}
+                  -> (Elab.sgn, 'state, 'abort) Search.mapfolder
+
+    val map : {kind : Elab.kind' -> Elab.kind',
+               con : Elab.con' -> Elab.con',
+               sgn_item : Elab.sgn_item' -> Elab.sgn_item',
+               sgn : Elab.sgn' -> Elab.sgn'}
+              -> Elab.sgn -> Elab.sgn
+
+end
+
 end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 39020652..24e772d6 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -109,6 +109,7 @@ fun mapfoldB {kind = fk, con = fc, bind} =
 
               | CRel _ => S.return2 cAll
               | CNamed _ => S.return2 cAll
+              | CModProj _ => S.return2 cAll
               | CApp (c1, c2) =>
                 S.bind2 (mfc ctx c1,
                       fn c1' =>
@@ -160,7 +161,13 @@ fun mapB {kind, con, bind} ctx c =
                    con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
                    bind = bind} ctx c () of
         S.Continue (c, ()) => c
-      | S.Return _ => raise Fail "Con.mapB: Impossible"
+      | S.Return _ => raise Fail "ElabUtil.Con.mapB: Impossible"
+
+fun map {kind, con} s =
+    case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
+                  con = fn c => fn () => S.Continue (con c, ())} s () of
+        S.Return () => raise Fail "ElabUtil.Con.map: Impossible"
+      | S.Continue (s, ()) => s
 
 fun exists {kind, con} k =
     case mapfold {kind = fn k => fn () =>
@@ -208,6 +215,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                 EPrim _ => S.return2 eAll
               | ERel _ => S.return2 eAll
               | ENamed _ => S.return2 eAll
+              | EModProj _ => S.return2 eAll
               | EApp (e1, e2) =>
                 S.bind2 (mfe ctx e1,
                       fn e1' =>
@@ -291,4 +299,91 @@ fun exists {kind, con, exp} k =
 
 end
 
+structure Sgn = struct
+
+datatype binder =
+         RelC of string * Elab.kind
+       | NamedC of string * Elab.kind
+       | Str of string * Elab.sgn
+
+fun mapfoldB {kind, con, sgn_item, sgn, bind} =
+    let
+        fun bind' (ctx, b) =
+            let
+                val b' = case b of
+                             Con.Rel x => RelC x
+                           | Con.Named x => NamedC x
+            in
+                bind (ctx, b')
+            end
+        val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
+
+        val kind = Kind.mapfold kind
+
+        fun sgi ctx si acc =
+            S.bindP (sgi' ctx si acc, sgn_item ctx)
+
+        and sgi' ctx (si, loc) =
+            case si of
+                SgiConAbs (x, n, k) =>
+                S.map2 (kind k,
+                     fn k' =>
+                        (SgiConAbs (x, n, k'), loc))
+              | SgiCon (x, n, k, c) =>
+                S.bind2 (kind k,
+                     fn k' =>
+                        S.map2 (con ctx c,
+                             fn c' =>
+                                (SgiCon (x, n, k', c'), loc)))
+              | SgiVal (x, n, c) =>
+                S.map2 (con ctx c,
+                     fn c' =>
+                        (SgiVal (x, n, c'), loc))
+              | SgiStr (x, n, s) =>
+                S.map2 (sg ctx s,
+                     fn s' =>
+                        (SgiStr (x, n, s'), loc))
+
+        and sg ctx s acc =
+            S.bindP (sg' ctx s acc, sgn ctx)
+
+        and sg' ctx (sAll as (s, loc)) =
+            case s of
+                SgnConst sgis =>
+                S.map2 (ListUtil.mapfoldB (fn (ctx, si)  =>
+                                              (case #1 si of
+                                                   SgiConAbs (x, _, k) =>
+                                                   bind (ctx, NamedC (x, k))
+                                                 | SgiCon (x, _, k, _) =>
+                                                   bind (ctx, NamedC (x, k))
+                                                 | SgiVal _ => ctx
+                                                 | SgiStr (x, _, sgn) =>
+                                                   bind (ctx, Str (x, sgn)),
+                                               sgi ctx si)) ctx sgis,
+                     fn sgis' =>
+                        (SgnConst sgis', loc))
+                
+              | SgnVar _ => S.return2 sAll
+              | SgnError => S.return2 sAll
+    in
+        sg
+    end
+
+fun mapfold {kind, con, sgn_item, sgn} =
+    mapfoldB {kind = kind,
+              con = fn () => con,
+              sgn_item = fn () => sgn_item,
+              sgn = fn () => sgn,
+              bind = fn ((), _) => ()} ()
+
+fun map {kind, con, sgn_item, sgn} s =
+    case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
+                  con = fn c => fn () => S.Continue (con c, ()),
+                  sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
+                  sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
+        S.Return () => raise Fail "Elab_util.Sgn.map"
+      | S.Continue (s, ()) => s
+
+end
+
 end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index b232a980..7cc510ec 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -108,12 +108,15 @@ fun unifyKinds k1 k2 =
 
 datatype con_error =
          UnboundCon of ErrorMsg.span * string
+       | UnboundStrInCon of ErrorMsg.span * string
        | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
 
 fun conError env err =
     case err of
         UnboundCon (loc, s) =>
         ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
+      | UnboundStrInCon (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound structure " ^ s)
       | WrongKind (c, k1, k2, kerr) =>
         (ErrorMsg.errorAt (#2 c) "Wrong kind";
          eprefaces' [("Constructor", p_con env c),
@@ -225,7 +228,7 @@ fun elabCon env (c, loc) =
             ((L'.TRecord c', loc), ktype)
         end
 
-      | L.CVar s =>
+      | L.CVar ([], s) =>
         (case E.lookupC env s of
              E.NotBound =>
              (conError env (UnboundCon (loc, s));
@@ -234,6 +237,27 @@ fun elabCon env (c, loc) =
              ((L'.CRel n, loc), k)
            | E.Named (n, k) =>
              ((L'.CNamed n, loc), k))
+      | L.CVar (m1 :: ms, s) =>
+        (case E.lookupStr env m1 of
+             NONE => (conError env (UnboundStrInCon (loc, s));
+                      (cerror, kerror))
+           | SOME (n, sgn) =>
+             let
+                 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                     case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                         NONE => (conError env (UnboundStrInCon (loc, m));
+                                                  (strerror, sgnerror))
+                                       | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                                  ((L'.StrVar n, loc), sgn) ms
+
+                 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
+                             NONE => (conError env (UnboundCon (loc, s));
+                                      kerror)
+                           | SOME (k, _) => k
+             in
+                 ((L'.CModProj (n, ms, s), loc), k)
+             end)
+                                                                       
       | L.CApp (c1, c2) =>
         let
             val (c1', k1) = elabCon env c1
@@ -404,6 +428,20 @@ fun kindof env (c, loc) =
 
       | L'.CRel xn => #2 (E.lookupCRel env xn)
       | L'.CNamed xn => #2 (E.lookupCNamed env xn)
+      | L'.CModProj (n, ms, x) =>
+        let
+            val (_, sgn) = E.lookupStrNamed env n
+            val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                       case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                           NONE => raise Fail "kindof: Unknown substructure"
+                                         | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                             ((L'.StrVar n, loc), sgn) ms
+        in
+            case E.projectCon env {sgn = sgn, str = str, field = x} of
+                NONE => raise Fail "kindof: Unknown con in structure"
+              | SOME (k, _) => k
+        end
+
       | L'.CApp (c, _) =>
         (case #1 (hnormKind (kindof env c)) of
              L'.KArrow (_, k) => k
@@ -541,7 +579,7 @@ and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
         pairOffUnifs (unifs1, unifs2)
     end
 
-and hnormCon env (cAll as (c, _)) =
+and hnormCon env (cAll as (c, loc)) =
     case c of
         L'.CUnif (_, _, ref (SOME c)) => hnormCon env c
 
@@ -550,6 +588,21 @@ and hnormCon env (cAll as (c, _)) =
              (_, _, SOME c') => hnormCon env c'
            | _ => cAll)
 
+      | L'.CModProj (n, ms, x) =>
+        let
+            val (_, sgn) = E.lookupStrNamed env n
+            val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                       case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                           NONE => raise Fail "hnormCon: Unknown substructure"
+                                         | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                             ((L'.StrVar n, loc), sgn) ms
+        in
+            case E.projectCon env {sgn = sgn, str = str, field = x} of
+                NONE => raise Fail "kindof: Unknown con in structure"
+              | SOME (_, NONE) => cAll
+              | SOME (_, SOME c) => hnormCon env c
+        end
+
       | L'.CApp (c1, c2) =>
         (case hnormCon env c1 of
              (L'.CAbs (_, _, cb), _) =>
@@ -610,6 +663,12 @@ and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
             else
                 err CIncompatible
 
+          | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
+            if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
+                ()
+            else
+                err CIncompatible
+
           | (L'.CError, _) => ()
           | (_, L'.CError) => ()
 
@@ -649,6 +708,7 @@ and unifyCons env c1 c2 =
 
 datatype exp_error =
        UnboundExp of ErrorMsg.span * string
+     | UnboundStrInExp of ErrorMsg.span * string
      | Unify of L'.exp * L'.con * L'.con * cunify_error
      | Unif of string * L'.con
      | WrongForm of string * L'.exp * L'.con
@@ -657,6 +717,8 @@ fun expError env err =
     case err of
         UnboundExp (loc, s) =>
         ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
+      | UnboundStrInExp (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound structure " ^ s)
       | Unify (e, c1, c2, uerr) =>
         (ErrorMsg.errorAt (#2 e) "Unification failure";
          eprefaces' [("Expression", p_exp env e),
@@ -695,6 +757,20 @@ fun typeof env (e, loc) =
         L'.EPrim p => (primType env p, loc)
       | L'.ERel n => #2 (E.lookupERel env n)
       | L'.ENamed n => #2 (E.lookupENamed env n)
+      | L'.EModProj (n, ms, x) =>
+        let
+            val (_, sgn) = E.lookupStrNamed env n
+            val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                       case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                           NONE => raise Fail "kindof: Unknown substructure"
+                                         | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                             ((L'.StrVar n, loc), sgn) ms
+        in
+            case E.projectVal env {sgn = sgn, str = str, field = x} of
+                NONE => raise Fail "typeof: Unknown val in structure"
+              | SOME t => t
+        end
+
       | L'.EApp (e1, _) =>
         (case #1 (typeof env e1) of
              L'.TFun (_, c) => c
@@ -739,13 +815,34 @@ fun elabExp env (e, loc) =
         end
 
       | L.EPrim p => ((L'.EPrim p, loc), (primType env p, loc))
-      | L.EVar s =>
+      | L.EVar ([], s) =>
         (case E.lookupE env s of
              E.NotBound =>
              (expError env (UnboundExp (loc, s));
               (eerror, cerror))
            | E.Rel (n, t) => ((L'.ERel n, loc), t)
            | E.Named (n, t) => ((L'.ENamed n, loc), t))
+      | L.EVar (m1 :: ms, s) =>
+        (case E.lookupStr env m1 of
+             NONE => (expError env (UnboundStrInExp (loc, s));
+                      (eerror, cerror))
+           | SOME (n, sgn) =>
+             let
+                 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                     case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                         NONE => (conError env (UnboundStrInCon (loc, m));
+                                                  (strerror, sgnerror))
+                                       | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                                  ((L'.StrVar n, loc), sgn) ms
+
+                 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
+                             NONE => (expError env (UnboundExp (loc, s));
+                                      cerror)
+                           | SOME t => t
+             in
+                 ((L'.EModProj (n, ms, s), loc), t)
+             end)
+
       | L.EApp (e1, e2) =>
         let
             val (e1', t1) = elabExp env e1
@@ -1209,6 +1306,15 @@ and elabStr env (str, loc) =
              (strError env (UnboundStr (loc, x));
               (strerror, sgnerror))
            | SOME (n, sgn) => ((L'.StrVar n, loc), sgn))
+      | L.StrProj (str, x) =>
+        let
+            val (str', sgn) = elabStr env str
+        in
+            case E.projectStr env {str = str', sgn = sgn, field = x} of
+                NONE => (strError env (UnboundStr (loc, x));
+                         (strerror, sgnerror))
+              | SOME sgn => ((L'.StrProj (str', x), loc), sgn)
+        end
 
 val elabFile = ListUtil.foldlMap elabDecl
 
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 0c708699..f8f54fca 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -60,6 +60,9 @@ val s = ErrorMsg.spanOf
  | kind of kind
  | kcolon of explicitness
 
+ | path of string list * string
+ | spath of str
+
  | cexp of con
  | capps of con
  | cterm of con
@@ -126,7 +129,10 @@ sgis   :                                ([])
        | sgi sgis                       (sgi :: sgis)
 
 str    : STRUCT decls END               (StrConst decls, s (STRUCTleft, ENDright))
-       | CSYMBOL                        (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+       | spath                          (spath)
+
+spath  : CSYMBOL                        (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+       | spath DOT CSYMBOL              (StrProj (spath, CSYMBOL), s (spathleft, CSYMBOLright))
 
 kind   : TYPE                           (KType, s (TYPEleft, TYPEright))
        | NAME                           (KName, s (NAMEleft, NAMEright))
@@ -153,6 +159,9 @@ cexp   : capps                          (capps)
 kcolon : DCOLON                         (Explicit)
        | TCOLON                         (Implicit)
 
+path   : SYMBOL                         ([], SYMBOL)
+       | CSYMBOL DOT path               (let val (ms, x) = path in (CSYMBOL :: ms, x) end)
+
 cterm  : LPAREN cexp RPAREN             (#1 cexp, s (LPARENleft, RPARENright))
        | LBRACK rcon RBRACK             (CRecord rcon, s (LBRACKleft, RBRACKright))
        | LBRACE rcone RBRACE            (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)),
@@ -160,7 +169,7 @@ cterm  : LPAREN cexp RPAREN             (#1 cexp, s (LPARENleft, RPARENright))
        | DOLLAR cterm                   (TRecord cterm, s (DOLLARleft, ctermright))
        | HASH CSYMBOL                   (CName CSYMBOL, s (HASHleft, CSYMBOLright))
 
-       | SYMBOL                         (CVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+       | path                           (CVar path, s (pathleft, pathright))
        | UNDER                          (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
 
 rcon   :                                ([])
@@ -172,7 +181,7 @@ rcone  :                                ([])
        | ident COLON cexp COMMA rcone   ((ident, cexp) :: rcone)
 
 ident  : CSYMBOL                        (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
-       | SYMBOL                         (CVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+       | SYMBOL                         (CVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright))
 
 eapps  : eterm                          (eterm)
        | eapps eterm                    (EApp (eapps, eterm), s (eappsleft, etermright))
@@ -188,7 +197,7 @@ eexp   : eapps                          (eapps)
 
 eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
 
-       | SYMBOL                         (EVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+       | path                           (EVar path, s (pathleft, pathright))
        | LBRACE rexp RBRACE             (ERecord rexp, s (LBRACEleft, RBRACEright))
 
        | INT                            (EPrim (Prim.Int INT), s (INTleft, INTright))
diff --git a/src/list_util.sig b/src/list_util.sig
index 62013d25..76d08d23 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -29,6 +29,8 @@ signature LIST_UTIL = sig
 
     val mapfold : ('data, 'state, 'abort) Search.mapfolder
                   -> ('data list, 'state, 'abort) Search.mapfolder
+    val mapfoldB : ('context * 'data -> 'context * ('state -> ('data * 'state, 'abort) Search.result))
+                   -> ('context, 'data list, 'state, 'abort) Search.mapfolderB
 
     val foldlMap : ('data1 * 'state -> 'data2 * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state
 
diff --git a/src/list_util.sml b/src/list_util.sml
index 7d3f8333..e3d8515e 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -45,6 +45,26 @@ fun mapfold f =
         mf
     end
 
+fun mapfoldB f =
+    let
+        fun mf ctx ls s =
+            case ls of
+                nil => S.Continue (nil, s)
+              | h :: t =>
+                let
+                    val (ctx, r) = f (ctx, h)
+                in
+                    case r s of
+                        S.Return x => S.Return x
+                      | S.Continue (h', s) =>
+                        case mf ctx t s of
+                            S.Return x => S.Return x
+                          | S.Continue (t', s) => S.Continue (h' :: t', s)
+                end
+    in
+        mf
+    end
+
 fun foldlMap f s =
     let
         fun fm (ls', s) ls =
diff --git a/src/source.sml b/src/source.sml
index 6fe07255..a7ff04c6 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -49,7 +49,7 @@ datatype con' =
        | TCFun of explicitness * string * kind * con
        | TRecord of con
 
-       | CVar of string
+       | CVar of string list * string
        | CApp of con * con
        | CAbs of string * kind * con
 
@@ -62,11 +62,24 @@ datatype con' =
 
 withtype con = con' located
 
+datatype sgn_item' =
+         SgiConAbs of string * kind
+       | SgiCon of string * kind option * con
+       | SgiVal of string * con
+       | SgiStr of string * sgn
+
+and sgn' =
+    SgnConst of sgn_item list
+  | SgnVar of string
+
+withtype sgn_item = sgn_item' located
+and sgn = sgn' located
+
 datatype exp' =
          EAnnot of exp * con
 
        | EPrim of Prim.t
-       | EVar of string
+       | EVar of string list * string
        | EApp of exp * exp
        | EAbs of string * con option * exp
        | ECApp of exp * con
@@ -77,19 +90,6 @@ datatype exp' =
 
 withtype exp = exp' located
 
-datatype sgn_item' =
-         SgiConAbs of string * kind
-       | SgiCon of string * kind option * con
-       | SgiVal of string * con
-       | SgiStr of string * sgn
-
-and sgn' =
-    SgnConst of sgn_item list
-  | SgnVar of string
-
-withtype sgn_item = sgn_item' located
-and sgn = sgn' located
-
 datatype decl' =
          DCon of string * kind option * con
        | DVal of string * con option * exp
@@ -99,6 +99,7 @@ datatype decl' =
      and str' =
          StrConst of decl list
        | StrVar of string
+       | StrProj of str * string
 
 withtype decl = decl' located
      and str = str' located
diff --git a/src/source_print.sml b/src/source_print.sml
index 5a2412a9..2005d09f 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -88,7 +88,7 @@ fun p_con' par (c, _) =
       | TRecord c => box [string "$",
                           p_con' true c]
 
-      | CVar s => string s
+      | CVar (ss, s) => p_list_sep (string ".") string (ss @ [s])
       | CApp (c1, c2) => parenIf par (box [p_con c1,
                                            space,
                                            p_con' true c2])
@@ -143,7 +143,7 @@ fun p_exp' par (e, _) =
                               string ")"]        
 
       | EPrim p => Prim.p_t p
-      | EVar s => string s
+      | EVar (ss, s) => p_list_sep (string ".") string (ss @ [s])
       | EApp (e1, e2) => parenIf par (box [p_exp e1,
                                            space,
                                            p_exp' true e2])
@@ -321,6 +321,9 @@ and p_str (str, _) =
                             newline,
                             string "end"]
       | StrVar x => string x
+      | StrProj (str, x) => box [p_str str,
+                                 string ".",
+                                 string x]
 
 val p_file = p_list_sep newline p_decl
 
diff --git a/tests/modproj.lac b/tests/modproj.lac
new file mode 100644
index 00000000..ef2364d1
--- /dev/null
+++ b/tests/modproj.lac
@@ -0,0 +1,11 @@
+signature S = sig
+        type t
+        val zero : t
+end
+structure S : S = struct
+        type t = int
+        val zero = 0
+end
+
+type t = S.t
+val zero : t = S.zero