Crud list works

6 files changed, 86 insertions, 45 deletions

diff --git a/lib/basis.urs b/lib/basis.urs
index 8737cbde..e1cb5082 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -251,6 +251,7 @@ val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {
 con xhtml = xml [Html]
 con page = xhtml [] []
 con xbody = xml [Body] [] []
+con xtr = xml [Body, Tr] [] []
 
 (*** HTML details *)
 
diff --git a/src/disjoint.sml b/src/disjoint.sml
index 069d3ec2..5602c8d2 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -199,6 +199,8 @@ fun decomposeRow (env, denv) c =
                           | _ => (Unknown cAll :: acc, gs)
                     end
             in
+                (*Print.prefaces "decomposeRow'" [("c", ElabPrint.p_con env c),
+                                                ("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*)
                 case #1 (#1 (hnormCon (env, denv) c)) of
                     CApp (
                     (CApp (
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 50c95ac7..6c75768b 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -98,36 +98,40 @@ fun hnormCon env (cAll as (c, loc)) =
                                     ("sc", p_con env sc)];*)
                  sc
              end
-           | CApp (c', i) =>
-             (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),
+           | c1' as CApp (c', i) =>
+             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),
+                                                      (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)*)
-                            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
-                          | _ => cAll)
-                     | _ => cAll)
-                | _ => cAll)
-           | _ => cAll)
+                                                          rest''), loc)), loc)
+                               end
+                             | _ => default ())
+                        | _ => default ())
+                   | _ => default ()
+             end
+           | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
 
       | CConcat (c1, c2) =>
         (case (hnormCon env c1, hnormCon env c2) of
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 5109feb4..8564b2dd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -896,17 +896,28 @@ and guessFold (env, denv) (c1, c2, gs, ex) =
     end
 
 and unifyCons' (env, denv) c1 c2 =
-    let
-        val (c1, gs1) = hnormCon (env, denv) c1
-        val (c2, gs2) = hnormCon (env, denv) c2
-    in
+    case (#1 c1, #1 c2) of
+        (L'.TDisjoint (x1, y1, t1), L'.TDisjoint (x2, y2, t2)) =>
         let
-            val gs3 = unifyCons'' (env, denv) c1 c2
+            val gs1 = unifyCons' (env, denv) x1 x2
+            val gs2 = unifyCons' (env, denv) y1 y2
+            val (denv', gs3) = D.assert env denv (x1, y1)
+            val gs4 = unifyCons' (env, denv') t1 t2
         in
-            gs1 @ gs2 @ gs3
+            gs1 @ gs2 @ gs3 @ gs4
+        end
+      | _ =>
+        let
+            val (c1, gs1) = hnormCon (env, denv) c1
+            val (c2, gs2) = hnormCon (env, denv) c2
+        in
+            let
+                val gs3 = unifyCons'' (env, denv) c1 c2
+            in
+                gs1 @ gs2 @ gs3
+            end
+            handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
         end
-        handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
-    end
     
 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
     let
@@ -1116,12 +1127,18 @@ fun foldType (dom, loc) =
                                     (L'.TCFun (L'.Explicit, "v", dom,
                                                (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
                                                           (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
-                                                                    (L'.CApp ((L'.CRel 3, loc),
-                                                                              recCons (dom,
-                                                                                       (L'.CRel 2, loc),
-                                                                                       (L'.CRel 1, loc),
-                                                                                       (L'.CRel 0, loc),
-                                                                                       loc)), loc)), loc)),
+                                                                    (L'.TDisjoint ((L'.CRecord
+                                                                                        ((L'.KUnit, loc),
+                                                                                         [((L'.CRel 2, loc),
+                                                                                           (L'.CUnit, loc))]), loc),
+                                                                                   (L'.CRel 0, loc),
+                                                                                   (L'.CApp ((L'.CRel 3, loc),
+                                                                                             recCons (dom,
+                                                                                                      (L'.CRel 2, loc),
+                                                                                                      (L'.CRel 1, loc),
+                                                                                                      (L'.CRel 0, loc),
+                                                                                                      loc)), loc)),
+                                                                     loc)), loc)),
                                                 loc)), loc)), loc),
                          (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
                                    (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
diff --git a/tests/crud.ur b/tests/crud.ur
index 101b1ba4..6bbcbe1f 100644
--- a/tests/crud.ur
+++ b/tests/crud.ur
@@ -1,3 +1,5 @@
+con colMeta = fn cols :: {Type} => $(Top.mapTT (fn t => {Show : t -> xbody}) cols)
+
 functor Make(M : sig
         con cols :: {Type}
         constraint [Id] ~ cols
@@ -5,7 +7,7 @@ functor Make(M : sig
 
         val title : string
 
-        val cols : $(mapTT (fn t => {Show : t -> xbody}) cols)
+        val cols : $(Top.mapTT (fn t => {Show : t -> xbody}) cols)
 end) = struct
 
 open constraints M
@@ -14,7 +16,20 @@ val tab = M.tab
 fun list () =
         rows <- query (SELECT * FROM tab AS T)
                 (fn fs acc => return <body>
-                        {acc} <tr> <td>{txt _ fs.T.Id}</td> </tr>
+                        {acc}
+                        <tr>
+                                <td>{txt _ fs.T.Id}</td>
+                                {fold [fn cols :: {Type} => $cols -> colMeta cols -> xtr]
+                                        (fn (nm :: Name) (t :: Type) (rest :: {Type}) acc =>
+                                                [[nm] ~ rest] =>
+                                                fn (r : $([nm = t] ++ rest)) cols =>
+                                                <tr>
+                                                        <td>{cols.nm.Show r.nm}</td>
+                                                        {acc (r -- nm) (cols -- nm)}
+                                                </tr>)
+                                        (fn _ _ => <tr></tr>)
+                                        [M.cols] (fs.T -- #Id) M.cols}
+                        </tr>
                 </body>) <body></body>;
         return <html><head>
                 <title>List</title>
diff --git a/tests/crud.urs b/tests/crud.urs
index 5f2ae695..c021bea3 100644
--- a/tests/crud.urs
+++ b/tests/crud.urs
@@ -1,3 +1,5 @@
+con colMeta = fn cols :: {Type} => $(mapTT (fn t => {Show : t -> xbody}) cols)
+
 functor Make(M : sig
         con cols :: {Type}
         constraint [Id] ~ cols
@@ -5,7 +7,7 @@ functor Make(M : sig
 
         val title : string
 
-        val cols : $(mapTT (fn t => {Show : t -> xbody}) cols)
+        val cols : colMeta cols
 end) : sig
         val main : unit -> transaction page
 end