changeset 182:d11754ffe252

Compiled pattern matching to C
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 Aug 2008 12:43:20 -0400 (2008-08-03)
parents 31dfab1d4050
children c0ea24dcb86f
files src/cjr.sml src/cjr_env.sml src/cjr_print.sml src/cjrize.sml src/core.sml src/core_env.sml src/core_print.sml src/core_util.sml src/corify.sml src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_print.sml src/expl_util.sml src/explify.sml src/mono.sml src/mono_env.sml src/mono_print.sml src/mono_util.sml src/monoize.sml
diffstat 22 files changed, 377 insertions(+), 136 deletions(-) [+]
line wrap: on
line diff
--- a/src/cjr.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/cjr.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -44,10 +44,10 @@
 
 datatype pat' =
          PWild
-       | PVar of string
+       | PVar of string * typ
        | PPrim of Prim.t
        | PCon of patCon * pat option
-       | PRecord of (string * pat) list
+       | PRecord of (string * pat * typ) list
 
 withtype pat = pat' located
 
@@ -63,7 +63,7 @@
        | ERecord of int * (string * exp) list
        | EField of exp * string
 
-       | ECase of exp * (pat * exp) list * typ
+       | ECase of exp * (pat * exp) list * { disc : typ, result : typ }
 
        | EWrite of exp
        | ESeq of exp * exp
--- a/src/cjr_env.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/cjr_env.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -61,8 +61,8 @@
 
 fun pushDatatype (env : env) x n xncs =
     {datatypes = IM.insert (#datatypes env, n, (x, xncs)),
-     constructors = foldl (fn ((x, n, to), constructors) =>
-                              IM.insert (constructors, n, (x, to, n)))
+     constructors = foldl (fn ((x, n', to), constructors) =>
+                              IM.insert (constructors, n', (x, to, n)))
                           (#constructors env) xncs,
 
      numRelE = #numRelE env,
--- a/src/cjr_print.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/cjr_print.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -85,7 +85,188 @@
     string ("__lwn_" ^ #1 (E.lookupENamed env n) ^ "_" ^ Int.toString n)
     handle CjrEnv.UnboundNamed _ => string ("__lwn_UNBOUND_" ^ Int.toString n)
 
-fun p_exp' par env (e, _) =
+fun p_con_named env n =
+    string ("__lwc_" ^ #1 (E.lookupConstructor env n) ^ "_" ^ Int.toString n)
+    handle CjrEnv.UnboundNamed _ => string ("__lwc_UNBOUND_" ^ Int.toString n)
+
+fun p_pat_preamble env (p, _) =
+    case p of
+        PWild => (box [],
+                  env)
+      | PVar (x, t) => (box [p_typ env t,
+                             space,
+                             string "__lwr_",
+                             string x,
+                             string "_",
+                             string (Int.toString (E.countERels env)),
+                             string ";",
+                             newline],
+                        env)
+      | PPrim _ => (box [], env)
+      | PCon (_, NONE) => (box [], env)
+      | PCon (_, SOME p) => p_pat_preamble env p
+      | PRecord xps =>
+        foldl (fn ((_, p, _), (pp, env)) =>
+                  let
+                      val (pp', env) = p_pat_preamble env p
+                  in
+                      (box [pp', pp], env)
+                  end) (box [], env) xps
+
+fun p_patCon env pc =
+    case pc of
+        PConVar n => p_con_named env n
+      | PConFfi _ => raise Fail "CjrPrint PConFfi"
+
+fun p_pat (env, exit, depth) (p, _) =
+    case p of
+        PWild =>
+        (box [], env)
+      | PVar (x, t) =>
+        (box [string "__lwr_",
+              string x,
+              string "_",
+              string (Int.toString (E.countERels env)),
+              space,
+              string "=",
+              space,
+              string "disc",
+              string (Int.toString depth),
+              string ";"],
+         E.pushERel env x t)
+      | PPrim (Prim.Int n) =>
+        (box [string "if",
+              space,
+              string "(disc",
+              string (Int.toString depth),
+              space,
+              string "!=",
+              space,
+              Prim.p_t (Prim.Int n),
+              string ")",
+              space,
+              exit],
+         env)
+      | PPrim (Prim.String s) =>
+        (box [string "if",
+              space,
+              string "(strcmp(disc",
+              string (Int.toString depth),
+              string ",",
+              space,
+              Prim.p_t (Prim.String s),
+              string "))",
+              space,
+              exit],
+         env)
+      | PPrim _ => raise Fail "CjrPrint: Disallowed PPrim primitive"
+
+      | PCon (pc, po) =>
+        let
+            val (p, env) =
+                case po of
+                    NONE => (box [], env)
+                  | SOME p =>
+                    let
+                        val (p, env) = p_pat (env, exit, depth + 1) p
+
+                        val (x, to) = case pc of
+                                          PConVar n =>
+                                          let
+                                              val (x, to, _) = E.lookupConstructor env n
+                                          in
+                                              (x, to)
+                                          end
+                                        | PConFfi _ => raise Fail "PConFfi"
+
+                        val t = case to of
+                                    NONE => raise Fail "CjrPrint: Constructor mismatch"
+                                  | SOME t => t
+                    in
+                        (box [string "{",
+                              newline,
+                              p_typ env t,
+                              space,
+                              string "disc",
+                              string (Int.toString (depth + 1)),
+                              space,
+                              string "=",
+                              space,
+                              string "disc",
+                              string (Int.toString depth),
+                              string "->data.__lwc_",
+                              string x,
+                              string ";",
+                              newline,
+                              p,
+                              newline,
+                              string "}"],
+                         env)
+                    end
+        in
+            (box [string "if",
+                  space,
+                  string "(disc",
+                  string (Int.toString depth),
+                  string "->tag",
+                  space,
+                  string "!=",
+                  space,
+                  p_patCon env pc,
+                  string ")",
+                  space,
+                  exit,
+                  newline,
+                  p],
+             env)
+        end
+
+      | PRecord xps =>
+        let
+            val (xps, env) =
+                ListUtil.foldlMap (fn ((x, p, t), env) =>
+                                      let
+                                          val (p, env) = p_pat (env, exit, depth + 1) p
+
+                                          val p = box [string "{",
+                                                       newline,
+                                                       p_typ env t,
+                                                       space,
+                                                       string "disc",
+                                                       string (Int.toString (depth + 1)),
+                                                       space,
+                                                       string "=",
+                                                       space,
+                                                       string "disc",
+                                                       string (Int.toString depth),
+                                                       string ".",
+                                                       string x,
+                                                       string ";",
+                                                       newline,
+                                                       p,
+                                                       newline,
+                                                       string "}"]
+                                      in
+                                          (p, env)
+                                      end) env xps
+        in
+            (p_list_sep newline (fn x => x) xps,
+             env)
+        end
+
+local
+    val count = ref 0
+in
+fun newGoto () =
+    let
+        val r = !count
+    in
+        count := r + 1;
+        string ("L" ^ Int.toString r)
+    end
+end
+
+fun p_exp' par env (e, loc) =
     case e of
         EPrim p => Prim.p_t p
       | ERel n => p_rel env n
@@ -95,7 +276,7 @@
             val (x, _, dn) = E.lookupConstructor env n
             val (dx, _) = E.lookupDatatype env dn
         in
-            box [string "{(",
+            box [string "({",
                  newline,
                  string "struct",
                  space,
@@ -123,7 +304,7 @@
                  newline,
                  case eo of
                      NONE => box []
-                   | SOME e => box [string "tmp->data.",
+                   | SOME e => box [string "tmp->data.__lwc_",
                                     string x,
                                     space,
                                     string "=",
@@ -180,10 +361,77 @@
                                  string "})" ]
       | EField (e, x) =>
         box [p_exp' true env e,
-             string ".",
+             string ".__lwf_",
              string x]
 
-      | ECase _ => raise Fail "CjrPrint ECase"
+      | ECase (e, pes, {disc, result}) =>
+        let
+            val final = newGoto ()
+
+            val body = foldl (fn ((p, e), body) =>
+                               let
+                                   val exit = newGoto ()
+                                   val (pr, _) = p_pat_preamble env p
+                                   val (p, env) = p_pat (env,
+                                                         box [string "goto",
+                                                              space,
+                                                              exit,
+                                                              string ";"],
+                                                         0) p
+                               in
+                                   box [body,
+                                        box [string "{",
+                                             newline,
+                                             pr,
+                                             newline,
+                                             p,
+                                             newline,
+                                             string "result",
+                                             space,
+                                             string "=",
+                                             space,
+                                             p_exp env e,
+                                             string ";",
+                                             newline,
+                                             string "goto",
+                                             space,
+                                             final,
+                                             string ";",
+                                             newline,
+                                             string "}"],
+                                        newline,
+                                        exit,
+                                        string ":",
+                                        newline]
+                               end) (box []) pes
+        in
+            box [string "({",
+                 newline,
+                 p_typ env disc,
+                 space,
+                 string "disc0",
+                 space,
+                 string "=",
+                 space,
+                 p_exp env e,
+                 string ";",
+                 newline,
+                 p_typ env result,
+                 space,
+                 string "result;",
+                 newline,
+                 body,
+                 string "lw_error(ctx, FATAL, \"",
+                 string (ErrorMsg.spanToString loc),
+                 string ": pattern match failure\");",
+                 newline,
+                 final,
+                 string ":",
+                 space,
+                 string "result;",
+                 newline,
+                 string "})"]
+        end
 
       | EWrite e => box [string "(lw_write(ctx, ",
                          p_exp env e,
@@ -236,6 +484,7 @@
              newline,
              p_list_sep (box []) (fn (x, t) => box [p_typ env t,
                                                     space,
+                                                    string "__lwf_",
                                                     string x,
                                                     string ";",
                                                     newline]) xts,
@@ -538,7 +787,7 @@
                                  newline,
                                  case to of
                                      NONE => box []
-                                   | SOME t => box [string "tmp->data.",
+                                   | SOME t => box [string "tmp->data.__lwc_",
                                                     string x',
                                                     space,
                                                     string "=",
--- a/src/cjrize.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/cjrize.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -108,13 +108,35 @@
         L.PConVar n => L'.PConVar n
       | L.PConFfi mx => L'.PConFfi mx
 
-fun cifyPat (p, loc) =
+fun cifyPat ((p, loc), sm) =
     case p of
-        L.PWild => (L'.PWild, loc)
-      | L.PVar x => (L'.PVar x, loc)
-      | L.PPrim p => (L'.PPrim p, loc)
-      | L.PCon (pc, po) => (L'.PCon (cifyPatCon pc, Option.map cifyPat po), loc)
-      | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, cifyPat p)) xps), loc)
+        L.PWild => ((L'.PWild, loc), sm)
+      | L.PVar (x, t) =>
+        let
+            val (t, sm) = cifyTyp (t, sm)
+        in
+            ((L'.PVar (x, t), loc), sm)
+        end
+      | L.PPrim p => ((L'.PPrim p, loc), sm)
+      | L.PCon (pc, NONE) => ((L'.PCon (cifyPatCon pc, NONE), loc), sm)
+      | L.PCon (pc, SOME p) =>
+        let
+            val (p, sm) = cifyPat (p, sm)
+        in
+            ((L'.PCon (cifyPatCon pc, SOME p), loc), sm)
+        end
+      | L.PRecord xps =>
+        let
+            val (xps, sm) = ListUtil.foldlMap (fn ((x, p, t), sm) =>
+                                                  let
+                                                      val (p, sm) = cifyPat (p, sm)
+                                                      val (t, sm) = cifyTyp (t, sm)
+                                                  in
+                                                      ((x, p, t), sm)
+                                                  end) sm xps
+        in
+            ((L'.PRecord xps, loc), sm)
+        end
 
 fun cifyExp ((e, loc), sm) =
     case e of
@@ -179,19 +201,21 @@
             ((L'.EField (e, x), loc), sm)
         end
 
-      | L.ECase (e, pes, t) =>
+      | L.ECase (e, pes, {disc, result}) =>
         let
                 val (e, sm) = cifyExp (e, sm)
                 val (pes, sm) = ListUtil.foldlMap
                                     (fn ((p, e), sm) =>
                                         let
                                             val (e, sm) = cifyExp (e, sm)
+                                            val (p, sm) = cifyPat (p, sm)
                                         in
-                                            ((cifyPat p, e), sm)
+                                            ((p, e), sm)
                                         end) sm pes
-                val (t, sm) = cifyTyp (t, sm)
+                val (disc, sm) = cifyTyp (disc, sm)
+                val (result, sm) = cifyTyp (result, sm)
             in
-                ((L'.ECase (e, pes, t), loc), sm)
+                ((L'.ECase (e, pes, {disc = disc, result = result}), loc), sm)
             end
 
       | L.EStrcat (e1, e2) =>
--- a/src/core.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/core.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -65,10 +65,10 @@
 
 datatype pat' =
          PWild
-       | PVar of string
+       | PVar of string * con
        | PPrim of Prim.t
        | PCon of patCon * pat option
-       | PRecord of (string * pat) list
+       | PRecord of (string * pat * con) list
 
 withtype pat = pat' located
 
@@ -89,7 +89,7 @@
        | ECut of exp * con * { field : con, rest : con }
        | EFold of kind
 
-       | ECase of exp * (pat * exp) list * con
+       | ECase of exp * (pat * exp) list * { disc : con, result : con }
 
        | EWrite of exp
 
--- a/src/core_env.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/core_env.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -113,8 +113,8 @@
      namedC = #namedC env,
 
      datatypes = IM.insert (#datatypes env, n, (x, xncs)),
-     constructors = foldl (fn ((x, n, to), constructors) =>
-                              IM.insert (constructors, n, (x, to, n)))
+     constructors = foldl (fn ((x, n', to), constructors) =>
+                              IM.insert (constructors, n', (x, to, n)))
                           (#constructors env) xncs,
      
      relE = #relE env,
--- a/src/core_print.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/core_print.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -171,7 +171,7 @@
 fun p_pat' par env (p, _) =
     case p of
         PWild => string "_"
-      | PVar s => string s
+      | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
       | PCon (n, NONE) => p_patCon env n
       | PCon (n, SOME p) => parenIf par (box [p_patCon env n,
@@ -179,7 +179,7 @@
                                               p_pat' true env p])
       | PRecord xps =>
         box [string "{",
-             p_list_sep (box [string ",", space]) (fn (x, p) =>
+             p_list_sep (box [string ",", space]) (fn (x, p, _) =>
                                                       box [string x,
                                                            space,
                                                            string "=",
--- a/src/core_util.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/core_util.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -302,16 +302,18 @@
                          fn k' =>
                             (EFold k', loc))
 
-              | ECase (e, pes, t) =>
+              | ECase (e, pes, {disc, result}) =>
                 S.bind2 (mfe ctx e,
                          fn e' =>
                             S.bind2 (ListUtil.mapfold (fn (p, e) =>
                                                          S.map2 (mfe ctx e,
                                                               fn e' => (p, e'))) pes,
                                     fn pes' =>
-                                       S.map2 (mfc ctx t,
-                                               fn t' =>
-                                                  (ECase (e', pes', t'), loc))))
+                                       S.bind2 (mfc ctx disc,
+                                                fn disc' =>
+                                                   S.map2 (mfc ctx result,
+                                                        fn result' =>
+                                                           (ECase (e', pes', {disc = disc', result = result'}), loc)))))
 
               | EWrite e =>
                 S.map2 (mfe ctx e,
--- a/src/corify.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/corify.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -411,10 +411,10 @@
 fun corifyPat st (p, loc) =
     case p of
         L.PWild => (L'.PWild, loc)
-      | L.PVar x => (L'.PVar x, loc)
+      | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
       | L.PPrim p => (L'.PPrim p, loc)
       | L.PCon (pc, po) => (L'.PCon (corifyPatCon st pc, Option.map (corifyPat st) po), loc)
-      | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, corifyPat st p)) xps), loc)
+      | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
 
 fun corifyExp st (e, loc) =
     case e of
@@ -473,10 +473,11 @@
                                                    {field = corifyCon st field, rest = corifyCon st rest}), loc)
       | L.EFold k => (L'.EFold (corifyKind k), loc)
 
-      | L.ECase (e, pes, t) => (L'.ECase (corifyExp st e,
-                                          map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
-                                          corifyCon st t),
-                                loc)
+      | L.ECase (e, pes, {disc, result}) =>
+        (L'.ECase (corifyExp st e,
+                   map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
+                   {disc = corifyCon st disc, result = corifyCon st result}),
+         loc)
 
       | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
 
--- a/src/elab.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/elab.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -77,10 +77,10 @@
 
 datatype pat' =
          PWild
-       | PVar of string
+       | PVar of string * con
        | PPrim of Prim.t
        | PCon of patCon * pat option
-       | PRecord of (string * pat) list
+       | PRecord of (string * pat * con) list
 
 withtype pat = pat' located
 
@@ -99,7 +99,7 @@
        | ECut of exp * con * { field : con, rest : con }
        | EFold of kind
 
-       | ECase of exp * (pat * exp) list * con
+       | ECase of exp * (pat * exp) list * { disc : con, result : con }
 
        | EError
 
--- a/src/elab_print.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/elab_print.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -214,7 +214,7 @@
 fun p_pat' par env (p, _) =
     case p of
         PWild => string "_"
-      | PVar s => string s
+      | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
       | PCon (pc, NONE) => p_patCon env pc
       | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
@@ -222,7 +222,7 @@
                                                p_pat' true env p])
       | PRecord xps =>
         box [string "{",
-             p_list_sep (box [string ",", space]) (fn (x, p) =>
+             p_list_sep (box [string ",", space]) (fn (x, p, _) =>
                                                       box [string x,
                                                            space,
                                                            string "=",
--- a/src/elab_util.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/elab_util.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -308,16 +308,18 @@
                          fn k' =>
                             (EFold k', loc))
 
-              | ECase (e, pes, t) =>
+              | ECase (e, pes, {disc, result}) =>
                 S.bind2 (mfe ctx e,
                          fn e' =>
                             S.bind2 (ListUtil.mapfold (fn (p, e) =>
                                                          S.map2 (mfe ctx e,
                                                               fn e' => (p, e'))) pes,
                                     fn pes' =>
-                                       S.map2 (mfc ctx t,
-                                               fn t' =>
-                                                  (ECase (e', pes', t'), loc))))
+                                       S.bind2 (mfc ctx disc,
+                                             fn disc' =>
+                                                S.map2 (mfc ctx result,
+                                                     fn result' =>
+                                                        (ECase (e', pes', {disc = disc', result = result'}), loc)))))
 
               | EError => S.return2 eAll
     in
--- a/src/elaborate.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/elaborate.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -904,45 +904,6 @@
                                               (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
                           loc)), loc)), loc)
 
-fun typeof env (e, loc) =
-    case e of
-        L'.EPrim p => primType env p
-      | L'.ERel n => #2 (E.lookupERel env n)
-      | L'.ENamed n => #2 (E.lookupENamed env n)
-      | L'.EModProj (n, ms, x) =>
-        let
-            val (_, sgn) = E.lookupStrNamed env n
-            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.projectVal env {sgn = sgn, str = str, field = x} of
-                NONE => raise Fail "typeof: Unknown val in structure"
-              | SOME t => t
-        end
-
-      | L'.EApp (e1, _) =>
-        (case #1 (typeof env e1) of
-             L'.TFun (_, c) => c
-           | _ => raise Fail "typeof: Bad EApp")
-      | L'.EAbs (_, _, ran, _) => ran
-      | L'.ECApp (e1, c) =>
-        (case #1 (typeof env e1) of
-             L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1
-           | _ => raise Fail "typeof: Bad ECApp")
-      | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc)
-
-      | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc)
-      | L'.EField (_, _, {field, ...}) => field
-      | L'.ECut (_, _, {rest, ...}) => (L'.TRecord rest, loc)
-      | L'.EFold dom => foldType (dom, loc)
-
-      | L'.ECase (_, _, t) => t
-
-      | L'.EError => cerror
-
 fun elabHead (env, denv) (e as (_, loc)) t =
     let
         fun unravel (t, e) =
@@ -1000,7 +961,7 @@
                         else
                             cunif (loc, (L'.KType, loc))
             in
-                (((L'.PVar x, loc), t),
+                (((L'.PVar (x, t), loc), t),
                  (E.pushERel env x t, SS.add (bound, x)))
             end
           | L.PPrim p => (((L'.PPrim p, loc), primType env p),
@@ -1018,7 +979,7 @@
                  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"
+                                                    NONE => raise Fail "elabPat: Unknown substructure"
                                                   | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
                                             ((L'.StrVar n, loc), sgn) ms
                  in
@@ -1051,7 +1012,7 @@
                     else
                         c
             in
-                (((L'.PRecord (map (fn (x, p', _) => (x, p')) xpts), loc),
+                (((L'.PRecord xpts, loc),
                   (L'.TRecord c, loc)),
                  (env, bound))
             end
@@ -1085,8 +1046,8 @@
               | L'.PPrim _ => None
               | L'.PCon (pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
               | L'.PCon (pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
-              | L'.PRecord xps => Record [foldl (fn ((x, p), fmap) =>
-                                                         SM.insert (fmap, x, coverage p)) SM.empty xps]
+              | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) =>
+                                                    SM.insert (fmap, x, coverage p)) SM.empty xps]
 
         fun merge (c1, c2) =
             case (c1, c2) of
@@ -1458,7 +1419,7 @@
                 else
                     expError env (Inexhaustive loc);
 
-                ((L'.ECase (e', pes', result), loc), result, gs' @ gs)
+                ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs' @ gs)
             end
     end
             
--- a/src/expl.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/expl.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -65,10 +65,10 @@
 
 datatype pat' =
          PWild
-       | PVar of string
+       | PVar of string * con
        | PPrim of Prim.t
        | PCon of patCon * pat option
-       | PRecord of (string * pat) list
+       | PRecord of (string * pat * con) list
 
 withtype pat = pat' located
 
@@ -87,7 +87,7 @@
        | ECut of exp * con * { field : con, rest : con }
        | EFold of kind
 
-       | ECase of exp * (pat * exp) list * con
+       | ECase of exp * (pat * exp) list * { disc : con, result : con }
 
        | EWrite of exp
 
--- a/src/expl_print.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/expl_print.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -179,7 +179,7 @@
 fun p_pat' par env (p, _) =
     case p of
         PWild => string "_"
-      | PVar s => string s
+      | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
       | PCon (pc, NONE) => p_patCon env pc
       | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
@@ -187,7 +187,7 @@
                                                p_pat' true env p])
       | PRecord xps =>
         box [string "{",
-             p_list_sep (box [string ",", space]) (fn (x, p) =>
+             p_list_sep (box [string ",", space]) (fn (x, p, _) =>
                                                       box [string x,
                                                            space,
                                                            string "=",
--- a/src/expl_util.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/expl_util.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -287,16 +287,18 @@
                      fn e' =>
                         (EWrite e', loc))
 
-              | ECase (e, pes, t) =>
+              | ECase (e, pes, {disc, result}) =>
                 S.bind2 (mfe ctx e,
                          fn e' =>
                             S.bind2 (ListUtil.mapfold (fn (p, e) =>
                                                          S.map2 (mfe ctx e,
                                                               fn e' => (p, e'))) pes,
                                     fn pes' =>
-                                       S.map2 (mfc ctx t,
-                                               fn t' =>
-                                                  (ECase (e', pes', t'), loc))))
+                                       S.bind2 (mfc ctx disc,
+                                                fn disc' =>
+                                                   S.map2 (mfc ctx result,
+                                                        fn result' =>
+                                                           (ECase (e', pes', {disc = disc', result = result'}), loc)))))
     in
         mfe
     end
--- a/src/explify.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/explify.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -79,10 +79,10 @@
 fun explifyPat (p, loc) =
     case p of
         L.PWild => (L'.PWild, loc)
-      | L.PVar x => (L'.PVar x, loc)
+      | L.PVar (x, t) => (L'.PVar (x, explifyCon t), loc)
       | L.PPrim p => (L'.PPrim p, loc)
       | L.PCon (pc, po) => (L'.PCon (explifyPatCon pc, Option.map explifyPat po), loc)
-      | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, explifyPat p)) xps), loc)
+      | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, explifyPat p, explifyCon t)) xps), loc)
 
 fun explifyExp (e, loc) =
     case e of
@@ -102,9 +102,10 @@
                                                      {field = explifyCon field, rest = explifyCon rest}), loc)
       | L.EFold k => (L'.EFold (explifyKind k), loc)
 
-      | L.ECase (e, pes, t) => (L'.ECase (explifyExp e,
-                                          map (fn (p, e) => (explifyPat p, explifyExp e)) pes,
-                                          explifyCon t), loc)
+      | L.ECase (e, pes, {disc, result}) =>
+        (L'.ECase (explifyExp e,
+                   map (fn (p, e) => (explifyPat p, explifyExp e)) pes,
+                   {disc = explifyCon disc, result = explifyCon result}), loc)
 
       | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc)
 
--- a/src/mono.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/mono.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -43,10 +43,10 @@
 
 datatype pat' =
          PWild
-       | PVar of string
+       | PVar of string * typ
        | PPrim of Prim.t
        | PCon of patCon * pat option
-       | PRecord of (string * pat) list
+       | PRecord of (string * pat * typ) list
 
 withtype pat = pat' located
 
@@ -63,7 +63,7 @@
        | ERecord of (string * exp * typ) list
        | EField of exp * string
 
-       | ECase of exp * (pat * exp) list * typ
+       | ECase of exp * (pat * exp) list * { disc : typ, result : typ }
 
        | EStrcat of exp * exp
 
--- a/src/mono_env.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/mono_env.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -53,8 +53,8 @@
 
 fun pushDatatype (env : env) x n xncs =
     {datatypes = IM.insert (#datatypes env, n, (x, xncs)),
-     constructors = foldl (fn ((x, n, to), constructors) =>
-                              IM.insert (constructors, n, (x, to, n)))
+     constructors = foldl (fn ((x, n', to), constructors) =>
+                              IM.insert (constructors, n', (x, to, n)))
                           (#constructors env) xncs,
 
      relE = #relE env,
@@ -107,15 +107,13 @@
       | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis
       | DExport _ => env
 
-val dummyt = (TFfi ("", ""), ErrorMsg.dummySpan)
-
 fun patBinds env (p, loc) =
     case p of
         PWild => env
-      | PVar x => pushERel env x dummyt
+      | PVar (x, t) => pushERel env x t
       | PPrim _ => env
       | PCon (_, NONE) => env
       | PCon (_, SOME p) => patBinds env p
-      | PRecord xps => foldl (fn ((_, p), env) => patBinds env p) env xps
+      | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
 
 end
--- a/src/mono_print.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/mono_print.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -89,7 +89,7 @@
 fun p_pat' par env (p, _) =
     case p of
         PWild => string "_"
-      | PVar s => string s
+      | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
       | PCon (n, NONE) => p_patCon env n
       | PCon (n, SOME p) => parenIf par (box [p_patCon env n,
@@ -97,7 +97,7 @@
                                               p_pat' true env p])
       | PRecord xps =>
         box [string "{",
-             p_list_sep (box [string ",", space]) (fn (x, p) =>
+             p_list_sep (box [string ",", space]) (fn (x, p, _) =>
                                                       box [string x,
                                                            space,
                                                            string "=",
--- a/src/mono_util.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/mono_util.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -181,30 +181,30 @@
                       fn e' =>
                          (EField (e', x), loc))
 
-              | ECase (e, pes, t) =>
+              | ECase (e, pes, {disc, result}) =>
                 S.bind2 (mfe ctx e,
                          fn e' =>
                             S.bind2 (ListUtil.mapfold (fn (p, e) =>
                                                           let
-                                                              val dummyt = (TFfi ("", ""), ErrorMsg.dummySpan)
-
                                                               fun pb ((p, _), ctx) =
                                                                   case p of
                                                                       PWild => ctx
-                                                                    | PVar x => bind (ctx, RelE (x, dummyt))
+                                                                    | PVar (x, t) => bind (ctx, RelE (x, t))
                                                                     | PPrim _ => ctx
                                                                     | PCon (_, NONE) => ctx
                                                                     | PCon (_, SOME p) => pb (p, ctx)
-                                                                    | PRecord xps => foldl (fn ((_, p), ctx) =>
+                                                                    | PRecord xps => foldl (fn ((_, p, _), ctx) =>
                                                                                                pb (p, ctx)) ctx xps
                                                           in
                                                               S.map2 (mfe (pb (p, ctx)) e,
                                                                    fn e' => (p, e'))
                                                           end) pes,
                                     fn pes' =>
-                                       S.map2 (mft t,
-                                               fn t' =>
-                                                  (ECase (e', pes', t'), loc))))
+                                       S.bind2 (mft disc,
+                                                fn disc' =>
+                                                   S.map2 (mft result,
+                                                        fn result' =>
+                                                           (ECase (e', pes', {disc = disc', result = result'}), loc)))))
 
               | EStrcat (e1, e2) =>
                 S.bind2 (mfe ctx e1,
--- a/src/monoize.sml	Sun Aug 03 11:17:33 2008 -0400
+++ b/src/monoize.sml	Sun Aug 03 12:43:20 2008 -0400
@@ -212,10 +212,10 @@
                                                  fm)
                                               | SOME t =>
                                                 let
-                                                    val (arg, fm) = fooify fm ((L'.ERel 0, loc),
-                                                                               monoType env t)
+                                                    val t = monoType env t
+                                                    val (arg, fm) = fooify fm ((L'.ERel 0, loc), t)
                                                 in
-                                                    (((L'.PCon (L'.PConVar n, SOME (L'.PVar "a", loc)), loc),
+                                                    (((L'.PCon (L'.PConVar n, SOME (L'.PVar ("a", t), loc)), loc),
                                                       (L'.EStrcat ((L'.EPrim (Prim.String (x ^ "/")), loc),
                                                                    arg), loc)),
                                                      fm)
@@ -233,7 +233,8 @@
                                                          ran,
                                                          (L'.ECase ((L'.ERel 0, loc),
                                                                     branches,
-                                                                    ran), loc)), loc),
+                                                                    {disc = dom,
+                                                                     result = ran}), loc)), loc),
                                                "")], loc),
                                  fm)
                             end       
@@ -284,13 +285,13 @@
         L.PConVar n => L'.PConVar n
       | L.PConFfi mx => L'.PConFfi mx
 
-fun monoPat (p, loc) =
+fun monoPat env (p, loc) =
     case p of
         L.PWild => (L'.PWild, loc)
-      | L.PVar x => (L'.PVar x, loc)
+      | L.PVar (x, t) => (L'.PVar (x, monoType env t), loc)
       | L.PPrim p => (L'.PPrim p, loc)
-      | L.PCon (pc, po) => (L'.PCon (monoPatCon pc, Option.map monoPat po), loc)
-      | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, monoPat p)) xps), loc)
+      | L.PCon (pc, po) => (L'.PCon (monoPatCon pc, Option.map (monoPat env) po), loc)
+      | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, monoPat env p, monoType env t)) xps), loc)
 
 fun monoExp (env, st, fm) (all as (e, loc)) =
     let
@@ -667,7 +668,7 @@
           | L.ECut _ => poly ()
           | L.EFold _ => poly ()
 
-          | L.ECase (e, pes, t) =>
+          | L.ECase (e, pes, {disc, result}) =>
             let
                 val (e, fm) = monoExp (env, st, fm) e
                 val (pes, fm) = ListUtil.foldlMap
@@ -675,10 +676,10 @@
                                         let
                                             val (e, fm) = monoExp (env, st, fm) e
                                         in
-                                            ((monoPat p, e), fm)
+                                            ((monoPat env p, e), fm)
                                         end) fm pes
             in
-                ((L'.ECase (e, pes, monoType env t), loc), fm)
+                ((L'.ECase (e, pes, {disc = monoType env disc, result = monoType env result}), loc), fm)
             end
 
           | L.EWrite e =>