Ported to Coq 8.4pl1. Merge of branches/coq-8.4.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

6 files changed, 215 insertions, 78 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 00c2103..442766d 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -16,75 +16,206 @@
 (* Library of useful Caml <-> Coq conversions *)
 
 open Datatypes
-open BinPos
+open BinNums
 open BinInt
+open BinPos
 open Floats
 
-(* Integers *)
+(* Coq's [nat] type and some of its operations *)
 
-let rec camlint_of_positive = function
-  | Coq_xI p -> Int32.add (Int32.shift_left (camlint_of_positive p) 1) 1l
-  | Coq_xO p -> Int32.shift_left (camlint_of_positive p) 1
-  | Coq_xH -> 1l
+module Nat = struct
 
-let camlint_of_z = function
-  | Z0 -> 0l
-  | Zpos p -> camlint_of_positive p
-  | Zneg p -> Int32.neg (camlint_of_positive p)
+  type t = nat = O | S of t
+
+  let rec to_int = function
+  | O -> 0
+  | S n -> succ (to_int n)
+
+  let rec to_int32 = function
+  | O -> 0l
+  | S n -> Int32.succ(to_int32 n)
+
+  let rec of_int n =
+    assert (n >= 0);
+    if n = 0 then O else S (of_int (pred n))
+
+  let rec of_int32 n =
+    assert (n >= 0l);
+    if n = 0l then O else S (of_int32 (Int32.pred n))
+
+end
+
+
+(* Coq's [positive] type and some of its operations *)
 
-let camlint_of_coqint : Integers.Int.int -> int32 = camlint_of_z
+module P = struct
 
-let rec camlint64_of_positive = function
-  | Coq_xI p -> Int64.add (Int64.shift_left (camlint64_of_positive p) 1) 1L
-  | Coq_xO p -> Int64.shift_left (camlint64_of_positive p) 1
+  type t = positive = Coq_xI of t | Coq_xO of t | Coq_xH
+
+  let one = Coq_xH
+  let succ = Pos.succ
+  let pred = Pos.pred
+  let add = Pos.add
+  let sub = Pos.sub
+  let eq x y = (Pos.compare x y = Eq)
+  let lt x y = (Pos.compare x y = Lt)
+  let gt x y = (Pos.compare x y = Gt)
+  let le x y = (Pos.compare x y <> Gt)
+  let ge x y = (Pos.compare x y <> Lt)
+
+  let rec to_int = function
+  | Coq_xI p -> (to_int p lsl 1) + 1
+  | Coq_xO p -> to_int p lsl 1
+  | Coq_xH -> 1
+
+  let rec of_int n =
+    if n = 0 then assert false else
+    if n = 1 then Coq_xH else
+    if n land 1 = 0
+    then Coq_xO (of_int (n lsr 1))
+    else Coq_xI (of_int (n lsr 1))
+
+  let rec to_int32 = function
+  | Coq_xI p -> Int32.add (Int32.shift_left (to_int32 p) 1) 1l
+  | Coq_xO p -> Int32.shift_left (to_int32 p) 1
+  | Coq_xH -> 1l
+
+  let rec of_int32 n =
+    if n = 0l then assert false else
+    if n = 1l then Coq_xH else
+    if Int32.logand n 1l = 0l
+    then Coq_xO (of_int32 (Int32.shift_right_logical n 1))
+    else Coq_xI (of_int32 (Int32.shift_right_logical n 1))
+
+  let rec to_int64 = function
+  | Coq_xI p -> Int64.add (Int64.shift_left (to_int64 p) 1) 1L
+  | Coq_xO p -> Int64.shift_left (to_int64 p) 1
   | Coq_xH -> 1L
 
-let camlint64_of_z = function
-  | Z0 -> 0L
-  | Zpos p -> camlint64_of_positive p
-  | Zneg p -> Int64.neg (camlint64_of_positive p)
+  let rec of_int64 n =
+    if n = 0L then assert false else
+    if n = 1L then Coq_xH else
+    if Int64.logand n 1L = 0L
+    then Coq_xO (of_int64 (Int64.shift_right_logical n 1))
+    else Coq_xI (of_int64 (Int64.shift_right_logical n 1))
+
+  let (+) = add
+  let (-) = sub
+  let (=) = eq
+  let (<) = lt
+  let (<=) = le
+  let (>) = gt
+  let (>=) = ge
+
+end
+
+(* Coq's [Z] type and some of its operations *)
+
+module Z = struct
+
+  type t = coq_Z = Z0 | Zpos of positive | Zneg of positive
+
+  let zero = Z0
+  let one = Zpos Coq_xH
+  let mone = Zneg Coq_xH
+  let succ = Z.succ
+  let pred = Z.pred
+  let neg = Z.opp
+  let add = Z.add
+  let sub = Z.sub
+  let mul = Z.mul
+  let eq x y = (Z.compare x y = Eq)
+  let lt x y = (Z.compare x y = Lt)
+  let gt x y = (Z.compare x y = Gt)
+  let le x y = (Z.compare x y <> Gt)
+  let ge x y = (Z.compare x y <> Lt)
+
+  let to_int = function
+  | Z0 -> 0
+  | Zpos p -> P.to_int p
+  | Zneg p -> - (P.to_int p)
+
+  let of_sint n =
+    if n = 0 then Z0 else
+    if n > 0 then Zpos (P.of_int n)
+    else Zneg (P.of_int (-n))
+
+  let of_uint n =
+    if n = 0 then Z0 else Zpos (P.of_int n)
+
+  let to_int32 = function
+  | Z0 -> 0l
+  | Zpos p -> P.to_int32 p
+  | Zneg p -> Int32.neg (P.to_int32 p)
 
-let camlint64_of_coqint : Integers.Int64.int -> int64 = camlint64_of_z
+  let of_sint32 n =
+    if n = 0l then Z0 else
+    if n > 0l then Zpos (P.of_int32 n)
+    else Zneg (P.of_int32 (Int32.neg n))
 
-let rec camlint_of_nat = function
-  | O -> 0
-  | S n -> camlint_of_nat n + 1
-
-let rec nat_of_camlint n =
-  assert (n >= 0l);
-  if n = 0l then O else S (nat_of_camlint (Int32.sub n 1l))
-
-let rec positive_of_camlint n =
-  if n = 0l then assert false else
-  if n = 1l then Coq_xH else
-  if Int32.logand n 1l = 0l
-  then Coq_xO (positive_of_camlint (Int32.shift_right_logical n 1))
-  else Coq_xI (positive_of_camlint (Int32.shift_right_logical n 1))
-
-let z_of_camlint n =
-  if n = 0l then Z0 else
-  if n > 0l then Zpos (positive_of_camlint n)
-  else Zneg (positive_of_camlint (Int32.neg n))
-
-let coqint_of_camlint (n: int32) : Integers.Int.int = 
-  (* Interpret n as unsigned so that resulting Z is in range *)
-  if n = 0l then Z0 else Zpos (positive_of_camlint n)
-
-let rec positive_of_camlint64 n =
-  if n = 0L then assert false else
-  if n = 1L then Coq_xH else
-  if Int64.logand n 1L = 0L
-  then Coq_xO (positive_of_camlint64 (Int64.shift_right_logical n 1))
-  else Coq_xI (positive_of_camlint64 (Int64.shift_right_logical n 1))
-
-let z_of_camlint64 n =
-  if n = 0L then Z0 else
-  if n > 0L then Zpos (positive_of_camlint64 n)
-  else Zneg (positive_of_camlint64 (Int64.neg n))
-
-let coqint_of_camlint64 (n: int64) : Integers.Int64.int = 
-  (* Interpret n as unsigned so that resulting Z is in range *)
-  if n = 0L then Z0 else Zpos (positive_of_camlint64 n)
+  let of_uint32 n =
+    if n = 0l then Z0 else Zpos (P.of_int32 n)
+
+  let to_int64 = function
+  | Z0 -> 0L
+  | Zpos p -> P.to_int64 p
+  | Zneg p -> Int64.neg (P.to_int64 p)
+
+  let of_sint64 n =
+    if n = 0L then Z0 else
+    if n > 0L then Zpos (P.of_int64 n)
+    else Zneg (P.of_int64 (Int64.neg n))
+
+  let of_uint64 n =
+    if n = 0L then Z0 else Zpos (P.of_int64 n)
+
+  let rec to_string_rec base buff x =
+    if x = Z0 then () else begin
+      let (q, r) = Z.div_eucl x base in
+      to_string_rec base buff q;
+      let q' = to_int q in
+      Buffer.add_char buff (Char.chr
+        (if q' < 10 then Char.code '0' + q'
+                         else Char.code 'A' + q' - 10))
+    end
+
+  let to_string_aux base x =
+    match x with
+    | Z0 -> "0"
+    | Zpos _ ->
+        let buff = Buffer.create 10 in
+        to_string_rec base buff x;
+        Buffer.contents buff
+    | Zneg p ->
+        let buff = Buffer.create 10 in
+        Buffer.add_char buff '-';
+        to_string_rec base buff (Zpos p);
+        Buffer.contents buff
+
+  let dec = to_string_aux (of_uint 10)
+
+  let hex = to_string_aux (of_uint 16)
+
+  let to_string = dec
+
+  let (+) = add
+  let (-) = sub
+  let ( * ) = mul
+  let (=) = eq
+  let (<) = lt
+  let (<=) = le
+  let (>) = gt
+  let (>=) = ge
+end
+
+(* Alternate names *)
+
+let camlint_of_coqint : Integers.Int.int -> int32 = Z.to_int32
+let coqint_of_camlint : int32 -> Integers.Int.int = Z.of_uint32
+   (* interpret the int32 as unsigned so that result Z is in range for int *)
+let camlint64_of_coqint : Integers.Int64.int -> int64 = Z.to_int64
+let coqint_of_camlint64 : int64 -> Integers.Int64.int = Z.of_uint64
+   (* interpret the int64 as unsigned so that result Z is in range for int *)
 
 (* Atoms (positive integers representing strings) *)
 
@@ -97,7 +228,7 @@ let intern_string s =
     Hashtbl.find atom_of_string s
   with Not_found ->
     let a = !next_atom in
-    next_atom := coq_Psucc !next_atom;
+    next_atom := Pos.succ !next_atom;
     Hashtbl.add atom_of_string s a;
     Hashtbl.add string_of_atom a s;
     a
@@ -106,7 +237,7 @@ let extern_atom a =
   try
     Hashtbl.find string_of_atom a
   with Not_found ->
-    Printf.sprintf "$%ld" (camlint_of_positive a)
+    Printf.sprintf "$%d" (P.to_int a)
 
 let first_unused_ident () = !next_atom
 
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 3d5df25..676aa0a 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -33,7 +33,7 @@ Ltac caseEq name :=
   generalize (refl_equal name); pattern name at -1 in |- *; case name.
 
 Ltac destructEq name :=
-  destruct name as []_eqn.
+  destruct name eqn:?.
 
 Ltac decEq :=
   match goal with
@@ -393,7 +393,7 @@ Qed.
 Lemma Zmin_spec:
   forall x y, Zmin x y = if zlt x y then x else y.
 Proof.
-  intros. case (zlt x y); unfold Zlt, Zge; intros.
+  intros. case (zlt x y); unfold Zlt, Zge; intro z.
   unfold Zmin. rewrite z. auto.
   unfold Zmin. caseEq (x ?= y); intro. 
   apply Zcompare_Eq_eq. auto.
@@ -404,7 +404,7 @@ Qed.
 Lemma Zmax_spec:
   forall x y, Zmax x y = if zlt y x then x else y.
 Proof.
-  intros. case (zlt y x); unfold Zlt, Zge; intros.
+  intros. case (zlt y x); unfold Zlt, Zge; intro z.
   unfold Zmax. rewrite <- (Zcompare_antisym y x).
   rewrite z. simpl. auto.
   unfold Zmax. rewrite <- (Zcompare_antisym y x).
@@ -565,7 +565,7 @@ Qed.
 Lemma Zdivides_trans:
   forall x y z, (x | y) -> (y | z) -> (x | z).
 Proof.
-  intros. inv H. inv H0. exists (q0 * q). ring.
+  intros x y z [a A] [b B]; subst. exists (a*b); ring.
 Qed.
 
 Definition Zdivide_dec:
diff --git a/lib/Floats.v b/lib/Floats.v
index aae2646..711fd61 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -362,7 +362,7 @@ Proof.
   destruct c, x, y; simpl; try destruct b; try destruct b0; try reflexivity;
   rewrite <- (Zcompare_antisym e e1); destruct (e ?= e1); try reflexivity;
   change Eq with (CompOpp Eq); rewrite <- (Pcompare_antisym m m0 Eq);
-    simpl; destruct ((m ?= m0)%positive Eq); try reflexivity.
+    simpl; destruct (Pcompare m m0 Eq); reflexivity.
 Qed.
 
 Theorem cmp_ne_eq:
@@ -524,6 +524,7 @@ Proof.
   destruct (binary_normalize64_exact (Int.unsigned x)); [now smart_omega|].
   match goal with [|- _ _ _ ?f = _] => destruct f end; intuition.
   exfalso; simpl in H2; change 0%R with (Z2R 0) in H2; apply eq_Z2R in H2; omega.
+  try (change (53 ?= 1024) with Lt in H1).  (* for Coq 8.4 *)
   simpl Zcompare in *.
   match goal with [|- _ _ _ ?f = _] => destruct f end; intuition.
   exfalso; simpl in H0; change 0%R with (Z2R 0) in H0; apply eq_Z2R in H0; omega.
@@ -718,6 +719,8 @@ Proof.
   rewrite (Ztrunc_floor (B2R _ _ x)), <- Zfloor_minus, <- Ztrunc_floor;
     [f_equal; assumption|apply Rle_0_minus; left; assumption|].
   left; eapply Rlt_trans; [|now apply H2]; apply (Z2R_lt 0); reflexivity.
+  try (change (0 ?= 53) with Lt in H6,H8).  (* for Coq 8.4 *)
+  try (change (53 ?= 1024) with Lt in H6,H8).  (* for Coq 8.4 *)
   exfalso; simpl Zcompare in H6, H8; rewrite H6, H8 in H9.
   destruct H9 as [|[]]; [discriminate|..].
   eapply Rle_trans in H9; [|apply Rle_0_minus; left; assumption]; apply (le_Z2R 0) in H9; apply H9; reflexivity.
@@ -761,7 +764,7 @@ unfold Int64.or, Int64.bitwise_binop in H0.
 rewrite Int64.unsigned_repr, Int64.bits_of_Z_of_bits in H0.
 rewrite orb_false_intro in H0; [discriminate|reflexivity|].
 rewrite Int64.sign_bit_of_Z.
-match goal with [|- ((if ?c then _ else _) = _)] => destruct c end.
+match goal with [|- ((if ?c then _ else _) = _)] => destruct c as [z0|z0] end.
 reflexivity.
 rewrite Int64.unsigned_repr in z0; [exfalso|]; now smart_omega.
 vm_compute; split; congruence.
@@ -793,7 +796,7 @@ Proof.
   intros; unfold from_words, double_of_bits, b64_of_bits, binary_float_of_bits. 
   rewrite B2R_FF2B; unfold is_finite; rewrite match_FF2B;
   unfold binary_float_of_bits_aux; rewrite split_bits_or; simpl; pose proof (Int.unsigned_range x).
-  destruct (Int.unsigned x + Zpower_pos 2 52) as []_eqn.
+  destruct (Int.unsigned x + Zpower_pos 2 52) eqn:?.
   exfalso; now smart_omega.
   simpl; rewrite <- Heqz;  unfold F2R; simpl.
   rewrite <- (Z2R_plus 4503599627370496), Rmult_1_r.
@@ -822,6 +825,7 @@ Proof.
   rewrite round_exact in H3 by smart_omega.
   match goal with [H3:if Rlt_bool ?x ?y then _ else _ |- _] => 
     pose proof (Rlt_bool_spec x y); destruct (Rlt_bool x y) end; destruct H3. 
+  try (change (53 ?= 1024) with Lt in H3,H5).  (* for Coq 8.4 *)
   simpl Zcompare in *; apply B2R_inj;
     try match goal with [H':B2R _ _ ?f = _ , H'':is_finite _ _ ?f = true |- is_finite_strict _ _ ?f = true] => 
       destruct f; [
@@ -869,6 +873,8 @@ Proof.
   rewrite round_exact in H3 by smart_omega.
   match goal with [H3:if Rlt_bool ?x ?y then _ else _ |- _] => 
     pose proof (Rlt_bool_spec x y); destruct (Rlt_bool x y) end; destruct H3. 
+  try (change (0 ?= 53) with Lt in H3,H5).  (* for Coq 8.4 *)
+  try (change (53 ?= 1024) with Lt in H3,H5).  (* for Coq 8.4 *)
   simpl Zcompare in *; apply B2R_inj;
     try match goal with [H':B2R _ _ ?f = _ , H'':is_finite _ _ ?f = true |- is_finite_strict _ _ ?f = true] => 
       destruct f; [
diff --git a/lib/Integers.v b/lib/Integers.v
index 7d5f016..9844ed1 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -168,7 +168,7 @@ Lemma Z_mod_two_p_range:
 Proof.
   induction n; simpl; intros.
   rewrite two_power_nat_O. omega.
-  rewrite two_power_nat_S. destruct (Z_bin_decomp x) as [b y]_eqn. 
+  rewrite two_power_nat_S. destruct (Z_bin_decomp x) as [b y] eqn:?. 
   rewrite Z_bin_comp_eq. generalize (IHn y). destruct b; omega.
 Qed.
 
@@ -179,7 +179,7 @@ Proof.
     induction n; simpl; intros.
     rewrite two_power_nat_O. exists x. ring.
     rewrite two_power_nat_S.
-    destruct (Z_bin_decomp x) as [b y]_eqn.
+    destruct (Z_bin_decomp x) as [b y] eqn:?.
     destruct (IHn y) as [z EQ]. 
     exists z. rewrite (Z_bin_comp_decomp2 _ _ _ Heqp). 
     repeat rewrite Z_bin_comp_eq. rewrite EQ at 1. ring.
@@ -1171,7 +1171,7 @@ Proof.
     Z_of_bits n (bits_of_Z n x) 0 = k * two_power_nat n + x).
   induction n; intros; simpl.
   rewrite two_power_nat_O. exists (-x). omega.
-  rewrite two_power_nat_S. destruct (Z_bin_decomp x) as [b y]_eqn.
+  rewrite two_power_nat_S. destruct (Z_bin_decomp x) as [b y] eqn:?.
   rewrite zeq_true. destruct (IHn y) as [k EQ].
   replace (Z_of_bits n (fun i => if zeq i 0 then b else bits_of_Z n y (i - 1)) 1)
      with (Z_of_bits n (bits_of_Z n y) 0).
@@ -1302,7 +1302,7 @@ Proof.
   auto.
   destruct (zlt i 0). apply bits_of_Z_below. auto.
   simpl. 
-  destruct (Z_bin_decomp x) as [b x1]_eqn.
+  destruct (Z_bin_decomp x) as [b x1] eqn:?.
   destruct (zeq i 0).
   subst i. simpl in H. assert (x = 0) by omega. subst x. simpl in Heqp. congruence.
   apply IHn.
@@ -2199,7 +2199,7 @@ Proof.
   simpl. rewrite two_power_nat_O in H0. 
   assert (x = 0). omega. subst x. omega.
   rewrite two_power_nat_S in H0. simpl Z_one_bits.
-  destruct (Z_bin_decomp x) as [b y]_eqn.
+  destruct (Z_bin_decomp x) as [b y] eqn:?.
   rewrite (Z_bin_comp_decomp2 _ _ _ Heqp).
   assert (EQ: y * two_p (i + 1) = powerserie (Z_one_bits n y (i + 1))).
     apply IHn. omega. 
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 235b650..1c3c9cc 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -171,7 +171,7 @@ Proof.
   intros. unfold iter in H1. rewrite unroll_Fix in H1. unfold iter_step in H1.
   destruct (peq x 1). discriminate.
   specialize (step_prop a H0). 
-  destruct (step a) as [b'|a']_eqn.
+  destruct (step a) as [b'|a'] eqn:?.
   inv H1. auto.
   apply H with (Ppred x) a'. apply Ppred_Plt; auto. auto. auto.
 Qed.
diff --git a/lib/Postorder.v b/lib/Postorder.v
index 3a76b0d..4a83ea5 100644
--- a/lib/Postorder.v
+++ b/lib/Postorder.v
@@ -148,8 +148,8 @@ Proof.
   constructor; intros.
   eauto.
   caseEq (s.(map)!root); intros. congruence. exploit GREY; eauto. intros [? ?]; contradiction.
-  destruct (s.(map)!x) as []_eqn; try congruence. 
-  destruct (s.(map)!y) as []_eqn; try congruence.
+  destruct (s.(map)!x) eqn:?; try congruence. 
+  destruct (s.(map)!y) eqn:?; try congruence.
   exploit COLOR; eauto. intros. exploit GREY; eauto. intros [? ?]; contradiction.
   (* not finished *)
   destruct succ_x as [ | y succ_x ].
@@ -189,7 +189,7 @@ Proof.
   exists l'; auto.
 
   (* children y needs traversing *)
-  destruct ((gr s)!y) as [ succs_y | ]_eqn.
+  destruct ((gr s)!y) as [ succs_y | ] eqn:?.
   (* y has children *)
   constructor; simpl; intros. 
   (* sub *)
@@ -241,7 +241,7 @@ Qed.
 Lemma initial_state_spec:
   invariant (init_state ginit root).
 Proof.
-  unfold init_state. destruct (ginit!root) as [succs|]_eqn.
+  unfold init_state. destruct (ginit!root) as [succs|] eqn:?.
   (* root has succs *)
   constructor; simpl; intros.
   (* sub *)
@@ -315,7 +315,7 @@ Proof.
   discriminate.
   destruct succs as [ | y succs ].
   inv H. simpl. apply lex_ord_right. omega.
-  destruct ((gr s)!y) as [succs'|]_eqn.
+  destruct ((gr s)!y) as [succs'|] eqn:?.
   inv H. simpl. apply lex_ord_left. eapply PTree_Properties.cardinal_remove; eauto.
   inv H. simpl. apply lex_ord_right. omega.
 Qed.