Add InterpretToPHOASInterp

2 files changed, 88 insertions, 5 deletions

diff --git a/src/Reflection/Named/InterpretToPHOAS.v b/src/Reflection/Named/InterpretToPHOAS.v
index 978d263d4..3972dbdad 100644
--- a/src/Reflection/Named/InterpretToPHOAS.v
+++ b/src/Reflection/Named/InterpretToPHOAS.v
@@ -3,6 +3,8 @@ Require Import Crypto.Reflection.Named.Wf.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Util.PointedProp.
 
+Local Notation eta_and x := (conj (let (a, b) := x in a) (let (a, b) := x in b)).
+
 Module Export Named.
   Section language.
     Context {base_type_code : Type}
@@ -26,17 +28,17 @@ Module Export Named.
            | Named.TT => fun _ => TT
            | Named.Pair tx ex ty ey
              => fun Hwf : prop_of_option (Named.wff _ _ /\ Named.wff _ _)%option_pointed_prop
-                => let Hwf' := proj1 (prop_of_option_and _ _) Hwf in
-                   Pair (@interpf_to_phoas ctx tx ex (proj1 Hwf')) (@interpf_to_phoas ctx ty ey (proj2 Hwf'))
+                => let (Hwf'1, Hwf'2) := eta_and (proj1 (prop_of_option_and _ _) Hwf) in
+                   Pair (@interpf_to_phoas ctx tx ex Hwf'1) (@interpf_to_phoas ctx ty ey Hwf'2)
            | Named.Op _ _ opc args
              => fun Hwf
                 => Op opc (@interpf_to_phoas ctx _ args Hwf)
            | Named.LetIn _ n ex _ eC
              => fun Hwf : prop_of_option (Named.wff _ _ /\ inject (forall k, prop_of_option (Named.wff _ _)))%option_pointed_prop
-                => let Hwf' := proj1 (prop_of_option_and _ _) Hwf in
-                   LetIn (@interpf_to_phoas ctx _ ex (proj1 Hwf'))
+                => let (Hwf'1, Hwf'2) := eta_and (proj1 (prop_of_option_and _ _) Hwf) in
+                   LetIn (@interpf_to_phoas ctx _ ex Hwf'1)
                          (fun v
-                          => @interpf_to_phoas (extend ctx n v) _ eC (proj2 Hwf' _))
+                          => @interpf_to_phoas (extend ctx n v) _ eC (Hwf'2 _))
            end.
 
       Definition interp_to_phoas
diff --git a/src/Reflection/Named/InterpretToPHOASInterp.v b/src/Reflection/Named/InterpretToPHOASInterp.v
new file mode 100644
index 000000000..1cd0c5494
--- /dev/null
+++ b/src/Reflection/Named/InterpretToPHOASInterp.v
@@ -0,0 +1,81 @@
+Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Reflection.Named.Wf.
+Require Import Crypto.Reflection.Named.ContextDefinitions.
+Require Import Crypto.Reflection.Named.ContextProperties.
+Require Import Crypto.Reflection.Named.InterpretToPHOAS.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Tactics.BreakMatch.
+
+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}.
+
+    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 ctx e Hwf)).
+    Proof.
+      revert dependent ctx; induction e;
+        repeat first [ progress intros
+                     | progress subst
+                     | progress inversion_option
+                     | 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 *
+                     | solve [ eauto | congruence ]
+                     | match goal with
+                       | [ H : forall ctx Hwf', Named.interpf ?e = Some _, Hwf : prop_of_option (Named.wff _ ?e) |- _ ]
+                         => specialize (H _ Hwf)
+                       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 ctx e Hwf) v).
+    Proof.
+      unfold interp, interp_to_phoas, Named.interp; apply interpf_interpf_to_phoas.
+    Qed.
+  End with_context.
+
+  Section all.
+    Context {Context : forall var, @Context base_type_code Name var}
+            {ContextOk : forall var, ContextOk (Context var)}.
+
+    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 ctx e Hwf) v).
+    Proof. apply interp_interp_to_phoas. 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 e Hwf) v).
+    Proof. apply interp_interp_to_phoas. Qed.
+  End all.
+End language.