Add InterpretToPHOAS

2 files changed, 51 insertions, 3 deletions

diff --git a/src/Reflection/Named/InterpretToPHOAS.v b/src/Reflection/Named/InterpretToPHOAS.v
new file mode 100644
index 000000000..94cab3b87
--- /dev/null
+++ b/src/Reflection/Named/InterpretToPHOAS.v
@@ -0,0 +1,50 @@
+Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Reflection.Named.Wf.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Util.PointedProp.
+
+Module Export Named.
+  Section language.
+    Context {base_type_code : Type}
+            {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+            {var : base_type_code -> Type}
+            (base_type_code_beq : base_type_code -> base_type_code -> bool)
+            (base_type_code_bl_transparent : forall x y, base_type_code_beq x y = true -> x = y)
+            {Name}
+            {Context : Context Name var}.
+
+    Fixpoint interpf_to_phoas
+             (ctx : Context)
+             {t} (e : @Named.exprf base_type_code op Name t)
+             {struct e}
+      : prop_of_option (wff ctx e) -> @Syntax.exprf base_type_code op var t
+      := match e in Named.exprf _ _ _ t return prop_of_option (wff ctx e) -> @Syntax.exprf base_type_code op var t with
+         | Named.Var t' x
+           => match lookupb ctx x t' as v return prop_of_option (if v return bool then true else false) -> _ with
+              | Some v => fun _ => Var v
+              | None => fun b => match b : False with end
+              end
+         | 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'))
+         | 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'))
+                       (fun v
+                        => @interpf_to_phoas (extend ctx n v) _ eC (proj2 Hwf' _))
+         end.
+
+    Definition interp_to_phoas
+             (ctx : Context)
+             {t} (e : @Named.expr base_type_code op Name t)
+             (Hwf : wf ctx e)
+      : @Syntax.expr base_type_code op var (domain t -> codomain t)
+      := Abs (fun v => interpf_to_phoas (extend ctx (Abs_name e) v) (invert_Abs e) (Hwf v)).
+  End language.
+End Named.
diff --git a/src/Reflection/Named/Wf.v b/src/Reflection/Named/Wf.v
index 9ae8fb596..07e08f27a 100644
--- a/src/Reflection/Named/Wf.v
+++ b/src/Reflection/Named/Wf.v
@@ -21,9 +21,7 @@ Module Export Named.
          end%option_pointed_prop.
 
     Definition wf (ctx : Context) {t} (e : @expr base_type_code op Name t) : Prop
-      := match e with
-         | Abs src _ n f => forall v, prop_of_option (@wff (extend ctx (t:=src) n v) _ f)
-         end.
+      := forall v, prop_of_option (@wff (extend ctx (Abs_name e) v) _ (invert_Abs e)).
   End language.
 End Named.