From cd05feb59d045f7618dd82ac8a5d3837531c34ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Mon, 28 Mar 2022 12:19:07 -0700 Subject: [PATCH] lib/ExprCompiler: Add support for word.gtu/gts & Z.gt (PLDI AE feedback) --- src/Rupicola/Lib/ExprCompiler.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/Rupicola/Lib/ExprCompiler.v b/src/Rupicola/Lib/ExprCompiler.v index 37ac9533..a5861948 100644 --- a/src/Rupicola/Lib/ExprCompiler.v +++ b/src/Rupicola/Lib/ExprCompiler.v @@ -135,6 +135,12 @@ Section ExprCompiler. Proof. rewrite word.b2w_if; eapply (@expr_compile_word_bop bopname.lts). Qed. Definition expr_compile_word_ltu : DOP bopname.ltu (of_bool (word.ltu w1 w2)). Proof. rewrite word.b2w_if; eapply (@expr_compile_word_bop bopname.ltu). Qed. + + Definition expr_compile_word_gts : DOP bopname.lts (of_bool (word.gts w2 w1)). + Proof. apply expr_compile_word_lts. Qed. + Definition expr_compile_word_gtu : DOP bopname.ltu (of_bool (word.gtu w2 w1)). + Proof. apply expr_compile_word_ltu. Qed. + Definition expr_compile_word_eqb : DOP bopname.eq (of_bool (word.eqb w1 w2)). Proof. rewrite word.b2w_if; eapply (@expr_compile_word_bop bopname.eq). Qed. @@ -180,6 +186,7 @@ Section ExprCompiler. Lemma expr_compile_Z_eqb (h: (ub z1 /\ ub z2) \/ (sb z1 /\ sb z2)) : DOP bopname.eq (of_bool (Z.eqb z1 z2)). Proof. rewrite <- word_morph_eqb; eauto using expr_compile_word_eqb. Qed. + Lemma expr_compile_Z_ltb_u (h1: ub z1) (h2: ub z2) : DOP bopname.ltu (of_bool (Z.ltb z1 z2)). Proof. rewrite word.morph_ltu; eauto using expr_compile_word_ltu. Qed. @@ -187,6 +194,13 @@ Section ExprCompiler. DOP bopname.lts (of_bool (Z.ltb z1 z2)). Proof. rewrite word.morph_lts; eauto using expr_compile_word_lts. Qed. + Lemma expr_compile_Z_gtb_u (h1: ub z1) (h2: ub z2) : + DOP bopname.ltu (of_bool (Z.gtb z2 z1)). + Proof. rewrite Z.gtb_ltb; auto using expr_compile_Z_ltb_u. Qed. + Lemma expr_compile_Z_gtb_s (h1: sb z1) (h2: sb z2) : + DOP bopname.lts (of_bool (Z.gtb z2 z1)). + Proof. rewrite Z.gtb_ltb; auto using expr_compile_Z_ltb_s. Qed. + Lemma expr_compile_Z_lnot : DX (expr.op bopname.xor e1 (expr.literal (-1))) (to_w (Z.lnot z1)). Proof. rewrite word.morph_not; eauto using expr_compile_word_not. Qed. @@ -460,6 +474,10 @@ Notation DPAT p := (DEXPR _ _ _ p) (only parsing). simple eapply expr_compile_word_lts; shelve : expr_compiler. #[export] Hint Extern 5 (DPAT (of_bool (word.ltu _ _))) => simple eapply expr_compile_word_ltu; shelve : expr_compiler. +#[export] Hint Extern 5 (DPAT (of_bool (word.gts _ _))) => + simple eapply expr_compile_word_gts; shelve : expr_compiler. +#[export] Hint Extern 5 (DPAT (of_bool (word.gtu _ _))) => + simple eapply expr_compile_word_gtu; shelve : expr_compiler. #[export] Hint Extern 5 (DPAT (of_bool (word.eqb _ _))) => simple eapply expr_compile_word_eqb; shelve : expr_compiler. @@ -501,6 +519,11 @@ Notation DPAT p := (DEXPR _ _ _ p) (only parsing). simple eapply expr_compile_Z_ltb_u; [ shelve.. | | ] : expr_compiler. #[export] Hint Extern 5 (DPAT (of_bool (Z.ltb _ _))) => simple eapply expr_compile_Z_ltb_s; [ shelve.. | | ] : expr_compiler. +(* Don't shelve side conditions for these two either *) +#[export] Hint Extern 5 (DPAT (of_bool (Z.gtb _ _))) => + simple eapply expr_compile_Z_gtb_u; [ shelve.. | | ] : expr_compiler. +#[export] Hint Extern 5 (DPAT (of_bool (Z.gtb _ _))) => + simple eapply expr_compile_Z_gtb_s; [ shelve.. | | ] : expr_compiler. #[export] Hint Extern 5 (DPAT (of_Z (Z.b2z _))) => simple eapply expr_compile_Z_b2z : expr_compiler.