In reassocation, don't reassociate additions

It was serving no purpose, and was messing up the associativity of
balance on sub.  I believe it was originally there because I thought I
had to handle 19 * (a * b + c * d) -> (19 * a) * b + (19 * c) * d, but
this case doesn't show up, and so I never wrote the code to handle it,
but also never removed the code to parse additions into lists (thereby
losing associativity information).

1 files changed, 4 insertions, 31 deletions

diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index b9f57ce1b..2b9e98833 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -6133,21 +6133,6 @@ Module Compilers.
              => [e]
            end.
 
-      Fixpoint to_add_mul_list (e : @expr var type.Z) : list (list (@expr var type.Z))
-        := match e in expr.expr t return list (list (@expr var t)) with
-           | AppIdent s type.Z ident.Z_add (Pair type.Z type.Z x y)
-             => to_add_mul_list x ++ to_add_mul_list y
-           | AppIdent s type.Z ident.Z_mul (Pair type.Z type.Z x y)
-             => [to_mul_list x ++ to_mul_list y]
-           | Var _ _ as e
-           | TT as e
-           | App _ _ _ _ as e
-           | Abs _ _ _ as e
-           | Pair _ _ _ _ as e
-           | AppIdent _ _ _ _ as e
-             => [ [ e ] ]
-           end.
-
       Definition is_small_prim (e : @expr var type.Z) : bool
         := match e with
            | AppIdent _ _ (ident.primitive type.Z v) _
@@ -6157,12 +6142,9 @@ Module Compilers.
       Definition is_not_small_prim (e : @expr var type.Z) : bool
         := negb (is_small_prim e).
 
-      Definition reorder_add_mul_list (ls : list (list (@expr var type.Z)))
-        : list (list (@expr var type.Z))
-        := List.map
-             (fun ls
-              => filter is_not_small_prim ls ++ filter is_small_prim ls)
-             ls.
+      Definition reorder_mul_list (ls : list (@expr var type.Z))
+        : list (@expr var type.Z)
+        := filter is_not_small_prim ls ++ filter is_small_prim ls.
 
       Fixpoint of_mul_list (ls : list (@expr var type.Z)) : @expr var type.Z
         := match ls with
@@ -6173,15 +6155,6 @@ Module Compilers.
              => AppIdent ident.Z_mul (x, of_mul_list xs)
            end.
 
-      Fixpoint of_add_mul_list (ls : list (list (@expr var type.Z))) : @expr var type.Z
-        := match ls with
-           | nil => AppIdent (ident.primitive (t:=type.Z) 0) TT
-           | cons x nil
-             => of_mul_list x
-           | cons x xs
-             => AppIdent ident.Z_add (of_mul_list x, of_add_mul_list xs)
-           end.
-
       Fixpoint reassociate {t} (e : @expr var t) : @expr var t
         := match e in expr.expr t return expr t with
            | Var _ _ as e
@@ -6192,7 +6165,7 @@ Module Compilers.
            | App s d f x => App (@reassociate _ f) (@reassociate _ x)
            | Abs s d f => Abs (fun v => @reassociate _ (f v))
            | AppIdent s type.Z idc args
-             => of_add_mul_list (reorder_add_mul_list (to_add_mul_list (AppIdent idc (@reassociate s args))))
+             => of_mul_list (reorder_mul_list (to_mul_list (AppIdent idc (@reassociate s args))))
            | AppIdent s d idc args
              => AppIdent idc (@reassociate s args)
            end.