Cleaned up old commented-out parts

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

6 files changed, 1 insertions, 194 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 383eeb8..e3b57c5 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -1653,20 +1653,6 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
   | _ => nil
   end.
 
-(*
-Definition at_external (S: state): option (external_function * list val * mem) :=
-  match S with
-  | Callstate (External ef _ _) vargs k m => Some (ef, vargs, m)
-  | _ => None
-  end.
-
-Definition after_external (S: state) (v: val) (m: mem): option state :=
-  match S with
-  | Callstate _ _ k _ => Some (Returnstate v k m)
-  | _ => None
-  end.
-*)
-
 Ltac myinv :=
   match goal with
   | [ |- In _ nil -> _ ] => intro X; elim X
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 0590a60..10ffbe4 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -479,10 +479,6 @@ Lemma match_env_alloc_same:
 Proof.
   intros until tv.
   intros ME ALLOC INCR ACOND OTHER TE E.
-(*
-  assert (ALLOC_RES: b = Mem.nextblock m1) by eauto with mem.
-  assert (ALLOC_NEXT: Mem.nextblock m2 = Zsucc(Mem.nextblock m1)) by eauto with mem.
-*)
   inv ME; constructor.
 (* vars *)
   intros. rewrite PMap.gsspec. destruct (peq id0 id). subst id0.
@@ -901,22 +897,6 @@ Proof.
   exists id; exists lv; intuition. apply PTree.elements_complete. auto.
 Qed.
 
-(*
-Lemma free_list_perm:
-  forall l m m',
-  Mem.free_list m l = Some m' ->
-  forall b ofs p,
-  Mem.perm m' b ofs p -> Mem.perm m b ofs p.
-Proof.
-  induction l; simpl; intros. 
-  inv H; auto.
-  revert H. destruct a as [[b' lo'] hi'].
-  caseEq (Mem.free m b' lo' hi'); try congruence.
-  intros m1 FREE1 FREE2.
-  eauto with mem. 
-Qed.
-*)
-
 Lemma match_callstack_freelist:
   forall f cenv tf e le te sp lo hi cs m m' tm,
   Mem.inject f m tm ->
@@ -1662,85 +1642,6 @@ Proof.
   eapply match_callstack_store_mapped; eauto.
 Qed.
 
-(*
-Lemma var_set_self_correct:
-  forall cenv id ty s a f tf e le te sp lo hi m cs tm tv te' v m' fn k,
-  var_set_self cenv id ty s = OK a ->
-  match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
-  val_inject f v tv ->
-  Mem.inject f m tm ->
-  exec_assign ge e m id v m' ->
-  te'!(for_var id) = Some tv ->
-  (forall i, i <> for_var id -> te'!i = te!i) ->
-  exists te'', exists tm',
-    star step tge (State fn a k (Vptr sp Int.zero) te' tm)
-               E0 (State fn s k (Vptr sp Int.zero) te'' tm') /\
-    Mem.inject f m' tm' /\
-    match_callstack f m' tm' (Frame cenv tf e le te'' sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm') /\
-    (forall id', id' <> for_var id -> te''!id' = te'!id').
-Proof.
-  intros until k. 
-  intros VS MCS VINJ MINJ ASG VAL OTHERS.
-  unfold var_set_self in VS. inv ASG. 
-  assert (NEXTBLOCK: Mem.nextblock m' = Mem.nextblock m).
-    eapply Mem.nextblock_store; eauto.
-  assert (MV: match_var f id e m te sp cenv!!id).
-    inv MCS. inv MENV. auto.
-  assert (EVAR: eval_expr tge (Vptr sp Int.zero) te' tm (Evar (for_var id)) tv).
-    constructor. auto.
-  revert VS; inv MV; intro VS; inv VS; inv H; try congruence.
-  (* var_local *)
-  assert (b0 = b) by congruence. subst b0.
-  assert (chunk0 = chunk) by congruence. subst chunk0.
-  exists te'; exists tm.
-  split. apply star_refl. 
-  split. eapply Mem.store_unmapped_inject; eauto. 
-  split. rewrite NEXTBLOCK. 
-  apply match_callstack_extensional with (PTree.set (for_var id) tv te).
-  intros. repeat rewrite PTree.gsspec.
-  destruct (peq (for_var id0) (for_var id)). congruence. auto.
-  intros. assert (for_temp id0 <> for_var id). unfold for_temp, for_var; congruence.
-  rewrite PTree.gso; auto. 
-  eapply match_callstack_store_local; eauto.
-  intros. auto. 
-  (* var_stack_scalar *)
-  assert (b0 = b) by congruence. subst b0.
-  assert (chunk0 = chunk) by congruence. subst chunk0.
-  assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
-  exploit make_store_correct.
-    eapply make_stackaddr_correct.
-    eauto. eauto. eauto. eauto. eauto. 
-  intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]].
-  exists te'; exists tm'.
-  split. eapply star_three. constructor. eauto. constructor. traceEq.
-  split. auto.
-  split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). 
-  apply match_callstack_extensional with te.
-  intros. apply OTHERS. unfold for_var; congruence.
-  intros. apply OTHERS. unfold for_var, for_temp; congruence.
-  eapply match_callstack_storev_mapped; eauto.
-  auto.
-  (* var_global_scalar *)
-  simpl in *.
-  assert (chunk0 = chunk). exploit H4; eauto. congruence. subst chunk0.  
-  assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
-  exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
-  exploit make_store_correct.
-    eapply make_globaladdr_correct; eauto.
-    rewrite symbols_preserved; eauto. eauto. eauto. eauto. eauto. eauto.
-  intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]].
-  exists te'; exists tm'.
-  split. eapply star_three. constructor. eauto. constructor. traceEq.
-  split. auto. 
-  split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). 
-  apply match_callstack_extensional with te.
-  intros. apply OTHERS. unfold for_var; congruence.
-  intros. apply OTHERS. unfold for_var, for_temp; congruence.
-  eapply match_callstack_store_mapped; eauto.
-  auto.
-Qed.
-*)
-
 (** * Correctness of stack allocation of local variables *)
 
 (** This section shows the correctness of the translation of Csharpminor
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 90bb2e3..426a753 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -61,40 +61,6 @@ Definition cast_float_float (sz: floatsize) (f: float) : float :=
   | F64 => f
   end.
 
-(*
-Definition neutral_for_cast (t: type) : bool :=
-  match t with
-  | Tint I32 sg => true
-  | Tpointer ty => true
-  | Tarray ty sz => true
-  | Tfunction targs tres => true
-  | _ => false
-  end.
-
-Function sem_cast (v: val) (t1 t2: type) : option val :=
-  match v, t1, t2 with
-  | Vint i, Tint sz1 si1, Tint sz2 si2 =>            (**r int to int *)
-      Some (Vint (cast_int_int sz2 si2 i))
-  | Vfloat f, Tfloat sz1, Tint sz2 si2 =>            (**r float to int *)
-      match cast_float_int si2 f with
-      | Some i => Some (Vint (cast_int_int sz2 si2 i))
-      | None => None
-      end
-  | Vint i, Tint sz1 si1, Tfloat sz2 =>              (**r int to float *)
-      Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
-  | Vfloat f, Tfloat sz1, Tfloat sz2 =>              (**r float to float *)
-      Some (Vfloat (cast_float_float sz2 f))
-  | Vptr b ofs, _, _ =>                              (**r int32|pointer to int32|pointer *)
-      if neutral_for_cast t1 && neutral_for_cast t2
-      then Some(Vptr b ofs) else None
-  | Vint n, _, _ =>                                  (**r int32|pointer to int32|pointer *)
-      if neutral_for_cast t1 && neutral_for_cast t2
-      then Some(Vint n) else None
-  | _, _, _ =>
-      None
-  end.
-*)
-
 Function sem_cast (v: val) (t1 t2: type) : option val :=
   match classify_cast t1 t2 with
   | cast_case_neutral =>
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index c192e46..a1ed8b3 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -416,15 +416,6 @@ Inductive exec_assign: env -> mem -> ident -> val -> mem -> Prop :=
     Mem.store chunk m b 0 v = Some m' ->
     exec_assign e m id v m'.
 
-(*
-Inductive exec_opt_assign: env -> mem -> option ident -> val -> mem -> Prop :=
-  | exec_assign_none: forall e m v,
-      exec_opt_assign e m None v m
-  | exec_assign_some: forall e m id v m',
-      exec_assign e m id v m' ->
-      exec_opt_assign e m (Some id) v m'.
-*)
-
 (** One step of execution *)
 
 Inductive step: state -> trace -> state -> Prop :=
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 9856b9e..bbd4cfe 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -209,32 +209,7 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type
   end.
 
 (** [make_cast from to e] applies to [e] the numeric conversions needed
-   to transform a result of type [from] to a result of type [to].
-   It is decomposed in two functions:
--  [make_cast1]  converts from integers to floats or from floats to integers;
--  [make_cast2]  converts to a "small" int or float type if necessary.
-*)
-(*
-Definition make_cast1 (from to: type) (e: expr) :=
-  match from, to with
-  | Tint _ uns, Tfloat _ => make_floatofint e uns
-  | Tfloat _, Tint _ uns => make_intoffloat e uns
-  | _, _ => e
-  end.
-
-Definition make_cast2 (from to: type) (e: expr) :=
-  match to with
-  | Tint I8 Signed => Eunop Ocast8signed e  
-  | Tint I8 Unsigned => Eunop Ocast8unsigned e  
-  | Tint I16 Signed => Eunop Ocast16signed e  
-  | Tint I16 Unsigned => Eunop Ocast16unsigned e  
-  | Tfloat F32 => Eunop Osingleoffloat e
-  | _ => e
-  end.
-
-Definition make_cast (from to: type) (e: expr) :=
-  make_cast2 from to (make_cast1 from to e).
-*)
+   to transform a result of type [from] to a result of type [to]. *)
 
 Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) :=
   match sz, si with
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index fa9ba1d..db5b7bc 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -494,18 +494,6 @@ Definition binary_constructor_correct
   eval_expr ge e le m b vb ->
   eval_expr ge e le m c v.
 
-(*
-Definition binary_constructor_correct'
-    (make: expr -> type -> expr -> type -> res expr)
-    (sem: val -> val -> option val): Prop :=
-  forall a tya b tyb c va vb v e le m,
-  sem va vb = Some v ->
-  make a tya b tyb = OK c ->  
-  eval_expr ge e le m a va ->
-  eval_expr ge e le m b vb ->
-  eval_expr ge e le m c v.
-*)
-
 Lemma make_add_correct: binary_constructor_correct make_add sem_add.
 Proof.
   red; intros until m. intro SEM. unfold make_add.