diff options
author | 2018-12-12 18:41:18 -0500 | |
---|---|---|
committer | 2018-12-12 18:44:36 -0500 | |
commit | bcccf309cf87b6d9377f020bd11a5103a66b7e29 (patch) | |
tree | 19d5641ba48632d8fcdb5d27ef18cae3f6aeb50f /src/Experiments | |
parent | 2688eef101a504648f627b78485b2b87faa12bd7 (diff) |
Generalize expr.interp_related
This is needed to handle exprs whose var types are value
Diffstat (limited to 'src/Experiments')
-rw-r--r-- | src/Experiments/NewPipeline/Language.v | 25 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/LanguageInversion.v | 27 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 2 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesInterpGood.v | 56 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 32 |
5 files changed, 85 insertions, 57 deletions
diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index c129675c9..eba5cf85a 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -458,31 +458,38 @@ Module Compilers. {interp_base_type : base_type -> Type} (interp_ident : forall t, ident t -> type.interp interp_base_type t). - Fixpoint interp_related {t} (e : @expr base_type ident (type.interp interp_base_type) t) : type.interp interp_base_type t -> Prop + Fixpoint interp_related_gen + {var : type base_type -> Type} + (R : forall t, var t -> type.interp interp_base_type t -> Prop) + {t} (e : @expr base_type ident var t) + : type.interp interp_base_type t -> Prop := match e in expr t return type.interp interp_base_type t -> Prop with - | expr.Var t v1 => fun v2 => v1 == v2 + | expr.Var t v1 => R t v1 | expr.App s d f x => fun v2 => exists fv xv, - @interp_related _ f fv - /\ @interp_related _ x xv + @interp_related_gen var R _ f fv + /\ @interp_related_gen var R _ x xv /\ fv xv = v2 | expr.Ident t idc => fun v2 => interp_ident _ idc == v2 | expr.Abs s d f1 => fun f2 => forall x1 x2, - x1 == x2 - -> @interp_related d (f1 x1) (f2 x2) + R _ x1 x2 + -> @interp_related_gen var R d (f1 x1) (f2 x2) | expr.LetIn s d x f (* combine the App rule with the Abs rule *) => fun v2 => exists fv xv, - @interp_related _ x xv + @interp_related_gen var R _ x xv /\ (forall x1 x2, - x1 == x2 - -> @interp_related d (f x1) (fv x2)) + R _ x1 x2 + -> @interp_related_gen var R d (f x1) (fv x2)) /\ fv xv = v2 end. + + Definition interp_related {t} (e : @expr base_type ident (type.interp interp_base_type) t) : type.interp interp_base_type t -> Prop + := @interp_related_gen (type.interp interp_base_type) (@type.eqv) t e. End with_interp. Definition Expr {base_type ident} t := forall var, @expr base_type ident var t. diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v index f5cc89b4f..bc9ad60be 100644 --- a/src/Experiments/NewPipeline/LanguageInversion.v +++ b/src/Experiments/NewPipeline/LanguageInversion.v @@ -603,14 +603,14 @@ Module Compilers. Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}. Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). - Lemma reify_list_interp_related_iff {t ls v} - : expr.interp_related (@ident_interp) (reify_list (t:=t) ls) v - <-> List.Forall2 (expr.interp_related (@ident_interp)) ls v. + Lemma reify_list_interp_related_gen_iff {var R t ls v} + : expr.interp_related_gen (var:=var) (@ident_interp) R (reify_list (t:=t) ls) v + <-> List.Forall2 (expr.interp_related_gen (@ident_interp) R) ls v. Proof using Type. revert v; induction ls as [|l ls IHls], v as [|v vs]. all: repeat first [ rewrite expr.reify_list_nil | rewrite expr.reify_list_cons - | progress cbn [expr.interp_related ident.gen_interp type.related] in * + | progress cbn [expr.interp_related_gen ident.gen_interp type.related] in * | progress cbv [Morphisms.respectful] in * | progress destruct_head'_ex | progress destruct_head'_and @@ -634,14 +634,25 @@ Module Compilers. end ]. Qed. - Lemma reflect_list_interp_related_iff {t ls ls' v} + Lemma reify_list_interp_related_iff {t ls v} + : expr.interp_related (@ident_interp) (reify_list (t:=t) ls) v + <-> List.Forall2 (expr.interp_related (@ident_interp)) ls v. + Proof using Type. apply reify_list_interp_related_gen_iff. Qed. + + Lemma reflect_list_interp_related_gen_iff {var R t ls ls' v} (Hls : invert_expr.reflect_list (t:=t) ls = Some ls') - : List.Forall2 (expr.interp_related (@ident_interp)) ls' v - <-> expr.interp_related (@ident_interp) ls v. + : List.Forall2 (expr.interp_related_gen (var:=var) (@ident_interp) R) ls' v + <-> expr.interp_related_gen (@ident_interp) R ls v. Proof using Type. apply reflect_list_Some in Hls; subst. - rewrite reify_list_interp_related_iff; reflexivity. + rewrite reify_list_interp_related_gen_iff; reflexivity. Qed. + + Lemma reflect_list_interp_related_iff {t ls ls' v} + (Hls : invert_expr.reflect_list (t:=t) ls = Some ls') + : List.Forall2 (expr.interp_related (@ident_interp)) ls' v + <-> expr.interp_related (@ident_interp) ls v. + Proof using Type. now apply reflect_list_interp_related_gen_iff. Qed. End with_interp. Ltac invert_subst_step_helper guard_tac := diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index a459df399..3919287d4 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -586,7 +586,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ : expr.interp_related interp_ident e v -> @type.eqv t (expr.interp interp_ident e) v. Proof using Type. - induction e; cbn [expr.interp_related expr.interp type.related]; cbv [respectful LetIn.Let_In]. + cbv [expr.interp_related]; induction e; cbn [expr.interp_related_gen expr.interp type.related]; cbv [respectful LetIn.Let_In]. all: repeat first [ progress intros | assumption | solve [ eauto ] diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v index 962161102..872cc2be0 100644 --- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v @@ -150,10 +150,11 @@ Module Compilers. let v'' := fresh in cut (v = v'); [ generalize v; intros v'' ?; subst v'' | symmetry ]) in match goal with + | _ => progress cbv [expr.interp_related] in * | _ => progress cbn [Compile.reify_expr] | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand - | [ |- expr.interp_related ?ident_interp ?f ?v ] + | [ |- expr.interp_related_gen ?ident_interp ?R ?f ?v ] => do_replace v | [ |- exists (fv : ?T1 -> ?T2) (ev : ?T1), _ /\ _ /\ fv ev = ?x ] @@ -162,18 +163,18 @@ Module Compilers. first [ do_replace x | is_evar x; do 2 eexists; repeat apply conj; [ | | reflexivity ] ] | _ => progress intros - | [ |- expr.interp_related _ _ ?ev ] => is_evar ev; eassumption - | [ |- expr.interp_related _ (?f @ ?x) ?ev ] + | [ |- expr.interp_related_gen _ _ _ ?ev ] => is_evar ev; eassumption + | [ |- expr.interp_related_gen _ _ (?f @ ?x) ?ev ] => is_evar ev; let fh := fresh in let xh := fresh in - set (fh := f); set (xh := x); cbn [expr.interp_related]; subst fh xh; + set (fh := f); set (xh := x); cbn [expr.interp_related_gen]; subst fh xh; do 2 eexists; repeat apply conj; [ | | reflexivity ] - | [ |- expr.interp_related _ (expr.Abs ?f) _ ] - => let fh := fresh in set (fh := f); cbn [expr.interp_related]; subst fh - | [ |- expr.interp_related _ (expr.Ident ?idc) ?ev ] + | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ] + => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh + | [ |- expr.interp_related_gen _ _ (expr.Ident ?idc) ?ev ] => is_evar ev; - cbn [expr.interp_related]; apply ident.gen_interp_Proper; reflexivity + cbn [expr.interp_related_gen]; apply ident.gen_interp_Proper; reflexivity | [ |- _ = _ :> ?T ] => lazymatch T with | BinInt.Z => idtac @@ -192,13 +193,13 @@ Module Compilers. | [ |- True ] => exact I | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence | [ |- ?G ] => has_evar G; reflexivity - | [ |- context[expr.interp_related _ _ _] ] => reflexivity + | [ |- context[expr.interp_related_gen _ _ _ _] ] => reflexivity | [ |- context[_ == _] ] => reflexivity (*| [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand*) end | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr bool_rect UnderLets.interp_related type.related] in * - | progress cbv [Compile.option_bind' respectful] in * + | progress cbv [Compile.option_bind' respectful expr.interp_related] in * | progress fold (@type.interp _ base.interp) | progress fold (@base.interp) | match goal with @@ -228,10 +229,10 @@ Module Compilers. => rewrite (@eq_map_list_rect A B f ls) | [ |- UnderLets.interp_related _ _ _ (@fold_right ?A ?B ?f ?v ?ls) ] => rewrite (@eq_fold_right_list_rect A B f v ls) - | [ |- context[expr.interp_related _ (reify_list _)] ] - => rewrite expr.reify_list_interp_related_iff - | [ H : context[expr.interp_related _ (reify_list _)] |- _ ] - => rewrite expr.reify_list_interp_related_iff in H + | [ |- context[expr.interp_related_gen _ _ (reify_list _)] ] + => rewrite expr.reify_list_interp_related_gen_iff + | [ H : context[expr.interp_related_gen _ _ (reify_list _)] |- _ ] + => rewrite expr.reify_list_interp_related_gen_iff in H | [ |- context[Forall2 _ (List.map _ _) _] ] => rewrite Forall2_map_l_iff | [ |- context[Forall2 _ _ (List.map _ _)] ] => rewrite Forall2_map_r_iff | [ |- context[Forall2 _ (List.repeat _ _) (List.repeat _ _)] ] => rewrite Forall2_repeat_iff @@ -281,27 +282,27 @@ Module Compilers. => let f := match (eval pattern (v1 yv) in f) with ?f _ => f end in eapply (@UnderLets.interp_related_Proper_impl_same_UnderLets _ _ _ _ _ _ _ _ _ (e xv) (v1 yv) f); [ | eapply H; assumption ] end - | [ |- expr.interp_related - _ + | [ |- expr.interp_related_gen + _ _ (#(ident.prod_rect) @ ?f @ ?e)%expr match ?e' with pair a b => @?f' a b end ] => let fh := fresh in let eh := fresh in - set (fh := f); set (eh := e); cbn [expr.interp_related]; subst fh eh; + set (fh := f); set (eh := e); cbn [expr.interp_related_gen]; subst fh eh; exists (fun ev => match ev with pair a b => f' a b end), e'; repeat apply conj; [ | assumption | reflexivity ]; exists (fun fv ev => match ev with pair a b => fv a b end), f'; repeat apply conj; [ cbn [type.interp type.related ident_interp]; cbv [respectful]; intros; subst; eta_expand; auto | | reflexivity ] - | [ |- expr.interp_related - _ + | [ |- expr.interp_related_gen + _ _ (#(ident.bool_rect) @ ?t @ ?f @ ?b)%expr (bool_rect ?P ?t' ?f' ?b') ] => let th := fresh in let fh := fresh in let bh := fresh in - set (th := t); set (fh := f); set (bh := b); cbn [expr.interp_related]; subst th fh bh; + set (th := t); set (fh := f); set (bh := b); cbn [expr.interp_related_gen]; subst th fh bh; unshelve ((exists (bool_rect P t' f'), b'); repeat apply conj; [ | shelve | reflexivity ]; @@ -309,7 +310,7 @@ Module Compilers. [ | shelve | reflexivity ]; (exists (fun tv fv => bool_rect P (tv tt) (fv tt)), (fun _ => t')); repeat apply conj; [ | shelve | reflexivity ]) - | [ |- @expr.interp_related _ _ _ _ (type.base ?t) _ _ ] + | [ |- @expr.interp_related_gen _ _ _ _ _ _ (type.base ?t) _ _ ] => lazymatch t with | base.type.type_base base.type.Z => idtac | base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z) => idtac @@ -320,12 +321,12 @@ Module Compilers. => lazymatch T1 with Z => idtac | (Z * Z)%type => idtac end; lazymatch T2 with Z => idtac | (Z * Z)%type => idtac end; progress repeat recurse_interp_related_step - | [ |- expr.interp_related _ (expr.Abs ?f) _ ] - => let fh := fresh in set (fh := f); cbn [expr.interp_related]; subst fh - | [ H : expr.interp_related _ ?x ?x' |- expr.interp_related _ (?f @ ?x) (?f' ?x') ] + | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ] + => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh + | [ H : expr.interp_related_gen _ _ ?x ?x' |- expr.interp_related_gen _ _ (?f @ ?x) (?f' ?x') ] => let fh := fresh in let xh := fresh in - set (fh := f); set (xh := x); cbn [expr.interp_related]; subst fh xh; + set (fh := f); set (xh := x); cbn [expr.interp_related_gen]; subst fh xh; exists f', x'; repeat apply conj; [ | exact H | reflexivity ] | [ |- List.Forall2 _ (update_nth _ _ _) (update_nth _ _ _) ] => apply Forall2_update_nth @@ -451,7 +452,7 @@ Module Compilers. | break_innermost_match_step | break_innermost_match_hyps_step | progress destruct_head'_or - | progress cbn [expr.interp_related] in * + | progress cbn [expr.interp_related_gen] in * | match goal with | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))] |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ] @@ -465,7 +466,7 @@ Module Compilers. end | progress cbv [Option.bind] in * | match goal with - | [ H : expr.interp_related _ ?e ?v |- _ ] => is_var e; clear H e + | [ H : expr.interp_related_gen _ _ ?e ?v |- _ ] => is_var e; clear H e end ]. Local Ltac interp_good_t_step_arith := @@ -541,6 +542,7 @@ Module Compilers. [ clear -H; cbv [is_bounded_by_bool] in H; cbn [lower upper] in H; Bool.split_andb; Z.ltb_to_lt; lia.. | ] end + | progress cbn [expr.interp_related_gen] in * | match goal with | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index 3a682e2e9..a290c8d95 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -2196,8 +2196,15 @@ Module Compilers. clear reify_interp_related reflect_interp_related ]. all: repeat first [ progress cbn [reify reflect] in * | progress fold (@reify) (@reflect) in * - | progress cbn [expr_interp_related value_interp_related] in * + | progress cbv [expr.interp_related] in * + | progress cbn [expr.interp_related_gen value_interp_related] in * | break_innermost_match_step + | match goal with + | [ |- context G[expr.interp_related_gen ?ii (@type.eqv) (UnderLets.to_expr ?v)] ] + => let G' := context G[expr_interp_related (UnderLets.to_expr v)] in + change G'; + rewrite <- UnderLets.to_expr_interp_related_iff + end | rewrite <- UnderLets.to_expr_interp_related_iff | exact id | assumption @@ -2211,12 +2218,12 @@ Module Compilers. : rawexpr_interp_related r v -> expr_interp_related (expr_of_rawexpr r) v. Proof using Type. - revert v; induction r; cbn [expr_of_rawexpr expr_interp_related rawexpr_interp_related]; intros. + cbv [expr.interp_related]; revert v; induction r; cbn [expr_of_rawexpr expr.interp_related_gen rawexpr_interp_related]; intros. all: repeat first [ progress destruct_head'_and | progress destruct_head'_ex | progress subst | progress inversion_sigma - | progress cbn [eq_rect type_of_rawexpr expr.interp expr_interp_related type_of_rawexpr] in * + | progress cbn [eq_rect type_of_rawexpr expr.interp expr.interp_related_gen type_of_rawexpr] in * | assumption | exfalso; assumption | apply conj @@ -2238,7 +2245,8 @@ Module Compilers. | progress destruct_head'_and | assumption | apply reflect_interp_related - | progress cbn [expr_interp_related] + | progress cbn [expr.interp_related_gen] + | progress cbv [expr.interp_related] | solve [ eauto ] ]. Qed. @@ -2249,7 +2257,8 @@ Module Compilers. Proof using Type. revert t e H v; induction re. all: repeat first [ progress intros - | progress cbn [rawexpr_equiv_expr eq_rect rawexpr_interp_related type_of_rawexpr expr_interp_related] in * + | progress cbn [rawexpr_equiv_expr eq_rect rawexpr_interp_related type_of_rawexpr expr.interp_related_gen] in * + | progress cbv [expr.interp_related] in * | progress subst | progress destruct_head'_and | progress destruct_head'_ex @@ -2302,7 +2311,8 @@ Module Compilers. -> rawexpr_interp_related re2 (rew [type.interp base.interp] eq_type_of_rawexpr_equiv H in v). Proof using Type. revert re2 H; induction re1, re2; intros H H'. - all: repeat first [ progress cbn [rawexpr_equiv rawexpr_interp_related eq_rect type_of_rawexpr projT1 projT2 rawexpr_equiv_expr expr_interp_related] in * + all: repeat first [ progress cbn [rawexpr_equiv rawexpr_interp_related eq_rect type_of_rawexpr projT1 projT2 rawexpr_equiv_expr expr.interp_related_gen] in * + | progress cbv [expr.interp_related] in * | eassumption | reflexivity | progress intros @@ -2419,12 +2429,10 @@ Module Compilers. | None => True | Some v1 => UnderLets.interp_related ident_interp - (fun e - => expr_interp_related - ((if should_do_again - return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> _ - then reify_expr - else fun v1 => v1) e)) + (if should_do_again + return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> _ + then expr.interp_related_gen ident_interp (fun t => value_interp_related) + else expr_interp_related) v1 v2 end. |