diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/Z/ArithmeticSimplifier.v | 34 | ||||
-rw-r--r-- | src/Compilers/Z/ArithmeticSimplifierInterp.v | 5 |
2 files changed, 37 insertions, 2 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v index 8f63e815b..a1775011d 100644 --- a/src/Compilers/Z/ArithmeticSimplifier.v +++ b/src/Compilers/Z/ArithmeticSimplifier.v @@ -48,6 +48,19 @@ Section language. end end. + Fixpoint uninterp_expr_or_const {t} : interp_flat_type inverted_expr t -> exprf (var:=var) t + := match t with + | Tbase T => fun e => match e with + | const_of v => Op (OpConst v) TT + | gen_expr e => e + | neg_expr e => Op (Opp _ _) e + end + | Unit => fun _ => TT + | Prod A B => fun (ab : interp_flat_type _ A * interp_flat_type _ B) + => Pair (@uninterp_expr_or_const A (fst ab)) + (@uninterp_expr_or_const B (snd ab)) + end. + Definition simplify_op_expr {src dst} (opc : op src dst) : exprf (var:=var) src -> exprf (var:=var) dst := match opc in op src dst return exprf src -> exprf dst with @@ -177,6 +190,27 @@ Section language. | _ => Op opc args end + | Zselect TZ TZ TZ TZ as opc + => fun args + => match interp_as_expr_or_const args with + | Some (const_of c, x, y) + => match (c =? 0)%Z, x, y with + | true, const_of c, _ + | false, _, const_of c + => Op (OpConst c) TT + | true, gen_expr e, _ + | false, _, gen_expr e + => e + | true, neg_expr e, _ + | false, _, neg_expr e + => Op (Opp TZ TZ) e + end + | Some (neg_expr e, x, y) + => let x := uninterp_expr_or_const (t:=Tbase _) x in + let y := uninterp_expr_or_const (t:=Tbase _) y in + Op (Zselect TZ TZ TZ TZ) (e, x, y)%expr + | _ => Op opc args + end | AddWithCarry TZ TZ TZ TZ as opc => fun args => if convert_adc_to_sbb diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v index 3dc11aa9e..6db34f1b8 100644 --- a/src/Compilers/Z/ArithmeticSimplifierInterp.v +++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v @@ -151,7 +151,7 @@ Proof. apply InterpRewriteOp; intros; unfold simplify_op_expr. break_innermost_match; repeat first [ fin_t - | progress cbv [LetIn.Let_In] + | progress cbv [LetIn.Let_In Z.zselect] | progress simpl in * | progress subst | progress subst_prod @@ -162,7 +162,8 @@ Proof. | progress Z.ltb_to_lt | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r | rewrite !Z.sub_with_borrow_to_add_get_carry - | progress autorewrite with zsimplify_fast ]. + | progress autorewrite with zsimplify_fast + | break_innermost_match_step ]. Qed. Hint Rewrite @InterpSimplifyArith : reflective_interp. |