Case through corify

7 files changed, 228 insertions, 19 deletions

diff --git a/src/core.sml b/src/core.sml
index b16766b3..5baa0351 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -59,10 +59,24 @@ datatype con' =
 
 withtype con = con' located
 
+datatype patCon =
+         PConVar of int
+       | PConFfi of string * 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
        | ENamed of int
+       | ECon of int * exp option
        | EFfi of string * string
        | EFfiApp of string * string * exp list
        | EApp of exp * exp
@@ -75,6 +89,8 @@ datatype exp' =
        | ECut of exp * con * { field : con, rest : con }
        | EFold of kind
 
+       | ECase of exp * (pat * exp) list * con
+
        | EWrite of exp
 
        | EClosure of int * exp list
diff --git a/src/core_env.sig b/src/core_env.sig
index b2005fa8..220c1da8 100644
--- a/src/core_env.sig
+++ b/src/core_env.sig
@@ -45,6 +45,8 @@ signature CORE_ENV = sig
     val pushDatatype : env -> string -> int -> (string * int * Core.con option) list -> env
     val lookupDatatype : env -> int -> string * (string * int * Core.con option) list
 
+    val lookupConstructor : env -> int -> string * Core.con option * int
+
     val pushERel : env -> string -> Core.con -> env
     val lookupERel : env -> int -> string * Core.con
 
diff --git a/src/core_env.sml b/src/core_env.sml
index cb10a354..4895de9c 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -62,6 +62,7 @@ type env = {
      namedC : (string * kind * con option) IM.map,
 
      datatypes : (string * (string * int * con option) list) IM.map,
+     constructors : (string * con option * int) IM.map,
 
      relE : (string * con) list,
      namedE : (string * con * exp option * string) IM.map
@@ -72,6 +73,7 @@ val empty = {
     namedC = IM.empty,
 
     datatypes = IM.empty,
+    constructors = IM.empty,
 
     relE = [],
     namedE = IM.empty
@@ -82,6 +84,7 @@ fun pushCRel (env : env) x k =
      namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
 
      datatypes = #datatypes env,
+     constructors = #constructors env,
 
      relE = map (fn (x, c) => (x, lift c)) (#relE env),
      namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)}
@@ -95,6 +98,7 @@ fun pushCNamed (env : env) x n k co =
      namedC = IM.insert (#namedC env, n, (x, k, co)),
 
      datatypes = #datatypes env,
+     constructors = #constructors env,
      
      relE = #relE env,
      namedE = #namedE env}
@@ -109,6 +113,9 @@ fun pushDatatype (env : env) x n xncs =
      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 env) xncs,
      
      relE = #relE env,
      namedE = #namedE env}
@@ -118,11 +125,17 @@ fun lookupDatatype (env : env) n =
         NONE => raise UnboundNamed n
       | SOME x => x
 
+fun lookupConstructor (env : env) n =
+    case IM.find (#constructors env, n) of
+        NONE => raise UnboundNamed n
+      | SOME x => x
+
 fun pushERel (env : env) x t =
     {relC = #relC env,
      namedC = #namedC env,
 
      datatypes = #datatypes env,
+     constructors = #constructors env,
 
      relE = (x, t) :: #relE env,
      namedE = #namedE env}
@@ -136,6 +149,7 @@ fun pushENamed (env : env) x n t eo s =
      namedC = #namedC env,
 
      datatypes = #datatypes env,
+     constructors = #constructors env,
 
      relE = #relE env,
      namedE = IM.insert (#namedE env, n, (x, t, eo, s))}
diff --git a/src/core_print.sml b/src/core_print.sml
index 28080bfa..7458fef0 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -152,6 +152,43 @@ fun p_enamed env n =
          string (#1 (E.lookupENamed env n)))
     handle E.UnboundNamed _ => string ("UNBOUNDN_" ^ Int.toString n)
 
+fun p_con_named env n =
+    (if !debug then
+        string (#1 (E.lookupConstructor env n) ^ "__" ^ Int.toString n)
+     else
+         string (#1 (E.lookupConstructor env n)))
+    handle E.UnboundNamed _ => string ("CONSTRUCTOR_" ^ Int.toString n)
+
+fun p_patCon env pc =
+    case pc of
+        PConVar n => p_con_named env n
+      | PConFfi (m, x) => box [string "FFI(",
+                               string m,
+                               string ".",
+                               string x,
+                               string ")"]
+
+fun p_pat' par env (p, _) =
+    case p of
+        PWild => string "_"
+      | 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,
+                                              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, _) =
     case e of
         EPrim p => Prim.p_t p
@@ -162,6 +199,10 @@ fun p_exp' par env (e, _) =
               string (#1 (E.lookupERel env n)))
          handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n))
       | ENamed n => p_enamed env n
+      | ECon (n, NONE) => p_con_named env n
+      | ECon (n, SOME e) => parenIf par (box [p_con_named env n,
+                                              space,
+                                              p_exp' true env e])
       | EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"]
       | EFfiApp (m, x, es) => box [string "FFI(",
                                    string m,
@@ -249,6 +290,19 @@ fun p_exp' par env (e, _) =
                               p_con' true env c])
       | EFold _ => string "fold"
 
+      | 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])
+
       | EWrite e => box [string "write(",
                          p_exp env e,
                          string ")"]
diff --git a/src/core_util.sml b/src/core_util.sml
index 95c4f10f..85cf24ac 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -227,6 +227,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                 EPrim _ => S.return2 eAll
               | ERel _ => S.return2 eAll
               | ENamed _ => S.return2 eAll
+              | ECon (_, NONE) => S.return2 eAll
+              | ECon (n, SOME e) =>
+                S.map2 (mfe ctx e,
+                        fn e' =>
+                           (ECon (n, SOME e'), loc))
               | EFfi _ => S.return2 eAll
               | EFfiApp (m, x, es) =>
                 S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es,
@@ -297,6 +302,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                          fn k' =>
                             (EFold k', 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))))
+
               | EWrite e =>
                 S.map2 (mfe ctx e,
                      fn e' =>
diff --git a/src/corify.sml b/src/corify.sml
index cf6d5658..44da20da 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -71,11 +71,15 @@ structure St : sig
     val lookupConById : t -> int -> int option
     val lookupConByName : t -> string -> core_con
 
+    val bindConstructor : t -> string -> int -> L'.patCon -> t
+    val lookupConstructorByName : t -> string -> L'.patCon
+    val lookupConstructorById : t -> int -> L'.patCon
+
     datatype core_val =
              ENormal of int
            | EFfi of string * L'.con
     val bindVal : t -> string -> int -> t * int
-    val bindConstructor : t -> string -> int -> t
+    val bindConstructorVal : t -> string -> int -> t
     val lookupValById : t -> int -> int option
     val lookupValByName : t -> string -> core_val
 
@@ -90,6 +94,7 @@ end = struct
 
 datatype flattening =
          FNormal of {cons : int SM.map,
+                     constructors : L'.patCon SM.map,
                      vals : int SM.map,
                      strs : flattening SM.map,
                      funs : (string * int * L.str) SM.map}
@@ -98,6 +103,7 @@ datatype flattening =
                            
 type t = {
      cons : int IM.map,
+     constructors : L'.patCon IM.map,
      vals : int IM.map,
      strs : flattening IM.map,
      funs : (string * int * L.str) IM.map,
@@ -107,15 +113,17 @@ type t = {
 
 val empty = {
     cons = IM.empty,
+    constructors = IM.empty,
     vals = IM.empty,
     strs = IM.empty,
     funs = IM.empty,
-    current = FNormal { cons = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
+    current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
     nested = []
 }
 
-fun debug ({current = FNormal {cons, vals, strs, funs}, ...} : t) =
+fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) =
     print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
+           ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
            ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
            ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
            ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
@@ -129,20 +137,22 @@ datatype core_val =
          ENormal of int
        | EFfi of string * L'.con
 
-fun bindCon {cons, vals, strs, funs, current, nested} s n =
+fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n =
     let
         val n' = alloc ()
 
         val current =
             case current of
                 FFfi _ => raise Fail "Binding inside FFfi"
-              | FNormal {cons, vals, strs, funs} =>
+              | FNormal {cons, constructors, vals, strs, funs} =>
                 FNormal {cons = SM.insert (cons, s, n'),
+                         constructors = constructors,
                          vals = vals,
                          strs = strs,
                          funs = funs}
     in
         ({cons = IM.insert (cons, n, n'),
+          constructors = constructors,
           vals = vals,
           strs = strs,
           funs = funs,
@@ -161,20 +171,22 @@ fun lookupConByName ({current, ...} : t) x =
             NONE => raise Fail "Corify.St.lookupConByName"
           | SOME n => CNormal n
 
-fun bindVal {cons, vals, strs, funs, current, nested} s n =
+fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n =
     let
         val n' = alloc ()
 
         val current =
             case current of
                 FFfi _ => raise Fail "Binding inside FFfi"
-              | FNormal {cons, vals, strs, funs} =>
+              | FNormal {cons, constructors, vals, strs, funs} =>
                 FNormal {cons = cons,
+                         constructors = constructors,
                          vals = SM.insert (vals, s, n'),
                          strs = strs,
                          funs = funs}
     in
         ({cons = cons,
+          constructors = constructors,
           vals = IM.insert (vals, n, n'),
           strs = strs,
           funs = funs,
@@ -183,18 +195,20 @@ fun bindVal {cons, vals, strs, funs, current, nested} s n =
          n')
     end
 
-fun bindConstructor {cons, vals, strs, funs, current, nested} s n =
+fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n =
     let
         val current =
             case current of
                 FFfi _ => raise Fail "Binding inside FFfi"
-              | FNormal {cons, vals, strs, funs} =>
+              | FNormal {cons, constructors, vals, strs, funs} =>
                 FNormal {cons = cons,
+                         constructors = constructors,
                          vals = SM.insert (vals, s, n),
                          strs = strs,
                          funs = funs}
     in
         {cons = cons,
+         constructors = constructors,
          vals = IM.insert (vals, n, n),
          strs = strs,
          funs = funs,
@@ -202,6 +216,7 @@ fun bindConstructor {cons, vals, strs, funs, current, nested} s n =
          nested = nested}
     end
 
+
 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
 
 fun lookupValByName ({current, ...} : t) x =
@@ -215,26 +230,64 @@ fun lookupValByName ({current, ...} : t) x =
             NONE => raise Fail "Corify.St.lookupValByName"
           | SOME n => ENormal n
 
-fun enter {cons, vals, strs, funs, current, nested} =
+fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' =
+    let
+        val current =
+            case current of
+                FFfi _ => raise Fail "Binding inside FFfi"
+              | FNormal {cons, constructors, vals, strs, funs} =>
+                FNormal {cons = cons,
+                         constructors = SM.insert (constructors, s, n'),
+                         vals = vals,
+                         strs = strs,
+                         funs = funs}
+    in
+        {cons = cons,
+         constructors = IM.insert (constructors, n, n'),
+         vals = vals,
+         strs = strs,
+         funs = funs,
+         current = current,
+         nested = nested}
+    end
+
+fun lookupConstructorById ({constructors, ...} : t) n =
+    case IM.find (constructors, n) of
+        NONE => raise Fail "Corify.St.lookupConstructorById"
+      | SOME x => x
+
+fun lookupConstructorByName ({current, ...} : t) x =
+    case current of
+        FFfi {mod = m, ...} => L'.PConFfi (m, x)
+      | FNormal {constructors, ...} =>
+        case SM.find (constructors, x) of
+            NONE => raise Fail "Corify.St.lookupConstructorByName"
+          | SOME n => n
+
+fun enter {cons, constructors, vals, strs, funs, current, nested} =
     {cons = cons,
+     constructors = constructors,
      vals = vals,
      strs = strs,
      funs = funs,
      current = FNormal {cons = SM.empty,
+                        constructors = SM.empty,
                         vals = SM.empty,
                         strs = SM.empty,
                         funs = SM.empty},
      nested = current :: nested}
 
 fun dummy f = {cons = IM.empty,
+               constructors = IM.empty,
                vals = IM.empty,
                strs = IM.empty,
                funs = IM.empty,
                current = f,
                nested = []}
 
-fun leave {cons, vals, strs, funs, current, nested = m1 :: rest} =
+fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
         {outer = {cons = cons,
+                  constructors = constructors,
                   vals = vals,
                   strs = strs,
                   funs = funs,
@@ -245,14 +298,17 @@ fun leave {cons, vals, strs, funs, current, nested = m1 :: rest} =
 
 fun ffi m vals = dummy (FFfi {mod = m, vals = vals})
 
-fun bindStr ({cons, vals, strs, funs,
-              current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
+fun bindStr ({cons, constructors, vals, strs, funs,
+              current = FNormal {cons = mcons, constructors = mconstructors,
+                                 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
             x n ({current = f, ...} : t) =
     {cons = cons,
+     constructors = constructors,
      vals = vals,
      strs = IM.insert (strs, n, f),
      funs = funs,
      current = FNormal {cons = mcons,
+                        constructors = mconstructors,
                         vals = mvals,
                         strs = SM.insert (mstrs, x, f),
                         funs = mfuns},
@@ -270,14 +326,17 @@ fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) =
        | SOME f => dummy f)
   | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
 
-fun bindFunctor ({cons, vals, strs, funs,
-                  current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
+fun bindFunctor ({cons, constructors, vals, strs, funs,
+                  current = FNormal {cons = mcons, constructors = mconstructors,
+                                     vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
                 x n xa na str =
     {cons = cons,
+     constructors = constructors,
      vals = vals,
      strs = strs,
      funs = IM.insert (funs, n, (xa, na, str)),
      current = FNormal {cons = mcons,
+                        constructors = mconstructors,
                         vals = mvals,
                         strs = mstrs,
                         funs = SM.insert (mfuns, x, (xa, na, str))},
@@ -338,6 +397,25 @@ fun corifyCon st (c, loc) =
       | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
       | L.CUnit => (L'.CUnit, loc)
 
+fun corifyPatCon st pc =
+    case pc of
+        L.PConVar n => St.lookupConstructorById st n
+      | L.PConProj (m1, ms, x) =>
+        let
+            val st = St.lookupStrById st m1
+            val st = foldl St.lookupStrByName st ms
+        in
+            St.lookupConstructorByName st x
+        end
+
+fun corifyPat st (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 (corifyPatCon st pc, Option.map (corifyPat st) po), loc)
+      | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, corifyPat st p)) xps), loc)
+
 fun corifyExp st (e, loc) =
     case e of
         L.EPrim p => (L'.EPrim p, loc)
@@ -394,7 +472,12 @@ 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.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.EWrite e => (L'.EWrite (corifyExp st e), loc)
 
 fun corifyDecl ((d, loc : EM.span), st) =
@@ -410,27 +493,47 @@ fun corifyDecl ((d, loc : EM.span), st) =
             val (st, n) = St.bindCon st x n
             val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
                                                    let
-                                                       val st = St.bindConstructor st x n
+                                                       val st = St.bindConstructor st x n (L'.PConVar n)
+                                                       val st = St.bindConstructorVal st x n
                                                        val co = Option.map (corifyCon st) co
                                                    in
                                                        ((x, n, co), st)
                                                    end) st xncs
+
+            val t = (L'.CNamed n, loc)
+            val dcons = map (fn (x, n, to) =>
+                                let
+                                    val (e, t) =
+                                        case to of
+                                            NONE => ((L'.ECon (n, NONE), loc), t)
+                                          | SOME t' => ((L'.EAbs ("x", t', t,
+                                                                  (L'.ECon (n, SOME (L'.ERel 0, loc)), loc)),
+                                                         loc),
+                                                        (L'.TFun (t', t), loc))
+                                in
+                                    (L'.DVal (x, n, t, e, ""), loc)
+                                end) xncs
         in
-            ([(L'.DDatatype (x, n, xncs), loc)], st)
+            ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
         end
       | L.DDatatypeImp (x, n, m1, ms, s, xncs) =>
         let
             val (st, n) = St.bindCon st x n
             val c = corifyCon st (L.CModProj (m1, ms, s), loc)
 
+            val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
+            val (_, {inner, ...}) = corifyStr (m, st)
+
             val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
                                                    let
+                                                       val n' = St.lookupConstructorByName inner x
+                                                       val st = St.bindConstructor st x n n'
                                                        val (st, n) = St.bindVal st x n
                                                        val co = Option.map (corifyCon st) co
                                                    in
                                                        ((x, n, co), st)
                                                    end) st xncs
-
+                             
             val cds = map (fn (x, n, co) =>
                               let
                                   val t = case co of
diff --git a/src/monoize.sml b/src/monoize.sml
index c8060937..50e705f2 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -171,6 +171,7 @@ fun monoExp (env, st) (all as (e, loc)) =
             L.EPrim p => (L'.EPrim p, loc)
           | L.ERel n => (L'.ERel n, loc)
           | L.ENamed n => (L'.ENamed n, loc)
+          | L.ECon _ => raise Fail "Monoize ECon"
           | L.EFfi mx => (L'.EFfi mx, loc)
           | L.EFfiApp (m, x, es) => (L'.EFfiApp (m, x, map (monoExp (env, st)) es), loc)
 
@@ -448,6 +449,9 @@ fun monoExp (env, st) (all as (e, loc)) =
           | L.EField (e, x, _) => (L'.EField (monoExp (env, st) e, monoName env x), loc)
           | L.ECut _ => poly ()
           | L.EFold _ => poly ()
+
+          | L.ECase _ => raise Fail "Monoize ECase"
+
           | L.EWrite e => (L'.EWrite (monoExp (env, st) e), loc)
 
           | L.EClosure (n, es) => (L'.EClosure (n, map (monoExp (env, st)) es), loc)