# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1226451505 18000
# Node ID 1bbcc3345d127815c24054dd51ca4fa6b3a9f0d7
# Parent  ae03d09043c1241965f6e96b7c608f039789429e
Map distributivity rule in hnormCon

diff -r ae03d09043c1 -r 1bbcc3345d12 src/elab_ops.sml
--- a/src/elab_ops.sml	Tue Nov 11 19:20:37 2008 -0500
+++ b/src/elab_ops.sml	Tue Nov 11 19:58:25 2008 -0500
@@ -150,6 +150,39 @@
                                          | 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') =
@@ -205,16 +238,17 @@
                                                                                      rR := SOME (CError, loc);
                                                                                      fuse (dom, v', r'))
                                                                                 else
-                                                                                    default ()
-                                                                              | _ => default ())
-                                                                         | _ => default ())
-                                                                    | _ => default ()
+                                                                                    tryDistributivity ()
+                                                                              | _ => tryDistributivity ())
+                                                                         | _ => tryDistributivity ())
+                                                                    | _ => tryDistributivity ()
                                                               end
-                                                            | _ => default ())
-                                                       | _ => default ())
-                                                  | _ => default ())
-                                             | _ => default ()
+                                                            | _ => tryDistributivity ())
+                                                       | _ => tryDistributivity ())
+                                                  | _ => tryDistributivity ())
+                                             | _ => tryDistributivity ()
                                        end
+
                                in
                                    (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
                                    case (hnormCon env i, unconstraint c) of
diff -r ae03d09043c1 -r 1bbcc3345d12 src/elab_print.sml
--- a/src/elab_print.sml	Tue Nov 11 19:20:37 2008 -0500
+++ b/src/elab_print.sml	Tue Nov 11 19:58:25 2008 -0500
@@ -335,7 +335,7 @@
                      else
                          box [p_exp' true env e1,
                               space,
-                              string "with",
+                              string "++",
                               space,
                               p_exp' true env e2])
       | ECut (e, c, {field, rest}) =>