diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-10 23:20:32 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-10 23:20:32 -0400 |
commit | 2e03b814b6ebf87e734ba66c0d3b653855bf5b42 (patch) | |
tree | 97267dac13c7654585d9f520ebabffbd98b2f31b | |
parent | 3ed51c2c21e37170f5c33ead2bf5bc24a948b559 (diff) |
Finish CSE_Wf
-rw-r--r-- | src/Compilers/CommonSubexpressionEliminationWf.v | 41 |
1 files changed, 34 insertions, 7 deletions
diff --git a/src/Compilers/CommonSubexpressionEliminationWf.v b/src/Compilers/CommonSubexpressionEliminationWf.v index 44253255b..93fb69225 100644 --- a/src/Compilers/CommonSubexpressionEliminationWf.v +++ b/src/Compilers/CommonSubexpressionEliminationWf.v @@ -51,6 +51,7 @@ Section symbolic. Local Notation CSE := (@CSE base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op). Local Notation SymbolicExprContext := (@SymbolicExprContext base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl). Local Notation SymbolicExprContextOk := (@SymbolicExprContextOk base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl base_type_code_lb op_code_bl op_code_lb). + Local Notation prepend_prefix := (@prepend_prefix base_type_code op_code op). Local Instance base_type_code_dec : DecidableRel (@eq base_type_code) := dec_rel_of_bool_dec_rel base_type_code_beq base_type_code_bl base_type_code_lb. @@ -122,7 +123,32 @@ Section symbolic. | solve [ intuition (eauto || congruence) ] ]. } Qed. + Lemma wff_prepend_prefix prefix1 prefix2 G t e1 e2 + (Hlen : length prefix1 = length prefix2) + (Hprefix : forall n t1 t2 e1 e2, + nth_error prefix1 n = Some (existT _ t1 e1) + -> nth_error prefix2 n = Some (existT _ t2 e2) + -> exists pf : t1 = t2, wff nil (eq_rect _ exprf e1 _ pf) e2) + (Hwf : wff G e1 e2) + : wff G (@prepend_prefix var1 t e1 prefix1) (@prepend_prefix var2 t e2 prefix2). + Proof. + revert dependent G; revert dependent prefix2; induction prefix1, prefix2; simpl; intros; try congruence. + { pose proof (Hprefix 0) as H0; specialize (fun n => Hprefix (S n)). + destruct_head sigT; simpl in *. + specialize (H0 _ _ _ _ eq_refl eq_refl); destruct_head ex; subst; simpl in *. + constructor. + { eapply wff_in_impl_Proper; [ eassumption | simpl; tauto ]. } + { intros. + apply IHprefix1; try congruence; auto. + eapply wff_in_impl_Proper; [ eassumption | simpl; intros; rewrite in_app_iff; auto ]. } } + Qed. + Lemma wf_cse prefix1 prefix2 t e1 e2 (Hwf : wf e1 e2) + (Hlen : length prefix1 = length prefix2) + (Hprefix : forall n t1 t2 e1 e2, + nth_error prefix1 n = Some (existT _ t1 e1) + -> nth_error prefix2 n = Some (existT _ t2 e2) + -> exists pf : t1 = t2, wff nil (eq_rect _ exprf e1 _ pf) e2) : wf (@cse var1 prefix1 t e1 empty) (@cse var2 prefix2 t e2 empty). Proof. destruct Hwf; simpl; constructor; intros. @@ -138,20 +164,21 @@ Section symbolic. break_innermost_match; subst; simpl; try setoid_rewrite lookupb_empty; eauto using SymbolicExprContextOk; try congruence. } { intros *; intro H'; exact (flatten_binding_list_SmartVarfMap2_pair_same_in_eq2 H'). } { intros *; intro H'; destruct (flatten_binding_list_SmartVarfMap2_pair_In_split H'); eauto. } - { admit. } - Admitted. + { apply wff_prepend_prefix; auto. } + Qed. End with_var. Lemma Wf_CSE t (e : Expr t) (prefix : forall var, list (sigT (fun t : flat_type => @exprf var t))) - (*Hprefix : forall var1 var2 t e1 e2, - List.In (existT _ t e1) (prefix var1) - -> List.In (existT _ t e2) (prefix var2) - -> wff nil e1 e2*) + (Hlen : forall var1 var2, length (prefix var1) = length (prefix var2)) + (Hprefix : forall var1 var2 n t1 t2 e1 e2, + nth_error (prefix var1) n = Some (existT _ t1 e1) + -> nth_error (prefix var2) n = Some (existT _ t2 e2) + -> exists pf : t1 = t2, wff nil (eq_rect _ exprf e1 _ pf) e2) (Hwf : Wf e) : Wf (@CSE t e prefix). Proof. - intros var1 var2; apply wf_cse; auto. + intros var1 var2; apply wf_cse; eauto. Qed. End symbolic. |