Case through explify

8 files changed, 114 insertions, 22 deletions

diff --git a/src/corify.sml b/src/corify.sml
index 7332395c..cf6d5658 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -394,6 +394,7 @@ fun corifyExp st (e, loc) =
       | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
                                                    {field = corifyCon st field, rest = corifyCon st rest}), loc)
       | L.EFold k => (L'.EFold (corifyKind k), loc)
+      | L.ECase _ => raise Fail "Corify ECase"
       | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
 
 fun corifyDecl ((d, loc : EM.span), st) =
diff --git a/src/elab.sml b/src/elab.sml
index af21def0..58e69629 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -80,7 +80,7 @@ datatype pat' =
        | PVar of string
        | PPrim of Prim.t
        | PCon of patCon * pat option
-       | PRecord of (string * pat) list * con option
+       | PRecord of (string * pat) list
 
 withtype pat = pat' located
 
diff --git a/src/elab_print.sml b/src/elab_print.sml
index d0ff8d5f..591e019b 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -220,17 +220,15 @@ fun p_pat' par env (p, _) =
       | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
                                                space,
                                                p_pat' true env p])
-      | PRecord (xps, flex) =>
-        let
-            val pps = map (fn (x, p) => box [string x, space, string "=", space, p_pat env p]) xps
-        in
-            box [string "{",
-                 p_list_sep (box [string ",", space]) (fn x => x)
-                 (case flex of
-                      NONE => pps
-                    | SOME _ => pps @ [string "..."]),
-                 string "}"]
-        end
+      | PRecord xps =>
+        box [string "{",
+             p_list_sep (box [string ",", space]) (fn (x, p) =>
+                                                      box [string x,
+                                                           space,
+                                                           string "=",
+                                                           space,
+                                                           p_pat env p]) xps,
+             string "}"]
 
 and p_pat x = p_pat' false x
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 0a71aa8c..da38cbba 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1045,17 +1045,13 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
 
                 val k = (L'.KType, loc)
                 val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc)
-                val (flex, c) =
+                val c =
                     if flex then
-                        let
-                            val flex = cunif (loc, (L'.KRecord k, loc))
-                        in
-                            (SOME flex, (L'.CConcat (c, flex), loc))
-                        end
+                        (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc)
                     else
-                        (NONE, c)
+                        c
             in
-                (((L'.PRecord (map (fn (x, p', _) => (x, p')) xpts, flex), loc),
+                (((L'.PRecord (map (fn (x, p', _) => (x, p')) xpts), loc),
                   (L'.TRecord c, loc)),
                  (env, bound))
             end
@@ -1089,8 +1085,9 @@ fun exhaustive (env, denv, t, ps) =
               | 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) =>
+              | 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
                 (None, _) => c2
diff --git a/src/expl.sml b/src/expl.sml
index 183dbc31..52dbee63 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -59,6 +59,19 @@ datatype con' =
 
 withtype con = con' located
 
+datatype patCon =
+         PConVar of int
+       | PConProj of int * string list * string
+
+datatype pat' =
+         PWild
+       | PVar of string
+       | PPrim of Prim.t
+       | PCon of patCon * pat option
+       | PRecord of (string * pat) list
+
+withtype pat = pat' located
+
 datatype exp' =
          EPrim of Prim.t
        | ERel of int
@@ -74,6 +87,8 @@ datatype exp' =
        | ECut of exp * con * { field : con, rest : con }
        | EFold of kind
 
+       | ECase of exp * (pat * exp) list * con
+
        | EWrite of exp
 
 withtype exp = exp' located
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 7d0bfebd..3595f65a 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -155,6 +155,48 @@ and p_name env (all as (c, _)) =
         CName s => string s
       | _ => p_con env all
 
+fun p_patCon env pc =
+    case pc of
+        PConVar n =>
+        ((if !debug then
+              string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
+          else
+              string (#1 (E.lookupENamed env n)))
+         handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n))
+      | PConProj (m1, ms, x) =>
+        let
+            val m1x = #1 (E.lookupStrNamed env m1)
+                handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
+                  
+            val m1s = if !debug then
+                          m1x ^ "__" ^ Int.toString m1
+                      else
+                          m1x
+        in
+            p_list_sep (string ".") string (m1x :: ms @ [x])
+        end
+
+fun p_pat' par env (p, _) =
+    case p of
+        PWild => string "_"
+      | 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,
+                                               space,
+                                               p_pat' true env p])
+      | PRecord xps =>
+        box [string "{",
+             p_list_sep (box [string ",", space]) (fn (x, p) =>
+                                                      box [string x,
+                                                           space,
+                                                           string "=",
+                                                           space,
+                                                           p_pat env p]) xps,
+             string "}"]
+
+and p_pat x = p_pat' false x
+
 fun p_exp' par env (e, loc) =
     case e of
         EPrim p => Prim.p_t p
@@ -264,6 +306,19 @@ fun p_exp' par env (e, loc) =
                          p_exp env e,
                          string ")"]
 
+      | ECase (e, pes, _) => parenIf par (box [string "case",
+                                               space,
+                                               p_exp env e,
+                                               space,
+                                               string "of",
+                                               space,
+                                               p_list_sep (box [space, string "|", space])
+                                                          (fn (p, e) => box [p_pat env p,
+                                                                             space,
+                                                                             string "=>",
+                                                                             space,
+                                                                             p_exp env e]) pes])
+
 and p_exp env = p_exp' false env
 
 fun p_named x n =
diff --git a/src/expl_util.sml b/src/expl_util.sml
index e1a5d30f..685605c3 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -286,6 +286,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                 S.map2 (mfe ctx e,
                      fn e' =>
                         (EWrite e', loc))
+
+              | ECase (e, pes, t) =>
+                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))))
     in
         mfe
     end
diff --git a/src/explify.sml b/src/explify.sml
index da94ba94..7c23c2f5 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -71,6 +71,19 @@ fun explifyCon (c, loc) =
       | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c
       | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
 
+fun explifyPatCon pc =
+    case pc of
+        L.PConVar n => L'.PConVar n
+      | L.PConProj x => L'.PConProj x
+
+fun explifyPat (p, loc) =
+    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 (explifyPatCon pc, Option.map explifyPat po), loc)
+      | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, explifyPat p)) xps), loc)
+
 fun explifyExp (e, loc) =
     case e of
         L.EPrim p => (L'.EPrim p, loc)
@@ -89,7 +102,9 @@ fun explifyExp (e, loc) =
                                                      {field = explifyCon field, rest = explifyCon rest}), loc)
       | L.EFold k => (L'.EFold (explifyKind k), loc)
 
-      | L.ECase _ => raise Fail "Explify ECase"
+      | L.ECase (e, pes, t) => (L'.ECase (explifyExp e,
+                                          map (fn (p, e) => (explifyPat p, explifyExp e)) pes,
+                                          explifyCon t), loc)
 
       | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc)