1 files changed, 88 insertions, 0 deletions
diff --git a/src/Compilers/Named/InterpretToPHOASInterp.v b/src/Compilers/Named/InterpretToPHOASInterp.v
new file mode 100644
index 000000000..0772721f6
--- /dev/null
+++ b/src/Compilers/Named/InterpretToPHOASInterp.v
@@ -0,0 +1,88 @@
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Wf.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.InterpretToPHOAS.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
+
+Section language.
+  Context {base_type_code : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {Name : Type}
+          {base_type_code_dec : DecidableRel (@eq base_type_code)}
+          {Name_dec : DecidableRel (@eq Name)}
+          {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}.
+  Section with_context.
+    Context {Context : Context Name interp_base_type}
+            {ContextOk : ContextOk Context}
+            (failb : forall t, @Syntax.exprf base_type_code op interp_base_type (Tbase t)).
+
+    Lemma interpf_interpf_to_phoas
+          (ctx : Context)
+          {t} (e : @Named.exprf base_type_code op Name t)
+          (Hwf : prop_of_option (Named.wff ctx e))
+      : Named.interpf (interp_op:=interp_op) (ctx:=ctx) e
+        = Some (Syntax.interpf interp_op (interpf_to_phoas failb ctx e)).
+    Proof using Type.
+      revert dependent ctx; induction e;
+        repeat first [ progress intros
+                     | progress subst
+                     | progress inversion_option
+                     | progress destruct_head' and
+                     | progress break_innermost_match_step
+                     | progress unfold option_map, LetIn.Let_In in *
+                     | apply (f_equal (@Some _))
+                     | apply (f_equal (@interp_op _ _ _))
+                     | progress simpl in *
+                     | progress autorewrite with push_prop_of_option in *
+                     | solve [ eauto | congruence | tauto ]
+                     | match goal with
+                       | [ H : forall ctx Hwf', Named.interpf ?e = Some _, Hwf : prop_of_option (Named.wff _ ?e) |- _ ]
+                         => specialize (H _ Hwf)
+                       | [ H : forall ctx Hwf, Named.interpf ?e = Some _ |- Named.interpf ?e = Some _ ]
+                         => rewrite H by auto
+                       end ].
+    Qed.
+
+    Lemma interp_interp_to_phoas
+          (ctx : Context)
+          {t} (e : @Named.expr base_type_code op Name t)
+          (Hwf : Named.wf ctx e)
+          v
+      : Named.interp (interp_op:=interp_op) (ctx:=ctx) e v
+        = Some (Syntax.interp interp_op (interp_to_phoas failb ctx e) v).
+    Proof using Type.
+      unfold interp, interp_to_phoas, Named.interp; apply interpf_interpf_to_phoas; auto.
+    Qed.
+  End with_context.
+
+  Section all.
+    Context {Context : forall var, @Context base_type_code Name var}
+            {ContextOk : forall var, ContextOk (Context var)}
+            (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)).
+
+    Lemma Interp_InterpToPHOAS_gen
+          {ctx : forall var, Context var}
+          {t} (e : @Named.expr base_type_code op Name t)
+          (Hwf : forall var, Named.wf (ctx var) e)
+          v
+      : Named.interp (interp_op:=interp_op) (ctx:=ctx _) e v
+        = Some (Interp interp_op (InterpToPHOAS_gen failb ctx e) v).
+    Proof using Type. apply interp_interp_to_phoas; auto. Qed.
+
+    Lemma Interp_InterpToPHOAS
+          {t} (e : @Named.expr base_type_code op Name t)
+          (Hwf : Named.Wf Context e)
+          v
+      : Named.interp (Context:=Context _) (interp_op:=interp_op) (ctx:=empty) e v
+        = Some (Interp interp_op (InterpToPHOAS (Context:=Context) failb e) v).
+    Proof using Type. apply interp_interp_to_phoas; auto. Qed.
+  End all.
+End language.