Add InlineConstAndOpByRewrite

3 files changed, 40 insertions, 0 deletions

diff --git a/src/Compilers/ZExtended/InlineConstAndOpByRewrite.v b/src/Compilers/ZExtended/InlineConstAndOpByRewrite.v
new file mode 100644
index 000000000..418a0e0f3
--- /dev/null
+++ b/src/Compilers/ZExtended/InlineConstAndOpByRewrite.v
@@ -0,0 +1,12 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InlineConstAndOpByRewrite.
+Require Import Crypto.Compilers.ZExtended.Syntax.
+
+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 (@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 (@Const) t e.
+  Definition InlineConstAndOp {t} (e : Expr t) : Expr t
+    := @InlineConstAndOp base_type op interp_base_type (@interp_op) (@Const) t e.
+End Rewrite.
diff --git a/src/Compilers/ZExtended/InlineConstAndOpByRewriteInterp.v b/src/Compilers/ZExtended/InlineConstAndOpByRewriteInterp.v
new file mode 100644
index 000000000..64d5263a7
--- /dev/null
+++ b/src/Compilers/ZExtended/InlineConstAndOpByRewriteInterp.v
@@ -0,0 +1,15 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InlineConstAndOpByRewriteInterp.
+Require Import Crypto.Compilers.ZExtended.Syntax.
+Require Import Crypto.Compilers.ZExtended.InlineConstAndOpByRewrite.
+
+Module Export Rewrite.
+  Lemma InterpInlineConstAndOp {t} (e : Expr t)
+  : forall x, Interp (InlineConstAndOp e) x = Interp e x.
+  Proof.
+    refine (@InterpInlineConstAndOp _ _ _ _ _ t e _).
+    clear; abstract (intros []; intros; reflexivity).
+  Defined.
+
+  Hint Rewrite @InterpInlineConstAndOp : reflective_interp.
+End Rewrite.
diff --git a/src/Compilers/ZExtended/InlineConstAndOpByRewriteWf.v b/src/Compilers/ZExtended/InlineConstAndOpByRewriteWf.v
new file mode 100644
index 000000000..281bee6ab
--- /dev/null
+++ b/src/Compilers/ZExtended/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.ZExtended.Syntax.
+Require Import Crypto.Compilers.ZExtended.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.