Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items

12 files changed, 120 insertions, 74 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 9147f7d3..2dab5c34 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -154,7 +154,7 @@ and sgn' =
     SgnConst of sgn_item list
   | SgnVar of int
   | SgnFun of string * int * sgn * sgn
-  | SgnWhere of sgn * string * con
+  | SgnWhere of sgn * string list * string * con
   | SgnProj of int * string list * string
   | SgnError
 
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 5d684817..465fb7e4 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1126,26 +1126,44 @@ and hnormSgn env (all as (sgn, loc)) =
                 NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
               | SOME sgn => hnormSgn env sgn
         end
-      | SgnWhere (sgn, x, c) =>
-        case #1 (hnormSgn env sgn) of
-            SgnError => (SgnError, loc)
-          | SgnConst sgis =>
-            let
-                fun traverse (pre, post) =
-                    case post of
-                        [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
-                      | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
-                        if x = x' then
-                            List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
-                        else
-                            traverse (sgi :: pre, rest)
-                      | sgi :: rest => traverse (sgi :: pre, rest)
-
-                val sgis = traverse ([], sgis)
-            in
-                (SgnConst sgis, loc)
-            end
-          | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
+      | SgnWhere (sgn, ms, x, c) =>
+	let
+	    fun rewrite (sgn, ms) =
+		case #1 (hnormSgn env sgn) of
+		    SgnError => (SgnError, loc)
+		  | SgnConst sgis =>
+		    let
+			fun traverse (ms, pre, post) =
+			    case post of
+				[] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
+
+			      | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
+				if List.null ms andalso x = x' then
+				    List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
+				else
+				    traverse (ms, sgi :: pre, rest)
+
+			      | (sgi as (SgiStr (x', n, sgn'), loc)) :: rest =>
+				(case ms of
+				     [] => traverse (ms, sgi :: pre, rest)
+				   | x :: ms' =>
+				     if x = x' then
+					 List.revAppend (pre,
+							 (SgiStr (x', n,
+								  rewrite (sgn', ms')), loc) :: rest)
+				     else
+					 traverse (ms, sgi :: pre, rest))
+
+			      | sgi :: rest => traverse (ms, sgi :: pre, rest)
+					       
+			val sgis = traverse (ms, [], sgis)
+		    in
+			(SgnConst sgis, loc)
+		    end
+		  | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
+	in
+	    rewrite (sgn, ms)
+	end
 
 fun manifest (m, ms, loc) =
     foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms
diff --git a/src/elab_print.sml b/src/elab_print.sml
index c32368a9..7ce94c97 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -680,17 +680,17 @@ and p_sgn env (sgn, _) =
                                          string ":",
                                          space,
                                          p_sgn (E.pushStrNamedAs 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]
+      | SgnWhere (sgn, ms, x, c) => box [p_sgn env sgn,
+					 space,
+					 string "where",
+					 space,
+					 string "con",
+					 space,
+					 p_list_sep (string ".") string (ms @ [x]),
+					 space,
+					 string "=",
+					 space,
+					 p_con env c]
       | SgnProj (m1, ms, x) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 51bcba5a..60245585 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -759,12 +759,12 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                     fn s2' =>
                                        (SgnFun (m, n, s1', s2'), loc)))
               | SgnProj _ => S.return2 sAll
-              | SgnWhere (sgn, x, c) =>
+              | SgnWhere (sgn, ms, x, c) =>
                 S.bind2 (sg ctx sgn,
                       fn sgn' =>
                          S.map2 (con ctx c,
                               fn c' =>
-                                 (SgnWhere (sgn', x, c'), loc)))
+                                 (SgnWhere (sgn', ms, x, c'), loc)))
               | SgnError => S.return2 sAll
     in
         sg
@@ -1248,7 +1248,7 @@ and maxNameSgn (sgn, _) =
         SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
       | SgnVar n => n
       | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
-      | SgnWhere (sgn, _, _) => maxNameSgn sgn
+      | SgnWhere (sgn, _, _, _) => maxNameSgn sgn
       | SgnProj (n, _, _) => n
       | SgnError => 0
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 426934bd..18010244 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2013, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -2640,8 +2640,9 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
          let
              val (sgn', gs') = elabSgn (env, denv) sgn
              val (env', n) = E.pushStrNamed env x sgn'
+             val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []}
          in
-             ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
+             ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv', gs' @ gs))
          end
 
        | L.SgiSgn (x, sgn) =>
@@ -2798,26 +2799,33 @@ and elabSgn (env, denv) (sgn, loc) =
         in
             ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
         end
-      | L.SgnWhere (sgn, x, c) =>
+      | L.SgnWhere (sgn, ms, x, c) =>
         let
             val (sgn', ds1) = elabSgn (env, denv) sgn
             val (c', ck, ds2) = elabCon (env, denv) c
-        in
-            case #1 (hnormSgn env sgn') of
-                L'.SgnError => (sgnerror, [])
-              | L'.SgnConst sgis =>
-                if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
-                                   x' = x andalso
-                                   (unifyKinds env k ck
-                                    handle KUnify x => sgnError env (WhereWrongKind x);
-                                    true)
-                                 | _ => false) sgis then
-                    ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2)
-                else
-                    (sgnError env (UnWhereable (sgn', x));
-                     (sgnerror, []))
-              | _ => (sgnError env (UnWhereable (sgn', x));
-                      (sgnerror, []))
+
+	    fun checkPath (ms, sgn') =
+		case #1 (hnormSgn env sgn') of
+		    L'.SgnConst sgis =>
+                    List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
+                                    List.null ms andalso x' = x andalso
+                                    (unifyKinds env k ck
+				     handle KUnify x => sgnError env (WhereWrongKind x);
+				     true)
+				  | (L'.SgiStr (x', _, sgn''), _) =>
+				    (case ms of
+					 [] => false
+				       | m :: ms' =>
+					 m = x' andalso
+					 checkPath (ms', sgn''))
+                                  | _ => false) sgis
+		  | _ => false
+	in
+	    if checkPath (ms, sgn') then
+                ((L'.SgnWhere (sgn', ms, x, c'), loc), ds1 @ ds2)
+            else
+                (sgnError env (UnWhereable (sgn', x));
+                 (sgnerror, []))
         end
       | L.SgnProj (m, ms, x) =>
         (case E.lookupStr env m of
@@ -3594,6 +3602,24 @@ and wildifyStr env (str, sgn) =
                               (SOME f, SOME x) => SOME (L.CApp (f, x), loc)
                             | _ => NONE)
 
+		       | L'.CTuple cs =>
+			 let
+			     val cs' = foldr (fn (c, cs') =>
+						 case cs' of
+						     NONE => NONE
+						   | SOME cs' =>
+						     case decompileCon env c of
+							 NONE => NONE
+						       | SOME c' => SOME (c' :: cs'))
+				       (SOME []) cs
+			 in
+			     case cs' of
+				 NONE => NONE
+			       | SOME cs' => SOME (L.CTuple cs', loc)
+			 end
+
+		       | L'.CMap _ => SOME (L.CMap, loc)
+
                        | c => (Print.preface ("WTF?", p_con env (c, loc)); NONE)
 
                  fun buildNeeded env sgis =
diff --git a/src/expl.sml b/src/expl.sml
index 119c1d92..0d4e63cc 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -125,7 +125,7 @@ and sgn' =
     SgnConst of sgn_item list
   | SgnVar of int
   | SgnFun of string * int * sgn * sgn
-  | SgnWhere of sgn * string * con
+  | SgnWhere of sgn * string list * string * con
   | SgnProj of int * string list * string
 
 withtype sgn_item = sgn_item' located
diff --git a/src/expl_print.sml b/src/expl_print.sml
index d89b0512..a830dccb 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -569,13 +569,13 @@ and p_sgn env (sgn, loc) =
                                          string ":",
                                          space,
                                          p_sgn (E.pushStrNamed env x n sgn) sgn']
-      | SgnWhere (sgn, x, c) => box [p_sgn env sgn,
+      | SgnWhere (sgn, ms, x, c) => box [p_sgn env sgn,
                                      space,
                                      string "where",
                                      space,
                                      string "con",
                                      space,
-                                     string x,
+                                     p_list_sep (string ".") string (ms @ [x]),
                                      space,
                                      string "=",
                                      space,
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 1932d52d..ff55823f 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -526,12 +526,12 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                             S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
                                     fn s2' =>
                                        (SgnFun (m, n, s1', s2'), loc)))
-              | SgnWhere (sgn, x, c) =>
+              | SgnWhere (sgn, ms, x, c) =>
                 S.bind2 (sg ctx sgn,
                       fn sgn' =>
                          S.map2 (con ctx c,
                               fn c' =>
-                                 (SgnWhere (sgn', x, c'), loc)))
+                                 (SgnWhere (sgn', ms, x, c'), loc)))
               | SgnProj _ => S.return2 sAll
     in
         sg
diff --git a/src/explify.sml b/src/explify.sml
index 65e78443..4c60bd20 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -162,7 +162,7 @@ and explifySgn (sgn, loc) =
         L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc)
       | L.SgnVar n => (L'.SgnVar n, loc)
       | 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.SgnWhere (sgn, ms, x, c) => (L'.SgnWhere (explifySgn sgn, ms, x, explifyCon c), loc)
       | L.SgnProj x => (L'.SgnProj x, loc)
       | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
 
diff --git a/src/source.sml b/src/source.sml
index 18f83d2b..d66160db 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -100,7 +100,7 @@ and sgn' =
     SgnConst of sgn_item list
   | SgnVar of string
   | SgnFun of string * sgn * sgn
-  | SgnWhere of sgn * string * con
+  | SgnWhere of sgn * string list * string * con
   | SgnProj of string * string list * string
 
 and pat' =
diff --git a/src/source_print.sml b/src/source_print.sml
index cd3314e1..c8a38922 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -505,17 +505,19 @@ and p_sgn (sgn, _) =
                                       string ":",
                                       space,
                                       p_sgn sgn']
-      | SgnWhere (sgn, x, c) => box [p_sgn sgn,
-                                     space,
-                                     string "where",
-                                     space,
-                                     string "con",
-                                     space,
-                                     string x,
-                                     space,
-                                     string "=",
-                                     space,
-                                     p_con c]
+      | SgnWhere (sgn, ms, x, c) => box [p_sgn sgn,
+					 space,
+					 string "where",
+					 space,
+					 string "con",
+					 space,
+					 p_list_sep (string ".")
+						    string (ms @ [x]),
+					 string x,
+					 space,
+					 string "=",
+					 space,
+					 p_con c]
       | SgnProj (m, ms, x) => p_list_sep (string ".") string (m :: ms @ [x])
                                    
 
diff --git a/src/urweb.grm b/src/urweb.grm
index c2a48742..29019649 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -802,8 +802,8 @@ sgntm  : SIG sgis END                   (SgnConst sgis, s (SIGleft, ENDright))
                                                                  List.take (ms, length ms - 1),
                                                                  List.nth (ms, length ms - 1)),
                                          s (mpathleft, mpathright))
-       | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
-       | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
+       | sgntm WHERE CON path EQ cexp   (SgnWhere (sgntm, #1 path, #2 path, cexp), s (sgntmleft, cexpright))
+       | sgntm WHERE LTYPE path EQ cexp (SgnWhere (sgntm, #1 path, #2 path, cexp), s (sgntmleft, cexpright))
        | LPAREN sgn RPAREN              (sgn)
 
 cexpO  :                                (NONE)