From 58dd754b868011a929b77c21814644fb3cded52e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 17 Mar 2017 14:57:43 -0400 Subject: Don't pass a wf proof into InterpToPHOAS Use a fail-value instead. This makes it easier to compose with other transformations. --- src/Reflection/Named/InterpretToPHOAS.v | 47 +++++++++++++-------------- src/Reflection/Named/InterpretToPHOASInterp.v | 27 +++++++++------ src/Reflection/Named/InterpretToPHOASWf.v | 38 +++++++++++----------- 3 files changed, 59 insertions(+), 53 deletions(-) diff --git a/src/Reflection/Named/InterpretToPHOAS.v b/src/Reflection/Named/InterpretToPHOAS.v index 3972dbdad..a9a44a93f 100644 --- a/src/Reflection/Named/InterpretToPHOAS.v +++ b/src/Reflection/Named/InterpretToPHOAS.v @@ -1,5 +1,6 @@ Require Import Crypto.Reflection.Named.Syntax. Require Import Crypto.Reflection.Named.Wf. +Require Import Crypto.Reflection.SmartMap. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Util.PointedProp. @@ -12,54 +13,52 @@ Module Export Named. {Name : Type}. Section with_var. Context {var : base_type_code -> Type} - {Context : Context Name var}. + {Context : Context Name var} + (failb : forall t, @Syntax.exprf base_type_code op var (Tbase t)). + + Local Notation failf t (* : @Syntax.exprf base_type_code op var t*) + := (SmartPairf (SmartValf _ failb t)). 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 + : @Syntax.exprf base_type_code op var t + := match e in Named.exprf _ _ _ t return @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 + => match lookupb ctx x t' with + | Some v => Var v + | None => failf _ end - | Named.TT => fun _ => TT + | Named.TT => TT | Named.Pair tx ex ty ey - => fun Hwf : prop_of_option (Named.wff _ _ /\ Named.wff _ _)%option_pointed_prop - => 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) + => Pair (@interpf_to_phoas ctx tx ex) (@interpf_to_phoas ctx ty ey) | Named.Op _ _ opc args - => fun Hwf - => Op opc (@interpf_to_phoas ctx _ args Hwf) + => Op opc (@interpf_to_phoas ctx _ args) | 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'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 (Hwf'2 _)) + => LetIn (@interpf_to_phoas ctx _ ex) + (fun v + => @interpf_to_phoas (extend ctx n v) _ eC) 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)). + := Abs (fun v => interpf_to_phoas (extend ctx (Abs_name e) v) (invert_Abs e)). End with_var. Section all. - Context {Context : forall var, @Context base_type_code Name var}. + Context {Context : forall var, @Context base_type_code Name var} + (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)). Definition InterpToPHOAS_gen (ctx : forall var, Context var) {t} (e : @Named.expr base_type_code op Name t) - (Hwf : forall var, wf (ctx var) e) : @Syntax.Expr base_type_code op (domain t -> codomain t) - := fun var => interp_to_phoas (ctx var) e (Hwf var). + := fun var => interp_to_phoas (failb var) (ctx var) e. - Definition InterpToPHOAS {t} e (Hwf : forall var, wf empty e) - := @InterpToPHOAS_gen (fun var => empty) t e Hwf. + Definition InterpToPHOAS {t} e + := @InterpToPHOAS_gen (fun var => empty) t e. End all. End language. End Named. diff --git a/src/Reflection/Named/InterpretToPHOASInterp.v b/src/Reflection/Named/InterpretToPHOASInterp.v index 1cd0c5494..7dcdc198b 100644 --- a/src/Reflection/Named/InterpretToPHOASInterp.v +++ b/src/Reflection/Named/InterpretToPHOASInterp.v @@ -9,6 +9,7 @@ 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} @@ -20,28 +21,33 @@ Section language. {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}. + {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 ctx e Hwf)). + = Some (Syntax.interpf interp_op (interpf_to_phoas failb ctx e)). Proof. 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 * - | solve [ eauto | congruence ] + | 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. @@ -51,15 +57,16 @@ Section language. (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). + = Some (Syntax.interp interp_op (interp_to_phoas failb ctx e) v). Proof. - unfold interp, interp_to_phoas, Named.interp; apply interpf_interpf_to_phoas. + 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)}. + {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} @@ -67,15 +74,15 @@ Section language. (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. + = Some (Interp interp_op (InterpToPHOAS_gen failb ctx e) v). + Proof. 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 e Hwf) v). - Proof. apply interp_interp_to_phoas. Qed. + = Some (Interp interp_op (InterpToPHOAS (Context:=Context) failb e) v). + Proof. apply interp_interp_to_phoas; auto. Qed. End all. End language. diff --git a/src/Reflection/Named/InterpretToPHOASWf.v b/src/Reflection/Named/InterpretToPHOASWf.v index b3c10a8c4..e265dd0dc 100644 --- a/src/Reflection/Named/InterpretToPHOASWf.v +++ b/src/Reflection/Named/InterpretToPHOASWf.v @@ -9,6 +9,7 @@ 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} @@ -18,10 +19,12 @@ Section language. {Name_dec : DecidableRel (@eq Name)}. Section with_var. Context {var1 var2 : base_type_code -> Type} - {Context1 : Context Name var2} - {Context2 : Context Name var1} + {Context1 : Context Name var1} + {Context2 : Context Name var2} {Context1Ok : ContextOk Context1} - {Context2Ok : ContextOk Context2}. + {Context2Ok : ContextOk Context2} + (failb1 : forall t, @Syntax.exprf base_type_code op var1 (Tbase t)) + (failb2 : forall t, @Syntax.exprf base_type_code op var2 (Tbase t)). Local Ltac t_step := first [ progress intros @@ -68,20 +71,16 @@ Section language. -> List.In (existT _ t (v1, v2)%core) G) (Hctx1_ctx2 : forall n t, lookupb ctx1 n t = None <-> lookupb ctx2 n t = None) - : wff G (interpf_to_phoas ctx1 e Hwf1) (interpf_to_phoas ctx2 e Hwf2). + : wff G (interpf_to_phoas failb1 ctx1 e) (interpf_to_phoas failb2 ctx2 e). Proof. revert dependent G; revert dependent ctx1; revert dependent ctx2; induction e; repeat first [ progress intros + | progress destruct_head' and | progress break_innermost_match_step | progress simpl in * - | solve [ eauto ] + | progress autorewrite with push_prop_of_option in * + | solve [ eauto | tauto ] | match goal with - | [ |- context[@proj1 ?A ?B (prop_of_option_and ?a ?b) ?H] ] - => destruct (@proj1 A B (prop_of_option_and a b) H); clear H - | [ |- context[@proj1 ?A ?B (@conj ?A' ?B' ?x ?y)] ] - => generalize (@proj1 A B (@conj A' B' x y)); - generalize (@proj2 A B (@conj A' B' x y)); - clear x y | [ |- wff _ _ _ ] => constructor end ]. match goal with H : _ |- _ => eapply H end; t. @@ -94,7 +93,7 @@ Section language. (Hwf2 : Named.wf ctx2 e) (Hctx1 : forall n t, lookupb ctx1 n t = None) (Hctx2 : forall n t, lookupb ctx2 n t = None) - : wf (interp_to_phoas ctx1 e Hwf1) (interp_to_phoas ctx2 e Hwf2). + : wf (interp_to_phoas failb1 ctx1 e) (interp_to_phoas failb2 ctx2 e). Proof. constructor; intros. apply wff_interpf_to_phoas; t. @@ -102,24 +101,25 @@ Section language. Lemma wf_interp_to_phoas {t} (e : @Named.expr base_type_code op Name t) - (Hwf1 : Named.wf empty e) - (Hwf2 : Named.wf empty e) - : wf (interp_to_phoas (Context:=Context1) empty e Hwf1) (interp_to_phoas (Context:=Context2) empty e Hwf2). + (Hwf1 : Named.wf (Context:=Context1) empty e) + (Hwf2 : Named.wf (Context:=Context2) empty e) + : wf (interp_to_phoas (Context:=Context1) failb1 empty e) (interp_to_phoas (Context:=Context2) failb2 empty e). Proof. - apply wf_interp_to_phoas_gen; apply lookupb_empty; assumption. + apply wf_interp_to_phoas_gen; auto using lookupb_empty. Qed. End with_var. Section all. Context {Context : forall var, @Context base_type_code Name var} - {ContextOk : forall var, ContextOk (Context var)}. + {ContextOk : forall var, ContextOk (Context var)} + (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)). Lemma Wf_InterpToPHOAS_gen {ctx : forall var, Context var} {t} (e : @Named.expr base_type_code op Name t) (Hctx : forall var n t, lookupb (ctx var) n t = None) (Hwf : forall var, Named.wf (ctx var) e) - : Wf (InterpToPHOAS_gen ctx e Hwf). + : Wf (InterpToPHOAS_gen failb ctx e). Proof. intros ??; apply wf_interp_to_phoas_gen; auto. Qed. @@ -127,7 +127,7 @@ Section language. Lemma Wf_InterpToPHOAS {t} (e : @Named.expr base_type_code op Name t) (Hwf : Named.Wf Context e) - : Wf (InterpToPHOAS e Hwf). + : Wf (InterpToPHOAS (Context:=Context) failb e). Proof. intros ??; apply wf_interp_to_phoas; auto. Qed. -- cgit v1.2.3