diff src/elaborate.sml @ 61:48b6d2c3df46

open
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 19:34:35 -0400
parents abb2b32c19fb
children d72b89a1b150
line wrap: on
line diff
--- a/src/elaborate.sml	Sun Jun 22 19:10:47 2008 -0400
+++ b/src/elaborate.sml	Sun Jun 22 19:34:35 2008 -0400
@@ -1016,6 +1016,7 @@
          UnboundStr of ErrorMsg.span * string
        | NotFunctor of L'.sgn
        | FunctorRebind of ErrorMsg.span
+       | UnOpenable of L'.sgn
 
 fun strError env err =
     case err of
@@ -1026,6 +1027,9 @@
          eprefaces' [("Signature", p_sgn env sgn)])
       | FunctorRebind loc =>
         ErrorMsg.errorAt loc "Attempt to rebind functor"
+      | UnOpenable sgn =>
+        (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
+         eprefaces' [("Signature", p_sgn env sgn)])
 
 val hnormSgn = E.hnormSgn
 
@@ -1360,6 +1364,35 @@
           | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
     end
 
+fun dopen env {str, strs, sgn} =
+    let
+        val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
+                (L'.StrVar str, #2 sgn) strs
+    in
+        case #1 (hnormSgn env sgn) of
+            L'.SgnConst sgis =>
+            ListUtil.foldlMap (fn ((sgi, loc), env') =>
+                                  case sgi of
+                                      L'.SgiConAbs (x, n, k) =>
+                                      ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
+                                       E.pushCNamedAs env' x n k NONE)
+                                    | L'.SgiCon (x, n, k, c) =>
+                                      ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
+                                       E.pushCNamedAs env' x n k (SOME c))
+                                    | L'.SgiVal (x, n, t) =>
+                                      ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
+                                       E.pushENamedAs env' x n t)
+                                    | L'.SgiStr (x, n, sgn) =>
+                                      ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
+                                       E.pushStrNamedAs env' x n sgn)
+                                    | L'.SgiSgn (x, n, sgn) =>
+                                      ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
+                                       E.pushSgnNamedAs env' x n sgn))
+                              env sgis
+          | _ => (strError env (UnOpenable sgn);
+                  ([], env))
+    end
+
 fun elabDecl ((d, loc), env) =
     let
         
@@ -1392,7 +1425,7 @@
                         ()
                     );
 
-                ((L'.DCon (x, n, k', c'), loc), env')
+                ([(L'.DCon (x, n, k', c'), loc)], env')
             end
           | L.DVal (x, co, e) =>
             let
@@ -1428,7 +1461,7 @@
                     else
                         ());
 
-                ((L'.DVal (x, n, c', e'), loc), env')
+                ([(L'.DVal (x, n, c', e'), loc)], env')
             end
 
           | L.DSgn (x, sgn) =>
@@ -1436,7 +1469,7 @@
                 val sgn' = elabSgn env sgn
                 val (env', n) = E.pushSgnNamed env x sgn'
             in
-                ((L'.DSgn (x, n, sgn'), loc), env')
+                ([(L'.DSgn (x, n, sgn'), loc)], env')
             end
 
           | L.DStr (x, sgno, str) =>
@@ -1459,7 +1492,7 @@
                        | _ => strError env (FunctorRebind loc))
                   | _ => ();
 
-                ((L'.DStr (x, n, sgn', str'), loc), env')
+                ([(L'.DStr (x, n, sgn', str'), loc)], env')
             end
 
           | L.DFfiStr (x, sgn) =>
@@ -1468,15 +1501,31 @@
 
                 val (env', n) = E.pushStrNamed env x sgn'
             in
-                ((L'.DFfiStr (x, n, sgn'), loc), env')
+                ([(L'.DFfiStr (x, n, sgn'), loc)], env')
             end
+
+          | L.DOpen (m, ms) =>
+            (case E.lookupStr env m of
+                 NONE => (strError env (UnboundStr (loc, m));
+                          ([], env))
+               | SOME (n, sgn) =>
+                 let
+                     val (_, sgn) = foldl (fn (m, (str, sgn)) =>
+                                              case E.projectStr env {str = str, sgn = sgn, field = m} of
+                                                  NONE => (strError env (UnboundStr (loc, m));
+                                                           (strerror, sgnerror))
+                                                | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                                          ((L'.StrVar n, loc), sgn) ms
+                 in
+                     dopen env {str = n, strs = ms, sgn = sgn}
+                 end)
     end
 
 and elabStr env (str, loc) =
     case str of
         L.StrConst ds =>
         let
-            val (ds', env') = ListUtil.foldlMap elabDecl env ds
+            val (ds', env') = ListUtil.foldlMapConcat elabDecl env ds
             val sgis = map sgiOfDecl ds'
         in
             ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
@@ -1540,28 +1589,7 @@
         val sgn = elabSgn env (L.SgnConst basis, ErrorMsg.dummySpan)
         val (env', basis_n) = E.pushStrNamed env "Basis" sgn
 
-        val (ds, env') =
-            case #1 (hnormSgn env' sgn) of
-                L'.SgnConst sgis =>
-                ListUtil.foldlMap (fn ((sgi, loc), env') =>
-                                      case sgi of
-                                          L'.SgiConAbs (x, n, k) =>
-                                          ((L'.DCon (x, n, k, (L'.CModProj (basis_n, [], x), loc)), loc),
-                                           E.pushCNamedAs env' x n k NONE)
-                                        | L'.SgiCon (x, n, k, c) =>
-                                          ((L'.DCon (x, n, k, (L'.CModProj (basis_n, [], x), loc)), loc),
-                                           E.pushCNamedAs env' x n k (SOME c))
-                                        | L'.SgiVal (x, n, t) =>
-                                          ((L'.DVal (x, n, t, (L'.EModProj (basis_n, [], x), loc)), loc),
-                                           E.pushENamedAs env' x n t)
-                                        | L'.SgiStr (x, n, sgn) =>
-                                          ((L'.DStr (x, n, sgn, (L'.StrProj ((L'.StrVar basis_n, loc), x), loc)), loc),
-                                           E.pushStrNamedAs env' x n sgn)
-                                        | L'.SgiSgn (x, n, sgn) =>
-                                          ((L'.DSgn (x, n, (L'.SgnProj (basis_n, [], x), loc)), loc),
-                                           E.pushSgnNamedAs env' x n sgn))
-                env' sgis
-              | _ => raise Fail "Non-constant Basis signature"
+        val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn}
 
         fun discoverC r x =
             case E.lookupC env' x of
@@ -1573,7 +1601,7 @@
         val () = discoverC float "float"
         val () = discoverC string "string"
 
-        val (file, _) = ListUtil.foldlMap elabDecl env' file
+        val (file, _) = ListUtil.foldlMapConcat elabDecl env' file
     in
         (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
     end