diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/NewPipeline/RewriterProofs.v | 3 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesGood.v | 96 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 11 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/RewriterWf2.v | 18 |
4 files changed, 61 insertions, 67 deletions
diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/Experiments/NewPipeline/RewriterProofs.v index 2632560be..d0d106a02 100644 --- a/src/Experiments/NewPipeline/RewriterProofs.v +++ b/src/Experiments/NewPipeline/RewriterProofs.v @@ -66,8 +66,7 @@ Module Compilers. pattern.ident.internal_ident_dec_bl, pattern.ident.try_make_transport_ident_cps_correct, pattern.ident.eta_ident_cps_correct - with nocore; - [ .. | intros; eapply UnderLets.wf_Proper_list; [ | | eapply wf_do_again; assumption ]; solve [ wf_t ] ]. + with nocore. Local Ltac start_Interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 := start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0. diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v index 605cbf5ca..3bdfa9913 100644 --- a/src/Experiments/NewPipeline/RewriterRulesGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesGood.v @@ -166,28 +166,27 @@ Module Compilers. N1 N2 C1 C2 ls1 ls2 G (Hwf : expr.wf G ls1 ls2) (HN : UnderLets.wf (fun G' v1 v2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) G N1 N2) + /\ expr.wf G'' v1 v2) G N1 N2) (HC : forall G' x xs y ys rec1 rec2, (exists seg, G' = (seg ++ G)%list) -> expr.wf G x y -> expr.wf G (reify_list xs) (reify_list ys) - -> (forall G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' rec1 rec2) + -> (exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' rec1 rec2) -> UnderLets.wf (fun G' v1 v2 - => forall G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) - G' (C1 x xs rec1) (C2 y ys rec2)) + => exists G'', + (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' v1 v2) + G' (C1 x xs rec1) (C2 y ys rec2)) : option_eq (UnderLets.wf (fun G' v1 v2 - => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P), - forall G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' - (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1) - (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2)) + => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P) G'', + (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' + (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1) + (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2)) G) (@rlist_rect var1 A P (@Compile.value _ ident var1) N1 C1 ls1 _ id) (@rlist_rect var2 A P (@Compile.value _ ident var2) N2 C2 ls2 _ id). @@ -199,8 +198,8 @@ Module Compilers. all: repeat first [ match goal with | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ] => first [ erewrite <- expr.wf_reflect_list in H' by eassumption - | erewrite -> expr.wf_reflect_list in H' by eassumption ]; - exfalso; clear -H H'; congruence + | erewrite -> expr.wf_reflect_list in H' by eassumption ]; + exfalso; clear -H H'; congruence | [ |- UnderLets.wf _ _ _ _ ] => constructor | [ |- Compile.wf_anyexpr _ _ _ _ ] => constructor end @@ -208,10 +207,11 @@ Module Compilers. | progress cbn [sequence_return option_eq] | assumption | reflexivity + | (exists eq_refl) | apply @UnderLets.wf_splice with (P:=fun G' v1 v2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) + /\ expr.wf G'' v1 v2) | progress intros ]. lazymatch goal with | [ H : expr.wf _ (reify_list ?l) (reify_list ?l') |- _ ] @@ -223,8 +223,8 @@ Module Compilers. all: repeat first [ match goal with | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ] => first [ erewrite <- expr.wf_reflect_list in H' by eassumption - | erewrite -> expr.wf_reflect_list in H' by eassumption ]; - exfalso; clear -H H'; congruence + | erewrite -> expr.wf_reflect_list in H' by eassumption ]; + exfalso; clear -H H'; congruence | [ |- UnderLets.wf _ _ _ _ ] => constructor end | progress expr.invert_subst @@ -235,9 +235,9 @@ Module Compilers. | solve [ auto ] | progress subst | apply @UnderLets.wf_splice with (P:=fun G' v1 v2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) + /\ expr.wf G'' v1 v2) | progress intros | wf_safe_t_step | progress type.inversion_type @@ -248,28 +248,27 @@ Module Compilers. N1 N2 C1 C2 ls1 ls2 G (Hwf : expr.wf G ls1 ls2) (HN : UnderLets.wf (fun G' x1 x2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> Compile.wf_anyexpr G'' (type.base P) (AnyExpr.wrap x1) (AnyExpr.wrap x2)) G N1 N2) + /\ Compile.wf_anyexpr G'' (type.base P) (AnyExpr.wrap x1) (AnyExpr.wrap x2)) G N1 N2) (HC : forall G' x xs y ys rec1 rec2, (exists seg, G' = (seg ++ G)%list) -> expr.wf G x y -> expr.wf G (reify_list xs) (reify_list ys) - -> (forall G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' rec1 rec2) + -> (exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' rec1 rec2) -> UnderLets.wf (fun G' v1 v2 - => forall G'', + => exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' v1 v2) + /\ expr.wf G'' v1 v2) G' (C1 x xs rec1) (C2 y ys rec2)) : option_eq (UnderLets.wf (fun G' v1 v2 - => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P), - forall G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - -> expr.wf G'' - (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1) - (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2)) + => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P) G'', + (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') + /\ expr.wf G'' + (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1) + (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2)) G) (@rlist_rect_cast var1 A A' P (@Compile.value _ ident var1) N1 C1 ls1 _ id) (@rlist_rect_cast var2 A A' P (@Compile.value _ ident var2) N2 C2 ls2 _ id). @@ -280,7 +279,8 @@ Module Compilers. apply wf_rlist_rectv; auto. eapply UnderLets.wf_Proper_list_impl; [ | | eassumption ]; trivial; cbn; intros ? ? ? H. repeat let x := fresh in intro x; specialize (H x). - inversion H; inversion_sigma; type.inversion_type; subst; assumption. + destruct H as [? [H0 H1] ]. + inversion H1; inversion_sigma; type.inversion_type; subst; eauto. Qed. @@ -394,16 +394,6 @@ Module Compilers. eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (inversion_prod; subst; eauto). Qed. - (** TODO: MOVE ME *) - Lemma combine_repeat {A B} (a : A) (b : B) n : combine (repeat a n) (repeat b n) = repeat (a, b) n. - Proof. induction n; cbn; congruence. Qed. - Lemma combine_rev_rev_samelength {A B} ls1 ls2 : length ls1 = length ls2 -> @combine A B (rev ls1) (rev ls2) = rev (combine ls1 ls2). - Proof. - revert ls2; induction ls1 as [|? ? IHls1], ls2; cbn in *; try congruence; intros. - rewrite combine_app_samelength, IHls1 by (rewrite ?rev_length; congruence); cbn [combine]. - reflexivity. - Qed. - Local Ltac start_good cps_id rewrite_rules := split; [ reflexivity | ]; repeat apply conj; try solve [ eapply cps_id ]; []; @@ -547,6 +537,13 @@ Module Compilers. => is_evar R; revert H; instantiate (1:=fun G' => expr.wf G'); solve [ auto ] | [ H : expr.wf ?G ?a ?b |- ?R ?G ?a ?b ] => is_evar R; instantiate (1:=fun G' => expr.wf G'); solve [ auto ] + | [ |- (forall t v1 v2, In _ _ -> _) /\ expr.wf _ _ _ ] => apply conj; revgoals + | [ |- (forall t v1 v2, In _ _ -> _) /\ Compile.wf_anyexpr _ _ _ _ ] => apply conj; revgoals + | [ H : expr.wf _ ?x ?y |- Compile.wf_value _ ?x ?y ] => hnf + | [ |- Compile.wf_value _ ?x ?y ] => eapply Compile.wf_value'_Proper_list; [ | solve [ cbv [Compile.wf_value] in *; eauto ] ]; solve [ wf_t ] + | [ |- In ?x ?ls ] => is_evar ls; refine (or_introl eq_refl : In x (x :: _)); shelve + | [ |- or (_ = _) ?G ] => first [ left; reflexivity | has_evar G; right ] + | [ H : @In ?A _ ?ls |- _ ] => is_evar ls; unify ls (@nil A); cbn [In] in H end | progress expr.invert_subst | solve [ wf_t ] @@ -557,12 +554,9 @@ Module Compilers. Lemma nbe_rewrite_rules_good : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules. Proof. - (*Time start_good (@nbe_cps_id) (@nbe_rewrite_rules). - Set Ltac Profiling. - Time all: try solve [ repeat repeat good_t_step ]. - Show Ltac Profile. - (*start_good (@nbe_cps_id) (@nbe_rewrite_rules). - all: repeat good_t_step.*) + (* + Time start_good (@nbe_cps_id) (@nbe_rewrite_rules). + Time all: repeat repeat good_t_step. *) Admitted. diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index 0cbaaaacf..06c71e480 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -623,12 +623,11 @@ Module Compilers. | true, true => UnderLets.wf (fun G' v1 v2 - => exists (pf1 : anyexpr_ty v1 = t) (pf2 : anyexpr_ty v2 = t), - forall G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G' v1' v2') - -> expr.wf G'' - (rew [fun t : base.type => expr t] pf1 in unwrap v1) - (rew [fun t : base.type => expr t] pf2 in unwrap v2)) + => exists (pf1 : anyexpr_ty v1 = t) (pf2 : anyexpr_ty v2 = t) G'', + (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G' v1' v2') + /\ expr.wf G'' + (rew [fun t : base.type => expr t] pf1 in unwrap v1) + (rew [fun t : base.type => expr t] pf2 in unwrap v2)) G | false, false => UnderLets.wf (fun G' => wf_anyexpr G' t) G diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v index bdad9d840..5d1bae6e4 100644 --- a/src/Experiments/NewPipeline/RewriterWf2.v +++ b/src/Experiments/NewPipeline/RewriterWf2.v @@ -484,7 +484,7 @@ Module Compilers. (do_again1 : forall t : base.type, @expr.expr base.type ident (@value var1) t -> @UnderLets var1 (@expr var1 t)) (do_again2 : forall t : base.type, @expr.expr base.type ident (@value var2) t -> @UnderLets var2 (@expr var2 t)) (wf_do_again : forall G (t : base.type) e1 e2, - expr.wf nil e1 e2 + (exists G', (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) /\ expr.wf G' e1 e2) -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2)) (d : @decision_tree pident) (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2) @@ -757,8 +757,9 @@ Module Compilers. (Hrew : rewrite_rules_goodT rew1 rew2) (do_again1 : forall t : base.type, @expr.expr base.type ident (@value var1) t -> @UnderLets var1 (@expr var1 t)) (do_again2 : forall t : base.type, @expr.expr base.type ident (@value var2) t -> @UnderLets var2 (@expr var2 t)) - (wf_do_again : forall G (t : base.type) e1 e2, - expr.wf nil e1 e2 + (wf_do_again : forall G G' (t : base.type) e1 e2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) + -> expr.wf G' e1 e2 -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2)). Local Notation assemble_identifier_rewriters' var := (@assemble_identifier_rewriters' ident var pident full_types invert_bind_args type_of_pident pident_to_typed of_typed_ident arg_types bind_args try_make_transport_ident_cps dtree). @@ -776,7 +777,8 @@ Module Compilers. Proof. revert dependent G; revert dependent re1; revert dependent re2; induction t as [t|s IHs d IHd]; intros; cbn [assemble_identifier_rewriters']. - { rewrite HK1, HK2; apply wf_eval_rewrite_rules; assumption. } + { rewrite HK1, HK2; apply wf_eval_rewrite_rules; try assumption. + intros; destruct_head'_ex; destruct_head'_and; eauto. } { hnf; intros; subst. unshelve eapply IHd; cbn [type_of_rawexpr]; [ shelve | shelve | constructor | cbn; reflexivity | cbn; reflexivity ]. all: rewrite ?HK1, ?HK2. @@ -903,9 +905,10 @@ Module Compilers. do_again1 do_again2 (wf_do_again - : forall (t : base.type) e1 e2, - expr.wf nil e1 e2 - -> UnderLets.wf (fun G' => expr.wf G') nil (do_again1 t e1) (do_again2 t e2)) + : forall G G' (t : base.type) e1 e2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) + -> expr.wf G' e1 e2 + -> UnderLets.wf (fun G' => expr.wf G') G (do_again1 t e1) (do_again2 t e2)) t (idc : ident t), wf_value_with_lets nil (rewrite_head var1 do_again1 t idc) (rewrite_head var2 do_again2 t idc)) fuel {t} (e : Expr t) (Hwf : Wf e) @@ -913,7 +916,6 @@ Module Compilers. Proof. intros var1 var2; cbv [Rewrite]; eapply wf_rewrite with (G:=nil); [ | apply Hwf | wf_t ]. intros; subst; eapply wf_value'_Proper_list; [ | eapply wf_rewrite_head ]; wf_t. - eapply wf_do_again; [ | eassumption ]; wf_t. Qed. End Compile. End RewriteRules. |