# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1235250716 18000
# Node ID d64533157f4024e4f88d515dbc97d37fae9ecebd
# Parent  8998114760c145066096261ecb16f951d4aa7e5c
Debug reverse-engineering unification

diff -r 8998114760c1 -r d64533157f40 demo/crud.ur
--- a/demo/crud.ur	Sat Feb 21 15:33:20 2009 -0500
+++ b/demo/crud.ur	Sat Feb 21 16:11:56 2009 -0500
@@ -6,7 +6,7 @@
                  Parse : t_formT.2 -> t_formT.1,
                  Inject : sql_injectable t_formT.1
                  }
-con colsMeta = fn cols :: {(Type * Type)} => $(Top.mapT2T colMeta cols)
+con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols)
 
 fun default (t ::: Type) (sh : show t) (rd : read t) (inj : sql_injectable t)
             name : colMeta (t, string) =
@@ -33,7 +33,7 @@
 functor Make(M : sig
                  con cols :: {(Type * Type)}
                  constraint [Id] ~ cols
-                 val tab : sql_table ([Id = int] ++ mapT2T fstTT cols)
+                 val tab : sql_table ([Id = int] ++ map fstTT cols)
 
                  val title : string
 
@@ -47,7 +47,7 @@
 
     fun list () =
         rows <- queryX (SELECT * FROM tab AS T)
-                       (fn (fs : {T : $([Id = int] ++ mapT2T fstTT M.cols)}) => <xml>
+                       (fn (fs : {T : $([Id = int] ++ map fstTT M.cols)}) => <xml>
                          <tr>
                            <td>{[fs.T.Id]}</td>
                            {foldT2RX2 [fstTT] [colMeta] [tr]
@@ -79,9 +79,9 @@
           <br/><hr/><br/>
 
           <form>
-            {foldT2R [colMeta] [fn cols :: {(Type * Type)} => xml form [] (mapT2T sndTT cols)]
+            {foldT2R [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
                      (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                                      [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (mapT2T sndTT rest)) => <xml>
+                                      [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map sndTT rest)) => <xml>
                                         <li> {cdata col.Nam}: {col.Widget [nm]}</li>
                                         {useMore acc}
                                       </xml>)
@@ -92,11 +92,11 @@
           </form>
         </xml>
 
-    and create (inputs : $(mapT2T sndTT M.cols)) =
+    and create (inputs : $(map sndTT M.cols)) =
         id <- nextval seq;
         dml (insert tab
                     (foldT2R2 [sndTT] [colMeta]
-                              [fn cols => $(mapT2T (fn t :: (Type * Type) =>
+                              [fn cols => $(map (fn t :: (Type * Type) =>
                                                        sql_exp [] [] [] t.1) cols)]
                               (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
                                                [[nm] ~ rest] =>
@@ -112,12 +112,12 @@
 
     and upd (id : int) =
         let
-            fun save (inputs : $(mapT2T sndTT M.cols)) =
-                dml (update [mapT2T fstTT M.cols]
+            fun save (inputs : $(map sndTT M.cols)) =
+                dml (update [map fstTT M.cols]
                             (foldT2R2 [sndTT] [colMeta]
-                                      [fn cols => $(mapT2T (fn t :: (Type * Type) =>
+                                      [fn cols => $(map (fn t :: (Type * Type) =>
                                                                sql_exp [T = [Id = int]
-                                                                                ++ mapT2T fstTT M.cols]
+                                                                                ++ map fstTT M.cols]
                                                                        [] [] t.1) cols)]
                                       (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
                                                        [[nm] ~ rest] =>
@@ -132,14 +132,14 @@
                   {ls}
                 </body></xml>
         in
-            fso <- oneOrNoRows (SELECT tab.{{mapT2T fstTT M.cols}} FROM tab WHERE tab.Id = {[id]});
-            case fso : (Basis.option {Tab : $(mapT2T fstTT M.cols)}) of
+            fso <- oneOrNoRows (SELECT tab.{{map fstTT M.cols}} FROM tab WHERE tab.Id = {[id]});
+            case fso : (Basis.option {Tab : $(map fstTT M.cols)}) of
                 None => return <xml><body>Not found!</body></xml>
               | Some fs => return <xml><body><form>
-                {foldT2R2 [fstTT] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (mapT2T sndTT cols)]
+                {foldT2R2 [fstTT] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
                           (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
                                            [[nm] ~ rest] (v : t.1) (col : colMeta t)
-                                           (acc : xml form [] (mapT2T sndTT rest)) =>
+                                           (acc : xml form [] (map sndTT rest)) =>
                               <xml>
                                 <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
                                 {useMore acc}
diff -r 8998114760c1 -r d64533157f40 demo/crud.urs
--- a/demo/crud.urs	Sat Feb 21 15:33:20 2009 -0500
+++ b/demo/crud.urs	Sat Feb 21 16:11:56 2009 -0500
@@ -6,7 +6,7 @@
                                     -> xml form [] [nm = t_formT.2],
                   Parse : t_formT.2 -> t_formT.1,
                   Inject : sql_injectable t_formT.1}
-con colsMeta = fn cols :: {(Type * Type)} => $(mapT2T colMeta cols)
+con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols)
 
 val int : string -> colMeta (int, string)
 val float : string -> colMeta (float, string)
@@ -16,7 +16,7 @@
 functor Make(M : sig
                  con cols :: {(Type * Type)}
                  constraint [Id] ~ cols
-                 val tab : sql_table ([Id = int] ++ mapT2T fstTT cols)
+                 val tab : sql_table ([Id = int] ++ map fstTT cols)
 
                  val title : string
 
diff -r 8998114760c1 -r d64533157f40 src/elaborate.sml
--- a/src/elaborate.sml	Sat Feb 21 15:33:20 2009 -0500
+++ b/src/elaborate.sml	Sat Feb 21 16:11:56 2009 -0500
@@ -782,7 +782,7 @@
                                  val v' = case dom of
                                               (L'.KUnit, _) => (L'.CUnit, loc)
                                             | _ => cunif (loc, dom)
-                                 val gs2 = unifyCons (env, denv) v' (L'.CApp (f, v), loc)
+                                 val gs2 = unifyCons (env, denv) v (L'.CApp (f, v'), loc)
 
                                  val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc)
                              in
@@ -792,10 +792,10 @@
                              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))
+
+                                 val gs2 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc))
+                                 val gs3 = unfold (r2, (L'.CRecord (ran, rest), loc))
+                                 val gs4 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
                              in
                                  gs1 @ gs2 @ gs3 @ gs4
                              end
@@ -803,10 +803,10 @@
                              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')
+
+                                 val gs2 = unfold (r1, c1')
+                                 val gs3 = unfold (r2, c2')
+                                 val gs4 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
                              in
                                  gs1 @ gs2 @ gs3 @ gs4
                              end
@@ -815,7 +815,7 @@
              in
                  unfold (r, c)
              end
-             handle _ => raise ex
+             handle _ => (TextIO.print "Guess failure!\n"; raise ex)
      in
          case (#1 c1, #1 c2) of
              (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>