diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Named/InterpretToPHOAS.v | 12 | ||||
-rw-r--r-- | src/Reflection/Named/InterpretToPHOASInterp.v | 81 |
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. |