3 files changed, 38 insertions, 0 deletions
diff --git a/src/Compilers/Z/InlineConstAndOpByRewrite.v b/src/Compilers/Z/InlineConstAndOpByRewrite.v
new file mode 100644
index 000000000..f4403e12b
--- /dev/null
+++ b/src/Compilers/Z/InlineConstAndOpByRewrite.v
@@ -0,0 +1,13 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InlineConstAndOpByRewrite.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+
+Module Export Rewrite.
+  Definition inline_const_and_opf {var} {t} (e : exprf _ _ t) : @exprf base_type op var t
+    := @inline_const_and_opf base_type op interp_base_type (@interp_op) var make_const t e.
+  Definition inline_const_and_op {var} {t} (e : expr _ _ t) : @expr base_type op var t
+    := @inline_const_and_op base_type op interp_base_type (@interp_op) var make_const t e.
+  Definition InlineConstAndOp {t} (e : Expr t) : Expr t
+    := @InlineConstAndOp base_type op interp_base_type interp_op make_const t e.
+End Rewrite.
diff --git a/src/Compilers/Z/InlineConstAndOpByRewriteInterp.v b/src/Compilers/Z/InlineConstAndOpByRewriteInterp.v
new file mode 100644
index 000000000..e67442c71
--- /dev/null
+++ b/src/Compilers/Z/InlineConstAndOpByRewriteInterp.v
@@ -0,0 +1,12 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InlineConstAndOpByRewriteInterp.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.InlineConstAndOpByRewrite.
+
+Module Export Rewrite.
+  Definition InterpInlineConstAndOp {t} (e : Expr t)
+  : forall x, Interp (InlineConstAndOp e) x = Interp e x
+    := @InterpInlineConstAndOp _ _ _ _ _ t e Syntax.Util.make_const_correct.
+
+  Hint Rewrite @InterpInlineConstAndOp : reflective_interp.
+End Rewrite.
diff --git a/src/Compilers/Z/InlineConstAndOpByRewriteWf.v b/src/Compilers/Z/InlineConstAndOpByRewriteWf.v
new file mode 100644
index 000000000..aa883f5e7
--- /dev/null
+++ b/src/Compilers/Z/InlineConstAndOpByRewriteWf.v
@@ -0,0 +1,13 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.InlineConstAndOpByRewriteWf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.InlineConstAndOpByRewrite.
+
+Module Export Rewrite.
+  Definition Wf_InlineConstAndOp {t} (e : Expr t) (Hwf : Wf e)
+  : Wf (InlineConstAndOp e)
+    := @Wf_InlineConstAndOp _ _ _ _ _ t e Hwf.
+
+  Hint Resolve Wf_InlineConstAndOp : wf.
+End Rewrite.