changeset 174:7ee424760d2f

Elaborating module constructor patterns; parsing record patterns
author Adam Chlipala <adamc@hcoop.net>
date Thu, 31 Jul 2008 11:28:55 -0400
parents 8221b95cc24c
children b2d752455182
files src/elab_env.sig src/elab_env.sml src/elaborate.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/caseMod.lac
diffstat 8 files changed, 125 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab_env.sig	Thu Jul 31 10:44:52 2008 -0400
+++ b/src/elab_env.sig	Thu Jul 31 11:28:55 2008 -0400
@@ -88,6 +88,8 @@
     val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option
     val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
                           -> (string * int * Elab.con option) list option
+    val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
+                             -> (int * Elab.con option * Elab.con) option
     val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option
     val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
     val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
--- a/src/elab_env.sml	Thu Jul 31 10:44:52 2008 -0400
+++ b/src/elab_env.sml	Thu Jul 31 11:28:55 2008 -0400
@@ -570,6 +570,25 @@
            | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
       | _ => NONE
 
+fun projectConstructor env {sgn, str, field} =
+    case #1 (hnormSgn env sgn) of
+        SgnConst sgis =>
+        let
+            fun consider (n, xncs) =
+                ListUtil.search (fn (x, n', to) =>
+                                    if x <> field then
+                                        NONE
+                                    else
+                                        SOME (n', to, (CNamed n, #2 str))) xncs
+        in
+            case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs)
+                           | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs)
+                           | _ => NONE) sgis of
+                NONE => NONE
+              | SOME ((n, to, t), subs) => SOME (n, Option.map (sgnSubCon (str, subs)) to, sgnSubCon (str, subs) t)
+        end
+      | _ => NONE
+
 fun projectVal env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
--- a/src/elaborate.sml	Thu Jul 31 10:44:52 2008 -0400
+++ b/src/elaborate.sml	Thu Jul 31 11:28:55 2008 -0400
@@ -812,7 +812,7 @@
      | IncompatibleCons of L'.con * L'.con
      | DuplicatePatternVariable of ErrorMsg.span * string
      | PatUnify of L'.pat * L'.con * L'.con * cunify_error
-     | UnboundConstructor of ErrorMsg.span * string
+     | UnboundConstructor of ErrorMsg.span * string list * string
      | PatHasArg of ErrorMsg.span
      | PatHasNoArg of ErrorMsg.span
      | Inexhaustive of ErrorMsg.span
@@ -848,8 +848,8 @@
                      ("Have con", p_con env c1),
                      ("Need con", p_con env c2)];
          cunifyError env uerr)
-      | UnboundConstructor (loc, s) =>
-        ErrorMsg.errorAt loc ("Unbound constructor " ^ s ^ " in pattern")
+      | UnboundConstructor (loc, ms, s) =>
+        ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
       | PatHasArg loc =>
         ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
       | PatHasNoArg loc =>
@@ -958,7 +958,7 @@
         unravel (t, e)
     end
 
-fun elabPat (pAll as (p, loc), (env, bound)) =
+fun elabPat (pAll as (p, loc), (env, denv, bound)) =
     let
         val perror = (L'.PWild, loc)
         val terror = (L'.CError, loc)
@@ -972,13 +972,13 @@
                                        rerror)
                   | (SOME _, NONE) => (expError env (PatHasArg loc);
                                        rerror)
-                  | (NONE, NONE) => (((L'.PCon (pc, NONE), loc), (L'.CNamed dn, loc)),
+                  | (NONE, NONE) => (((L'.PCon (pc, NONE), loc), dn),
                                      (env, bound))
                   | (SOME p, SOME t) =>
                     let
-                        val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
+                        val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
                     in
-                        (((L'.PCon (pc, SOME p'), loc), (L'.CNamed dn, loc)),
+                        (((L'.PCon (pc, SOME p'), loc), dn),
                          (env, bound))
                     end
     in
@@ -1000,10 +1000,28 @@
                           (env, bound))
           | L.PCon ([], x, po) =>
             (case E.lookupConstructor env x of
-                 NONE => (expError env (UnboundConstructor (loc, x));
+                 NONE => (expError env (UnboundConstructor (loc, [], x));
                           rerror)
-               | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, dn))
-          | L.PCon _ => raise Fail "uhoh"
+               | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc)))
+          | L.PCon (m1 :: ms, x, po) =>
+            (case E.lookupStr env m1 of
+                 NONE => (expError env (UnboundStrInExp (loc, m1));
+                          rerror)
+               | SOME (n, sgn) =>
+                 let
+                     val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                                case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                                    NONE => raise Fail "typeof: Unknown substructure"
+                                                  | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                                            ((L'.StrVar n, loc), sgn) ms
+                 in
+                     case E.projectConstructor env {str = str, sgn = sgn, field = x} of
+                         NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
+                                  rerror)
+                       | SOME (_, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn)
+                 end)
+
+          | L.PRecord _ => raise Fail "Elaborate PRecord"
     end
 
 datatype coverage =
@@ -1016,7 +1034,14 @@
         fun pcCoverage pc =
             case pc of
                 L'.PConVar n => n
-              | _ => raise Fail "uh oh^2"
+              | L'.PConProj (m1, ms, x) =>
+                let
+                    val (str, sgn) = E.chaseMpath env (m1, ms)
+                in
+                    case E.projectConstructor env {str = str, sgn = sgn, field = x} of
+                        NONE => raise Fail "exhaustive: Can't project constructor"
+                      | SOME (n, _, _) => n
+                end
 
         fun coverage (p, _) =
             case p of
@@ -1049,6 +1074,21 @@
               | Datatype cm =>
                 let
                     val ((t, _), gs) = hnormCon (env, denv) t
+
+                    fun dtype cons =
+                        foldl (fn ((_, n, to), (total, gs)) =>
+                                  case IM.find (cm, n) of
+                                      NONE => (false, gs)
+                                    | SOME c' =>
+                                      case to of
+                                          NONE => (total, gs)
+                                        | SOME t' =>
+                                          let
+                                              val (total, gs') = isTotal (c', t')
+                                          in
+                                              (total, gs' @ gs)
+                                          end)
+                              (true, gs) cons
                 in
                     case t of
                         L'.CNamed n =>
@@ -1056,19 +1096,15 @@
                             val dt = E.lookupDatatype env n
                             val cons = E.constructors dt
                         in
-                            foldl (fn ((_, n, to), (total, gs)) =>
-                                      case IM.find (cm, n) of
-                                          NONE => (false, gs)
-                                        | SOME c' =>
-                                          case to of
-                                              NONE => (total, gs)
-                                            | SOME t' =>
-                                              let
-                                                  val (total, gs') = isTotal (c', t')
-                                              in
-                                                  (total, gs' @ gs)
-                                              end)
-                                  (true, gs) cons
+                            dtype cons
+                        end
+                      | L'.CModProj (m1, ms, x) =>
+                        let
+                            val (str, sgn) = E.chaseMpath env (m1, ms)
+                        in
+                            case E.projectDatatype env {str = str, sgn = sgn, field = x} of
+                                NONE => raise Fail "isTotal: Can't project datatype"
+                              | SOME cons => dtype cons
                         end
                       | L'.CError => (true, gs)
                       | _ => raise Fail "isTotal: Not a datatype"
@@ -1295,7 +1331,7 @@
                 val (pes', gs) = ListUtil.foldlMap
                                  (fn ((p, e), gs) =>
                                      let
-                                         val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty))
+                                         val ((p', pt), (env, _)) = elabPat (p, (env, denv, SS.empty))
 
                                          val gs1 = checkPatCon (env, denv) p' pt et
                                          val (e', et, gs2) = elabExp (env, denv) e
--- a/src/lacweb.grm	Thu Jul 31 10:44:52 2008 -0400
+++ b/src/lacweb.grm	Thu Jul 31 11:28:55 2008 -0400
@@ -43,7 +43,7 @@
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
- | DIVIDE | GT
+ | DIVIDE | GT | DOTDOTDOT
  | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT
  | DATATYPE | OF
  | TYPE | NAME
@@ -104,6 +104,7 @@
  | branchs of (pat * exp) list
  | pat of pat
  | pterm of pat
+ | rpat of (string * pat) list * bool
 
  | attrs of (con * exp) list
  | attr of con * exp
@@ -351,6 +352,13 @@
        | INT                            (PPrim (Prim.Int INT), s (INTleft, INTright))
        | STRING                         (PPrim (Prim.String STRING), s (STRINGleft, STRINGright))
        | LPAREN pat RPAREN              (pat)
+       | LBRACE RBRACE                  (PRecord ([], false), s (LBRACEleft, RBRACEright))
+       | UNIT                           (PRecord ([], false), s (UNITleft, UNITright))
+       | LBRACE rpat RBRACE             (PRecord rpat, s (LBRACEleft, RBRACEright))
+
+rpat   : STRING EQ pat                  ([(STRING, pat)], false)
+       | DOTDOTDOT                      ([], true)
+       | STRING EQ pat COMMA rpat       ((STRING, pat) :: #1 rpat, #2 rpat)
 
 rexp   :                                ([])
        | ident EQ eexp                  ([(ident, eexp)])
--- a/src/lacweb.lex	Thu Jul 31 10:44:52 2008 -0400
+++ b/src/lacweb.lex	Thu Jul 31 11:28:55 2008 -0400
@@ -242,6 +242,7 @@
 <INITIAL> ":::"       => (Tokens.TCOLON (pos yypos, pos yypos + size yytext));
 <INITIAL> "::"        => (Tokens.DCOLON (pos yypos, pos yypos + size yytext));
 <INITIAL> ":"         => (Tokens.COLON (pos yypos, pos yypos + size yytext));
+<INITIAL> "..."       => (Tokens.DOTDOTDOT (pos yypos, pos yypos + size yytext));
 <INITIAL> "."         => (Tokens.DOT (pos yypos, pos yypos + size yytext));
 <INITIAL> "$"         => (Tokens.DOLLAR (pos yypos, pos yypos + size yytext));
 <INITIAL> "#"         => (Tokens.HASH (pos yypos, pos yypos + size yytext));
--- a/src/source.sml	Thu Jul 31 10:44:52 2008 -0400
+++ b/src/source.sml	Thu Jul 31 11:28:55 2008 -0400
@@ -94,6 +94,7 @@
        | PVar of string
        | PPrim of Prim.t
        | PCon of string list * string * pat option
+       | PRecord of (string * pat) list * bool
 
 withtype pat = pat' located
 
--- a/src/source_print.sml	Thu Jul 31 10:44:52 2008 -0400
+++ b/src/source_print.sml	Thu Jul 31 11:28:55 2008 -0400
@@ -171,8 +171,20 @@
       | PCon (ms, x, SOME p) => parenIf par (box [p_list_sep (string ".") string (ms @ [x]),
                                                   space,
                                                   p_pat' true p])
+      | PRecord (xps, flex) =>
+        let
+            val pps = map (fn (x, p) => box [string "x", space, string "=", space, p_pat p]) xps
+        in
+            box [string "{",
+                 p_list_sep (box [string ",", space]) (fn x => x)
+                 (if flex then
+                      pps
+                  else
+                      pps @ [string "..."]),
+                 string "}"]
+        end
 
-val p_pat = p_pat' false
+and p_pat x = p_pat' false x
 
 fun p_exp' par (e, _) =
     case e of
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/caseMod.lac	Thu Jul 31 11:28:55 2008 -0400
@@ -0,0 +1,19 @@
+structure M = struct
+        datatype t = A | B
+end
+
+val f = fn x : M.t => case x of M.A => M.B | M.B => M.A
+
+datatype t = datatype M.t
+
+val g = fn x : t => case x of M.A => B | B => M.A
+
+structure N = struct
+        datatype t = C of t | D
+end
+
+val h = fn x : N.t => case x of N.C x => x | N.D => M.A
+
+datatype u = datatype N.t
+
+val i = fn x : u => case x of N.C x => x | D => M.A