1 files changed, 37 insertions, 0 deletions
diff --git a/src/Compilers/SmartCastInterp.v b/src/Compilers/SmartCastInterp.v
new file mode 100644
index 000000000..e755cd168
--- /dev/null
+++ b/src/Compilers/SmartCastInterp.v
@@ -0,0 +1,37 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.SmartCast.
+Require Import Crypto.Util.Notations.
+
+Local Open Scope expr_scope.
+Local Open Scope ctype_scope.
+Section language.
+  Context {base_type_code : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {interp_base_type : base_type_code -> Type}
+          {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}
+          {base_type_beq : base_type_code -> base_type_code -> bool}
+          {base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y}
+          {Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')}
+          (interpf_Cast_id : forall A x, interpf interp_op (Cast _ A A x) = interpf interp_op x)
+          {cast_val : forall A A', interp_base_type A -> interp_base_type A'}
+          (interpf_cast : forall A A' e, interpf interp_op (Cast _ A A' e) = cast_val A A' (interpf interp_op e)).
+
+  Local Notation exprf := (@exprf base_type_code op).
+  Local Notation SmartCast_base := (@SmartCast_base _ _ _ base_type_bl_transparent Cast).
+  Local Notation SmartCast := (@SmartCast _ _ _ base_type_bl_transparent Cast).
+
+  Lemma interpf_SmartCast_base {A A'} (x : exprf (Tbase A))
+    : interpf interp_op (SmartCast_base x) = interpf interp_op (Cast _ A A' x).
+  Proof using interpf_Cast_id.
+    clear dependent cast_val.
+    unfold SmartCast_base.
+    destruct (Sumbool.sumbool_of_bool (base_type_beq A A')) as [H|H].
+    { destruct (base_type_bl_transparent A A' H).
+      rewrite interpf_Cast_id; reflexivity. }
+    { reflexivity. }
+  Qed.
+End language.
+
+Hint Rewrite @interpf_SmartCast_base using solve [ eassumption | eauto ] : reflective_interp.