Specialization of single-parameter datatypes

19 files changed, 672 insertions, 61 deletions

diff --git a/src/compiler.sig b/src/compiler.sig
index 9f856158..43224a49 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -46,6 +46,7 @@ signature COMPILER = sig
     val shake' : job -> Core.file option
     val tag : job -> Core.file option
     val reduce : job -> Core.file option
+    val specialize : job -> Core.file option
     val shake : job -> Core.file option
     val monoize : job -> Mono.file option
     val mono_opt' : job -> Mono.file option
@@ -62,6 +63,7 @@ signature COMPILER = sig
     val testShake' : job -> unit
     val testTag : job -> unit
     val testReduce : job -> unit
+    val testSpecialize : job -> unit
     val testShake : job -> unit
     val testMonoize : job -> unit
     val testMono_opt' : job -> unit
diff --git a/src/compiler.sml b/src/compiler.sml
index 15d27b6b..20164b83 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -214,15 +214,24 @@ fun reduce job =
         if ErrorMsg.anyErrors () then
             NONE
         else
-            SOME (Reduce.reduce (Shake.shake file))
+            SOME (Reduce.reduce file)
 
-fun shake job =
+fun specialize job =
     case reduce job of
         NONE => NONE
       | SOME file =>
         if ErrorMsg.anyErrors () then
             NONE
         else
+            SOME (Specialize.specialize file)
+
+fun shake job =
+    case specialize job of
+        NONE => NONE
+      | SOME file =>
+        if ErrorMsg.anyErrors () then
+            NONE
+        else
             SOME (Shake.shake file)
 
 fun monoize job =
@@ -332,8 +341,8 @@ fun testShake' job =
     handle CoreEnv.UnboundNamed n =>
            print ("Unbound named " ^ Int.toString n ^ "\n")
 
-fun testTag job =
-    (case tag job of
+fun testReduce job =
+    (case reduce job of
          NONE => print "Failed\n"
        | SOME file =>
          (Print.print (CorePrint.p_file CoreEnv.empty file);
@@ -341,8 +350,17 @@ fun testTag job =
     handle CoreEnv.UnboundNamed n =>
            print ("Unbound named " ^ Int.toString n ^ "\n")
 
-fun testReduce job =
-    (case reduce job of
+fun testSpecialize job =
+    (case specialize job of
+         NONE => print "Failed\n"
+       | SOME file =>
+         (Print.print (CorePrint.p_file CoreEnv.empty file);
+          print "\n"))
+    handle CoreEnv.UnboundNamed n =>
+           print ("Unbound named " ^ Int.toString n ^ "\n")
+
+fun testTag job =
+    (case tag job of
          NONE => print "Failed\n"
        | SOME file =>
          (Print.print (CorePrint.p_file CoreEnv.empty file);
diff --git a/src/core_env.sig b/src/core_env.sig
index b0cf8304..7b72235f 100644
--- a/src/core_env.sig
+++ b/src/core_env.sig
@@ -28,6 +28,7 @@
 signature CORE_ENV = sig
 
     val liftConInCon : int -> Core.con -> Core.con
+    val subConInCon : (int * Core.con) -> Core.con -> Core.con
 
     type env
 
@@ -54,5 +55,6 @@ signature CORE_ENV = sig
     val lookupENamed : env -> int -> string * Core.con * Core.exp option * string
 
     val declBinds : env -> Core.decl -> env
+    val patBinds : env -> Core.pat -> env
                                                  
 end
diff --git a/src/core_env.sml b/src/core_env.sml
index 5b7cfa2e..d59e3d3d 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -51,6 +51,19 @@ val liftConInCon =
 
 val lift = liftConInCon 0
 
+val subConInCon =
+    U.Con.mapB {kind = fn k => k,
+                con = fn (xn, rep) => fn c =>
+                                  case c of
+                                      CRel xn' =>
+                                      (case Int.compare (xn', xn) of
+                                           EQUAL => #1 rep
+                                         | GREATER => CRel (xn' - 1)
+                                         | LESS => c)
+                                    | _ => c,
+                bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
+                        | (ctx, _) => ctx}
+
 
 (* Back to environments *)
 
@@ -175,4 +188,13 @@ fun declBinds env (d, loc) =
       | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis
       | DExport _ => env
 
+fun patBinds env (p, loc) =
+    case p of
+        PWild => env
+      | 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
+
 end
diff --git a/src/core_print.sig b/src/core_print.sig
index 1899ce15..dfad5827 100644
--- a/src/core_print.sig
+++ b/src/core_print.sig
@@ -30,6 +30,7 @@
 signature CORE_PRINT = sig
     val p_kind : Core.kind Print.printer
     val p_con : CoreEnv.env -> Core.con Print.printer
+    val p_pat : CoreEnv.env -> Core.pat Print.printer
     val p_exp : CoreEnv.env -> Core.exp Print.printer
     val p_decl : CoreEnv.env -> Core.decl Print.printer
     val p_file : CoreEnv.env -> Core.file Print.printer
diff --git a/src/core_print.sml b/src/core_print.sml
index 05e3c81f..e4eae55e 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -199,10 +199,14 @@ 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 (_, pc, _, NONE) => p_patCon env pc
-      | ECon (_, pc, _, SOME e) => parenIf par (box [p_patCon env pc,
-                                                     space,
-                                                     p_exp' true env e])
+      | ECon (_, pc, _, NONE) => box [string "[",
+                                      p_patCon env pc,
+                                      string "]"]
+      | ECon (_, pc, _, SOME e) => box [string "[",
+                                        p_patCon env pc,
+                                        space,
+                                        p_exp' true env e,
+                                        string "]"]
       | EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"]
       | EFfiApp (m, x, es) => box [string "FFI(",
                                    string m,
@@ -301,7 +305,7 @@ fun p_exp' par env (e, _) =
                                                                              space,
                                                                              string "=>",
                                                                              space,
-                                                                             p_exp env e]) pes])
+                                                                             p_exp (E.patBinds env p) e]) pes])
 
       | EWrite e => box [string "write(",
                          p_exp env e,
@@ -349,10 +353,15 @@ fun p_datatype env (x, n, xs, cons) =
         val k = (KType, ErrorMsg.dummySpan)
         val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE
         val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
+
+        val xp = if !debug then
+                     string (x ^ "__" ^ Int.toString n)
+                 else
+                     string x
     in
         box [string "datatype",
              space,
-             string x,
+             xp,
              p_list_sep (box []) (fn x => box [space, string x]) xs,
              space,
              string "=",
@@ -360,7 +369,7 @@ fun p_datatype env (x, n, xs, cons) =
              p_list_sep (box [space, string "|", space])
                         (fn (x, n, NONE) => if !debug then (string (x ^ "__" ^ Int.toString n))
                                             else string x
-                          | (x, _, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n))
+                          | (x, n, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n))
                                                    else string x, space, string "of", space, p_con env t])
                         cons]
     end
diff --git a/src/core_util.sig b/src/core_util.sig
index ebfcf54b..aa957794 100644
--- a/src/core_util.sig
+++ b/src/core_util.sig
@@ -30,6 +30,8 @@ signature CORE_UTIL = sig
 val classifyDatatype : (string * int * Core.con option) list -> Core.datatype_kind
 
 structure Kind : sig
+    val compare : Core.kind * Core.kind -> order
+
     val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder
                   -> (Core.kind, 'state, 'abort) Search.mapfolder
     val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind
@@ -37,6 +39,8 @@ structure Kind : sig
 end
 
 structure Con : sig
+    val compare : Core.con * Core.con -> order
+
     datatype binder =
              Rel of string * Core.kind
            | Named of string * int * Core.kind * Core.con option
@@ -64,6 +68,10 @@ structure Con : sig
 
     val exists : {kind : Core.kind' -> bool,
                   con : Core.con' -> bool} -> Core.con -> bool
+
+    val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state,
+                   con : Core.con' * 'state -> Core.con' * 'state}
+                  -> 'state -> Core.con -> Core.con * 'state
 end
 
 structure Exp : sig
diff --git a/src/core_util.sml b/src/core_util.sml
index b7a16dc2..3fc57739 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -39,6 +39,28 @@ structure S = Search
 
 structure Kind = struct
 
+open Order
+
+fun compare ((k1, _), (k2, _)) =
+    case (k1, k2) of
+        (KType, KType) => EQUAL
+      | (KType, _) => LESS
+      | (_, KType) => GREATER
+
+      | (KArrow (d1, r1), KArrow (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
+      | (KArrow _, _) => LESS
+      | (_, KArrow _) => GREATER
+
+      | (KName, KName) => EQUAL
+      | (KName, _) => LESS
+      | (_, KName) => GREATER
+
+      | (KRecord k1, KRecord k2) => compare (k1, k2)
+      | (KRecord _, _) => LESS
+      | (_, KRecord _) => GREATER
+
+      | (KUnit, KUnit) => EQUAL
+
 fun mapfold f =
     let
         fun mfk k acc =
@@ -85,6 +107,76 @@ end
 
 structure Con = struct
 
+open Order
+
+fun compare ((c1, _), (c2, _)) =
+    case (c1, c2) of
+        (TFun (d1, r1), TFun (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
+      | (TFun _, _) => LESS
+      | (_, TFun _) => GREATER
+
+      | (TCFun (x1, k1, r1), TCFun (x2, k2, r2)) =>
+        join (String.compare (x1, x2),
+           fn () => join (Kind.compare (k1, k2),
+                          fn () => compare (r1, r2)))
+      | (TCFun _, _) => LESS
+      | (_, TCFun _) => GREATER
+
+      | (TRecord c1, TRecord c2) => compare (c1, c2)
+      | (TRecord _, _) => LESS
+      | (_, TRecord _) => GREATER
+
+      | (CRel n1, CRel n2) => Int.compare (n1, n2)
+      | (CRel _, _) => LESS
+      | (_, CRel _) => GREATER
+
+      | (CNamed n1, CNamed n2) => Int.compare (n1, n2)
+      | (CNamed _, _) => LESS
+      | (_, CNamed _) => GREATER
+
+      | (CFfi (m1, s1), CFfi (m2, s2)) => join (String.compare (m1, m2),
+                                                fn () => String.compare (s1, s2))
+      | (CFfi _, _) => LESS
+      | (_, CFfi _) => GREATER
+
+      | (CApp (f1, x1), CApp (f2, x2)) => join (compare (f1, f2),
+                                                fn () => compare (x1, x2))
+      | (CApp _, _) => LESS
+      | (_, CApp _) => GREATER
+
+      | (CAbs (x1, k1, b1), CAbs (x2, k2, b2)) =>
+        join (String.compare (x1, x2),
+              fn () => join (Kind.compare (k1, k2),
+                             fn () => compare (b1, b2)))
+      | (CAbs _, _) => LESS
+      | (_, CAbs _) => GREATER
+
+      | (CName s1, CName s2) => String.compare (s1, s2)
+      | (CName _, _) => LESS
+      | (_, CName _) => GREATER
+
+      | (CRecord (k1, xvs1), CRecord (k2, xvs2)) =>
+        join (Kind.compare (k1, k2),
+              fn () => joinL (fn ((x1, v1), (x2, v2)) =>
+                                 join (compare (x1, x2),
+                                       fn () => compare (v1, v2))) (xvs1, xvs2))
+      | (CRecord _, _) => LESS
+      | (_, CRecord _) => GREATER
+
+      | (CConcat (f1, s1), CConcat (f2, s2)) =>
+        join (compare (f1, f2),
+              fn () => compare (s1, s2))
+      | (CConcat _, _) => LESS
+      | (_, CConcat _) => GREATER
+
+      | (CFold (d1, r1), CFold (d2, r2)) =>
+        join (Kind.compare (d1, r2),
+              fn () => Kind.compare (r1, r2))
+      | (CFold _, _) => LESS
+      | (_, CFold _) => GREATER
+
+      | (CUnit, CUnit) => EQUAL
+
 datatype binder =
          Rel of string * kind
        | Named of string * int * kind * con option
@@ -201,6 +293,12 @@ fun exists {kind, con} k =
         S.Return _ => true
       | S.Continue _ => false
 
+fun foldMap {kind, con} s c =
+    case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
+                  con = fn c => fn s => S.Continue (con (c, s))} c s of
+        S.Continue v => v
+      | S.Return _ => raise Fail "CoreUtil.Con.foldMap: Impossible"
+
 end
 
 structure Exp = struct
@@ -317,8 +415,22 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                 S.bind2 (mfe ctx e,
                          fn e' =>
                             S.bind2 (ListUtil.mapfold (fn (p, e) =>
-                                                         S.map2 (mfe ctx e,
-                                                              fn e' => (p, e'))) pes,
+                                                          let
+                                                              fun pb ((p, _), ctx) =
+                                                                  case p of
+                                                                      PWild => ctx
+                                                                    | 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) =>
+                                                                                               pb (p, ctx)) ctx xps
+                                                          in
+                                                              S.bind2 (mfp ctx p,
+                                                                       fn p' =>
+                                                                          S.map2 (mfe (pb (p', ctx)) e,
+                                                                               fn e' => (p', e')))
+                                                          end) pes,
                                     fn pes' =>
                                        S.bind2 (mfc ctx disc,
                                                 fn disc' =>
@@ -335,6 +447,45 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                 S.map2 (ListUtil.mapfold (mfe ctx) es,
                      fn es' =>
                         (EClosure (n, es'), loc))
+
+        and mfp ctx (pAll as (p, loc)) =
+            case p of
+                PWild => S.return2 pAll
+              | PVar (x, t) =>
+                S.map2 (mfc ctx t,
+                        fn t' =>
+                           (PVar (x, t'), loc))
+              | PPrim _ => S.return2 pAll
+              | PCon (dk, pc, args, po) =>
+                S.bind2 (mfpc ctx pc,
+                         fn pc' =>
+                            S.bind2 (ListUtil.mapfold (mfc ctx) args,
+                                     fn args' =>
+                                        S.map2 ((case po of
+                                                     NONE => S.return2 NONE
+                                                   | SOME p => S.map2 (mfp ctx p, SOME)),
+                                                fn po' =>
+                                                   (PCon (dk, pc', args', po'), loc))))
+              | PRecord xps =>
+                S.map2 (ListUtil.mapfold (fn (x, p, c) =>
+                                              S.bind2 (mfp ctx p,
+                                                       fn p' =>
+                                                          S.map2 (mfc ctx c,
+                                                                  fn c' =>
+                                                                     (x, p', c')))) xps,
+                         fn xps' =>
+                            (PRecord xps', loc))
+
+        and mfpc ctx pc =
+            case pc of
+                PConVar _ => S.return2 pc
+              | PConFfi {mod = m, datatyp, params, con, arg, kind} =>
+                S.map2 ((case arg of
+                             NONE => S.return2 NONE
+                           | SOME c => S.map2 (mfc ctx c, SOME)),
+                        fn arg' =>
+                           PConFfi {mod = m, datatyp = datatyp, params = params,
+                                    con = con, arg = arg', kind = kind})
     in
         mfe
     end
diff --git a/src/corify.sml b/src/corify.sml
index 1be29665..075939bf 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -538,7 +538,7 @@ structure St : sig
              val k = (L'.KType, loc)
              val dcons = map (fn (x, n, to) =>
                                  let
-                                     val args = ListUtil.mapi (fn (i, _) => (L'.CRel n, loc)) xs
+                                     val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
                                      val (e, t) =
                                          case to of
                                              NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t)
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 60075a70..d3638d18 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -345,7 +345,7 @@ fun p_datatype env (x, n, xs, cons) =
              p_list_sep (box [space, string "|", space])
                         (fn (x, n, NONE) => if !debug then (string (x ^ "__" ^ Int.toString n))
                                             else string x
-                          | (x, _, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n))
+                          | (x, n, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n))
                                                    else string x, space, string "of", space, p_con env t])
                         cons]
     end
diff --git a/src/mono_util.sml b/src/mono_util.sml
index 68cbda08..f00db1fd 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -39,18 +39,7 @@ structure S = Search
 
 structure Typ = struct
 
-fun join (o1, o2) =
-    case o1 of
-        EQUAL => o2 ()
-      | v => v
-
-fun joinL f (os1, os2) =
-    case (os1, os2) of
-        (nil, nil) => EQUAL
-      | (nil, _) => LESS
-      | (h1 :: t1, h2 :: t2) =>
-        join (f (h1, h2), fn () => joinL f (t1, t2))
-      | (_ :: _, nil) => GREATER
+open Order
 
 fun compare ((t1, _), (t2, _)) =
     case (t1, t2) of
diff --git a/src/monoize.sml b/src/monoize.sml
index aef65135..9f75e8f9 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -67,14 +67,16 @@ fun monoType env (all as (c, loc)) =
             (L'.TFfi ("Basis", "string"), loc)
 
           | L.CRel _ => poly ()
-          | L.CNamed n => raise Fail "Monoize CNamed"
-            (*let
-                val (_, xncs) = Env.lookupDatatype env n
+          | L.CNamed n =>
+            let
+                val (_, xs, xncs) = Env.lookupDatatype env n
 
                 val xncs = map (fn (x, n, to) => (x, n, Option.map (monoType env) to)) xncs
             in
-                (L'.TDatatype (MonoUtil.classifyDatatype xncs, n, xncs), loc)
-            end*)
+                case xs of
+                    [] => (L'.TDatatype (MonoUtil.classifyDatatype xncs, n, xncs), loc)
+                  | _ => poly ()
+            end
           | L.CFfi mx => (L'.TFfi mx, loc)
           | L.CApp _ => poly ()
           | L.CAbs _ => poly ()
@@ -206,7 +208,7 @@ fun fooifyExp fk env =
                     let
                         fun makeDecl n fm =
                             let
-                                val (x, xncs) = raise Fail "Monoize TDataype" (*Env.lookupDatatype env i*)
+                                val (x, _, xncs) = Env.lookupDatatype env i
 
                                 val (branches, fm) =
                                     ListUtil.foldlMap
@@ -292,13 +294,23 @@ fun monoPatCon env pc =
       | L.PConFfi {mod = m, datatyp, con, arg, ...} => L'.PConFfi {mod = m, datatyp = datatyp, con = con,
                                                                    arg = Option.map (monoType env) arg}
 
-fun monoPat env (p, loc) =
-    case p of
-        L.PWild => (L'.PWild, loc)
-      | L.PVar (x, t) => (L'.PVar (x, monoType env t), loc)
-      | L.PPrim p => (L'.PPrim p, loc)
-      | L.PCon (dk, pc, _, po) => raise Fail "Monoize PCon" (*(L'.PCon (dk, monoPatCon env 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)
+val dummyPat = (L'.PPrim (Prim.Int 0), ErrorMsg.dummySpan)
+
+fun monoPat env (all as (p, loc)) =
+    let
+        fun poly () =
+            (E.errorAt loc "Unsupported pattern";
+             Print.eprefaces' [("Pattern", CorePrint.p_pat env all)];
+             dummyPat)
+    in
+        case p of
+            L.PWild => (L'.PWild, loc)
+          | L.PVar (x, t) => (L'.PVar (x, monoType env t), loc)
+          | L.PPrim p => (L'.PPrim p, loc)
+          | L.PCon (dk, pc, [], po) => (L'.PCon (dk, monoPatCon env pc, Option.map (monoPat env) po), loc)
+          | L.PCon _ => poly ()
+          | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, monoPat env p, monoType env t)) xps), loc)
+    end
 
 fun monoExp (env, st, fm) (all as (e, loc)) =
     let
@@ -311,8 +323,8 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             L.EPrim p => ((L'.EPrim p, loc), fm)
           | L.ERel n => ((L'.ERel n, loc), fm)
           | L.ENamed n => ((L'.ENamed n, loc), fm)
-          | L.ECon (dk, pc, _, eo) => raise Fail "Monoize ECon"
-            (*let
+          | L.ECon (dk, pc, [], eo) =>
+            let
                 val (eo, fm) =
                     case eo of
                         NONE => (NONE, fm)
@@ -324,7 +336,8 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                         end
             in
                 ((L'.ECon (dk, monoPatCon env pc, eo), loc), fm)
-            end*)
+            end
+          | L.ECon _ => poly ()
           | L.EFfi mx => ((L'.EFfi mx, loc), fm)
           | L.EFfiApp (m, x, es) =>
             let
@@ -718,12 +731,13 @@ fun monoDecl (env, fm) (all as (d, loc)) =
     in
         case d of
             L.DCon _ => NONE
-          | L.DDatatype (x, n, _, xncs) => raise Fail "Monoize DDatatype"
-            (*let
+          | L.DDatatype (x, n, [], xncs) =>
+            let
                 val d = (L'.DDatatype (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env) to)) xncs), loc)
             in
                 SOME (Env.declBinds env all, fm, d)
-            end*)
+            end
+          | L.DDatatype _ => poly ()
           | L.DVal (x, n, t, e, s) =>
             let
                 val (e, fm) = monoExp (env, St.empty, fm) e
diff --git a/src/order.sig b/src/order.sig
new file mode 100644
index 00000000..c648f78b
--- /dev/null
+++ b/src/order.sig
@@ -0,0 +1,35 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Utility code for implementing comparisons *)
+
+signature ORDER = sig
+    
+    val join : order * (unit -> order) -> order
+    val joinL : ('a * 'b -> order) -> 'a list * 'b list -> order
+                                                       
+end
diff --git a/src/order.sml b/src/order.sml
new file mode 100644
index 00000000..4a78823b
--- /dev/null
+++ b/src/order.sml
@@ -0,0 +1,45 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Utility code for implementing comparisons *)
+
+structure Order :> ORDER = struct
+
+fun join (o1, o2) =
+    case o1 of
+        EQUAL => o2 ()
+      | v => v
+             
+fun joinL f (os1, os2) =
+    case (os1, os2) of
+        (nil, nil) => EQUAL
+      | (nil, _) => LESS
+      | (h1 :: t1, h2 :: t2) =>
+        join (f (h1, h2), fn () => joinL f (t1, t2))
+      | (_ :: _, nil) => GREATER
+
+end
diff --git a/src/reduce.sml b/src/reduce.sml
index ecb0777d..c2359c26 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -35,19 +35,7 @@ structure E = CoreEnv
 structure U = CoreUtil
 
 val liftConInCon = E.liftConInCon
-
-val subConInCon =
-    U.Con.mapB {kind = fn k => k,
-                con = fn (xn, rep) => fn c =>
-                                  case c of
-                                      CRel xn' =>
-                                      (case Int.compare (xn', xn) of
-                                           EQUAL => #1 rep
-                                         | GREATER => CRel (xn' - 1)
-                                         | LESS => c)
-                                    | _ => c,
-                bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
-                        | (ctx, _) => ctx}
+val subConInCon = E.subConInCon
 
 val liftExpInExp =
     U.Exp.mapB {kind = fn k => k,
diff --git a/src/sources b/src/sources
index 23379bf4..94c37050 100644
--- a/src/sources
+++ b/src/sources
@@ -4,6 +4,9 @@ search.sml
 list_util.sig
 list_util.sml
 
+order.sig
+order.sml
+
 errormsg.sig
 errormsg.sml
 
@@ -75,6 +78,9 @@ reduce.sml
 shake.sig
 shake.sml
 
+specialize.sig
+specialize.sml
+
 tag.sig
 tag.sml
 
diff --git a/src/specialize.sig b/src/specialize.sig
new file mode 100644
index 00000000..f45c8b19
--- /dev/null
+++ b/src/specialize.sig
@@ -0,0 +1,34 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Simplify a Core program by repeating polymorphic definitions *)
+
+signature SPECIALIZE = sig
+
+    val specialize : Core.file -> Core.file
+    
+end
diff --git a/src/specialize.sml b/src/specialize.sml
new file mode 100644
index 00000000..9690f6e7
--- /dev/null
+++ b/src/specialize.sml
@@ -0,0 +1,276 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Simplify a Core program algebraically *)
+
+structure Specialize :> SPECIALIZE = struct
+
+open Core
+
+structure E = CoreEnv
+structure U = CoreUtil
+
+val liftConInCon = E.liftConInCon
+val subConInCon = E.subConInCon
+
+structure CK = struct
+type ord_key = con list
+val compare = Order.joinL U.Con.compare
+end
+
+structure CM = BinaryMapFn(CK)
+structure IM = IntBinaryMap
+
+type datatyp' = {
+     name : int,
+     constructors : int IM.map
+}
+
+type datatyp = {
+     name : string,
+     params : int,
+     constructors : (string * int * con option) list,
+     specializations : datatyp' CM.map
+}
+
+type state = {
+     count : int,
+     datatypes : datatyp IM.map,
+     constructors : int IM.map,
+     decls : decl list
+}
+
+fun kind (k, st) = (k, st)
+
+val isOpen = U.Con.exists {kind = fn _ => false,
+                           con = fn c =>
+                                    case c of
+                                        CRel _ => true
+                                      | _ => false}
+
+fun considerSpecialization (st : state, n, args, dt : datatyp) =
+    case CM.find (#specializations dt, args) of
+        SOME dt' => (#name dt', #constructors dt', st)
+      | NONE =>
+        let
+            val n' = #count st
+
+            fun sub t = ListUtil.foldli (fn (i, arg, t) =>
+                                            subConInCon (i, arg) t) t args
+
+            val (cons, (count, cmap)) =
+                ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) =>
+                                      let
+                                          val to = Option.map sub to
+                                      in
+                                          ((x, count, to),
+                                           (count + 1,
+                                            IM.insert (cmap, n, count)))
+                                      end) (n' + 1, IM.empty) (#constructors dt)
+
+            val st = {count = count,
+                      datatypes = IM.insert (#datatypes st, n,
+                                             {name = #name dt,
+                                              params = #params dt,
+                                              constructors = #constructors dt,
+                                              specializations = CM.insert (#specializations dt,
+                                                                           args,
+                                                                           {name = n',
+                                                                            constructors = cmap})}),
+                      constructors = #constructors st,
+                      decls = #decls st}
+
+            val (cons, st) = ListUtil.foldlMap (fn ((x, n, NONE), st) => ((x, n, NONE), st)
+                                                 | ((x, n, SOME t), st) =>
+                                                   let
+                                                       val (t, st) = specCon st t
+                                                   in
+                                                       ((x, n, SOME t), st)
+                                                   end) st cons
+
+            val d = (DDatatype (#name dt ^ "_s",
+                                n',
+                                [],
+                                cons), #2 (List.hd args))
+        in
+            (n', cmap, {count = #count st,
+                        datatypes = #datatypes st,
+                        constructors = #constructors st,
+                        decls = d :: #decls st})
+        end
+
+and con (c, st : state) =
+    let
+        fun findApp (c, args) =
+            case c of
+                CApp ((c', _), arg) => findApp (c', arg :: args)
+              | CNamed n => SOME (n, args)
+              | _ => NONE
+    in
+        case findApp (c, []) of
+            SOME (n, args as (_ :: _)) =>
+            if List.exists isOpen args then
+                (c, st)
+            else
+                (case IM.find (#datatypes st, n) of
+                     NONE => (c, st)
+                   | SOME dt =>
+                     if length args <> #params dt then
+                         (c, st)
+                     else
+                         let
+                             val (n, _, st) = considerSpecialization (st, n, args, dt)
+                         in
+                             (CNamed n, st)
+                         end)
+          | _ => (c, st)
+    end
+
+and specCon st = U.Con.foldMap {kind = kind, con = con} st
+
+fun pat (p, st) =
+    case #1 p of
+        PWild => (p, st)
+      | PVar _ => (p, st)
+      | PPrim _ => (p, st)
+      | PCon (dk, PConVar pn, args as (_ :: _), po) =>
+        let
+            val (po, st) =
+                case po of
+                    NONE => (NONE, st)
+                  | SOME p =>
+                    let
+                        val (p, st) = pat (p, st)
+                    in
+                        (SOME p, st)
+                    end
+            val p = (PCon (dk, PConVar pn, args, po), #2 p)
+        in
+            if List.exists isOpen args then
+                (p, st)
+            else
+                case IM.find (#constructors st, pn) of
+                    NONE => (p, st)
+                  | SOME n =>
+                    case IM.find (#datatypes st, n) of
+                        NONE => (p, st)
+                      | SOME dt =>
+                        let
+                            val (n, cmap, st) = considerSpecialization (st, n, args, dt)
+                        in
+                            case IM.find (cmap, pn) of
+                                NONE => raise Fail "Specialize: Missing datatype constructor (pat)"
+                              | SOME pn' => ((PCon (dk, PConVar pn', [], po), #2 p), st)
+                        end
+        end
+      | PCon _ => (p, st)
+      | PRecord xps =>
+        let
+            val (xps, st) = ListUtil.foldlMap (fn ((x, p, t), st) =>
+                                                  let
+                                                      val (p, st) = pat (p, st)
+                                                  in
+                                                      ((x, p, t), st)
+                                                  end)
+                            st xps
+        in
+            ((PRecord xps, #2 p), st)
+        end
+
+fun exp (e, st) =
+    case e of
+        ECon (dk, PConVar pn, args as (_ :: _), eo) =>
+        if List.exists isOpen args then
+            (e, st)
+        else
+            (case IM.find (#constructors st, pn) of
+                 NONE => (e, st)
+               | SOME n =>
+                 case IM.find (#datatypes st, n) of
+                     NONE => (e, st)
+                   | SOME dt =>
+                     let
+                         val (n, cmap, st) = considerSpecialization (st, n, args, dt)
+                     in
+                         case IM.find (cmap, pn) of
+                             NONE => raise Fail "Specialize: Missing datatype constructor"
+                           | SOME pn' => (ECon (dk, PConVar pn', [], eo), st)
+                     end)
+      | ECase (e, pes, r) =>
+        let
+            val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) =>
+                                                  let
+                                                      val (p, st) = pat (p, st)
+                                                  in
+                                                      ((p, e), st)
+                                                  end) st pes
+        in
+            (ECase (e, pes, r), st)
+        end
+      | _ => (e, st)
+
+fun decl (d, st) = (d, st)
+
+val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
+
+fun specialize file =
+    let
+        fun doDecl (all as (d, _), st : state) =
+            case d of
+                DDatatype (x, n, xs, xnts) =>
+                ([all], {count = #count st,
+                         datatypes = IM.insert (#datatypes st, n,
+                                                {name = x,
+                                                 params = length xs,
+                                                 constructors = xnts,
+                                                 specializations = CM.empty}),
+                         constructors = foldl (fn ((_, n', _), constructors) =>
+                                                  IM.insert (constructors, n', n))
+                                              (#constructors st) xnts,
+                         decls = []})
+              | _ =>
+                let
+                    val (d, st) = specDecl st all
+                in
+                    (rev (d :: #decls st),
+                     {count = #count st,
+                      datatypes = #datatypes st,
+                      constructors = #constructors st,
+                      decls = []})
+                end
+
+        val (ds, _) = ListUtil.foldlMapConcat doDecl
+                      {count = U.File.maxName file + 1,
+                       datatypes = IM.empty,
+                       constructors = IM.empty,
+                       decls = []} file
+    in
+        ds
+    end
+
+
+end
diff --git a/tests/datatypeP.lac b/tests/datatypeP.lac
index 12389322..171d8812 100644
--- a/tests/datatypeP.lac
+++ b/tests/datatypeP.lac
@@ -8,3 +8,14 @@ val f = fn t ::: Type => fn x : option t =>
 
 val none_again = f none
 val some_1_again = f some_1
+
+val show = fn t ::: Type => fn x : option t => case x of None => "None" | Some _ => "Some"
+
+val page = fn x => <html><body>
+        {cdata (show x)}
+</body></html>
+
+val main : unit -> page = fn () => <html><body>
+        <li><a link={page none_again}>None</a></li>
+        <li><a link={page some_1_again}>Some 1</a></li>
+</body></html>