diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-19 18:56:45 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-05-20 10:58:45 -0400 |
| commit | 5fbdcbf7d22ef36537a11f630d05a33abf3ac9fc (patch) | |
| tree | 03ef6e91f8b5545f917eadf53cb28b8557f3dce8 /src/Compilers/Z/ArithmeticSimplifierWf.v | |
| parent | 8dc27e30c257afb20f540914fd436787f43f5055 (diff) | |
Get sbb conversion working in the pipeline
After | File Name | Before || Change
--------------------------------------------------------------------------------
4m56.46s | Total | 4m54.81s || +0m01.64s
--------------------------------------------------------------------------------
2m19.22s | Specific/IntegrationTestLadderstep | 2m18.29s || +0m00.93s
0m53.92s | Specific/IntegrationTestLadderstep130 | 0m53.83s || +0m00.09s
0m26.24s | Compilers/Z/ArithmeticSimplifierWf | 0m25.65s || +0m00.58s
0m24.93s | Compilers/Z/ArithmeticSimplifierInterp | 0m24.87s || +0m00.05s
0m15.38s | Specific/IntegrationTestFreeze | 0m15.97s || -0m00.58s
0m11.83s | Specific/IntegrationTestMul | 0m11.82s || +0m00.00s
0m10.57s | Specific/IntegrationTestSub | 0m10.50s || +0m00.07s
0m09.18s | Specific/IntegrationTestSquare | 0m09.07s || +0m00.10s
0m02.80s | Compilers/Z/Bounds/Pipeline/Definition | 0m02.57s || +0m00.23s
0m00.78s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.64s || +0m00.14s
0m00.64s | Compilers/Z/ArithmeticSimplifier | 0m00.66s || -0m00.02s
0m00.62s | Compilers/Z/Bounds/Pipeline | 0m00.59s || +0m00.03s
0m00.35s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.36s || -0m00.01s
Diffstat (limited to 'src/Compilers/Z/ArithmeticSimplifierWf.v')
| -rw-r--r-- | src/Compilers/Z/ArithmeticSimplifierWf.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v index ff5068b89..ba5dd39cd 100644 --- a/src/Compilers/Z/ArithmeticSimplifierWf.v +++ b/src/Compilers/Z/ArithmeticSimplifierWf.v @@ -220,9 +220,9 @@ Local Ltac pose_wff_prod3 := => pose proof (wff_interp_as_expr_or_const_prod3_base Hwf H1 H2); clear H1 H2 end. -Lemma Wf_SimplifyArith {t} (e : Expr t) +Lemma Wf_SimplifyArith {convert_adc_to_sbb} {t} (e : Expr t) (Hwf : Wf e) - : Wf (SimplifyArith e). + : Wf (SimplifyArith convert_adc_to_sbb e). Proof. apply Wf_RewriteOp; [ | assumption ]. intros ???????? Hwf'; unfold simplify_op_expr; |