diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-14 00:47:16 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-14 00:47:16 -0400 |
| commit | 1f50e0bd9c8dd9efcbff2770b4da790cd0e28c69 (patch) | |
| tree | 4703473233ebf0b77593cd7a6f39780f6e7636e3 /src/Compilers/Z | |
| parent | d5bfa641ac3269b90bf8fd23511d110b99b3f5fb (diff) | |
Add constant-pushing IdWithAlt optimization
Diffstat (limited to 'src/Compilers/Z')
| -rw-r--r-- | src/Compilers/Z/ArithmeticSimplifier.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v index cfa7934ad..f96b6cec6 100644 --- a/src/Compilers/Z/ArithmeticSimplifier.v +++ b/src/Compilers/Z/ArithmeticSimplifier.v @@ -1,6 +1,7 @@ (** * SimplifyArith: Remove things like (_ * 1), (_ + 0), etc *) Require Import Coq.ZArith.ZArith. Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.ExprInversion. Require Import Crypto.Compilers.Rewriter. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Syntax.Equality. @@ -228,6 +229,36 @@ Section language. | None => Op opc args end + | IdWithAlt TZ TZ TZ as opc + => fun args + => match interp_as_expr_or_const args with + | Some (gen_expr e1, gen_expr e2) + => match invert_Op e1, invert_Op e2 with + | Some (existT _ (Add TZ TZ TZ as opc1, args1)), + Some (existT _ (Add TZ TZ TZ as opc2, args2)) + | Some (existT _ (Sub TZ TZ TZ as opc1, args1)), + Some (existT _ (Sub TZ TZ TZ as opc2, args2)) + | Some (existT _ (Mul TZ TZ TZ as opc1, args1)), + Some (existT _ (Mul TZ TZ TZ as opc2, args2)) + => match interp_as_expr_or_const args1, interp_as_expr_or_const args2 with + | Some (gen_expr e1, const_of c1), + Some (gen_expr e2, const_of c2) + => if Z.eqb c1 c2 + then Op opc1 (Op opc (e1, e2), Op (OpConst c1) TT)%expr + else Op opc args + | _, _ + => Op opc args + end + | _, _ + => Op opc args + end + | Some (neg_expr e1, neg_expr e2) + => Op (Opp _ _) (Op opc (e1, e2)%expr) + | Some (const_of c1, const_of c2) + => Op (OpConst c1) TT + | _ + => Op opc args + end | Zselect TZ TZ TZ TZ as opc => fun args => match interp_as_expr_or_const args with |