Beginning of functor elaboration

7 files changed, 135 insertions, 38 deletions

diff --git a/src/elab.sml b/src/elab.sml
index da64febf..07bb7f8d 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -91,6 +91,7 @@ datatype sgn_item' =
 and sgn' =
     SgnConst of sgn_item list
   | SgnVar of int
+  | SgnFun of string * int * sgn * sgn
   | SgnError
 
 withtype sgn_item = sgn_item' located
@@ -106,6 +107,7 @@ datatype decl' =
          StrConst of decl list
        | StrVar of int
        | StrProj of str * string
+       | StrFun of string * int * sgn * sgn * str
        | StrError
 
 withtype decl = decl' located
diff --git a/src/elab_env.sml b/src/elab_env.sml
index b10882a7..9d308ddc 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -376,6 +376,7 @@ fun projectCon env {sgn = (sgn, _), str, field} =
             projectCon env {sgn = sgn, str = str, field = field}
         end
       | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
+      | SgnFun _ => NONE
 
 fun projectVal env {sgn = (sgn, _), str, field} =
     case sgn of
@@ -390,6 +391,7 @@ fun projectVal env {sgn = (sgn, _), str, field} =
             projectVal env {sgn = sgn, str = str, field = field}
         end
       | SgnError => SOME (CError, ErrorMsg.dummySpan)
+      | SgnFun _ => NONE
 
 fun projectStr env {sgn = (sgn, _), str, field} =
     case sgn of
@@ -404,6 +406,7 @@ fun projectStr env {sgn = (sgn, _), str, field} =
             projectStr env {sgn = sgn, str = str, field = field}
         end
       | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
+      | SgnFun _ => NONE
 
 
 val ktype = (KType, ErrorMsg.dummySpan)
diff --git a/src/elab_print.sig b/src/elab_print.sig
index 49af2ded..9ab9eae7 100644
--- a/src/elab_print.sig
+++ b/src/elab_print.sig
@@ -34,6 +34,7 @@ signature ELAB_PRINT = sig
     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_sgn : ElabEnv.env -> Elab.sgn 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 b214d5d4..03792e03 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -310,6 +310,19 @@ and p_sgn env (sgn, _) =
                               newline,
                               string "end"]
       | SgnVar n => string (#1 (E.lookupSgnNamed env n))
+      | SgnFun (x, n, sgn, sgn') => box [string "functor",
+                                         space,
+                                         string "(",
+                                         string x,
+                                         space,
+                                         string ":",
+                                         space,
+                                         p_sgn env sgn,
+                                         string ")",
+                                         space,
+                                         string ":",
+                                         space,
+                                         p_sgn (E.pushStrNamedAs env x n sgn) sgn']
       | SgnError => string "<ERROR>"
 
 fun p_decl env ((d, _) : decl) =
@@ -367,6 +380,28 @@ and p_str env (str, _) =
       | StrProj (str, s) => box [p_str env str,
                                  string ".",
                                  string s]
+      | StrFun (x, n, sgn, sgn', str) =>
+        let
+            val env' = E.pushStrNamedAs env x n sgn
+        in
+            box [string "functor",
+                 space,
+                 string "(",
+                 string x,
+                 space,
+                 string ":",
+                 space,
+                 p_sgn env sgn,
+                 string ")",
+                 space,
+                 string ":",
+                 space,
+                 p_sgn env' sgn',
+                 space,
+                 string "=>",
+                 space,
+                 p_str env' str]
+        end
       | StrError => string "<ERROR>"
 
 and p_file env file =
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 24e772d6..e2b4f113 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -364,6 +364,12 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                         (SgnConst sgis', loc))
                 
               | SgnVar _ => S.return2 sAll
+              | SgnFun (m, n, s1, s2) =>
+                S.bind2 (sg ctx s1,
+                         fn s1' =>
+                            S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
+                                    fn s2' =>
+                                       (SgnFun (m, n, s1', s2'), loc)))
               | SgnError => S.return2 sAll
     in
         sg
diff --git a/src/elaborate.sml b/src/elaborate.sml
index d482f9a0..10fa3898 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -968,6 +968,7 @@ datatype sgn_error =
        | 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
+       | SgnWrongForm of L'.sgn * L'.sgn
 
 fun sgnError env err =
     case err of
@@ -990,6 +991,10 @@ fun sgnError env err =
                      ("Con 1", p_con env c1),
                      ("Con 2", p_con env c2)];
          cunifyError env cerr)
+      | SgnWrongForm (sgn1, sgn2) =>
+        (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
+         eprefaces' [("Sig 1", p_sgn env sgn1),
+                     ("Sig 2", p_sgn env sgn2)])
 
 datatype str_error =
          UnboundStr of ErrorMsg.span * string
@@ -1097,7 +1102,14 @@ and elabSgn env (sgn, loc) =
              (sgnError env (UnboundSgn (loc, x));
               (L'.SgnError, loc))
            | SOME (n, sgis) => (L'.SgnVar n, loc))
-      | L.SgnFun _ => raise Fail "Elaborate functor sig"
+      | L.SgnFun (m, dom, ran) =>
+        let
+            val dom' = elabSgn env dom
+            val (env', n) = E.pushStrNamed env m dom'
+            val ran' = elabSgn env' ran
+        in
+            (L'.SgnFun (m, n, dom', ran'), loc)
+        end
 
 fun sgiOfDecl (d, loc) =
     case d of
@@ -1111,15 +1123,13 @@ fun hnormSgn env (all as (sgn, _)) =
         L'.SgnError => all
       | L'.SgnVar n => hnormSgn env (#2 (E.lookupSgnNamed env n))
       | L'.SgnConst _ => all
+      | L'.SgnFun _ => all
 
 fun subSgn env sgn1 (sgn2 as (_, loc2)) =
     case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
         (L'.SgnError, _) => ()
       | (_, L'.SgnError) => ()
 
-      | (L'.SgnVar n, _) => raise Fail "subSgn: Variable remains"
-      | (_, L'.SgnVar n) => raise Fail "subSgn: Variable remains"
-
       | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
         let
             fun folder (sgi2All as (sgi, _), env) =
@@ -1142,57 +1152,69 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
                         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
+                                     fun found (x', n1, k1, co1) =
+                                         if x = x' then
+                                             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
+                                         else
+                                             NONE
                                  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)
+                                         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
+                                     L'.SgiCon (x', n1, k1, c1) =>
+                                     if x = x' then
+                                         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
+                                     else
+                                         NONE
                                    | _ => NONE)
 
                       | L'.SgiVal (x, n2, c2) =>
                         seek (fn sgi1All as (sgi1, _) =>
                                  case sgi1 of
-                                     L'.SgiVal (x, n1, c1) =>
-                                     let
-                                         val () = unifyCons env c1 c2
-                                             handle CUnify (c1, c2, err) =>
-                                                    sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err))
-                                     in
-                                         SOME env
-                                     end
+                                     L'.SgiVal (x', n1, c1) =>
+                                     if x = x' then
+                                         let
+                                             val () = unifyCons env c1 c2
+                                                 handle CUnify (c1, c2, err) =>
+                                                        sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err))
+                                         in
+                                             SOME env
+                                         end
+                                     else
+                                         NONE
                                    | _ => NONE)
 
                       | L'.SgiStr (x, n2, sgn2) =>
                         seek (fn sgi1All as (sgi1, _) =>
                                  case sgi1 of
-                                     L'.SgiStr (x, n1, sgn1) =>
-                                     (subSgn env sgn1 sgn2;
-                                      SOME env)
+                                     L'.SgiStr (x', n1, sgn1) =>
+                                     if x = x' then
+                                         (subSgn env sgn1 sgn2;
+                                          SOME env)
+                                     else
+                                         NONE
                                    | _ => NONE)
                         (* Add type equations between structures here some day. *)
                 end
@@ -1200,6 +1222,12 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
             ignore (foldl folder env sgis2)
         end
 
+      | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
+        (subSgn env dom2 dom1;
+         subSgn env ran1 ran2)
+
+      | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
+
 fun selfify env {str, strs, sgn} =
     case #1 (hnormSgn env sgn) of
         L'.SgnError => sgn
@@ -1211,6 +1239,7 @@ fun selfify env {str, strs, sgn} =
                             | (L'.SgiStr (x, n, sgn), loc) =>
                               (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
                             | x => x) sgis), #2 sgn)
+      | L'.SgnFun _ => sgn
 
 fun elabDecl ((d, loc), env) =
     let
@@ -1344,7 +1373,26 @@ and elabStr env (str, loc) =
                          (strerror, sgnerror))
               | SOME sgn => ((L'.StrProj (str', x), loc), sgn)
         end
-      | L.StrFun _ => raise Fail "Elaborate functor"
+      | L.StrFun (m, dom, ranO, str) =>
+        let
+            val dom' = elabSgn env dom
+            val (env', n) = E.pushStrNamed env m dom'
+            val (str', actual) = elabStr env' str
+
+            val formal =
+                case ranO of
+                    NONE => actual
+                  | SOME ran =>
+                    let
+                        val ran' = elabSgn env ran
+                    in
+                        subSgn env' actual ran';
+                        ran'
+                    end
+        in
+            ((L'.StrFun (m, n, dom', formal, str'), loc),
+             (L'.SgnFun (m, n, dom', formal), loc))
+        end
 
 val elabFile = ListUtil.foldlMap elabDecl
 
diff --git a/src/explify.sml b/src/explify.sml
index a1953fab..caba15d1 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -92,6 +92,7 @@ and explifySgn (sgn, loc) =
     case sgn of
         L.SgnConst sgis => (L'.SgnConst (map explifySgi sgis), loc)
       | L.SgnVar n => (L'.SgnVar n, loc)
+      | L.SgnFun _ => raise Fail "Explify functor signature"
       | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
 
 fun explifyDecl (d, loc : EM.span) =
@@ -107,6 +108,7 @@ and explifyStr (str, loc) =
         L.StrConst ds => (L'.StrConst (map explifyDecl ds), 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.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc)
 
 val explify = map explifyDecl