Assorted cleanups, esp. to avoid generating _rec and _rect recursors in

submodules.  (Extraction does not remove them, then.)  
common/Switch: replaced use of FMaps by our own Maps.


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

3 files changed, 79 insertions, 51 deletions

diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index d426440..3d9f499 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -53,6 +53,23 @@ Local Open Scope error_monad_scope.
 
 Set Implicit Arguments.
 
+(** Auxiliary function for initialization of global variables. *)
+
+Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem :=
+  if zle n 0 then Some m else
+    match Mem.store Mint8unsigned m b p Vzero with
+    | Some m' => store_zeros m' b (p + 1) (n - 1)
+    | None => None
+    end.
+Proof.
+  intros. red. omega.
+  apply Zwf_well_founded.
+Qed.
+
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 Module Genv.
 
 (** * Global environments *)
@@ -486,18 +503,6 @@ Proof.
   destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega.
 Qed.
 
-Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem :=
-  if zle n 0 then Some m else
-    let n' := n - 1 in
-    match Mem.store Mint8unsigned m b p Vzero with
-    | Some m' => store_zeros m' b (p + 1) n'
-    | None => None
-    end.
-Proof.
-  intros. red. omega.
-  apply Zwf_well_founded.
-Qed.
-
 Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem :=
   match id with
   | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n)
diff --git a/common/Memory.v b/common/Memory.v
index 04a3dda..bfaf67d 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -36,6 +36,10 @@ Require Import Values.
 Require Export Memdata.
 Require Export Memtype.
 
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 Local Notation "a # b" := (ZMap.get b a) (at level 1).
 
 Module Mem <: MEM.
diff --git a/common/Switch.v b/common/Switch.v
index 0ba6186..3e25851 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -17,14 +17,34 @@
     to comparison trees. *)
 
 Require Import EqNat.
-Require Import FMaps.
-Require FMapAVL.
 Require Import Coqlib.
+Require Import Maps.
 Require Import Integers.
-Require Import Ordered.
 
-Module IntMap := FMapAVL.Make(OrderedInt).
-Module IntMapF := FMapFacts.Facts(IntMap).
+Module IntIndexed <: INDEXED_TYPE.
+
+  Definition t := int.
+
+  Definition index (n: int) : positive :=
+    match Int.unsigned n with
+    | Z0 => xH
+    | Zpos p => xO p
+    | Zneg p => xI p  (**r never happens *)
+    end.
+
+  Lemma index_inj: forall n m, index n = index m -> n = m.
+  Proof.
+    unfold index; intros. 
+    rewrite <- (Int.repr_unsigned n). rewrite <- (Int.repr_unsigned m).
+    f_equal. 
+    destruct (Int.unsigned n); destruct (Int.unsigned m); congruence.
+  Qed.
+
+  Definition eq := Int.eq_dec.
+
+End IntIndexed.
+
+Module IntMap := IMap(IntIndexed).
 
 (** A multi-way branch is composed of a list of (key, action) pairs,
   plus a default action.  *)
@@ -93,14 +113,14 @@ Fixpoint split_eq (pivot: int) (cases: table)
       else (same, (key, act) :: others)
   end.
 
-Fixpoint split_between (ofs sz: int) (cases: table)
+Fixpoint split_between (dfl: nat) (ofs sz: int) (cases: table)
                        {struct cases} : IntMap.t nat * table :=
   match cases with
-  | nil => (IntMap.empty nat, nil)
+  | nil => (IntMap.init dfl, nil)
   | (key, act) :: rem =>
-      let (inside, outside) := split_between ofs sz rem in
+      let (inside, outside) := split_between dfl ofs sz rem in
       if Int.ltu (Int.sub key ofs) sz
-      then (IntMap.add key act inside, outside)
+      then (IntMap.set key act inside, outside)
       else (inside, (key, act) :: outside)
   end.
 
@@ -110,13 +130,13 @@ Definition refine_low_bound (v lo: Z) :=
 Definition refine_high_bound (v hi: Z) :=
   if zeq v hi then hi - 1 else hi.
 
-Fixpoint validate_jumptable (cases: IntMap.t nat) (default: nat)
+Fixpoint validate_jumptable (cases: IntMap.t nat) 
                             (tbl: list nat) (n: int) {struct tbl} : bool :=
   match tbl with
   | nil => true
   | act :: rem =>
-      beq_nat act (match IntMap.find n cases with Some a => a | None => default end)
-      && validate_jumptable cases default rem (Int.add n Int.one)
+      beq_nat act (IntMap.get n cases)
+      && validate_jumptable cases rem (Int.add n Int.one)
   end.
 
 Fixpoint validate (default: nat) (cases: table) (t: comptree)
@@ -147,11 +167,11 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree)
       end
   | CTjumptable ofs sz tbl t' =>
       let tbl_len := list_length_z tbl in
-      match split_between ofs sz cases with
+      match split_between default ofs sz cases with
       | (inside, outside) =>
           zle (Int.unsigned sz) tbl_len
           && zle tbl_len Int.max_signed
-          && validate_jumptable inside default tbl ofs
+          && validate_jumptable inside tbl ofs
           && validate default outside t' lo hi
      end
   end.
@@ -207,33 +227,33 @@ Qed.
 
 Lemma split_between_prop:
   forall v default ofs sz cases inside outside,
-  split_between ofs sz cases = (inside, outside) ->
+  split_between default ofs sz cases = (inside, outside) ->
   switch_target v default cases =
     (if Int.ltu (Int.sub v ofs) sz
-     then match IntMap.find v inside with Some a => a | None => default end
+     then IntMap.get v inside
      else switch_target v default outside).
 Proof.
-  induction cases; intros until outside; simpl.
-  intros. inv H. simpl. destruct (Int.ltu (Int.sub v ofs) sz); auto.
-  destruct a as [key act]. case_eq (split_between ofs sz cases). intros ins outs SEQ.
-  rewrite (IHcases _ _ SEQ). 
-  case_eq (Int.ltu (Int.sub key ofs) sz); intros; inv H0; simpl.
-  rewrite IntMapF.add_o. 
-  predSpec Int.eq Int.eq_spec v key. 
-  subst v. rewrite H. rewrite dec_eq_true. auto.
-  rewrite dec_eq_false; auto.
-  case_eq (Int.ltu (Int.sub v ofs) sz); intros; auto.
-  predSpec Int.eq Int.eq_spec v key. 
-  subst v. congruence.
-  auto.
+  induction cases; intros until outside; simpl; intros SEQ.
+- inv SEQ. destruct (Int.ltu (Int.sub v ofs) sz); auto. rewrite IntMap.gi. auto.
+- destruct a as [key act].
+  destruct (split_between default ofs sz cases) as [ins outs].
+  erewrite IHcases; eauto. 
+  destruct (Int.ltu (Int.sub key ofs) sz) eqn:LT; inv SEQ.
+  + predSpec Int.eq Int.eq_spec v key. 
+    subst v. rewrite LT. rewrite IntMap.gss. auto. 
+    destruct (Int.ltu (Int.sub v ofs) sz). 
+    rewrite IntMap.gso; auto.
+    auto.
+  + simpl. destruct (Int.ltu (Int.sub v ofs) sz) eqn:LT'. 
+    rewrite Int.eq_false. auto. congruence. 
+    auto.
 Qed.
 
 Lemma validate_jumptable_correct_rec:
-  forall cases default tbl base v,
-  validate_jumptable cases default tbl base = true ->
+  forall cases tbl base v,
+  validate_jumptable cases tbl base = true ->
   0 <= Int.unsigned v < list_length_z tbl ->
-  list_nth_z tbl (Int.unsigned v) =
-  Some(match IntMap.find (Int.add base v) cases with Some a => a | None => default end).
+  list_nth_z tbl (Int.unsigned v) = Some(IntMap.get (Int.add base v) cases).
 Proof.
   induction tbl; intros until v; simpl.
   unfold list_length_z; simpl. intros. omegaContradiction.
@@ -254,16 +274,15 @@ Proof.
 Qed.
 
 Lemma validate_jumptable_correct:
-  forall cases default tbl ofs v sz,
-  validate_jumptable cases default tbl ofs = true ->
+  forall cases tbl ofs v sz,
+  validate_jumptable cases tbl ofs = true ->
   Int.ltu (Int.sub v ofs) sz = true ->
   Int.unsigned sz <= list_length_z tbl ->
-  list_nth_z tbl (Int.unsigned (Int.sub v ofs)) =
-  Some(match IntMap.find v cases with Some a => a | None => default end).
+  list_nth_z tbl (Int.unsigned (Int.sub v ofs)) = Some(IntMap.get v cases).
 Proof.
   intros.
   exploit Int.ltu_inv; eauto. intros. 
-  rewrite (validate_jumptable_correct_rec cases default tbl ofs).
+  rewrite (validate_jumptable_correct_rec cases tbl ofs).
   rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite <- Int.sub_add_opp. 
   rewrite Int.sub_idem. rewrite Int.add_zero. auto. 
   auto.
@@ -312,7 +331,7 @@ Opaque Int.sub.
   eapply IHt1. eauto. omega.
   eapply IHt2. eauto. omega.
   (* jumptable node *)
-  case_eq (split_between i i0 cases). intros ins outs EQ V RANGE.
+  case_eq (split_between default i i0 cases). intros ins outs EQ V RANGE.
   destruct (andb_prop _ _ V). clear V.
   destruct (andb_prop _ _ H). clear H.
   destruct (andb_prop _ _ H1). clear H1.