From 0bbbdfede48aed7a74ac2fb95440256ed60fb6e8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Feb 2019 18:17:11 -0500 Subject: Add support for reifying `zrange` and `option` This is needed to reify statements for the rewriter. --- src/AbstractInterpretationWf.v | 72 ++++++++++++++++++++++++++++++------------ 1 file changed, 51 insertions(+), 21 deletions(-) (limited to 'src/AbstractInterpretationWf.v') diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v index 3d9f03f79..a1e2f180e 100644 --- a/src/AbstractInterpretationWf.v +++ b/src/AbstractInterpretationWf.v @@ -305,6 +305,7 @@ Module Compilers. (bottom' : forall A, abstract_domain' A) (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t) (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (abstract_domain' A))) + (extract_option_state : forall A, abstract_domain' (base.type.option A) -> option (option (abstract_domain' A))) (is_annotated_for : forall t t', ident t -> abstract_domain' t' -> bool). Context (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop). Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' abstract_domain'_R). @@ -313,7 +314,8 @@ Module Compilers. {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)} {is_annotated_for_Proper : forall t t', Proper (eq ==> abstract_domain'_R _ ==> eq) (@is_annotated_for t t')} (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2)) - (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2). + (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2) + (extract_option_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_eq (option_eq (abstract_domain'_R _)) (extract_option_state t v1) (extract_option_state t v2)). Local Instance abstract_interp_ident_Proper_arrow s d : Proper (eq ==> abstract_domain'_R s ==> abstract_domain'_R d) (abstract_interp_ident (type.arrow s d)) @@ -324,14 +326,14 @@ Module Compilers. Local Notation update_annotation1 := (@ident.update_annotation var1 abstract_domain' annotate_ident is_annotated_for). Local Notation update_annotation2 := (@ident.update_annotation var2 abstract_domain' annotate_ident is_annotated_for). - Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident extract_list_state is_annotated_for). - Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident extract_list_state is_annotated_for). + Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident extract_list_state extract_option_state is_annotated_for). + Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident extract_list_state extract_option_state is_annotated_for). Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident is_annotated_for). Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident is_annotated_for). Local Notation annotate_with_ident1 := (@ident.annotate_with_ident var1 abstract_domain' annotate_ident is_annotated_for). Local Notation annotate_with_ident2 := (@ident.annotate_with_ident var2 abstract_domain' annotate_ident is_annotated_for). - Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for). - Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for). + Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for). + Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for). Local Notation reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom'). Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom'). @@ -408,7 +410,7 @@ Module Compilers. v1 v2 (Hv : abstract_domain'_R t v1 v2) e1 e2 (He : expr.wf G e1 e2) : UnderLets.wf (fun G' => expr.wf G') G (@annotate1 is_let_bound t v1 e1) (@annotate2 is_let_bound t v2 e2). - Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper. revert dependent G; induction t; intros; cbn [ident.annotate]; try apply wf_annotate_base; trivial. all: repeat first [ lazymatch goal with @@ -430,6 +432,13 @@ Module Compilers. pose proof (extract_list_state_length _ v1 v2 Hv) as Hl; pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl'; rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H' + | [ H : abstract_domain'_R _ ?v1 ?v2, H1 : extract_option_state _ ?v1 = _, H2 : extract_option_state _ ?v2 = _ |- _ ] + => let H' := fresh in + pose proof H as H'; + apply extract_option_state_rel in H'; + rewrite H1, H2 in H'; + cbv [option_eq] in H'; + clear H1 H2 | [ H : ?x = ?x |- _ ] => clear H | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H' end @@ -476,6 +485,9 @@ Module Compilers. | progress rewrite_type_transport_correct | apply conj | congruence + | progress destruct_head' option + | progress cbn [Option.combine option_map UnderLets.splice_option reify_option option_rect] in * + | progress cbn [type.decode f_equal eq_rect fst snd] in * | solve [ wf_t ] ]. Qed. @@ -492,7 +504,7 @@ Module Compilers. end. Lemma wf_interp_ident_nth_default (annotate_with_state : bool) G T : wf_value_with_lets G (@interp_ident1 annotate_with_state _ (@ident.List_nth_default T)) (@interp_ident2 annotate_with_state _ (@ident.List_nth_default T)). - Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper. cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain]. { intros; subst. destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *. @@ -600,7 +612,7 @@ Module Compilers. Lemma wf_interp_ident_not_nth_default (annotate_with_state : bool) G {t} (idc : ident t) : wf_value_with_lets G (Base (reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))). - Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper. constructor; eapply wf_reflect; solve [ apply bottom'_Proper | apply wf_annotate @@ -610,41 +622,41 @@ Module Compilers. Lemma wf_interp_ident (annotate_with_state : bool) G {t} idc1 idc2 (Hidc : idc1 = idc2) : wf_value_with_lets G (@interp_ident1 annotate_with_state t idc1) (@interp_ident2 annotate_with_state t idc2). - Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper. cbv [wf_value_with_lets ident.interp_ident]; subst idc2; destruct idc1; first [ apply wf_interp_ident_nth_default | apply wf_interp_ident_not_nth_default ]. Qed. - Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for). - Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for). + Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for). + Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for). Lemma wf_eval_with_bound (annotate_with_state : bool) {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) : expr.wf G' (@eval_with_bound1 annotate_with_state t e1 st1) (@eval_with_bound2 annotate_with_state t e2 st2). - Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper. eapply wf_eval_with_bound'; solve [ eassumption | eapply wf_annotate | eapply wf_interp_ident ]. Qed. - Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for). - Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for). + Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for). + Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for). Lemma wf_eval {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) : expr.wf G' (@eval1 t e1) (@eval2 t e2). - Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper. eapply wf_eval'; solve [ eassumption | eapply wf_annotate | eapply wf_interp_ident ]. Qed. - Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for). - Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for). + Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for). + Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for). Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) : expr.wf G (@eta_expand_with_bound1 t e1 st1) (@eta_expand_with_bound2 t e2 st2). - Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper. eapply wf_eta_expand_with_bound'; solve [ eassumption | eapply wf_annotate @@ -682,6 +694,8 @@ Module Compilers. | progress destruct_head'_prod | progress destruct_head'_bool | progress destruct_head' option + | progress inversion_option + | discriminate | solve [ eauto ] | apply NatUtil.nat_rect_Proper_nondep | apply ListUtil.list_rect_Proper @@ -691,8 +705,15 @@ Module Compilers. | apply ListUtil.update_nth_Proper | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature) | cbn; apply (f_equal (@Some _)) + | progress cbn [ZRange.ident.option.interp] + | progress cbv [zrange_rect] + | apply (f_equal2 pair) + | break_innermost_match_step | match goal with | [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity)) + | [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl) + | [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ] + => specialize (H y); rewrite H1, H2 in H end ]. Qed. @@ -719,6 +740,12 @@ Module Compilers. destruct_head'_ex; destruct_head'_and; inversion_prod; subst; reflexivity. Qed. + Lemma extract_option_state_rel + : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_eq (option_eq (abstract_domain'_R _)) (extract_option_state t v1) (extract_option_state t v2). + Proof. + cbv [extract_option_state option_eq]; intros; subst; break_match; reflexivity. + Qed. + Section with_var2. Context {var1 var2 : type -> Type}. Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident abstract_domain' (fun t => abstract_domain'_R t) var1 var2). @@ -731,7 +758,8 @@ Module Compilers. solve [ eassumption | exact _ | apply extract_list_state_length - | apply extract_list_state_rel ]. + | apply extract_list_state_rel + | apply extract_option_state_rel ]. Qed. Lemma wf_eval_with_bound {relax_zrange t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) @@ -742,7 +770,8 @@ Module Compilers. solve [ eassumption | exact _ | apply extract_list_state_length - | apply extract_list_state_rel ]. + | apply extract_list_state_rel + | apply extract_option_state_rel ]. Qed. @@ -753,7 +782,8 @@ Module Compilers. solve [ eassumption | exact _ | apply extract_list_state_length - | apply extract_list_state_rel ]. + | apply extract_list_state_rel + | apply extract_option_state_rel ]. Qed. End with_var2. -- cgit v1.2.3