Elaborating functor applications

7 files changed, 51 insertions, 13 deletions

diff --git a/src/elab.sml b/src/elab.sml
index edec2e3d..e675144d 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -109,6 +109,7 @@ datatype decl' =
        | StrVar of int
        | StrProj of str * string
        | StrFun of string * int * sgn * sgn * str
+       | StrApp of str * str
        | StrError
 
 withtype decl = decl' located
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 88dcdfaa..cdbb652d 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -413,6 +413,10 @@ and p_str env (str, _) =
                  space,
                  p_str env' str]
         end
+      | StrApp (str1, str2) => box [p_str env str1,
+                                    string "(",
+                                    p_str env str2,
+                                    string ")"]
       | StrError => string "<ERROR>"
 
 and p_file env file =
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 5e0ba5fc..73cf185d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1014,11 +1014,15 @@ fun sgnError env err =
 
 datatype str_error =
          UnboundStr of ErrorMsg.span * string
+       | NotFunctor of L'.sgn
 
 fun strError env err =
     case err of
         UnboundStr (loc, s) =>
         ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
+      | NotFunctor sgn =>
+        (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
+         eprefaces' [("Signature", p_sgn env sgn)])
 
 val hnormSgn = E.hnormSgn
 
@@ -1279,6 +1283,22 @@ fun selfify env {str, strs, sgn} =
       | L'.SgnFun _ => sgn
       | L'.SgnWhere _ => sgn
 
+fun selfifyAt env {str, sgn} =
+    let
+        fun self (str, _) =
+            case str of
+                L'.StrVar x => SOME (x, [])
+              | L'.StrProj (str, x) =>
+                (case self str of
+                     NONE => NONE
+                   | SOME (m, ms) => SOME (m, ms @ [x]))
+              | _ => NONE
+    in
+        case self str of
+            NONE => sgn
+          | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
+    end
+
 fun elabDecl ((d, loc), env) =
     let
         
@@ -1363,20 +1383,8 @@ fun elabDecl ((d, loc), env) =
                 val formal = Option.map (elabSgn env) sgno
                 val (str', actual) = elabStr env str
 
-                fun self (str, _) =
-                    case str of
-                        L'.StrVar x => SOME (x, [])
-                      | L'.StrProj (str, x) =>
-                        (case self str of
-                             NONE => NONE
-                           | SOME (m, ms) => SOME (m, ms @ [x]))
-                      | _ => NONE
-
                 val sgn' = case formal of
-                               NONE =>
-                               (case self str' of
-                                    NONE => actual
-                                  | SOME (str, strs) => selfify env {sgn = actual, str = str, strs = strs})
+                               NONE => selfifyAt env {str = str', sgn = actual}
                              | SOME formal =>
                                (subSgn env actual formal;
                                 formal)
@@ -1431,6 +1439,24 @@ and elabStr env (str, loc) =
             ((L'.StrFun (m, n, dom', formal, str'), loc),
              (L'.SgnFun (m, n, dom', formal), loc))
         end
+      | L.StrApp (str1, str2) =>
+        let
+            val (str1', sgn1) = elabStr env str1
+            val (str2', sgn2) = elabStr env str2
+        in
+            case #1 (hnormSgn env sgn1) of
+                L'.SgnError => (strerror, sgnerror)
+              | L'.SgnFun (m, n, dom, ran) =>
+                (subSgn env sgn2 dom;
+                 case #1 (hnormSgn env ran) of
+                     L'.SgnError => (strerror, sgnerror)
+                   | L'.SgnConst sgis =>
+                     ((L'.StrApp (str1', str2'), loc),
+                      (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc))
+                   | _ => raise Fail "Unable to hnormSgn in functor application")
+              | _ => (strError env (NotFunctor sgn1);
+                      (strerror, sgnerror))
+        end
 
 val elabFile = ListUtil.foldlMap elabDecl
 
diff --git a/src/explify.sml b/src/explify.sml
index 73c9aed2..2df414a9 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -110,6 +110,7 @@ and explifyStr (str, loc) =
       | L.StrVar n => (L'.StrVar n, loc)
       | L.StrProj (str, s) => (L'.StrProj (explifyStr str, s), loc)
       | L.StrFun _ => raise Fail "Explify functor"
+      | L.StrApp _ => raise Fail "Explify functor app"
       | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc)
 
 val explify = map explifyDecl
diff --git a/src/lacweb.grm b/src/lacweb.grm
index e917396c..85a58eb8 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -154,6 +154,7 @@ str    : STRUCT decls END               (StrConst decls, s (STRUCTleft, ENDright
                                         (StrFun (CSYMBOL, sgn, NONE, str), s (FUNCTORleft, strright))
        | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn DARROW str
                                         (StrFun (CSYMBOL, sgn1, SOME sgn2, str), s (FUNCTORleft, strright))
+       | spath LPAREN str RPAREN        (StrApp (spath, str), s (spathleft, RPARENright))
 
 spath  : CSYMBOL                        (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
        | spath DOT CSYMBOL              (StrProj (spath, CSYMBOL), s (spathleft, CSYMBOLright))
diff --git a/src/source.sml b/src/source.sml
index 1bcb248c..b8aa33aa 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -103,6 +103,7 @@ datatype decl' =
        | StrVar of string
        | StrProj of str * string
        | StrFun of string * sgn * sgn option * str
+       | StrApp of str * str
 
 withtype decl = decl' located
      and str = str' located
diff --git a/src/source_print.sml b/src/source_print.sml
index c3a333e8..1522e6da 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -375,6 +375,10 @@ and p_str (str, _) =
                                                 string "=>",
                                                 space,
                                                 p_str str]
+      | StrApp (str1, str2) => box [p_str str1,
+                                    string "(",
+                                    p_str str2,
+                                    string ")"]
 
 val p_file = p_list_sep newline p_decl