"Hello world" compiles, after replacing type-level fold with map

22 files changed, 190 insertions, 336 deletions

diff --git a/src/core.sml b/src/core.sml
index c6e0cfef..d7a57493 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -54,7 +54,7 @@ datatype con' =
 
        | CRecord of kind * (con * con) list
        | CConcat of con * con
-       | CFold of kind * kind
+       | CMap of kind * kind
 
        | CUnit
 
diff --git a/src/core_print.sml b/src/core_print.sml
index 405ae14e..db8c3907 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -138,7 +138,7 @@ fun p_con' par env (c, _) =
                                               string "++",
                                               space,
                                               p_con env c2])
-      | CFold _ => string "fold"
+      | CMap _ => string "map"
       | CUnit => string "()"
 
       | CTuple cs => box [string "(",
diff --git a/src/core_util.sml b/src/core_util.sml
index a222dca4..e76da387 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -178,11 +178,11 @@ fun compare ((c1, _), (c2, _)) =
       | (CConcat _, _) => LESS
       | (_, CConcat _) => GREATER
 
-      | (CFold (d1, r1), CFold (d2, r2)) =>
+      | (CMap (d1, r1), CMap (d2, r2)) =>
         join (Kind.compare (d1, r2),
               fn () => Kind.compare (r1, r2))
-      | (CFold _, _) => LESS
-      | (_, CFold _) => GREATER
+      | (CMap _, _) => LESS
+      | (_, CMap _) => GREATER
 
       | (CUnit, CUnit) => EQUAL
       | (CUnit, _) => LESS
@@ -261,12 +261,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                          S.map2 (mfc ctx c2,
                               fn c2' =>
                                  (CConcat (c1', c2'), loc)))
-              | CFold (k1, k2) =>
+              | CMap (k1, k2) =>
                 S.bind2 (mfk k1,
                          fn k1' =>
                             S.map2 (mfk k2,
                                     fn k2' =>
-                                       (CFold (k1', k2'), loc)))
+                                       (CMap (k1', k2'), loc)))
 
               | CUnit => S.return2 cAll
 
diff --git a/src/corify.sml b/src/corify.sml
index 2383ee03..c464e5a5 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -473,7 +473,7 @@ fun corifyCon st (c, loc) =
       | L.CRecord (k, xcs) =>
         (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
       | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
-      | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
+      | L.CMap (k1, k2) => (L'.CMap (corifyKind k1, corifyKind k2), loc)
       | L.CUnit => (L'.CUnit, loc)
 
       | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc)
diff --git a/src/disjoint.sml b/src/disjoint.sml
index c6a8d50f..81023972 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -213,37 +213,8 @@ fun decomposeRow (env, denv) c =
                                                 ("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*)
                 case #1 (#1 (hnormCon (env, denv) c)) of
                     CApp (
-                    (CApp (
-                     (CApp ((CFold (dom, ran), _), f), _),
-                     i), _),
-                    r) =>
-                    let
-                        val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE
-                        val (env', v) = E.pushCNamed env' "v" dom NONE
-                        val (env', st) = E.pushCNamed env' "st" ran NONE
-
-                        val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc),
-                                                                              (CUnit, loc))]), loc),
-                                                             (CNamed st, loc))
-
-                        val c' = (CApp (f, (CNamed nm, loc)), loc)
-                        val c' = (CApp (c', (CNamed v, loc)), loc)
-                        val c' = (CApp (c', (CNamed st, loc)), loc)
-                        val (ps, gs'') = decomposeRow (env', denv') c'
-
-                        fun covered p =
-                            case p of
-                                Unknown _ => false
-                              | Piece p =>
-                                case p of
-                                    (NameN n, []) => n = nm
-                                  | (RowN n, []) => n = st
-                                  | _ => false
-
-                        val ps = List.filter (not o covered) ps
-                    in
-                        decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs)))
-                    end
+                    (CApp ((CMap _, _), _), _),
+                    r) => decomposeRow' (r, (acc, gs))
                   | _ => default ()
             end
     in
diff --git a/src/elab.sml b/src/elab.sml
index 8e44c43c..ec8a910a 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -66,7 +66,7 @@ datatype con' =
 
        | CRecord of kind * (con * con) list
        | CConcat of con * con
-       | CFold of kind * kind
+       | CMap of kind * kind
 
        | CUnit
 
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 0648d704..c3e9274c 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -114,181 +114,98 @@ fun hnormCon env (cAll as (c, loc)) =
                                           ("sc", ElabPrint.p_con env sc)];*)
                  sc
              end
-           | c1' as CApp (c', i) =>
+           | c1' as CApp (c', f) =>
              let
                  fun default () = (CApp ((c1', loc), hnormCon env c2), loc)
              in
                  case #1 (hnormCon env c') of
-                     CApp (c', f) =>
-                     (case #1 (hnormCon env c') of
-                          CFold ks =>
-                          (case #1 (hnormCon env c2) of
-                               CRecord (_, []) => hnormCon env i
-                             | CRecord (k, (x, c) :: rest) =>
-                               hnormCon env
-                                        (CApp ((CApp ((CApp (f, x), loc), c), loc),
-                                               (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
-                                                      (CRecord (k, rest), loc)), loc)), loc)
-                             | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
-                               let
-                                   val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
-
-                               (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc),
-                                                  (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
-                                                         rest''), loc)), loc)*)
-                               in
-                                   (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
-                                   hnormCon env
-                                            (CApp ((CApp ((CApp (f, x), loc), c), loc),
-                                                   (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
-                                                          rest''), loc)), loc)
-                               end
-                             | _ =>
-                               let
-                                   fun cunif () =
-                                       let
-                                           val r = ref NONE
-                                       in
-                                           (r, (CUnif (loc, (KType, loc), "_", r), loc))
-                                       end
-
-                                   val (nmR, nm) = cunif ()
-                                   val (vR, v) = cunif ()
-                                   val (rR, r) = cunif ()
-
-                                   val c = f
-                                   val c = (CApp (c, nm), loc)
-                                   val c = (CApp (c, v), loc)
-                                   val c = (CApp (c, r), loc)
-                                   fun unconstraint c =
-                                       case hnormCon env c of
-                                           (CDisjoint (_, _, _, c), _) => unconstraint c
-                                         | c => c
-                                   val c = unconstraint c
-
-                                   fun tryDistributivity () =
-                                       let
-                                           fun distribute (c1, c2) =
-                                               let
-                                                   val c = (CFold ks, loc)
-                                                   val c = (CApp (c, f), loc)
-                                                   val c = (CApp (c, i), loc)
-
-                                                   val c1 = (CApp (c, c1), loc)
-                                                   val c2 = (CApp (c, c2), loc)
-                                                   val c = (CConcat (c1, c2), loc)
-                                               in
-                                                   hnormCon env c
-                                               end
-                                       in
-                                           case (hnormCon env i, hnormCon env c2, hnormCon env c) of
-                                               ((CRecord (_, []), _),
-                                                (CConcat (arg1, arg2), _),
-                                                (CConcat (c1, c2'), _)) =>
-                                               (case (hnormCon env c1, hnormCon env c2') of
-                                                    ((CRecord (_, [(nm', v')]), _),
-                                                     (CUnif (_, _, _, rR'), _)) =>
-                                                    (case hnormCon env nm' of
-                                                         (CUnif (_, _, _, nmR'), _) =>
-                                                         if nmR' = nmR andalso rR' = rR then
-                                                             distribute (arg1, arg2)
-                                                         else
-                                                             default ()
-                                                       | _ => default ())
-                                                  | _ => default ())
-                                             | _ => default ()
-                                       end
-
-                                   fun tryFusion () =
-                                       let
-                                           fun fuse (dom, new_v, r') =
-                                               let
-                                                   val ran = #2 ks
-
-                                                   val f = (CApp (f, (CRel 2, loc)), loc)
-                                                   val f = (CApp (f, new_v), loc)
-                                                   val f = (CApp (f, (CRel 0, loc)), loc)
-                                                   val f = (CAbs ("acc", ran, f), loc)
-                                                   val f = (CAbs ("v", dom, f), loc)
-                                                   val f = (CAbs ("nm", (KName, loc), f), loc)
-
-                                                   val c = (CFold (dom, ran), loc)
-                                                   val c = (CApp (c, f), loc)
-                                                   val c = (CApp (c, i), loc)
-                                                   val c = (CApp (c, r'), loc)
-                                               in
-                                                   hnormCon env c
-                                               end
-                                       in
-                                           case #1 (hnormCon env c2) of
-                                               CApp (f, r') =>
-                                               (case #1 (hnormCon env f) of
-                                                    CApp (f, inner_i) =>
-                                                    (case (#1 (hnormCon env f), #1 (hnormCon env inner_i)) of
-                                                         (CApp (f, inner_f), CRecord (_, [])) =>
-                                                         (case #1 (hnormCon env f) of
-                                                              CFold (dom, _) =>
-                                                              let
-                                                                  val c = inner_f
-                                                                  val c = (CApp (c, nm), loc)
-                                                                  val c = (CApp (c, v), loc)
-                                                                  val c = (CApp (c, r), loc)
-                                                                  val c = unconstraint c
-
-                                                                  (*val () = Print.prefaces "Onto something!"
-                                                                           [("c", ElabPrint.p_con env cAll),
-                                                                            ("c'", ElabPrint.p_con env c)]*)
-
-                                                              in
-                                                                  case #1 (hnormCon env c) of
-                                                                      CConcat (first, rest) =>
-                                                                      (case (#1 (hnormCon env first),
-                                                                             #1 (hnormCon env rest)) of
-                                                                           (CRecord (_, [(nm', v')]),
-                                                                            CUnif (_, _, _, rR')) =>
-                                                                           (case #1 (hnormCon env nm') of
-                                                                                CUnif (_, _, _, nmR') =>
-                                                                                if rR' = rR andalso nmR' = nmR then
-                                                                                    (nmR := SOME (CRel 2, loc);
-                                                                                     vR := SOME (CRel 1, loc);
-                                                                                     rR := SOME (CError, loc);
-                                                                                     fuse (dom, v', r'))
-                                                                                else
-                                                                                    tryDistributivity ()
-                                                                              | _ => tryDistributivity ())
-                                                                         | _ => tryDistributivity ())
-                                                                    | _ => tryDistributivity ()
-                                                              end
-                                                            | _ => tryDistributivity ())
-                                                       | _ => tryDistributivity ())
-                                                  | _ => tryDistributivity ())
-                                             | _ => tryDistributivity ()
-                                       end
-
-                               in
-                                   (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
-                                   case (hnormCon env i, unconstraint c) of
-                                       ((CRecord (_, []), _),
-                                        (CConcat (c1, c2'), _)) =>
-                                       (case (hnormCon env c1, hnormCon env c2') of
-                                            ((CRecord (_, [(nm', v')]), _),
-                                             (CUnif (_, _, _, rR'), _)) =>
-                                            (case (hnormCon env nm', hnormCon env v') of
-                                                 ((CUnif (_, _, _, nmR'), _),
-                                                  (CUnif (_, _, _, vR'), _)) =>
-                                                 if nmR' = nmR andalso vR' = vR andalso rR' = rR then
-                                                     hnormCon env c2
-                                                 else
-                                                     tryFusion ()
-                                               | _ => tryFusion ())
-                                          | _ => tryFusion ())
-                                     | _ => tryFusion ()
-                               end)
-                        | _ => default ())
+                     CMap (ks as (k1, k2)) =>
+                     (case #1 (hnormCon env c2) of
+                          CRecord (_, []) => (CRecord (k2, []), loc)
+                        | CRecord (_, (x, c) :: rest) =>
+                          hnormCon env
+                                   (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+                                             (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
+                        | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
+                          let
+                              val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
+                          in
+                              hnormCon env
+                                       (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+                                                 (CApp (c1, rest''), loc)), loc)
+                          end
+                        | _ =>
+                          let
+                              fun unconstraint c =
+                                  case hnormCon env c of
+                                      (CDisjoint (_, _, _, c), _) => unconstraint c
+                                    | c => c
+
+                              fun tryDistributivity () =
+                                  case hnormCon env c2 of
+                                      (CConcat (c1, c2'), _) =>
+                                      let
+                                          val c = (CMap ks, loc)
+                                          val c = (CApp (c, f), loc)
+                                                  
+                                          val c1 = (CApp (c, c1), loc)
+                                          val c2 = (CApp (c, c2'), loc)
+                                          val c = (CConcat (c1, c2), loc)
+                                      in
+                                          hnormCon env c
+                                      end
+                                    | _ => default ()
+
+                              fun tryFusion () =
+                                  case #1 (hnormCon env c2) of
+                                      CApp (f', r') =>
+                                      (case #1 (hnormCon env f') of
+                                           CApp (f', inner_f) =>
+                                           (case #1 (hnormCon env f') of
+                                                CMap (dom, _) =>
+                                                let
+                                                    val f' = (CApp (inner_f, (CRel 0, loc)), loc)
+                                                    val f' = (CApp (f, f'), loc)
+                                                    val f' = (CAbs ("v", dom, f'), loc)
+
+                                                    val c = (CMap (dom, k2), loc)
+                                                    val c = (CApp (c, f'), loc)
+                                                    val c = (CApp (c, r'), loc)
+                                                in
+                                                    hnormCon env c
+                                                end
+                                              | _ => tryDistributivity ())
+                                         | _ => tryDistributivity ())
+                                    | _ => tryDistributivity ()
+
+                              fun tryIdentity () =
+                                  let
+                                      fun cunif () =
+                                          let
+                                              val r = ref NONE
+                                          in
+                                              (r, (CUnif (loc, (KType, loc), "_", r), loc))
+                                          end
+                                          
+                                      val (vR, v) = cunif ()
+
+                                      val c = (CApp (f, v), loc)
+                                  in
+                                      case unconstraint c of
+                                          (CUnif (_, _, _, vR'), _) =>
+                                          if vR' = vR then
+                                              hnormCon env c2
+                                          else
+                                              tryFusion ()
+                                        | _ => tryFusion ()
+                                  end
+                          in
+                              tryIdentity ()
+                          end)
                    | _ => default ()
              end
            | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
-
+        
       | CConcat (c1, c2) =>
         (case (hnormCon env c1, hnormCon env c2) of
              ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 0e6c9767..098c9259 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -167,7 +167,7 @@ fun p_con' par env (c, _) =
                                               string "++",
                                               space,
                                               p_con env c2])
-      | CFold _ => string "fold"
+      | CMap _ => string "map"
 
       | CUnit => string "()"
 
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 6e78907d..f052a06d 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -168,12 +168,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                          S.map2 (mfc ctx c2,
                               fn c2' =>
                                  (CConcat (c1', c2'), loc)))
-              | CFold (k1, k2) =>
+              | CMap (k1, k2) =>
                 S.bind2 (mfk k1,
                          fn k1' =>
                             S.map2 (mfk k2,
                                     fn k2' =>
-                                       (CFold (k1', k2'), loc)))
+                                       (CMap (k1', k2'), loc)))
 
               | CUnit => S.return2 cAll
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 39cb85b2..fa97bdf8 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -182,13 +182,10 @@
        | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
        | L.KWild => kunif loc
 
- fun foldKind (dom, ran, loc)=
-     (L'.KArrow ((L'.KArrow ((L'.KName, loc),
-                             (L'.KArrow (dom,
-                                         (L'.KArrow (ran, ran), loc)), loc)), loc),
-                 (L'.KArrow (ran,
-                             (L'.KArrow ((L'.KRecord dom, loc),
-                                         ran), loc)), loc)), loc)
+ fun mapKind (dom, ran, loc)=
+     (L'.KArrow ((L'.KArrow (dom, ran), loc),
+                 (L'.KArrow ((L'.KRecord dom, loc),
+                             (L'.KRecord ran, loc)), loc)), loc)
 
  fun hnormKind (kAll as (k, _)) =
      case k of
@@ -355,13 +352,13 @@
              ((L'.CConcat (c1', c2'), loc), k,
               D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
          end
-       | L.CFold =>
+       | L.CMap =>
          let
              val dom = kunif loc
              val ran = kunif loc
          in
-             ((L'.CFold (dom, ran), loc),
-              foldKind (dom, ran, loc),
+             ((L'.CMap (dom, ran), loc),
+              mapKind (dom, ran, loc),
               [])
          end
 
@@ -489,7 +486,7 @@
 
        | L'.CRecord (k, _) => (L'.KRecord k, loc)
        | L'.CConcat (c, _) => kindof env c
-       | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
+       | L'.CMap (dom, ran) => mapKind (dom, ran, loc)
 
        | L'.CUnit => (L'.KUnit, loc)
 
@@ -504,41 +501,21 @@
 
  val hnormCon = D.hnormCon
 
- datatype con_summary =
-          Nil
-        | Cons
-        | Unknown
-
- fun compatible cs =
-     case cs of
-         (Unknown, _) => false
-       | (_, Unknown) => false
-       | (s1, s2) => s1 = s2
-
- fun summarizeCon (env, denv) c =
+ fun deConstraintCon (env, denv) c =
      let
          val (c, gs) = hnormCon (env, denv) c
      in
          case #1 c of
-             L'.CRecord (_, []) => (Nil, gs)
-           | L'.CRecord (_, _ :: _) => (Cons, gs)
-           | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
-           | L'.CDisjoint (_, _, _, c) =>
+             L'.CDisjoint (_, _, _, c) =>
              let
-                 val (s, gs') = summarizeCon (env, denv) c
+                 val (c', gs') = deConstraintCon (env, denv) c
              in
-                 (s, gs @ gs')
+                 (c', gs @ gs')
              end
-           | _ => (Unknown, gs)
+           | _ => (c, gs)
      end
 
- fun p_con_summary s =
-     Print.PD.string (case s of
-                          Nil => "Nil"
-                        | Cons => "Cons"
-                        | Unknown => "Unknown")
-
- exception SummaryFailure
+ exception GuessFailure
 
  fun isUnitCon env (c, loc) =
      case c of
@@ -574,7 +551,7 @@
 
        | L'.CRecord _ => false
        | L'.CConcat _ => false
-       | L'.CFold _ => false
+       | L'.CMap _ => false
 
        | L'.CUnit => true
 
@@ -720,14 +697,14 @@
 
          fun isGuessable (other, fs) =
              let
-                 val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure)
+                 val gs = guessMap (env, denv) (other, (L'.CRecord (k, fs), loc), [], GuessFailure)
              in
                  List.all (fn (loc, env, denv, c1, c2) =>
                               case D.prove env denv (c1, c2, loc) of
                                   [] => true
                                 | _ => false) gs
              end
-             handle SummaryFailure => false
+             handle GuessFailure => false
 
          val (fs1, fs2, others1, others2) =
              case (fs1, fs2, others1, others2) of
@@ -783,79 +760,68 @@
                                        ("#2", p_summary env s2)]*)
      end
 
- and guessFold (env, denv) (c1, c2, gs, ex) =
+ and guessMap (env, denv) (c1, c2, gs, ex) =
      let
          val loc = #2 c1
 
-         fun unfold (dom, ran, f, i, r, c) =
+         fun unfold (dom, ran, f, r, c) =
              let
-                 val nm = cunif (loc, (L'.KName, loc))
-                 val v =
-                     case dom of
-                         (L'.KUnit, _) => (L'.CUnit, loc)
-                       | _ => cunif (loc, dom)
-                 val rest = cunif (loc, (L'.KRecord dom, loc))
-                 val acc = (L'.CFold (dom, ran), loc)
-                 val acc = (L'.CApp (acc, f), loc)
-                 val acc = (L'.CApp (acc, i), loc)
-                 val acc = (L'.CApp (acc, rest), loc)
-
-                 val (iS, gs3) = summarizeCon (env, denv) i
-
-                 val app = (L'.CApp (f, nm), loc)
-                 val app = (L'.CApp (app, v), loc)
-                 val app = (L'.CApp (app, acc), loc)
-                 val (appS, gs4) = summarizeCon (env, denv) app
-
-                 val (cS, gs5) = summarizeCon (env, denv) c
-             in
-                 (*prefaces "Summaries" [("iS", p_con_summary iS),
-                                         ("appS", p_con_summary appS),
-                                         ("cS", p_con_summary cS)];*)
-
-                 if compatible (iS, appS) then
-                     raise ex
-                 else if compatible (cS, iS) then
+                 fun unfold (r, c) =
                      let
-                         (*val () = prefaces "Same?" [("i", p_con env i),
-                                                    ("c", p_con env c)]*)
-                         val gs6 = unifyCons (env, denv) i c
-                         (*val () = TextIO.print "Yes!\n"*)
-
-                         val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
+                         val (c', gs1) = deConstraintCon (env, denv) c
                      in
-                         gs @ gs3 @ gs5 @ gs6 @ gs7
-                     end
-                 else if compatible (cS, appS) then
-                     let
-                         (*val () = prefaces "Same?" [("app", p_con env app),
-                                                      ("c", p_con env c),
-                                                      ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
-                         val gs6 = unifyCons (env, denv) app c
-                         (*val () = TextIO.print "Yes!\n"*)
-
-                         val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
-                         val concat = (L'.CConcat (singleton, rest), loc)
-                         (*val () = prefaces "Pre-crew" [("r", p_con env r),
-                                                         ("concat", p_con env concat)]*)
-                         val gs7 = unifyCons (env, denv) r concat
-                     in
-                         (*prefaces "The crew" [("nm", p_con env nm),
-                                                ("v", p_con env v),
-                                                ("rest", p_con env rest)];*)
+                         case #1 c' of
+                             L'.CRecord (_, []) =>
+                             let
+                                 val gs2 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
+                             in
+                                 gs1 @ gs2
+                             end
+                           | L'.CRecord (_, [(x, v)]) =>
+                             let
+                                 val v' = case dom of
+                                              (L'.KUnit, _) => (L'.CUnit, loc)
+                                            | _ => cunif (loc, dom)
+                                 val gs2 = unifyCons (env, denv) v' (L'.CApp (f, v), loc)
 
-                         gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
+                                 val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc)
+                             in
+                                 gs1 @ gs2 @ gs3
+                             end
+                           | L'.CRecord (_, (x, v) :: rest) =>
+                             let
+                                 val r1 = cunif (loc, (L'.KRecord dom, loc))
+                                 val r2 = cunif (loc, (L'.KRecord dom, loc))
+                                 val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
+
+                                 val gs3 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc))
+                                 val gs4 = unfold (r2, (L'.CRecord (ran, rest), loc))
+                             in
+                                 gs1 @ gs2 @ gs3 @ gs4
+                             end
+                           | L'.CConcat (c1', c2') =>
+                             let
+                                 val r1 = cunif (loc, (L'.KRecord dom, loc))
+                                 val r2 = cunif (loc, (L'.KRecord dom, loc))
+                                 val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
+
+                                 val gs3 = unfold (r1, c1')
+                                 val gs4 = unfold (r2, c2')
+                             in
+                                 gs1 @ gs2 @ gs3 @ gs4
+                             end
+                           | _ => raise ex
                      end
-                 else
-                     raise ex
+             in
+                 unfold (r, c)
              end
              handle _ => raise ex
      in
          case (#1 c1, #1 c2) of
-             (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) =>
-             unfold (dom, ran, f, i, r, c2)
-           | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) =>
-             unfold (dom, ran, f, i, r, c1)
+             (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
+             unfold (dom, ran, f, r, c2)
+           | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>
+             unfold (dom, ran, f, r, c1)
            | _ => raise ex
      end
 
@@ -890,7 +856,7 @@
                                                                                  (Time.- (Time.now (), befor)))))];*)
                      gs1 @ gs2 @ gs3
                  end
-                 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
+                 handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex)
              end
 
  and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
@@ -1017,7 +983,7 @@
                  (r := SOME c1All;
                   [])
 
-           | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
+           | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
              (unifyKinds dom1 dom2;
               unifyKinds ran1 ran2;
               [])
@@ -2740,7 +2706,7 @@ fun positive self =
 
               | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
               | CConcat (c1, c2) => none c1 andalso none c2
-              | CFold => true
+              | CMap => true
 
               | CUnit => true
 
@@ -2766,7 +2732,7 @@ fun positive self =
 
               | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
               | CConcat (c1, c2) => pos c1 andalso pos c2
-              | CFold => true
+              | CMap => true
 
               | CUnit => true
 
diff --git a/src/elisp/urweb-defs.el b/src/elisp/urweb-defs.el
index 5551b7a2..e1382692 100644
--- a/src/elisp/urweb-defs.el
+++ b/src/elisp/urweb-defs.el
@@ -107,7 +107,7 @@ notion of \"the end of an outline\".")
                  "if" "then" "else" "case" "of" "fn" "fun" "val" "and"
                  "datatype" "type" "open" "include"
                  urweb-module-head-syms
-                 "con" "fold" "where" "extern" "constraint" "constraints"
+                 "con" "map" "where" "extern" "constraint" "constraints"
                  "table" "sequence" "class" "cookie")
   "Symbols starting an sexp.")
 
@@ -192,7 +192,7 @@ for all symbols and in all lines starting with the given symbol."
   "The starters of new expressions.")
 
 (defconst urweb-exptrail-syms
-  '("if" "then" "else" "case" "of" "fn" "with" "fold"))
+  '("if" "then" "else" "case" "of" "fn" "with" "map"))
 
 (defconst urweb-pipeheads
    '("|" "of" "fun" "fn" "and" "datatype")
diff --git a/src/elisp/urweb-mode.el b/src/elisp/urweb-mode.el
index 223006fc..e7615cc3 100644
--- a/src/elisp/urweb-mode.el
+++ b/src/elisp/urweb-mode.el
@@ -133,7 +133,7 @@ See doc for the variable `urweb-mode-info'."
 
 (defconst urweb-keywords-regexp
   (urweb-syms-re "and" "case" "class" "con" "constraint" "constraints"
-	       "datatype" "else" "end" "extern" "fn" "fold"
+	       "datatype" "else" "end" "extern" "fn" "map"
 	       "fun" "functor" "if" "include"
 	       "of" "open" "let" "in"
 	       "rec" "sequence" "sig" "signature" "cookie"
diff --git a/src/expl.sml b/src/expl.sml
index cce0fc22..c0d291b5 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -54,7 +54,7 @@ datatype con' =
 
        | CRecord of kind * (con * con) list
        | CConcat of con * con
-       | CFold of kind * kind
+       | CMap of kind * kind
 
        | CUnit
 
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 2ce0c5e2..7044bfa2 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -149,7 +149,7 @@ fun p_con' par env (c, _) =
                                               string "++",
                                               space,
                                               p_con env c2])
-      | CFold _ => string "fold"
+      | CMap _ => string "map"
       | CUnit => string "()"
 
       | CTuple cs => box [string "(",
diff --git a/src/expl_util.sml b/src/expl_util.sml
index d2073a23..a2b5f2f6 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -145,12 +145,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                          S.map2 (mfc ctx c2,
                               fn c2' =>
                                  (CConcat (c1', c2'), loc)))
-              | CFold (k1, k2) =>
+              | CMap (k1, k2) =>
                 S.bind2 (mfk k1,
                          fn k1' =>
                             S.map2 (mfk k2,
                                     fn k2' =>
-                                       (CFold (k1', k2'), loc)))
+                                       (CMap (k1', k2'), loc)))
 
               | CUnit => S.return2 cAll
 
diff --git a/src/explify.sml b/src/explify.sml
index a10037ef..a4eab0ba 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -63,7 +63,7 @@ fun explifyCon (c, loc) =
 
       | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc)
       | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc)
-      | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc)
+      | L.CMap (dom, ran) => (L'.CMap (explifyKind dom, explifyKind ran), loc)
 
       | L.CUnit => (L'.CUnit, loc)
 
diff --git a/src/monoize.sml b/src/monoize.sml
index 4efa2fea..898d3e61 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -206,7 +206,7 @@ fun monoType env =
 
                   | L.CRecord _ => poly ()
                   | L.CConcat _ => poly ()
-                  | L.CFold _ => poly ()
+                  | L.CMap _ => poly ()
                   | L.CUnit => poly ()
 
                   | L.CTuple _ => poly ()
diff --git a/src/reduce.sml b/src/reduce.sml
index b428c01f..949b2a6d 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -103,14 +103,13 @@ fun conAndExp (namedC, namedE) =
                         CAbs (_, _, b) =>
                         con (KnownC c2 :: deKnown env) b
 
-                      | CApp ((CApp ((CFold _, _), f), _), i) =>
+                      | CApp ((CMap (dom, ran), _), f) =>
                         (case #1 c2 of
-                             CRecord (_, []) => i
-                           | CRecord (k, (x, c) :: rest) =>
+                             CRecord (_, []) => (CRecord (ran, []), loc)
+                           | CRecord (_, (x, c) :: rest) =>
                              con (deKnown env)
-                                 (CApp ((CApp ((CApp (f, x), loc), c), loc),
-                                        (CApp (c1,
-                                               (CRecord (k, rest), loc)), loc)), loc)
+                                 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
+                                           (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc)
                            | _ => (CApp (c1, c2), loc))                           
 
                       | _ => (CApp (c1, c2), loc)
@@ -130,7 +129,7 @@ fun conAndExp (namedC, namedE) =
                         (CRecord (k, xcs1 @ xcs2), loc)
                       | _ => (CConcat (c1, c2), loc)
                 end
-              | CFold _ => all
+              | CMap _ => all
 
               | CUnit => all
 
diff --git a/src/source.sml b/src/source.sml
index a5c86f66..d70d0f5d 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -60,7 +60,7 @@ datatype con' =
 
        | CRecord of (con * con) list
        | CConcat of con * con
-       | CFold
+       | CMap
 
        | CUnit
 
diff --git a/src/source_print.sml b/src/source_print.sml
index d6568efe..148157c2 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -139,7 +139,7 @@ fun p_con' par (c, _) =
                                               string "++",
                                               space,
                                               p_con c2])
-      | CFold => string "fold"
+      | CMap => string "map"
 
       | CUnit => string "()"
 
diff --git a/src/urweb.grm b/src/urweb.grm
index 5f2c0575..d425caec 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -184,7 +184,7 @@ fun tagIn bt =
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
  | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT
- | CON | LTYPE | VAL | REC | AND | FUN | FOLD | UNIT | KUNIT | CLASS
+ | CON | LTYPE | VAL | REC | AND | FUN | MAP | FOLD | UNIT | KUNIT | CLASS
  | DATATYPE | OF
  | TYPE | NAME
  | ARROW | LARROW | DARROW | STAR | SEMI
@@ -681,7 +681,7 @@ cterm  : LPAREN cexp RPAREN             (#1 cexp, s (LPARENleft, RPARENright))
        | path DOT INT                   (CProj ((CVar path, s (pathleft, pathright)), Int64.toInt INT),
                                          s (pathleft, INTright))
        | UNDER                          (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
-       | FOLD                           (CFold, s (FOLDleft, FOLDright))
+       | MAP                            (CMap, s (MAPleft, MAPright))
        | UNIT                           (CUnit, s (UNITleft, UNITright))
        | LPAREN ctuplev RPAREN          (CTuple ctuplev, s (LPARENleft, RPARENright))
 
diff --git a/src/urweb.lex b/src/urweb.lex
index aef68ad1..29e07194 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -290,6 +290,7 @@ notags = [^<{\n]+;
 <INITIAL> "and"       => (Tokens.AND (pos yypos, pos yypos + size yytext));
 <INITIAL> "fun"       => (Tokens.FUN (pos yypos, pos yypos + size yytext));
 <INITIAL> "fn"        => (Tokens.FN (pos yypos, pos yypos + size yytext));
+<INITIAL> "map"       => (Tokens.MAP (pos yypos, pos yypos + size yytext));
 <INITIAL> "fold"      => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
 <INITIAL> "case"      => (Tokens.CASE (pos yypos, pos yypos + size yytext));
 <INITIAL> "if"        => (Tokens.IF (pos yypos, pos yypos + size yytext));