Add InterpEta

It's a version of [Interp] that works even when there are destructuring lets.

2 files changed, 18 insertions, 1 deletions

diff --git a/src/Reflection/Eta.v b/src/Reflection/Eta.v
index eda74f4a5..d40267858 100644
--- a/src/Reflection/Eta.v
+++ b/src/Reflection/Eta.v
@@ -63,3 +63,13 @@ Section language.
   Definition ExprEta' {t} (e : Expr t) : Expr (Arrow (domain t) (codomain t))
     := fun var => expr_eta' (e var).
 End language.
+(* put these outside the section so the argument order lines up with
+   [interp] and [Interp] *)
+Definition interp_eta {base_type_code interp_base_type op} interp_op
+           {t} (e : @expr base_type_code op interp_base_type t)
+  : interp_type interp_base_type t
+  := interp_flat_type_eta (interp interp_op e).
+Definition InterpEta {base_type_code interp_base_type op} interp_op
+           {t} (e : @Expr base_type_code op t)
+  : interp_type interp_base_type t
+  := interp_eta interp_op (e _).
diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v
index 4dd5b00bb..4ab42a63f 100644
--- a/src/Reflection/EtaInterp.v
+++ b/src/Reflection/EtaInterp.v
@@ -93,6 +93,13 @@ Section language.
   Lemma InterpExprEta'_arrow {s d e}
     : forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta' (t:=Arrow s d) e) x = Interp (@interp_op) e x.
   Proof. exact (@InterpExprEta' (Arrow s d) e). Qed.
+
+  Lemma eq_interp_eta {t e}
+    : forall x, interp_eta interp_op (t:=t) e x = interp interp_op e x.
+  Proof. apply eq_interp_flat_type_eta. Qed.
+  Lemma eq_InterpEta {t e}
+    : forall x, InterpEta interp_op (t:=t) e x = Interp interp_op e x.
+  Proof. apply eq_interp_eta. Qed.
 End language.
 
-Hint Rewrite @eq_interp_flat_type_eta @eq_interp_flat_type_eta' @interpf_exprf_eta @interpf_exprf_eta' @interp_expr_eta @interp_expr_eta' @InterpExprEta @InterpExprEta' @InterpExprEta_arrow @InterpExprEta'_arrow : reflective_interp.
+Hint Rewrite @eq_interp_flat_type_eta @eq_interp_flat_type_eta' @interpf_exprf_eta @interpf_exprf_eta' @interp_expr_eta @interp_expr_eta' @InterpExprEta @InterpExprEta' @InterpExprEta_arrow @InterpExprEta'_arrow @eq_interp_eta @eq_InterpEta : reflective_interp.