From 2882da783bf4a45cbdab2ff53d6acaea74c71f22 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 2 Apr 2017 00:18:29 -0400
Subject: Add reflective_interp rewrite db

---
 src/Reflection/EtaInterp.v                    | 2 ++
 src/Reflection/InlineCastInterp.v             | 2 ++
 src/Reflection/InlineInterp.v                 | 2 ++
 src/Reflection/InterpProofs.v                 | 3 +++
 src/Reflection/LinearizeInterp.v              | 3 +++
 src/Reflection/RewriterInterp.v               | 2 ++
 src/Reflection/SmartCastInterp.v              | 2 ++
 src/Reflection/Z/ArithmeticSimplifierInterp.v | 2 ++
 8 files changed, 18 insertions(+)

(limited to 'src')

diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v
index 170056a02..4dd5b00bb 100644
--- a/src/Reflection/EtaInterp.v
+++ b/src/Reflection/EtaInterp.v
@@ -94,3 +94,5 @@ Section language.
     : 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.
 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.
diff --git a/src/Reflection/InlineCastInterp.v b/src/Reflection/InlineCastInterp.v
index 8e6719f0c..aa9fbb119 100644
--- a/src/Reflection/InlineCastInterp.v
+++ b/src/Reflection/InlineCastInterp.v
@@ -111,3 +111,5 @@ Section language.
       = Interp interp_op e x.
   Proof. apply InterpInlineConstGen; auto. Qed.
 End language.
+
+Hint Rewrite @interpf_exprf_of_push_cast @InterpInlineCast using solve [ eassumption | eauto with wf ] : reflective_interp.
diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v
index 7d3909c79..caf1931fb 100644
--- a/src/Reflection/InlineInterp.v
+++ b/src/Reflection/InlineInterp.v
@@ -130,3 +130,5 @@ Section language.
     eapply InterpInlineConstGen; eauto.
   Qed.
 End language.
+
+Hint Rewrite @InterpInlineConst @interp_inline_const @interpf_inline_constf using solve [ eassumption | eauto with wf ] : reflective_interp.
diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v
index b0aa20ccf..a9ecdd674 100644
--- a/src/Reflection/InterpProofs.v
+++ b/src/Reflection/InterpProofs.v
@@ -60,3 +60,6 @@ Section language.
     subst; eapply interpf_SmartVarVarf; eassumption.
   Qed.
 End language.
+
+Hint Rewrite @interpf_LetIn @interpf_SmartVarf : reflective_interp.
+Hint Rewrite @interpf_SmartVarVarf using assumption : reflective_interp.
diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v
index e124ced5b..443cb9e3c 100644
--- a/src/Reflection/LinearizeInterp.v
+++ b/src/Reflection/LinearizeInterp.v
@@ -81,3 +81,6 @@ Section language.
     eapply interp_linearize.
   Qed.
 End language.
+
+Hint Rewrite @interpf_under_letsf : reflective_interp.
+Hint Rewrite @InterpLinearize @interp_linearize @interpf_linearizef using solve [ eassumption | eauto with wf ] : reflective_interp.
diff --git a/src/Reflection/RewriterInterp.v b/src/Reflection/RewriterInterp.v
index 4de516dfd..66315ec0d 100644
--- a/src/Reflection/RewriterInterp.v
+++ b/src/Reflection/RewriterInterp.v
@@ -46,3 +46,5 @@ Section language.
     apply interp_rewrite_op; assumption.
   Qed.
 End language.
+
+Hint Rewrite @InterpRewriteOp using assumption : reflective_interp.
diff --git a/src/Reflection/SmartCastInterp.v b/src/Reflection/SmartCastInterp.v
index 4266deb8a..410d108e3 100644
--- a/src/Reflection/SmartCastInterp.v
+++ b/src/Reflection/SmartCastInterp.v
@@ -33,3 +33,5 @@ Section language.
     { reflexivity. }
   Qed.
 End language.
+
+Hint Rewrite @interpf_SmartCast_base using solve [ eassumption | eauto ] : reflective_interp.
diff --git a/src/Reflection/Z/ArithmeticSimplifierInterp.v b/src/Reflection/Z/ArithmeticSimplifierInterp.v
index 271cbcacc..927f904b7 100644
--- a/src/Reflection/Z/ArithmeticSimplifierInterp.v
+++ b/src/Reflection/Z/ArithmeticSimplifierInterp.v
@@ -98,3 +98,5 @@ Proof.
                  | progress Z.ltb_to_lt
                  | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r ].
 Qed.
+
+Hint Rewrite @InterpSimplifyArith : reflective_interp.
-- 
cgit v1.2.3