Elaborating 'where'

11 files changed, 121 insertions, 43 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 07bb7f8d..edec2e3d 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -92,6 +92,7 @@ and sgn' =
     SgnConst of sgn_item list
   | SgnVar of int
   | SgnFun of string * int * sgn * sgn
+  | SgnWhere of sgn * string * con
   | SgnError
 
 withtype sgn_item = sgn_item' located
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 98f59c38..511497c4 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -76,10 +76,10 @@ signature ELAB_ENV = sig
     val declBinds : env -> Elab.decl -> env
     val sgiBinds : env -> Elab.sgn_item -> env
 
+    val hnormSgn : env -> Elab.sgn -> Elab.sgn
+
     val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option
     val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option
     val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
 
-
-
 end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 9d308ddc..6f20733a 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -361,52 +361,61 @@ fun sgnSubSgn (str, (strs, cons)) =
                       sgn_item = id,
                       sgn = id}
 
-fun projectCon env {sgn = (sgn, _), str, field} =
+fun hnormSgn env (all as (sgn, loc)) =
     case sgn of
+        SgnError => all
+      | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
+      | SgnConst _ => all
+      | SgnFun _ => all
+      | 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]"
+
+fun projectCon env {sgn, str, field} =
+    case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
         (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
                         | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
                         | _ => NONE) sgis of
              NONE => NONE
            | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
-      | SgnVar n =>
-        let
-            val (_, sgn) = lookupSgnNamed env n
-        in
-            projectCon env {sgn = sgn, str = str, field = field}
-        end
       | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
-      | SgnFun _ => NONE
+      | _ => NONE
 
-fun projectVal env {sgn = (sgn, _), str, field} =
-    case sgn of
+fun projectVal env {sgn, str, field} =
+    case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
         (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of
              NONE => NONE
            | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
-      | SgnVar n =>
-        let
-            val (_, sgn) = lookupSgnNamed env n
-        in
-            projectVal env {sgn = sgn, str = str, field = field}
-        end
       | SgnError => SOME (CError, ErrorMsg.dummySpan)
-      | SgnFun _ => NONE
+      | _ => NONE
 
-fun projectStr env {sgn = (sgn, _), str, field} =
-    case sgn of
+fun projectStr env {sgn, str, field} =
+    case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
         (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
              NONE => NONE
            | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
-      | SgnVar n =>
-        let
-            val (_, sgn) = lookupSgnNamed env n
-        in
-            projectStr env {sgn = sgn, str = str, field = field}
-        end
       | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
-      | SgnFun _ => NONE
+      | _ => NONE
 
 
 val ktype = (KType, ErrorMsg.dummySpan)
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 03792e03..88dcdfaa 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -323,6 +323,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]
       | SgnError => string "<ERROR>"
 
 fun p_decl env ((d, _) : decl) =
diff --git a/src/elab_util.sml b/src/elab_util.sml
index e2b4f113..e112a180 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -370,6 +370,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) =>
+                S.bind2 (sg ctx sgn,
+                      fn sgn' =>
+                         S.map2 (con ctx c,
+                              fn c' =>
+                                 (SgnWhere (sgn', x, c'), loc)))
               | SgnError => S.return2 sAll
     in
         sg
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 10fa3898..9c96060d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -239,7 +239,7 @@ fun elabCon env (c, loc) =
              ((L'.CNamed n, loc), k))
       | L.CVar (m1 :: ms, s) =>
         (case E.lookupStr env m1 of
-             NONE => (conError env (UnboundStrInCon (loc, s));
+             NONE => (conError env (UnboundStrInCon (loc, m1));
                       (cerror, kerror))
            | SOME (n, sgn) =>
              let
@@ -824,7 +824,7 @@ fun elabExp env (e, loc) =
            | E.Named (n, t) => ((L'.ENamed n, loc), t))
       | L.EVar (m1 :: ms, s) =>
         (case E.lookupStr env m1 of
-             NONE => (expError env (UnboundStrInExp (loc, s));
+             NONE => (expError env (UnboundStrInExp (loc, m1));
                       (eerror, cerror))
            | SOME (n, sgn) =>
              let
@@ -969,6 +969,7 @@ datatype sgn_error =
        | 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
+       | UnWhereable of L'.sgn * string
 
 fun sgnError env err =
     case err of
@@ -995,6 +996,10 @@ fun sgnError env err =
         (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
          eprefaces' [("Sig 1", p_sgn env sgn1),
                      ("Sig 2", p_sgn env sgn2)])
+      | UnWhereable (sgn, x) =>
+        (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
+         eprefaces' [("Signature", p_sgn env sgn),
+                     ("Field", PD.string x)])
 
 datatype str_error =
          UnboundStr of ErrorMsg.span * string
@@ -1004,6 +1009,7 @@ fun strError env err =
         UnboundStr (loc, s) =>
         ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
 
+val hnormSgn = E.hnormSgn
 
 fun elabSgn_item ((sgi, loc), env) =
     let
@@ -1110,6 +1116,25 @@ and elabSgn env (sgn, loc) =
         in
             (L'.SgnFun (m, n, dom', ran'), loc)
         end
+      | L.SgnWhere (sgn, x, c) =>
+        let
+            val sgn' = elabSgn env sgn
+            val (c', ck) = elabCon env c
+        in
+            case #1 (hnormSgn env sgn') of
+                L'.SgnError => sgnerror
+              | L'.SgnConst sgis =>
+                if List.exists (fn (L'.SgiConAbs (x, _, k), _) =>
+                                   (unifyKinds k ck;
+                                    true)
+                                 | _ => false) sgis then
+                    (L'.SgnWhere (sgn', x, c'), loc)
+                else
+                    (sgnError env (UnWhereable (sgn', x));
+                     sgnerror)
+              | _ => (sgnError env (UnWhereable (sgn', x));
+                      sgnerror)
+        end
 
 fun sgiOfDecl (d, loc) =
     case d of
@@ -1118,13 +1143,6 @@ fun sgiOfDecl (d, loc) =
       | L'.DSgn _ => NONE
       | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
 
-fun hnormSgn env (all as (sgn, _)) =
-    case sgn of
-        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, _) => ()
@@ -1240,6 +1258,7 @@ fun selfify env {str, strs, sgn} =
                               (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
                             | x => x) sgis), #2 sgn)
       | L'.SgnFun _ => sgn
+      | L'.SgnWhere _ => sgn
 
 fun elabDecl ((d, loc), env) =
     let
@@ -1384,7 +1403,7 @@ and elabStr env (str, loc) =
                     NONE => actual
                   | SOME ran =>
                     let
-                        val ran' = elabSgn env ran
+                        val ran' = elabSgn env' ran
                     in
                         subSgn env' actual ran';
                         ran'
diff --git a/src/explify.sml b/src/explify.sml
index caba15d1..73c9aed2 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -93,6 +93,7 @@ and explifySgn (sgn, loc) =
         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.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
 
 fun explifyDecl (d, loc : EM.span) =
diff --git a/src/lacweb.grm b/src/lacweb.grm
index ea40c236..e917396c 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -44,7 +44,7 @@ val s = ErrorMsg.spanOf
  | TYPE | NAME
  | ARROW | LARROW | DARROW
  | FN | PLUSPLUS | DOLLAR
- | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR
+ | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE
 
 %nonterm
    file of decl list
@@ -52,6 +52,7 @@ val s = ErrorMsg.spanOf
  | decl of decl
 
  | sgn of sgn
+ | sgntm of sgn
  | sgi of sgn_item
  | sgis of sgn_item list
 
@@ -110,12 +111,25 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
        | SIGNATURE CSYMBOL EQ sgn       (DSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
        | STRUCTURE CSYMBOL EQ str       (DStr (CSYMBOL, NONE, str), s (STRUCTUREleft, strright))
        | STRUCTURE CSYMBOL COLON sgn EQ str (DStr (CSYMBOL, SOME sgn, str), s (STRUCTUREleft, strright))
-
-sgn    : SIG sgis END                   (SgnConst sgis, s (SIGleft, ENDright))
-       | CSYMBOL                        (SgnVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+       | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN EQ str
+                                        (DStr (CSYMBOL1, NONE,
+                                               (StrFun (CSYMBOL2, sgn1, NONE, str), s (FUNCTORleft, strright))),
+                                         s (FUNCTORleft, strright))
+       | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn EQ str
+                                        (DStr (CSYMBOL1, NONE,
+                                               (StrFun (CSYMBOL2, sgn1, SOME sgn2, str), s (FUNCTORleft, strright))),
+                                         s (FUNCTORleft, strright))
+
+sgn    : sgntm                          (sgntm)
        | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
                                         (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right))
 
+sgntm  : SIG sgis END                   (SgnConst sgis, s (SIGleft, ENDright))
+       | CSYMBOL                        (SgnVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+       | 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))
+       | LPAREN sgn RPAREN              (sgn)
+
 sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, kindright))
        | LTYPE SYMBOL                   (SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))),
                                          s (LTYPEleft, SYMBOLright))
@@ -126,6 +140,10 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
        | VAL SYMBOL COLON cexp          (SgiVal (SYMBOL, cexp), s (VALleft, cexpright))
 
        | STRUCTURE CSYMBOL COLON sgn    (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright))
+       | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
+                                        (SgiStr (CSYMBOL1,
+                                                 (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
+                                         s (FUNCTORleft, sgn2right))
 
 sgis   :                                ([])
        | sgi sgis                       (sgi :: sgis)
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 56f19060..337da093 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -134,6 +134,7 @@ realconst = [0-9]+\.[0-9]*;
 <INITIAL> "sig"       => (Tokens.SIG (yypos, yypos + size yytext));
 <INITIAL> "end"       => (Tokens.END (yypos, yypos + size yytext));
 <INITIAL> "functor"   => (Tokens.FUNCTOR (yypos, yypos + size yytext));
+<INITIAL> "where"     => (Tokens.WHERE (yypos, yypos + size yytext));
 
 <INITIAL> "Type"      => (Tokens.TYPE (yypos, yypos + size yytext));
 <INITIAL> "Name"      => (Tokens.NAME (yypos, yypos + size yytext));
diff --git a/src/source.sml b/src/source.sml
index 6f8c932f..1bcb248c 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -72,6 +72,7 @@ and sgn' =
     SgnConst of sgn_item list
   | SgnVar of string
   | SgnFun of string * sgn * sgn
+  | SgnWhere of sgn * string * con
 
 withtype sgn_item = sgn_item' located
 and sgn = sgn' located
diff --git a/src/source_print.sml b/src/source_print.sml
index fb416a60..c3a333e8 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -259,7 +259,18 @@ 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]
+
 fun p_decl ((d, _) : decl) =
     case d of
         DCon (x, NONE, c) => box [string "con",