diff options
Diffstat (limited to 'src/AbstractInterpretationWf.v')
| -rw-r--r-- | src/AbstractInterpretationWf.v | 90 |
1 files changed, 42 insertions, 48 deletions
diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v index a2ba63c01..a6a2d8d6b 100644 --- a/src/AbstractInterpretationWf.v +++ b/src/AbstractInterpretationWf.v @@ -171,23 +171,23 @@ Module Compilers. | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] ]. Qed. - Fixpoint wf_reify (is_let_bound : bool) G {t} + Fixpoint wf_reify (annotate_with_state : bool) (is_let_bound : bool) G {t} : forall v1 v2 (Hv : @wf_value G t v1 v2) s1 s2 (Hs : type.and_for_each_lhs_of_arrow (@abstract_domain_R) s1 s2), - UnderLets.wf (fun G' => expr.wf G') G (@reify1 is_let_bound t v1 s1) (@reify2 is_let_bound t v2 s2) - with wf_reflect G {t} + UnderLets.wf (fun G' => expr.wf G') G (@reify1 annotate_with_state is_let_bound t v1 s1) (@reify2 annotate_with_state is_let_bound t v2 s2) + with wf_reflect (annotate_with_state : bool) G {t} : forall e1 e2 (He : expr.wf G e1 e2) s1 s2 (Hs : abstract_domain_R s1 s2), - @wf_value G t (@reflect1 t e1 s1) (@reflect2 t e2 s2). + @wf_value G t (@reflect1 annotate_with_state t e1 s1) (@reflect2 annotate_with_state t e2 s2). Proof using annotate_Proper bottom'_Proper. all: clear -wf_reflect wf_reify annotate_Proper type_base bottom'_Proper. all: pose proof (@bottom_for_each_lhs_of_arrow_Proper); cbv [Proper abstract_domain_R] in *. all: destruct t as [t|s d]; [ clear wf_reify wf_reflect - | pose proof (fun G => wf_reflect G s) as wf_reflect_s; - pose proof (fun G => wf_reflect G d) as wf_reflect_d; - pose proof (fun G => wf_reify false G s) as wf_reify_s; - pose proof (fun G => wf_reify false G d) as wf_reify_d; + | pose proof (fun G => wf_reflect annotate_with_state G s) as wf_reflect_s; + pose proof (fun G => wf_reflect annotate_with_state G d) as wf_reflect_d; + pose proof (fun G => wf_reify annotate_with_state false G s) as wf_reify_s; + pose proof (fun G => wf_reify annotate_with_state false G d) as wf_reify_d; pose proof (@bottom_Proper s); clear wf_reify wf_reflect ]. all: cbn [reify reflect] in *. @@ -208,9 +208,9 @@ Module Compilers. | [ |- expr.wf _ _ _ ] => constructor | [ He : forall seg G' sv1 sv2, G' = (seg ++ ?G)%list -> _ |- UnderLets.wf _ (?v :: ?G) (UnderLets.splice _ _) (UnderLets.splice _ _) ] => eapply UnderLets.wf_splice; [ apply (He (cons v nil)) | ] - | [ |- UnderLets.wf _ _ (UnderLets.splice (reify1 _ _ _) _) (UnderLets.splice (reify2 _ _ _) _) ] + | [ |- UnderLets.wf _ _ (UnderLets.splice (reify1 _ _ _ _) _) (UnderLets.splice (reify2 _ _ _ _) _) ] => eapply UnderLets.wf_splice; [ apply wf_reify_s || apply wf_reify_d | ] - | [ |- wf_value _ (reflect1 _ _) (reflect2 _ _) ] => apply wf_reflect_s || apply wf_reflect_d + | [ |- wf_value _ (reflect1 _ _ _) (reflect2 _ _ _) ] => apply wf_reflect_s || apply wf_reflect_d | [ H : wf_value _ ?x ?y |- wf_value _ ?x ?y ] => eapply wf_value_Proper_list; [ | eassumption ] | [ H : forall x y, ?R x y -> ?R' (?f x) (?g y) |- ?R' (?f _) (?g _) ] @@ -259,10 +259,10 @@ Module Compilers. end | break_innermost_match_step ]. - Lemma wf_interp G G' {t} (e1 : @expr (@value_with_lets1) t) (e2 : @expr (@value_with_lets2) t) + Lemma wf_interp (annotate_with_state : bool) G G' {t} (e1 : @expr (@value_with_lets1) t) (e2 : @expr (@value_with_lets2) t) (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) - : wf_value_with_lets G' (interp1 e1) (interp2 e2). + : wf_value_with_lets G' (interp1 annotate_with_state e1) (interp2 annotate_with_state e2). Proof using annotate_Proper bottom'_Proper interp_ident_Proper. revert dependent G'; induction Hwf; intros; cbn [interp]; try solve [ apply interp_ident_Proper; auto @@ -270,9 +270,9 @@ Module Compilers. wf_interp_t. Qed. - Lemma wf_eval_with_bound' G G' {t} e1 e2 (He : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) + Lemma wf_eval_with_bound' (annotate_with_state : bool) G G' {t} e1 e2 (He : 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_bound'1 t e1 st1) (@eval_with_bound'2 t e2 st2). + : expr.wf G' (@eval_with_bound'1 annotate_with_state t e1 st1) (@eval_with_bound'2 annotate_with_state t e2 st2). Proof using annotate_Proper bottom'_Proper interp_ident_Proper. eapply UnderLets.wf_to_expr, UnderLets.wf_splice. { eapply wf_interp; solve [ eauto ]. } @@ -303,7 +303,6 @@ Module Compilers. Context (annotate_ident : forall t, abstract_domain' t -> option (ident (t -> t))) (bottom' : forall A, abstract_domain' A) (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t) - (update_literal_with_state : forall A : base.type.base, abstract_domain' A -> base.interp A -> base.interp A) (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (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). @@ -311,7 +310,6 @@ Module Compilers. Context {annotate_ident_Proper : forall t, Proper (abstract_domain'_R t ==> eq) (annotate_ident t)} {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)} {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)} - {update_literal_with_state_Proper : forall t, Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state 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). @@ -325,14 +323,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 update_literal_with_state extract_list_state is_annotated_for). - Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for). - Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident update_literal_with_state is_annotated_for). - Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident update_literal_with_state 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 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 update_literal_with_state extract_list_state is_annotated_for). - Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state 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 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 reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom'). Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom'). @@ -382,7 +380,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 (@annotate_base1 is_let_bound t v1 e1) (@annotate_base2 is_let_bound t v2 e2). - Proof using abstract_interp_ident_Proper annotate_ident_Proper update_literal_with_state_Proper is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper is_annotated_for_Proper. cbv [ident.annotate_base]; repeat first [ apply wf_annotate_with_ident | break_innermost_match_step @@ -409,7 +407,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 update_literal_with_state_Proper is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_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 @@ -491,9 +489,9 @@ Module Compilers. let b' := type_of_value b in constr:(type.arrow a' b') end. - Lemma wf_interp_ident_nth_default G T - : wf_value_with_lets G (@interp_ident1 _ (@ident.List_nth_default T)) (@interp_ident2 _ (@ident.List_nth_default T)). - Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper. + 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. 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 *. @@ -599,9 +597,9 @@ Module Compilers. end ]. } Qed. - Lemma wf_interp_ident_not_nth_default G {t} (idc : ident t) - : wf_value_with_lets G (Base (reflect1 (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 (###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 update_literal_with_state_Proper is_annotated_for_Proper. + 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. constructor; eapply wf_reflect; solve [ apply bottom'_Proper | apply wf_annotate @@ -609,43 +607,43 @@ Module Compilers. | apply abstract_interp_ident_Proper; reflexivity ]. Qed. - Lemma wf_interp_ident G {t} idc1 idc2 (Hidc : idc1 = idc2) - : wf_value_with_lets G (@interp_ident1 t idc1) (@interp_ident2 t idc2). - Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper. + 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. 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 update_literal_with_state 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 update_literal_with_state extract_list_state is_annotated_for). - Lemma wf_eval_with_bound {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) + 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). + 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 t e1 st1) (@eval_with_bound2 t e2 st2). - Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper is_annotated_for_Proper. + : 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. 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 update_literal_with_state extract_list_state is_annotated_for). - Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for). + 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). 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 update_literal_with_state_Proper is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_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 update_literal_with_state 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 update_literal_with_state 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 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). 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 update_literal_with_state_Proper is_annotated_for_Proper. + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper. eapply wf_eta_expand_with_bound'; solve [ eassumption | eapply wf_annotate @@ -697,10 +695,6 @@ Module Compilers. end ]. Qed. - Global Instance update_literal_with_state_Proper {t} - : Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state t). - Proof. repeat intro; congruence. Qed. - Global Instance extract_list_state_Proper {t} : Proper (abstract_domain'_R _ ==> option_eq (SetoidList.eqlistA (@abstract_domain'_R t))) (extract_list_state t). |