Add ZExtended/InlineConstAndOp.v

4 files changed, 32 insertions, 1 deletions

diff --git a/src/Compilers/ZExtended/InlineConstAndOp.v b/src/Compilers/ZExtended/InlineConstAndOp.v
new file mode 100644
index 000000000..f12f273c9
--- /dev/null
+++ b/src/Compilers/ZExtended/InlineConstAndOp.v
@@ -0,0 +1,6 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InlineConstAndOp.
+Require Import Crypto.Compilers.ZExtended.Syntax.
+
+Definition InlineConstAndOp {t} (e : Expr t) : Expr t
+  := @InlineConstAndOp base_type op interp_base_type (@interp_op) (@Const) t e.
diff --git a/src/Compilers/ZExtended/InlineConstAndOpInterp.v b/src/Compilers/ZExtended/InlineConstAndOpInterp.v
new file mode 100644
index 000000000..3f1a83f3d
--- /dev/null
+++ b/src/Compilers/ZExtended/InlineConstAndOpInterp.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.InlineConstAndOpInterp.
+Require Import Crypto.Compilers.ZExtended.Syntax.
+Require Import Crypto.Compilers.ZExtended.InlineConstAndOp.
+
+Definition InterpInlineConstAndOp {t} (e : Expr t) (Hwf : Wf e)
+  : forall x, Interp (InlineConstAndOp e) x = Interp e x.
+Proof.
+  refine (@InterpInlineConstAndOp _ _ _ _ _ t e Hwf _).
+  clear; abstract (intros []; intros; reflexivity).
+Defined.
+
+Hint Rewrite @InterpInlineConstAndOp using solve_wf_side_condition : reflective_interp.
diff --git a/src/Compilers/ZExtended/InlineConstAndOpWf.v b/src/Compilers/ZExtended/InlineConstAndOpWf.v
new file mode 100644
index 000000000..3ce24e237
--- /dev/null
+++ b/src/Compilers/ZExtended/InlineConstAndOpWf.v
@@ -0,0 +1,11 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.InlineConstAndOpWf.
+Require Import Crypto.Compilers.ZExtended.Syntax.
+Require Import Crypto.Compilers.ZExtended.InlineConstAndOp.
+
+Definition Wf_InlineConstAndOp {t} (e : Expr t) (Hwf : Wf e)
+  : Wf (InlineConstAndOp e)
+  := @Wf_InlineConstAndOp _ _ _ _ _ t e Hwf.
+
+Hint Resolve Wf_InlineConstAndOp : wf.
diff --git a/src/Compilers/ZExtended/Syntax.v b/src/Compilers/ZExtended/Syntax.v
index 3d92e7b4e..5f6d5b3eb 100644
--- a/src/Compilers/ZExtended/Syntax.v
+++ b/src/Compilers/ZExtended/Syntax.v
@@ -74,4 +74,4 @@ Definition interp_op {s d} (opv : op s d) : interp_flat_type interp_base_type s
      end.
 
 Notation Expr := (Expr base_type op).
-Notation Interp := (Interp interp_op).
+Notation Interp := (Interp (@interp_op)).