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, 250 insertions, 0 deletions

diff --git a/common/AST.v b/common/AST.v
new file mode 100644
index 0000000..1342bef
--- /dev/null
+++ b/common/AST.v
@@ -0,0 +1,250 @@
+(** 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.
+