diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 12:50:57 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 12:50:57 +0000 |
commit | 74487f079dd56663f97f9731cea328931857495c (patch) | |
tree | 9de10b895da39adffaf66bff983d6ed573898068 /lib/Ordered.v | |
parent | 0486654fac91947fec93d18a0738dd7aa10bcf96 (diff) | |
download | compcert-74487f079dd56663f97f9731cea328931857495c.tar.gz compcert-74487f079dd56663f97f9731cea328931857495c.zip |
Added support for jump tables in back end.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Ordered.v')
-rw-r--r-- | lib/Ordered.v | 41 |
1 files changed, 40 insertions, 1 deletions
diff --git a/lib/Ordered.v b/lib/Ordered.v index eddc3721..1c7c7f43 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -11,11 +11,12 @@ (* *********************************************************************) (** Constructions of ordered types, for use with the [FSet] functors - for finite sets. *) + for finite sets and the [FMap] functors for finite maps. *) Require Import FSets. Require Import Coqlib. Require Import Maps. +Require Import Integers. (** The ordered type of positive numbers *) @@ -49,6 +50,44 @@ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq. End OrderedPositive. +(** The ordered type of machine integers *) + +Module OrderedInt <: OrderedType. + +Definition t := int. +Definition eq (x y: t) := x = y. +Definition lt (x y: t) := Int.unsigned x < Int.unsigned y. + +Lemma eq_refl : forall x : t, eq x x. +Proof (@refl_equal t). +Lemma eq_sym : forall x y : t, eq x y -> eq y x. +Proof (@sym_equal t). +Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. +Proof (@trans_equal t). +Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. +Proof. + unfold lt; intros. omega. +Qed. +Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. +Proof. + unfold lt,eq; intros; red; intros. subst. omega. +Qed. +Lemma compare : forall x y : t, Compare lt eq x y. +Proof. + intros. destruct (zlt (Int.unsigned x) (Int.unsigned y)). + apply LT. auto. + destruct (Int.eq_dec x y). + apply EQ. auto. + apply GT. + assert (Int.unsigned x <> Int.unsigned y). + red; intros. rewrite <- (Int.repr_unsigned x) in n. rewrite <- (Int.repr_unsigned y) in n. congruence. + red. omega. +Qed. + +Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := Int.eq_dec. + +End OrderedInt. + (** Indexed types (those that inject into [positive]) are ordered. *) Module OrderedIndexed(A: INDEXED_TYPE) <: OrderedType. |