Revu la repartition des sources Coq en sous-repertoires

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

1 files changed, 0 insertions, 250 deletions

diff --git a/backend/AST.v b/backend/AST.v
deleted file mode 100644
index 1342bef1..00000000
--- a/backend/AST.v
+++ /dev/null
@@ -1,250 +0,0 @@
-(** This file defines a number of data types and operations used in
-  the abstract syntax trees of many of the intermediate languages. *)
-
-Require Import Coqlib.
-Require Import Integers.
-Require Import Floats.
-
-Set Implicit Arguments.
-
-(** Identifiers (names of local variables, of global symbols and functions,
-  etc) are represented by the type [positive] of positive integers. *)
-
-Definition ident := positive.
-
-Definition ident_eq := peq.
-
-(** The languages are weakly typed, using only two types: [Tint] for
-  integers and pointers, and [Tfloat] for floating-point numbers. *)
-
-Inductive typ : Set :=
-  | Tint : typ
-  | Tfloat : typ.
-
-Definition typesize (ty: typ) : Z :=
-  match ty with Tint => 4 | Tfloat => 8 end.
-
-(** Additionally, function definitions and function calls are annotated
-  by function signatures indicating the number and types of arguments,
-  as well as the type of the returned value if any.  These signatures
-  are used in particular to determine appropriate calling conventions
-  for the function. *)
-
-Record signature : Set := mksignature {
-  sig_args: list typ;
-  sig_res: option typ
-}.
-
-Definition proj_sig_res (s: signature) : typ :=
-  match s.(sig_res) with
-  | None => Tint
-  | Some t => t
-  end.
-
-(** Memory accesses (load and store instructions) are annotated by
-  a ``memory chunk'' indicating the type, size and signedness of the
-  chunk of memory being accessed. *)
-
-Inductive memory_chunk : Set :=
-  | Mint8signed : memory_chunk     (**r 8-bit signed integer *)
-  | Mint8unsigned : memory_chunk   (**r 8-bit unsigned integer *)
-  | Mint16signed : memory_chunk    (**r 16-bit signed integer *)
-  | Mint16unsigned : memory_chunk  (**r 16-bit unsigned integer *)
-  | Mint32 : memory_chunk          (**r 32-bit integer, or pointer *)
-  | Mfloat32 : memory_chunk        (**r 32-bit single-precision float *)
-  | Mfloat64 : memory_chunk.       (**r 64-bit double-precision float *)
-
-(** Initialization data for global variables. *)
-
-Inductive init_data: Set :=
-  | Init_int8: int -> init_data
-  | Init_int16: int -> init_data
-  | Init_int32: int -> init_data
-  | Init_float32: float -> init_data
-  | Init_float64: float -> init_data
-  | Init_space: Z -> init_data.
-
-(** Whole programs consist of:
-- a collection of function definitions (name and description);
-- the name of the ``main'' function that serves as entry point in the program;
-- a collection of global variable declarations (name and initializer).
-
-The type of function descriptions varies among the various intermediate
-languages and is taken as parameter to the [program] type.  The other parts
-of whole programs are common to all languages. *)
-
-Record program (funct: Set) : Set := mkprogram {
-  prog_funct: list (ident * funct);
-  prog_main: ident;
-  prog_vars: list (ident * list init_data)
-}.
-
-(** We now define a general iterator over programs that applies a given
-  code transformation function to all function descriptions and leaves
-  the other parts of the program unchanged. *)
-
-Section TRANSF_PROGRAM.
-
-Variable A B: Set.
-Variable transf: A -> B.
-
-Fixpoint transf_program (l: list (ident * A)) : list (ident * B) :=
-  match l with
-  | nil => nil
-  | (id, fn) :: rem => (id, transf fn) :: transf_program rem
-  end.
-
-Definition transform_program (p: program A) : program B :=
-  mkprogram
-    (transf_program p.(prog_funct))
-    p.(prog_main)
-    p.(prog_vars).
-
-Remark transf_program_functions:
-  forall fl i tf,
-  In (i, tf) (transf_program fl) ->
-  exists f, In (i, f) fl /\ transf f = tf.
-Proof.
-  induction fl; simpl.
-  tauto.
-  destruct a. simpl. intros.
-  elim H; intro. exists a. split. left. congruence. congruence.
-  generalize (IHfl _ _ H0). intros [f [IN TR]].
-  exists f. split. right. auto. auto.
-Qed.
-
-Lemma transform_program_function:
-  forall p i tf,
-  In (i, tf) (transform_program p).(prog_funct) ->
-  exists f, In (i, f) p.(prog_funct) /\ transf f = tf.
-Proof.
-  simpl. intros. eapply transf_program_functions; eauto.
-Qed.
-
-End TRANSF_PROGRAM.
-
-(** The following is a variant of [transform_program] where the
-  code transformation function can fail and therefore returns an
-  option type. *)
-
-Section TRANSF_PARTIAL_PROGRAM.
-
-Variable A B: Set.
-Variable transf_partial: A -> option B.
-
-Fixpoint transf_partial_program
-            (l: list (ident * A)) : option (list (ident * B)) :=
-  match l with
-  | nil => Some nil
-  | (id, fn) :: rem =>
-      match transf_partial fn with
-      | None => None
-      | Some fn' =>
-          match transf_partial_program rem with
-          | None => None
-          | Some res => Some ((id, fn') :: res)
-          end
-      end
-  end.
-
-Definition transform_partial_program (p: program A) : option (program B) :=
-  match transf_partial_program p.(prog_funct) with
-  | None => None
-  | Some fl => Some (mkprogram fl p.(prog_main) p.(prog_vars))
-  end.
-
-Remark transf_partial_program_functions:
-  forall fl tfl i tf,
-  transf_partial_program fl = Some tfl ->
-  In (i, tf) tfl ->
-  exists f, In (i, f) fl /\ transf_partial f = Some tf.
-Proof.
-  induction fl; simpl.
-  intros; injection H; intro; subst tfl; contradiction.
-  case a; intros id fn. intros until tf.
-  caseEq (transf_partial fn).
-  intros tfn TFN.
-  caseEq (transf_partial_program fl).
-  intros tfl1 TFL1 EQ. injection EQ; intro; clear EQ; subst tfl.
-  simpl.  intros [EQ1|IN1].
-  exists fn. intuition congruence.
-  generalize (IHfl _ _ _ TFL1 IN1).
-  intros [f [X Y]].
-  exists f. intuition congruence.
-  intros; discriminate.
-  intros; discriminate.
-Qed.
-
-Lemma transform_partial_program_function:
-  forall p tp i tf,
-  transform_partial_program p = Some tp ->
-  In (i, tf) tp.(prog_funct) ->
-  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = Some tf.
-Proof.
-  intros until tf.
-  unfold transform_partial_program.
-  caseEq (transf_partial_program (prog_funct p)).
-  intros. apply transf_partial_program_functions with l; auto.
-  injection H0; intros; subst tp. exact H1.
-  intros; discriminate.
-Qed.
-
-Lemma transform_partial_program_main:
-  forall p tp,
-  transform_partial_program p = Some tp ->
-  tp.(prog_main) = p.(prog_main).
-Proof.
-  intros p tp. unfold transform_partial_program.
-  destruct (transf_partial_program (prog_funct p)).
-  intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; reflexivity.
-  intro; discriminate.
-Qed.
-
-End TRANSF_PARTIAL_PROGRAM.
-
-(** For most languages, the functions composing the program are either
-  internal functions, defined within the language, or external functions
-  (a.k.a. system calls) that emit an event when applied.  We define
-  a type for such functions and some generic transformation functions. *)
-
-Record external_function : Set := mkextfun {
-  ef_id: ident;
-  ef_sig: signature
-}.
-
-Inductive fundef (F: Set): Set :=
-  | Internal: F -> fundef F
-  | External: external_function -> fundef F.
-
-Implicit Arguments External [F].
-
-Section TRANSF_FUNDEF.
-
-Variable A B: Set.
-Variable transf: A -> B.
-
-Definition transf_fundef (fd: fundef A): fundef B :=
-  match fd with
-  | Internal f => Internal (transf f)
-  | External ef => External ef
-  end.
-
-End TRANSF_FUNDEF.
-
-Section TRANSF_PARTIAL_FUNDEF.
-
-Variable A B: Set.
-Variable transf_partial: A -> option B.
-
-Definition transf_partial_fundef (fd: fundef A): option (fundef B) :=
-  match fd with
-  | Internal f =>
-      match transf_partial f with
-      | None => None
-      | Some f' => Some (Internal f')
-      end
-  | External ef => Some (External ef)
-  end.
-
-End TRANSF_PARTIAL_FUNDEF.
-