From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: 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 --- lib/Camlcoq.ml | 251 ++++++++++++++++++++++++++++++++++++++++++-------------- lib/Coqlib.v | 8 +- lib/Floats.v | 12 ++- lib/Integers.v | 10 +-- lib/Iteration.v | 2 +- lib/Postorder.v | 10 +-- 6 files changed, 215 insertions(+), 78 deletions(-) (limited to 'lib') 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. -- cgit v1.2.3