diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-04-24 14:02:32 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-26 13:59:17 +0200 |
| commit | 08fd5faf30c18e17caa610076e67cf002a01d8b4 (patch) | |
| tree | f88a2e1b3de21ebb748850c1b8bf13f3d715979e /common | |
| parent | 51c497b2e5a2b09788f2cf05f414634b037f52bf (diff) | |
| download | compcert-08fd5faf30c18e17caa610076e67cf002a01d8b4.tar.gz compcert-08fd5faf30c18e17caa610076e67cf002a01d8b4.zip | |
Move Z definitions out of Integers and into Zbits
The module Integers.Make contained lots of definitions and theorems
about Z integers that were independent of the word size. These
definitions and theorems are useful outside Integers.Make, but
it felt unnatural to fetch them from modules Int or Int64.
This commit moves the word-size-independent definitions and theorems
to a new module, lib/Zbits.v, and fixes their uses in the code base.
Diffstat (limited to 'common')
| -rw-r--r-- | common/Memdata.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index c53f0e5d..7144d72c 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -17,6 +17,7 @@ (** In-memory representation of values. *) Require Import Coqlib. +Require Import Zbits. Require Archi. Require Import AST. Require Import Integers. @@ -272,7 +273,7 @@ Qed. Lemma bytes_of_int_mod: forall n x y, - Int.eqmod (two_p (Z.of_nat n * 8)) x y -> + eqmod (two_p (Z.of_nat n * 8)) x y -> bytes_of_int n x = bytes_of_int n y. Proof. induction n. @@ -284,7 +285,7 @@ Proof. intro EQM. simpl; decEq. apply Byte.eqm_samerepr. red. - eapply Int.eqmod_divides; eauto. apply Z.divide_factor_r. + eapply eqmod_divides; eauto. apply Z.divide_factor_r. apply IHn. destruct EQM as [k EQ]. exists k. rewrite EQ. rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega. @@ -292,7 +293,7 @@ Qed. Lemma encode_int_8_mod: forall x y, - Int.eqmod (two_p 8) x y -> + eqmod (two_p 8) x y -> encode_int 1%nat x = encode_int 1%nat y. Proof. intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto. @@ -300,7 +301,7 @@ Qed. Lemma encode_int_16_mod: forall x y, - Int.eqmod (two_p 16) x y -> + eqmod (two_p 16) x y -> encode_int 2%nat x = encode_int 2%nat y. Proof. intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto. |