rm old select/selectl/selectf/selectfs

1 files changed, 0 insertions, 244 deletions

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 3c1162bd..8125741b 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1719,250 +1719,6 @@ Opaque Int.eq.
 - (* Ocmp *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto with asmgen.
-- (* Oselect *)
-  destruct cond in *; simpl in *; try congruence;
-    try monadInv EQ3;
-    try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
-  econstructor; split;
-  try ( eapply exec_straight_one; simpl; reflexivity ).
-  (* Cmp *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl;
-      destruct (Val.cmp_bool _ _); simpl; try constructor;
-        destruct b; simpl; rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-  (* Cmpu *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl in *; inv EQ2; simpl.
-      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
-         destruct (Val.cmpu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
-         destruct (Val.cmpu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-
-  (* Cmpl *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl;
-      destruct (Val.cmpl_bool _ _); simpl; try constructor;
-        destruct b; simpl; rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-      
-  (* Cmplu *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl in *; inv EQ2; simpl.
-      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
-         destruct (Val.cmplu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
-         destruct (Val.cmplu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-
-- (* Oselectl *)
-  destruct cond in *; simpl in *; try congruence;
-    try monadInv EQ3;
-    try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
-  econstructor; split;
-  try ( eapply exec_straight_one; simpl; reflexivity ).
-  (* Cmp *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl;
-      destruct (Val.cmp_bool _ _); simpl; try constructor;
-        destruct b; simpl; rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-  (* Cmpu *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl in *; inv EQ2; simpl.
-      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
-         destruct (Val.cmpu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
-         destruct (Val.cmpu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-
-  (* Cmpl *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl;
-      destruct (Val.cmpl_bool _ _); simpl; try constructor;
-        destruct b; simpl; rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-      
-  (* Cmplu *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl in *; inv EQ2; simpl.
-      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
-         destruct (Val.cmplu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
-         destruct (Val.cmplu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-
-- (* Oselectf *)
-  destruct cond in *; simpl in *; try congruence;
-    try monadInv EQ3;
-    try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
-  econstructor; split;
-  try ( eapply exec_straight_one; simpl; reflexivity ).
-  (* Cmp *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl;
-      destruct (Val.cmp_bool _ _); simpl; try constructor;
-        destruct b; simpl; rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-  (* Cmpu *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl in *; inv EQ2; simpl.
-      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
-         destruct (Val.cmpu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
-         destruct (Val.cmpu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-
-  (* Cmpl *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl;
-      destruct (Val.cmpl_bool _ _); simpl; try constructor;
-        destruct b; simpl; rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-      
-  (* Cmplu *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl in *; inv EQ2; simpl.
-      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
-         destruct (Val.cmplu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
-         destruct (Val.cmplu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-
-
-- (* Oselectfs *)
-  destruct cond in *; simpl in *; try congruence;
-    try monadInv EQ3;
-    try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
-  econstructor; split;
-  try ( eapply exec_straight_one; simpl; reflexivity ).
-  (* Cmp *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl;
-      destruct (Val.cmp_bool _ _); simpl; try constructor;
-        destruct b; simpl; rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-  (* Cmpu *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl in *; inv EQ2; simpl.
-      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
-         destruct (Val.cmpu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
-         destruct (Val.cmpu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-
-  (* Cmpl *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl;
-      destruct (Val.cmpl_bool _ _); simpl; try constructor;
-        destruct b; simpl; rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
-      
-  (* Cmplu *)
-  + split.
-    * unfold eval_select.
-      destruct (rs x) eqn:eqX; try constructor.
-      destruct (rs x0) eqn:eqX0; try constructor.
-      destruct c0 in *; simpl in *; inv EQ2; simpl.
-      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
-         destruct (Val.cmplu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
-         destruct (Val.cmplu_bool _ _); simpl; try constructor.
-         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
-         rewrite Pregmap.gss; constructor.
-    * intros.
-      rewrite Pregmap.gso; congruence.
 Qed.
 
 (** Memory accesses *)