# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1213909884 14400
# Node ID 3c1ce1b4eb3ddb3efe91f6e4e14954ed3fd90dce
# Parent  a9f3ce2d1b9b9c0d78a4f12cf26d5ca3fbb3a1b2
Explifying functors

diff -r a9f3ce2d1b9b -r 3c1ce1b4eb3d src/corify.sml
--- a/src/corify.sml	Thu Jun 19 17:04:08 2008 -0400
+++ b/src/corify.sml	Thu Jun 19 17:11:24 2008 -0400
@@ -257,6 +257,8 @@
         in
             (ds, {inner = St.lookupStrByName (x, inner), outer = outer})
         end
+      | L.StrFun _ => raise Fail "Corify functor"
+      | L.StrApp _ => raise Fail "Corify functor app"
 
 fun maxName ds = foldl (fn ((d, _), n) =>
                            case d of
@@ -271,6 +273,8 @@
         L.StrConst ds => maxName ds
       | L.StrVar n => n
       | L.StrProj (str, _) => maxNameStr str
+      | L.StrFun (_, _, _, _, str) => maxNameStr str
+      | L.StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
 
 fun corify ds =
     let
diff -r a9f3ce2d1b9b -r 3c1ce1b4eb3d src/expl.sml
--- a/src/expl.sml	Thu Jun 19 17:04:08 2008 -0400
+++ b/src/expl.sml	Thu Jun 19 17:11:24 2008 -0400
@@ -79,6 +79,8 @@
 and sgn' =
     SgnConst of sgn_item list
   | SgnVar of int
+  | SgnFun of string * int * sgn * sgn
+  | SgnWhere of sgn * string * con
 
 withtype sgn_item = sgn_item' located
 and sgn = sgn' located
@@ -93,6 +95,8 @@
          StrConst of decl list
        | StrVar of int
        | StrProj of str * string
+       | StrFun of string * int * sgn * sgn * str
+       | StrApp of str * str
 
 withtype decl = decl' located
      and str = str' located
diff -r a9f3ce2d1b9b -r 3c1ce1b4eb3d src/expl_print.sml
--- a/src/expl_print.sml	Thu Jun 19 17:04:08 2008 -0400
+++ b/src/expl_print.sml	Thu Jun 19 17:11:24 2008 -0400
@@ -293,6 +293,30 @@
                               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.pushStrNamed env x n sgn) sgn']
+      | SgnWhere (sgn, x, c) => box [p_sgn env sgn,
+                                     space,
+                                     string "where",
+                                     space,
+                                     string "con",
+                                     space,
+                                     string x,
+                                     space,
+                                     string "=",
+                                     space,
+                                     p_con env c]
 
 fun p_decl env ((d, _) : decl) =
     case d of
@@ -349,6 +373,32 @@
       | StrProj (str, s) => box [p_str env str,
                                  string ".",
                                  string s]
+      | StrFun (x, n, sgn, sgn', str) =>
+        let
+            val env' = E.pushStrNamed 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
+      | StrApp (str1, str2) => box [p_str env str1,
+                                    string "(",
+                                    p_str env str2,
+                                    string ")"]
 
 and p_file env file =
     let
diff -r a9f3ce2d1b9b -r 3c1ce1b4eb3d src/expl_util.sml
--- a/src/expl_util.sml	Thu Jun 19 17:04:08 2008 -0400
+++ b/src/expl_util.sml	Thu Jun 19 17:11:24 2008 -0400
@@ -353,6 +353,19 @@
                         (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)))
+              | SgnWhere (sgn, x, c) =>
+                S.bind2 (sg ctx sgn,
+                      fn sgn' =>
+                         S.map2 (con ctx c,
+                              fn c' =>
+                                 (SgnWhere (sgn', x, c'), loc)))
     in
         sg
     end
diff -r a9f3ce2d1b9b -r 3c1ce1b4eb3d src/explify.sml
--- a/src/explify.sml	Thu Jun 19 17:04:08 2008 -0400
+++ b/src/explify.sml	Thu Jun 19 17:11:24 2008 -0400
@@ -92,8 +92,8 @@
     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.SgnWhere _ => raise Fail "Explify where"
+      | 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.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
 
 fun explifyDecl (d, loc : EM.span) =
@@ -109,8 +109,8 @@
         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.StrApp _ => raise Fail "Explify functor app"
+      | L.StrFun (m, n, dom, ran, str) => (L'.StrFun (m, n, explifySgn dom, explifySgn ran, explifyStr str), loc)
+      | L.StrApp (str1, str2) => (L'.StrApp (explifyStr str1, explifyStr str2), loc)
       | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc)
 
 val explify = map explifyDecl