changeset 41:1405d8c26790

Beginning of functor elaboration
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 16:04:28 -0400 (2008-06-19)
parents e3d3c2791105
children b3fbbc6cb1e5
files src/elab.sml src/elab_env.sml src/elab_print.sig src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml tests/functor.lac
diffstat 8 files changed, 140 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Thu Jun 19 15:15:00 2008 -0400
+++ b/src/elab.sml	Thu Jun 19 16:04:28 2008 -0400
@@ -91,6 +91,7 @@
 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 @@
          StrConst of decl list
        | StrVar of int
        | StrProj of str * string
+       | StrFun of string * int * sgn * sgn * str
        | StrError
 
 withtype decl = decl' located
--- a/src/elab_env.sml	Thu Jun 19 15:15:00 2008 -0400
+++ b/src/elab_env.sml	Thu Jun 19 16:04:28 2008 -0400
@@ -376,6 +376,7 @@
             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 @@
             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 @@
             projectStr env {sgn = sgn, str = str, field = field}
         end
       | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
+      | SgnFun _ => NONE
 
 
 val ktype = (KType, ErrorMsg.dummySpan)
--- a/src/elab_print.sig	Thu Jun 19 15:15:00 2008 -0400
+++ b/src/elab_print.sig	Thu Jun 19 16:04:28 2008 -0400
@@ -34,6 +34,7 @@
     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
--- a/src/elab_print.sml	Thu Jun 19 15:15:00 2008 -0400
+++ b/src/elab_print.sml	Thu Jun 19 16:04:28 2008 -0400
@@ -310,6 +310,19 @@
                               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 @@
       | 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 =
--- a/src/elab_util.sml	Thu Jun 19 15:15:00 2008 -0400
+++ b/src/elab_util.sml	Thu Jun 19 16:04:28 2008 -0400
@@ -364,6 +364,12 @@
                         (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
--- a/src/elaborate.sml	Thu Jun 19 15:15:00 2008 -0400
+++ b/src/elaborate.sml	Thu Jun 19 16:04:28 2008 -0400
@@ -968,6 +968,7 @@
        | 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 @@
                      ("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 @@
              (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 @@
         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 @@
                         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 @@
             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 @@
                             | (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 @@
                          (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
 
--- a/src/explify.sml	Thu Jun 19 15:15:00 2008 -0400
+++ b/src/explify.sml	Thu Jun 19 16:04:28 2008 -0400
@@ -92,6 +92,7 @@
     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 @@
         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
--- a/tests/functor.lac	Thu Jun 19 15:15:00 2008 -0400
+++ b/tests/functor.lac	Thu Jun 19 16:04:28 2008 -0400
@@ -9,7 +9,11 @@
         val three : t
 end
 
+signature F = functor (M : S) : T
+
 structure F = functor (M : S) : T => struct
-        val t = M.t
+        type t = M.t
         val three = M.s (M.s (M.s M.z))
 end
+
+structure F2 : F = F