From e73d5db97cdb22cce2ee479469f62af3c4b6264a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 8 Jul 2016 14:43:57 +0200 Subject: Port to Coq 8.5pl2 Manual merging of branch jhjourdan:coq8.5. No other change un functionality. --- arm/Archi.v | 4 ++-- arm/Asmgen.v | 9 ++++----- arm/Asmgenproof.v | 8 ++++---- arm/Asmgenproof1.v | 10 ++++------ 4 files changed, 14 insertions(+), 17 deletions(-) (limited to 'arm') diff --git a/arm/Archi.v b/arm/Archi.v index e4abf009..6b282022 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -26,7 +26,7 @@ Notation align_int64 := 8%Z (only parsing). Notation align_float64 := 8%Z (only parsing). Program Definition default_pl_64 : bool * nan_pl 53 := - (false, nat_iter 51 xO xH). + (false, iter_nat 51 _ xO xH). Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := (** Choose second NaN if pl2 is sNaN but pl1 is qNan. @@ -35,7 +35,7 @@ Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_p negb (Pos.testbit (proj1_sig pl2) 51))%bool. Program Definition default_pl_32 : bool * nan_pl 24 := - (false, nat_iter 22 xO xH). + (false, iter_nat 22 _ xO xH). Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := (** Choose second NaN if pl2 is sNaN but pl1 is qNan. diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 7b3f2fdc..90d3b189 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -173,13 +173,13 @@ Definition loadimm (r: ireg) (n: int) (k: code) := let d2 := decompose_int (Int.not n) in let l1 := List.length d1 in let l2 := List.length d2 in - if NPeano.leb l1 1%nat then + if Nat.leb l1 1%nat then Pmov r (SOimm n) :: k - else if NPeano.leb l2 1%nat then + else if Nat.leb l2 1%nat then Pmvn r (SOimm (Int.not n)) :: k else if thumb tt then loadimm_thumb r n k - else if NPeano.leb l1 l2 then + else if Nat.leb l1 l2 then iterate_op (Pmov r) (Porr r r) d1 k else iterate_op (Pmvn r) (Pbic r r) d2 k. @@ -190,7 +190,7 @@ Definition addimm (r1 r2: ireg) (n: int) (k: code) := else (let d1 := decompose_int n in let d2 := decompose_int (Int.neg n) in - if NPeano.leb (List.length d1) (List.length d2) + if Nat.leb (List.length d1) (List.length d2) then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k). @@ -801,4 +801,3 @@ Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := Definition transf_program (p: Mach.program) : res Asm.program := transform_partial_program transf_fundef p. - diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 5bd2b54f..431743c6 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -166,11 +166,11 @@ Proof. intros. unfold loadimm. set (l1 := length (decompose_int n)). set (l2 := length (decompose_int (Int.not n))). - destruct (NPeano.leb l1 1%nat). TailNoLabel. - destruct (NPeano.leb l2 1%nat). TailNoLabel. + destruct (Nat.leb l1 1%nat). TailNoLabel. + destruct (Nat.leb l2 1%nat). TailNoLabel. destruct (thumb tt). unfold loadimm_thumb. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero); TailNoLabel. - destruct (NPeano.leb l1 l2); auto with labels. + destruct (Nat.leb l1 l2); auto with labels. Qed. Hint Resolve loadimm_label: labels. @@ -179,7 +179,7 @@ Remark addimm_label: Proof. intros; unfold addimm. destruct (Int.ltu (Int.repr (-256)) n). TailNoLabel. - destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))); + destruct (Nat.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))); auto with labels. Qed. Hint Resolve addimm_label: labels. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 3e222ba4..76a7b080 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -333,11 +333,11 @@ Proof. intros. unfold loadimm. set (l1 := length (decompose_int n)). set (l2 := length (decompose_int (Int.not n))). - destruct (NPeano.leb l1 1%nat). + destruct (Nat.leb l1 1%nat). { (* single mov *) econstructor; split. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } - destruct (NPeano.leb l2 1%nat). + destruct (Nat.leb l2 1%nat). { (* single movn *) econstructor; split. apply exec_straight_one. simpl. rewrite Int.not_involutive. reflexivity. auto. @@ -359,7 +359,7 @@ Proof. rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega. } - destruct (NPeano.leb l1 l2). + destruct (Nat.leb l1 l2). { (* mov - orr* *) replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero). apply iterate_op_correct. @@ -390,7 +390,7 @@ Proof. (* sub *) econstructor; split. apply exec_straight_one; simpl; auto. split; intros; Simpl. apply Val.sub_opp_add. - destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))). + destruct (Nat.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))). (* add - add* *) replace (Val.add (rs r2) (Vint n)) with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)). @@ -1498,5 +1498,3 @@ Proof. Qed. End CONSTRUCTORS. - - -- cgit