Support for inlined built-ins.

AST: add ef_inline flag to external functions.
Selection: recognize calls to inlined built-ins and inline them as Sbuiltin.
CminorSel to Asm: added Sbuiltin/Ibuiltin instruction.
PrintAsm: adapted expansion of builtins.
C2Clight: adapted detection of builtins.
Conventions: refactored in a machine-independent part (backend/Conventions)
  and a machine-dependent part (ARCH/SYS/Conventions1).


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

1 files changed, 45 insertions, 13 deletions

diff --git a/lib/Axioms.v b/lib/Axioms.v
index 0d82ed4..52a7fff 100644
--- a/lib/Axioms.v
+++ b/lib/Axioms.v
@@ -1,27 +1,59 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** This file collects some axioms used throughout the CompCert development. *)
+
 Require ClassicalFacts.
 
-(* We use just 2 axioms of extensionality:
+(** * Extensionality axioms *)
+
+(** The following [Require Export] gives us functional extensionality for dependent function types:
+<<
+Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, 
+  forall (f g : forall x : A, B x), 
+  (forall x, f x = g x) -> f = g.
+>> 
+and, as a corollary, functional extensionality for non-dependent functions:
+<<
+Lemma functional_extensionality {A B} (f g : A -> B) : 
+  (forall x, f x = g x) -> f = g.
+>>
+*)
+Require Export FunctionalExtensionality.
 
-1.  Functional extensionality for dependent functions
-  (FunctionalExtensionality.functional_extensionality_dep)
-   forall {A} {B : A -> Type},   forall (f g : forall x : A, B x), (forall x, f x = g x) -> f = g.
+(** For compatibility with earlier developments, [extensionality]
+  is an alias for [functional_extensionality]. *)
 
-2.  Propositional extensionality  (forall A B:Prop, (A <-> B) -> A = B.)
+Lemma extensionality:
+  forall (A B: Type) (f g : A -> B),  (forall x, f x = g x) -> f = g.
+Proof. intros; apply functional_extensionality. auto. Qed.
 
-*)
+Implicit Arguments extensionality.
 
-Require Export FunctionalExtensionality.  (* Contains one Axiom *)
+(** We also assert propositional extensionality. *)
 
 Axiom prop_ext: ClassicalFacts.prop_extensionality.
 Implicit Arguments prop_ext.
 
+(** * Proof irrelevance *)
+
+(** We also use proof irrelevance, which is a consequence of propositional
+    extensionality. *)
+
 Lemma proof_irr: ClassicalFacts.proof_irrelevance.
 Proof.
-exact (ClassicalFacts.ext_prop_dep_proof_irrel_cic prop_ext).
+  exact (ClassicalFacts.ext_prop_dep_proof_irrel_cic prop_ext).
 Qed.
 Implicit Arguments proof_irr.
-
-Lemma extensionality:
- forall (A B: Type) (f g : A -> B),  (forall x, f x = g x) -> f = g.
-Proof. intros; apply functional_extensionality. auto. Qed.
-Implicit Arguments extensionality.