From e4542668e6d348e0300e76bb77105af24aff4233 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 19 Apr 2021 19:08:08 +0200 Subject: Use List.repeat from Coq's standard library instead of list_repeat --- common/Globalenvs.v | 12 ++++++------ common/Memdata.v | 18 +++++++++--------- 2 files changed, 15 insertions(+), 15 deletions(-) (limited to 'common') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 40496044..a83f2caf 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -887,7 +887,7 @@ Qed. Definition readbytes_as_zero (m: mem) (b: block) (ofs len: Z) : Prop := forall p n, ofs <= p -> p + Z.of_nat n <= ofs + len -> - Mem.loadbytes m b p (Z.of_nat n) = Some (list_repeat n (Byte Byte.zero)). + Mem.loadbytes m b p (Z.of_nat n) = Some (List.repeat (Byte Byte.zero) n). Lemma store_zeros_loadbytes: forall m b p n m', @@ -901,8 +901,8 @@ Proof. + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. lia. rewrite Nat2Z.inj_succ in H1. rewrite Nat2Z.inj_succ. replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by lia. - change (list_repeat (S n0) (Byte Byte.zero)) - with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)). + change (List.repeat (Byte Byte.zero) (S n0)) + with ((Byte Byte.zero :: nil) ++ List.repeat (Byte Byte.zero) n0). apply Mem.loadbytes_concat. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p). eapply store_zeros_unchanged; eauto. intros; lia. @@ -924,11 +924,11 @@ Definition bytes_of_init_data (i: init_data): list memval := | Init_int64 n => inj_bytes (encode_int 8%nat (Int64.unsigned n)) | Init_float32 n => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n))) | Init_float64 n => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n))) - | Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero) + | Init_space n => List.repeat (Byte Byte.zero) (Z.to_nat n) | Init_addrof id ofs => match find_symbol ge id with | Some b => inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b ofs) - | None => list_repeat (if Archi.ptr64 then 8%nat else 4%nat) Undef + | None => List.repeat Undef (if Archi.ptr64 then 8%nat else 4%nat) end end. @@ -1020,7 +1020,7 @@ Lemma store_zeros_read_as_zero: read_as_zero m' b p n. Proof. intros; red; intros. - transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))). + transitivity (Some(decode_val chunk (List.repeat (Byte Byte.zero) (size_chunk_nat chunk)))). apply Mem.loadbytes_load; auto. rewrite size_chunk_conv. eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto. f_equal. destruct chunk; unfold decode_val; unfold decode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity. diff --git a/common/Memdata.v b/common/Memdata.v index 05a3d4ed..411cbc58 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -371,14 +371,14 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval := | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n)) | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n)) | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n)) - | Vptr b ofs, Mint32 => if Archi.ptr64 then list_repeat 4%nat Undef else inj_value Q32 v + | Vptr b ofs, Mint32 => if Archi.ptr64 then List.repeat Undef 4%nat else inj_value Q32 v | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n)) - | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else list_repeat 8%nat Undef + | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else List.repeat Undef 8%nat | Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n))) | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n))) | _, Many32 => inj_value Q32 v | _, Many64 => inj_value Q64 v - | _, _ => list_repeat (size_chunk_nat chunk) Undef + | _, _ => List.repeat Undef (size_chunk_nat chunk) end. Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := @@ -674,10 +674,10 @@ Local Transparent inj_value. constructor; auto. unfold inj_bytes; intros. exploit list_in_map_inv; eauto. intros (b & P & Q); exists b; auto. } - assert (D: shape_encoding chunk v (list_repeat (size_chunk_nat chunk) Undef)). + assert (D: shape_encoding chunk v (List.repeat Undef (size_chunk_nat chunk))). { intros. rewrite EQ; simpl; constructor; auto. - intros. eapply in_list_repeat; eauto. + intros. eapply repeat_spec; eauto. } generalize (encode_val_length chunk v). intros LEN. unfold encode_val; unfold encode_val in LEN; @@ -882,21 +882,21 @@ Qed. Lemma repeat_Undef_inject_any: forall f vl, - list_forall2 (memval_inject f) (list_repeat (length vl) Undef) vl. + list_forall2 (memval_inject f) (List.repeat Undef (length vl)) vl. Proof. induction vl; simpl; constructor; auto. constructor. Qed. Lemma repeat_Undef_inject_encode_val: forall f chunk v, - list_forall2 (memval_inject f) (list_repeat (size_chunk_nat chunk) Undef) (encode_val chunk v). + list_forall2 (memval_inject f) (List.repeat Undef (size_chunk_nat chunk)) (encode_val chunk v). Proof. intros. rewrite <- (encode_val_length chunk v). apply repeat_Undef_inject_any. Qed. Lemma repeat_Undef_inject_self: forall f n, - list_forall2 (memval_inject f) (list_repeat n Undef) (list_repeat n Undef). + list_forall2 (memval_inject f) (List.repeat Undef n) (List.repeat Undef n). Proof. induction n; simpl; constructor; auto. constructor. Qed. @@ -915,7 +915,7 @@ Theorem encode_val_inject: Val.inject f v1 v2 -> list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2). Proof. -Local Opaque list_repeat. +Local Opaque List.repeat. intros. inversion H; subst; simpl; destruct chunk; auto using inj_bytes_inject, inj_value_inject, repeat_Undef_inject_self, repeat_Undef_inject_encode_val. - destruct Archi.ptr64; auto using inj_value_inject, repeat_Undef_inject_self. -- cgit