Add InlineConstAndOpp

4 files changed, 20 insertions, 2 deletions

diff --git a/src/Compilers/Z/Inline.v b/src/Compilers/Z/Inline.v
index 8a8bea98b..df46c0ecf 100644
--- a/src/Compilers/Z/Inline.v
+++ b/src/Compilers/Z/Inline.v
@@ -3,5 +3,8 @@ Require Import Crypto.Compilers.Inline.
 Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Z.Syntax.Util.
 
+Definition InlineConstAndOpp {t} (e : Expr base_type op t) : Expr base_type op t
+  := @InlineConst base_type op (is_const_or_opp) t e.
+
 Definition InlineConst {t} (e : Expr base_type op t) : Expr base_type op t
   := @InlineConst base_type op (is_const) t e.
diff --git a/src/Compilers/Z/InlineInterp.v b/src/Compilers/Z/InlineInterp.v
index b0cd0b8df..46e5064e9 100644
--- a/src/Compilers/Z/InlineInterp.v
+++ b/src/Compilers/Z/InlineInterp.v
@@ -4,8 +4,12 @@ Require Import Crypto.Compilers.InlineInterp.
 Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Z.Inline.
 
+Definition InterpInlineConstAndOpp {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e)
+  : forall x, Interp interp_op (InlineConstAndOpp e) x = Interp interp_op e x
+  := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf.
+
 Definition InterpInlineConst {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e)
   : forall x, Interp interp_op (InlineConst e) x = Interp interp_op e x
   := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf.
 
-Hint Rewrite @InterpInlineConst using solve_wf_side_condition : reflective_interp.
+Hint Rewrite @InterpInlineConstAndOpp @InterpInlineConst using solve_wf_side_condition : reflective_interp.
diff --git a/src/Compilers/Z/InlineWf.v b/src/Compilers/Z/InlineWf.v
index 32b84aa1f..d6b846460 100644
--- a/src/Compilers/Z/InlineWf.v
+++ b/src/Compilers/Z/InlineWf.v
@@ -4,8 +4,12 @@ Require Import Crypto.Compilers.InlineWf.
 Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Z.Inline.
 
+Definition Wf_InlineConstAndOpp {t} (e : Expr base_type op t) (Hwf : Wf e)
+  : Wf (InlineConstAndOpp e)
+  := @Wf_InlineConst _ _ _ t e Hwf.
+
 Definition Wf_InlineConst {t} (e : Expr base_type op t) (Hwf : Wf e)
   : Wf (InlineConst e)
   := @Wf_InlineConst _ _ _ t e Hwf.
 
-Hint Resolve Wf_InlineConst : wf.
+Hint Resolve Wf_InlineConstAndOpp Wf_InlineConst : wf.
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v
index b84a00dee..daf3d65be 100644
--- a/src/Compilers/Z/Syntax/Util.v
+++ b/src/Compilers/Z/Syntax/Util.v
@@ -18,6 +18,13 @@ Definition make_const t : interp_base_type t -> op Unit (Tbase t)
 Definition is_const s d (v : op s d) : bool
   := match v with OpConst _ _ => true | _ => false end.
 Arguments is_const [s d] v.
+Definition is_opp s d (v : op s d) : bool
+  := match v with Opp _ _ => true | _ => false end.
+Arguments is_opp [s d] v.
+Definition is_const_or_opp s d (v : op s d) : bool
+  := (is_const v || is_opp v)%bool.
+Arguments is_const_or_opp [s d] v.
+
 
 Definition cast_back_flat_const {var t f V}
            (v : interp_flat_type interp_base_type (@SmartFlatTypeMap base_type var f t V))