Changed ptr64 to be always true

6 files changed, 7 insertions, 28 deletions

diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index a1664262..bbe66c5b 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -20,7 +20,7 @@ Require Import ZArith.
 Require Import Fappli_IEEE.
 Require Import Fappli_IEEE_bits.
 
-Parameter ptr64 : bool.
+Definition ptr64 := true.
 
 Definition big_endian := false.
 
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index 7f070c12..8bbdbd4c 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -553,9 +553,9 @@ Lemma transl_cond_int32s_correct:
 Proof.
   intros. destruct cmp; simpl. 
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
+  split; intros; Simpl. destruct (rs##r1); auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
+  split; intros; Simpl. destruct (rs##r1); auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
   split; intros; Simpl.
 - econstructor; split.
diff --git a/mppa_k1c/ConstpropOpproof.v b/mppa_k1c/ConstpropOpproof.v
index 765aa035..b6c73281 100644
--- a/mppa_k1c/ConstpropOpproof.v
+++ b/mppa_k1c/ConstpropOpproof.v
@@ -201,7 +201,6 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
   subst. exists (e#r); split; auto.
   destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto.
-  destruct Archi.ptr64; auto.
   exists (Val.add e#r (Vint n)); split; auto.
 Qed.
 
@@ -374,7 +373,6 @@ Proof.
   predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
   subst. exists (e#r); split; auto.
   destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto.
-  destruct Archi.ptr64; auto.
   exists (Val.addl e#r (Vlong n)); split; auto.
 Qed.
 
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index bb04f786..74101f53 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -522,7 +522,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* addrsymbol *)
   - unfold Genv.symbol_address. destruct (Genv.find_symbol genv id)...
   (* addrstack *)
-  - destruct sp... apply Val.Vptr_has_type.
+  - destruct sp...
   (* castsigned *)
   - destruct v0...
   - destruct v0...
@@ -532,8 +532,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* neg, sub *)
   - destruct v0...
   - unfold Val.sub. destruct v0; destruct v1... 
-    unfold Val.has_type; destruct Archi.ptr64...
-    destruct Archi.ptr64... destruct (eq_block b b0)...
   (* mul, mulhs, mulhu *)
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
@@ -582,7 +580,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0...
   - unfold Val.subl. destruct v0; destruct v1... 
     unfold Val.has_type; destruct Archi.ptr64...
-    destruct Archi.ptr64... destruct (eq_block b b0)...
+    destruct (eq_block b b0)...
   (* mull, mullhs, mullhu *)
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 78a1935d..511dee92 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -123,7 +123,6 @@ Proof.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
   subst. exists x; split; auto.
   destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto.
-  destruct Archi.ptr64; auto.
   destruct (addlimm_match a); InvEval.
 - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto.
 - econstructor; split. EvalOp. simpl; eauto. 
@@ -169,7 +168,6 @@ Proof.
     destruct Archi.ptr64 eqn:SF; auto. 
     apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. 
     rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; auto.
   - subst. econstructor; split.
     EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
     destruct sp; simpl; auto.
@@ -177,7 +175,6 @@ Proof.
     destruct Archi.ptr64 eqn:SF; auto. 
     apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
     rewrite Ptrofs.add_commut. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; auto.
   - subst.
     replace (Val.addl (Val.addl v1 (Vlong n1)) y)
        with (Val.addl (Val.addl v1 y) (Vlong n1)).
@@ -346,7 +343,6 @@ Proof.
   subst x. destruct v1; simpl; auto.
   simpl in B2; inv B2. simpl in B3; inv B3. rewrite Int64.mul_add_distr_l.
   rewrite (Int64.mul_commut n). auto.
-  destruct Archi.ptr64; simpl; auto.
 - apply eval_mullimm_base; auto.
 Qed.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 90f077db..e7577fb5 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -143,15 +143,12 @@ Proof.
   - subst n. intros. exists x; split; auto.
     destruct x; simpl; auto.
     rewrite Int.add_zero; auto.
-    destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. 
   - case (addimm_match a); intros; InvEval; simpl.
     + TrivialExists; simpl. rewrite Int.add_commut. auto.
     + econstructor; split. EvalOp. simpl; eauto. 
       unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto.
-      destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto.
     + econstructor; split. EvalOp. simpl; eauto. 
-      destruct sp; simpl; auto. destruct Archi.ptr64; auto. 
-      rewrite Ptrofs.add_assoc. rewrite (Ptrofs.add_commut m0). auto.
+      destruct sp; simpl; auto.
     + TrivialExists; simpl. subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
     + TrivialExists.
 Qed.
@@ -171,18 +168,10 @@ Proof.
     EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
     rewrite Val.add_commut. destruct sp; simpl; auto.
     destruct v1; simpl; auto.
-    destruct Archi.ptr64 eqn:SF; auto. 
-    apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. 
-    rewrite (Ptrofs.add_commut (Ptrofs.of_int n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; auto.
   - subst. econstructor; split.
     EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
     destruct sp; simpl; auto.
     destruct v1; simpl; auto.
-    destruct Archi.ptr64 eqn:SF; auto. 
-    apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
-    rewrite Ptrofs.add_commut. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; auto.
   - subst.
     replace (Val.add (Val.add v1 (Vint n1)) y)
        with (Val.add (Val.add v1 y) (Vint n1)).
@@ -889,8 +878,7 @@ Proof.
     constructor. EvalOp. simpl. congruence. constructor. simpl. rewrite Ptrofs.add_zero. congruence.
   + exists (@nil val); split. constructor. simpl; auto.
   - exists (v1 :: nil); split. eauto with evalexpr. simpl.
-    destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
-    simpl. auto.
+    destruct v1; simpl in H; try discriminate.
   - exists (v1 :: nil); split. eauto with evalexpr. simpl.
     destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
     simpl. auto.
@@ -917,7 +905,6 @@ Proof.
 - destruct Archi.ptr64 eqn:SF.
 + InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vlong n) else Val.add v1 (Vlong n)).
   repeat constructor; auto.
-  rewrite SF; auto.
 + constructor; auto.
 - constructor; auto.
 Qed.