diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-05-03 11:18:32 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-05-03 11:18:32 +0200 |
| commit | 7873af34a9520ee5a8a6f10faddf3255a4ff02b2 (patch) | |
| tree | 74500c845c99b39ba91a5507656060dea60404ea /lib/BoolEqual.v | |
| parent | 25ea686abc4cce13aba92196dbeb284f727b6e0e (diff) | |
| download | compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.tar.gz compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.zip | |
Hybrid 64bit/32bit PowerPC port
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
Diffstat (limited to 'lib/BoolEqual.v')
| -rw-r--r-- | lib/BoolEqual.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v index a5b543e1..c9e7bad5 100644 --- a/lib/BoolEqual.v +++ b/lib/BoolEqual.v @@ -17,7 +17,7 @@ (** The [decide equality] tactic can generate a term of type [forall (x y: A), {x=y} + {x<>y}] if [A] is an inductive type. -This term is a decidable equality function. +This term is a decidable equality function. Similarly, this module defines a [boolean_equality] tactic that generates a term of type [A -> A -> bool]. This term is a Boolean-valued equality @@ -33,7 +33,7 @@ a decidable equality of type [forall (x y: A), {x=y} + {x<>y}]. The advantage of the present tactics over the standard [decide equality] tactic is that the former produce smaller transparent definitions than -the latter. +the latter. For a type [A] that has N constructors, [decide equality] produces a single term of size O(N^3), which must be kept transparent so that @@ -91,7 +91,7 @@ Ltac bool_eq := end. Lemma proj_sumbool_is_true: - forall (A: Type) (f: forall (x y: A), {x=y} + {x<>y}) (x: A), + forall (A: Type) (f: forall (x y: A), {x=y} + {x<>y}) (x: A), proj_sumbool (f x x) = true. Proof. intros. unfold proj_sumbool. destruct (f x x). auto. elim n; auto. @@ -119,7 +119,7 @@ Lemma proj_sumbool_true: forall (A: Type) (x y: A) (a: {x=y} + {x<>y}), proj_sumbool a = true -> x = y. Proof. - intros. destruct a. auto. discriminate. + intros. destruct a. auto. discriminate. Qed. Ltac bool_eq_sound_case := |