Subsignatures

11 files changed, 182 insertions, 34 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 99468146..43837413 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -87,12 +87,14 @@ datatype sgn_item' =
        | SgiCon of string * int * kind * con
        | SgiVal of string * int * con
        | SgiStr of string * int * sgn
+       | SgiSgn of string * int * sgn
 
 and sgn' =
     SgnConst of sgn_item list
   | SgnVar of int
   | SgnFun of string * int * sgn * sgn
   | SgnWhere of sgn * string * con
+  | SgnProj of int * string list * string
   | SgnError
 
 withtype sgn_item = sgn_item' located
diff --git a/src/elab_env.sig b/src/elab_env.sig
index ec97ebbf..54e53607 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -79,6 +79,7 @@ signature ELAB_ENV = sig
 
     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 projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn 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 a673c523..4c27c98d 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -298,23 +298,25 @@ fun sgiBinds env (sgi, _) =
       | 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
+      | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
 
 fun sgnSeek f sgis =
     let
-        fun seek (sgis, strs, cons) =
+        fun seek (sgis, sgns, strs, cons) =
             case sgis of
                 [] => NONE
               | (sgi, _) :: sgis =>
                 case f sgi of
-                    SOME v => SOME (v, (strs, cons))
+                    SOME v => SOME (v, (sgns, 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)
+                          SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                        | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                        | SgiVal _ => seek (sgis, sgns, strs, cons)
+                        | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
+                        | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
     in
-        seek (sgis, IM.empty, IM.empty)
+        seek (sgis, IM.empty, IM.empty, IM.empty)
     end
 
 fun id x = x
@@ -330,7 +332,7 @@ fun unravelStr (str, _) =
         end
       | _ => raise Fail "unravelStr"
 
-fun sgnS_con (str, (strs, cons)) c =
+fun sgnS_con (str, (sgns, strs, cons)) c =
     case c of
         CModProj (m1, ms, x) =>
         (case IM.find (strs, m1) of
@@ -352,15 +354,37 @@ fun sgnS_con (str, (strs, cons)) c =
              end)
       | _ => c
 
-fun sgnSubCon (str, (strs, cons)) =
+fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
+    case sgn of
+        SgnProj (m1, ms, x) =>
+        (case IM.find (strs, m1) of
+             NONE => sgn
+           | SOME m1x =>
+             let
+                 val (m1, ms') = unravelStr str
+             in
+                 SgnProj (m1, ms' @ m1x :: ms, x)
+             end)
+      | SgnVar n =>
+        (case IM.find (sgns, n) of
+             NONE => sgn
+           | SOME nx =>
+             let
+                 val (m1, ms) = unravelStr str
+             in
+                 SgnProj (m1, ms, nx)
+             end)
+      | _ => sgn
+
+fun sgnSubCon x =
     ElabUtil.Con.map {kind = id,
-                      con = sgnS_con (str, (strs, cons))}
+                      con = sgnS_con x}
 
-fun sgnSubSgn (str, (strs, cons)) =
+fun sgnSubSgn x =
     ElabUtil.Sgn.map {kind = id,
-                      con = sgnS_con (str, (strs, cons)),
+                      con = sgnS_con x,
                       sgn_item = id,
-                      sgn = id}
+                      sgn = sgnS_sgn x}
 
 fun hnormSgn env (all as (sgn, loc)) =
     case sgn of
@@ -368,6 +392,16 @@ fun hnormSgn env (all as (sgn, loc)) =
       | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
       | SgnConst _ => all
       | SgnFun _ => all
+      | SgnProj (m, ms, x) =>
+        let
+            val (_, sgn) = lookupStrNamed env m
+        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 => sgn
+        end
       | SgnWhere (sgn, x, c) =>
         case #1 (hnormSgn env sgn) of
             SgnError => (SgnError, loc)
@@ -389,6 +423,24 @@ fun hnormSgn env (all as (sgn, loc)) =
             end
           | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
 
+and projectSgn env {sgn, str, field} =
+    case #1 (hnormSgn env sgn) of
+        SgnConst sgis =>
+        (case sgnSeek (fn SgiSgn (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 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 projectCon env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
@@ -409,13 +461,5 @@ fun projectVal env {sgn, str, field} =
       | SgnError => SOME (CError, ErrorMsg.dummySpan)
       | _ => NONE
 
-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
 
 end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 85271a89..4c02c495 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -294,6 +294,13 @@ fun p_sgn_item env (sgi, _) =
                                    string ":",
                                    space,
                                    p_sgn env sgn]
+      | SgiSgn (x, n, sgn) => box [string "signature",
+                                   space,
+                                   p_named x n,
+                                   space,
+                                   string "=",
+                                   space,
+                                   p_sgn env sgn]
 
 and p_sgn env (sgn, _) =
     case sgn of
@@ -334,6 +341,17 @@ and p_sgn env (sgn, _) =
                                      string "=",
                                      space,
                                      p_con env c]
+      | SgnProj (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
       | SgnError => string "<ERROR>"
 
 fun p_decl env ((d, _) : decl) =
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 0917d126..d6d8acaa 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -83,6 +83,7 @@ structure Sgn : sig
              RelC of string * Elab.kind
            | NamedC of string * Elab.kind
            | Str of string * Elab.sgn
+           | Sgn of string * Elab.sgn
 
     val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
                     con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
diff --git a/src/elab_util.sml b/src/elab_util.sml
index e112a180..2d075fb4 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -305,6 +305,7 @@ datatype binder =
          RelC of string * Elab.kind
        | NamedC of string * Elab.kind
        | Str of string * Elab.sgn
+       | Sgn of string * Elab.sgn
 
 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
     let
@@ -343,6 +344,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                 S.map2 (sg ctx s,
                      fn s' =>
                         (SgiStr (x, n, s'), loc))
+              | SgiSgn (x, n, s) =>
+                S.map2 (sg ctx s,
+                     fn s' =>
+                        (SgiSgn (x, n, s'), loc))
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -358,7 +363,9 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                    bind (ctx, NamedC (x, k))
                                                  | SgiVal _ => ctx
                                                  | SgiStr (x, _, sgn) =>
-                                                   bind (ctx, Str (x, sgn)),
+                                                   bind (ctx, Str (x, sgn))
+                                                 | SgiSgn (x, _, sgn) =>
+                                                   bind (ctx, Sgn (x, sgn)),
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
@@ -370,6 +377,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                             S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
                                     fn s2' =>
                                        (SgnFun (m, n, s1', s2'), loc)))
+              | SgnProj _ => S.return2 sAll
               | SgnWhere (sgn, x, c) =>
                 S.bind2 (sg ctx sgn,
                       fn sgn' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 56c23bfc..a96d90c7 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -988,15 +988,15 @@ fun sgnError env err =
          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),
+         eprefaces' [("Have", p_sgn_item env sgi1),
+                     ("Need", 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),
+         eprefaces' [("Have", p_sgn_item env sgi1),
+                     ("Need", p_sgn_item env sgi2),
                      ("Con 1", p_con env c1),
                      ("Con 2", p_con env c2)];
          cunifyError env cerr)
@@ -1110,6 +1110,14 @@ fun elabSgn_item ((sgi, loc), env) =
                 ([(L'.SgiStr (x, n, sgn'), loc)], env')
             end
 
+          | L.SgiSgn (x, sgn) =>
+            let
+                val sgn' = elabSgn env sgn
+                val (env', n) = E.pushSgnNamed env x sgn'
+            in
+                ([(L'.SgiSgn (x, n, sgn'), loc)], env')
+            end
+
           | L.SgiInclude sgn =>
             let
                 val sgn' = elabSgn env sgn
@@ -1120,6 +1128,7 @@ fun elabSgn_item ((sgi, loc), env) =
                   | _ => (sgnError env (NotIncludable sgn');
                           ([], env))
             end
+
     end
 
 and elabSgn env (sgn, loc) =
@@ -1163,14 +1172,33 @@ and elabSgn env (sgn, loc) =
               | _ => (sgnError env (UnWhereable (sgn', x));
                       sgnerror)
         end
+      | L.SgnProj (m, ms, x) =>
+        (case E.lookupStr env m of
+             NONE => (strError env (UnboundStr (loc, m));
+                      sgnerror)
+           | SOME (n, sgn) =>
+             let
+                 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                          case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                              NONE => (strError env (UnboundStr (loc, m));
+                                                       (strerror, sgnerror))
+                                            | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                                ((L'.StrVar n, loc), sgn) ms
+             in
+                 case E.projectSgn env {sgn = sgn, str = str, field = x} of
+                     NONE => (sgnError env (UnboundSgn (loc, x));
+                              sgnerror)
+                   | SOME _ => (L'.SgnProj (n, ms, x), loc)
+             end)
+                                                              
 
 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)
-      | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc)
+        L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc)
+      | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc)
+      | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc)
+      | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc)
+      | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc)
 
 fun subSgn env sgn1 (sgn2 as (_, loc2)) =
     case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
@@ -1264,6 +1292,18 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
                                          NONE
                                    | _ => NONE)
                         (* Add type equations between structures here some day. *)
+
+                      | L'.SgiSgn (x, n2, sgn2) =>
+                        seek (fn sgi1All as (sgi1, _) =>
+                                 case sgi1 of
+                                     L'.SgiSgn (x', n1, sgn1) =>
+                                     if x = x' then
+                                         (subSgn env sgn1 sgn2;
+                                          subSgn env sgn2 sgn1;
+                                          SOME env)
+                                     else
+                                         NONE
+                                   | _ => NONE)
                 end
         in
             ignore (foldl folder env sgis2)
@@ -1296,6 +1336,13 @@ fun selfify env {str, strs, sgn} =
                             | x => x) sgis), #2 sgn)
       | L'.SgnFun _ => sgn
       | L'.SgnWhere _ => sgn
+      | L'.SgnProj (m, ms, x) =>
+        case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
+                                           (L'.StrVar m, #2 sgn) ms,
+                               sgn = #2 (E.lookupStrNamed env m),
+                               field = x} of
+            NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
+          | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
 
 fun selfifyAt env {str, sgn} =
     let
@@ -1430,7 +1477,7 @@ and elabStr env (str, loc) =
         L.StrConst ds =>
         let
             val (ds', env') = ListUtil.foldlMap elabDecl env ds
-            val sgis = List.mapPartial sgiOfDecl ds'
+            val sgis = map sgiOfDecl ds'
         in
             ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
         end
@@ -1509,7 +1556,10 @@ fun elabFile basis env file =
                                            E.pushENamedAs env' x n t)
                                         | L'.SgiStr (x, n, sgn) =>
                                           ((L'.DStr (x, n, sgn, (L'.StrProj ((L'.StrVar basis_n, loc), x), loc)), loc),
-                                           E.pushStrNamedAs env' x n sgn))
+                                           E.pushStrNamedAs env' x n sgn)
+                                        | L'.SgiSgn (x, n, sgn) =>
+                                          ((L'.DSgn (x, n, (L'.SgnProj (basis_n, [], x), loc)), loc),
+                                           E.pushSgnNamedAs env' x n sgn))
                 env' sgis
               | _ => raise Fail "Non-constant Basis signature"
 
diff --git a/src/explify.sml b/src/explify.sml
index 00d58fcf..03744dba 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -87,6 +87,7 @@ fun explifySgi (sgi, loc) =
       | L.SgiCon (x, n, k, c) => (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
       | L.SgiVal (x, n, c) => (L'.SgiVal (x, n, explifyCon c), loc)
       | L.SgiStr (x, n, sgn) => (L'.SgiStr (x, n, explifySgn sgn), loc)
+      | L.SgiSgn _ => raise Fail "Explify SgiSgn"
 
 and explifySgn (sgn, loc) =
     case sgn of
@@ -94,6 +95,7 @@ and explifySgn (sgn, loc) =
       | L.SgnVar n => (L'.SgnVar n, loc)
       | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc)
       | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc)
+      | L.SgnProj _ => raise Fail "Explify SgnProj"
       | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
 
 fun explifyDecl (d, loc : EM.span) =
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 021e862e..4c3ed51e 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -63,6 +63,7 @@ val s = ErrorMsg.spanOf
 
  | path of string list * string
  | spath of str
+ | mpath of string list
 
  | cexp of con
  | capps of con
@@ -128,7 +129,13 @@ sgn    : sgntm                          (sgntm)
                                         (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right))
 
 sgntm  : SIG sgis END                   (SgnConst sgis, s (SIGleft, ENDright))
-       | CSYMBOL                        (SgnVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+       | mpath                          (case mpath of
+                                             [] => raise Fail "Impossible mpath parse"
+                                           | [x] => SgnVar x
+                                           | m :: ms => SgnProj (m,
+                                                                 List.take (ms, length ms - 1),
+                                                                 List.nth (ms, length ms - 1)),
+                                         s (mpathleft, mpathright))
        | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
        | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
        | LPAREN sgn RPAREN              (sgn)
@@ -143,6 +150,7 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
        | VAL SYMBOL COLON cexp          (SgiVal (SYMBOL, cexp), s (VALleft, cexpright))
 
        | STRUCTURE CSYMBOL COLON sgn    (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright))
+       | SIGNATURE CSYMBOL EQ sgn       (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
        | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
                                         (SgiStr (CSYMBOL1,
                                                  (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
@@ -191,6 +199,9 @@ kcolon : DCOLON                         (Explicit)
 path   : SYMBOL                         ([], SYMBOL)
        | CSYMBOL DOT path               (let val (ms, x) = path in (CSYMBOL :: ms, x) end)
 
+mpath  : CSYMBOL                        ([CSYMBOL])
+       | CSYMBOL DOT mpath              (CSYMBOL :: mpath)
+
 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)),
diff --git a/src/source.sml b/src/source.sml
index 266e8629..2939664c 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -67,6 +67,7 @@ datatype sgn_item' =
        | SgiCon of string * kind option * con
        | SgiVal of string * con
        | SgiStr of string * sgn
+       | SgiSgn of string * sgn
        | SgiInclude of sgn
 
 and sgn' =
@@ -74,6 +75,7 @@ and sgn' =
   | SgnVar of string
   | SgnFun of string * sgn * sgn
   | SgnWhere of sgn * string * con
+  | SgnProj of string * string list * string
 
 withtype sgn_item = sgn_item' located
 and sgn = sgn' located
diff --git a/src/source_print.sml b/src/source_print.sml
index 208aa23a..49adadc3 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -238,6 +238,13 @@ fun p_sgn_item (sgi, _) =
                                 string ":",
                                 space,
                                 p_sgn sgn]
+      | SgiSgn (x, sgn) => box [string "signature",
+                                space,
+                                string x,
+                                space,
+                                string "=",
+                                space,
+                                p_sgn sgn]
       | SgiInclude sgn => box [string "include",
                                space,
                                p_sgn sgn]
@@ -273,6 +280,8 @@ and p_sgn (sgn, _) =
                                      string "=",
                                      space,
                                      p_con c]
+      | SgnProj (m, ms, x) => p_list_sep (string ".") string (m :: ms @ [x])
+                                   
 
 fun p_decl ((d, _) : decl) =
     case d of