From 9c7c84cc40eaacc1e2c13091165785cddecba5ad Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jun 2010 08:27:14 +0000 Subject: 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 --- lib/Axioms.v | 58 +++++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 45 insertions(+), 13 deletions(-) (limited to 'lib/Axioms.v') diff --git a/lib/Axioms.v b/lib/Axioms.v index 0d82ed4b..52a7fffa 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. -- cgit