changeset 44:a9f3ce2d1b9b

Elaborating functor applications
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 17:04:08 -0400
parents d94c484337d0
children 3c1ce1b4eb3d
files src/elab.sml src/elab_print.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/source.sml src/source_print.sml tests/functor.lac
diffstat 8 files changed, 71 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Thu Jun 19 16:43:24 2008 -0400
+++ b/src/elab.sml	Thu Jun 19 17:04:08 2008 -0400
@@ -109,6 +109,7 @@
        | StrVar of int
        | StrProj of str * string
        | StrFun of string * int * sgn * sgn * str
+       | StrApp of str * str
        | StrError
 
 withtype decl = decl' located
--- a/src/elab_print.sml	Thu Jun 19 16:43:24 2008 -0400
+++ b/src/elab_print.sml	Thu Jun 19 17:04:08 2008 -0400
@@ -413,6 +413,10 @@
                  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 =
--- a/src/elaborate.sml	Thu Jun 19 16:43:24 2008 -0400
+++ b/src/elaborate.sml	Thu Jun 19 17:04:08 2008 -0400
@@ -1014,11 +1014,15 @@
 
 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 @@
       | 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 @@
                 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 @@
             ((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
 
--- a/src/explify.sml	Thu Jun 19 16:43:24 2008 -0400
+++ b/src/explify.sml	Thu Jun 19 17:04:08 2008 -0400
@@ -110,6 +110,7 @@
       | 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
--- a/src/lacweb.grm	Thu Jun 19 16:43:24 2008 -0400
+++ b/src/lacweb.grm	Thu Jun 19 17:04:08 2008 -0400
@@ -154,6 +154,7 @@
                                         (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))
--- a/src/source.sml	Thu Jun 19 16:43:24 2008 -0400
+++ b/src/source.sml	Thu Jun 19 17:04:08 2008 -0400
@@ -103,6 +103,7 @@
        | 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
--- a/src/source_print.sml	Thu Jun 19 16:43:24 2008 -0400
+++ b/src/source_print.sml	Thu Jun 19 17:04:08 2008 -0400
@@ -375,6 +375,10 @@
                                                 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
 
--- a/tests/functor.lac	Thu Jun 19 16:43:24 2008 -0400
+++ b/tests/functor.lac	Thu Jun 19 17:04:08 2008 -0400
@@ -18,3 +18,23 @@
 structure F3 : functor (M : S) : T = F
 (*structure F4 : functor (M : S) : sig type q end = F*)
 (*structure F5 : functor (M : S) : T where type t = int = F*)
+
+
+structure O = F (struct
+        type t = int
+        val z = 0
+        val s = fn x : t => x
+end)
+val three : int = O.three
+
+structure S = struct
+        type t = int
+        val z = 0
+        val s = fn x : t => x
+end
+structure SO = F (S)
+val three : int = SO.three
+
+structure SS : S = S
+structure SSO = F (SS)
+val three : SS.t = SSO.three