Un peu d'avancement dans exec_straight_control et cie

1 files changed, 12 insertions, 13 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index d34578d5..6afa6e56 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -389,8 +389,8 @@ Definition non_empty_bblock (body: list basic) (exit: option control): Prop
 (* Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res,
   exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil.
  *)
-(* Definition wf_bblock (header: list label) (body: list basic) (exit: option control) :=
-  non_empty_bblock body exit (* /\ builtin_alone body exit *). *)
+Definition wf_bblock (header: list label) (body: list basic) (exit: option control) :=
+  non_empty_bblock body exit (* /\ builtin_alone body exit *).
 
 (** A bblock is well-formed if he contains at least one instruction,
     and if there is a builtin then it must be alone in this bblock. *)
@@ -399,7 +399,7 @@ Record bblock := mk_bblock {
   header: list label;
   body: list basic;
   exit: option control;
-(*   correct: wf_bblock header body exit *)
+  correct: wf_bblock header body exit
 }.
 
 Ltac bblock_auto_correct := ((* split;  *)try discriminate; try (left; discriminate); try (right; discriminate)).
@@ -416,12 +416,12 @@ Definition length_opt {A} (o: option A) : nat :=
    We ignore labels here...
    The result is in Z to be compatible with operations on PC
 *)
-Definition size (b:bblock): Z :=
-  match (body b, exit b) with
+Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)).
+(*   match (body b, exit b) with
   | (nil, None) => 1
-  | _ => Z.of_nat (length (body b) + length_opt (exit b))
+  | _ => 
   end.
-
+ *)
 
 Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat.
 Proof.
@@ -439,10 +439,9 @@ Qed.
 
 Lemma size_positive (b:bblock): size b > 0.
 Proof.
-  unfold size. destruct (body b). destruct (exit b).
-  - apply to_nat_pos. rewrite Nat2Z.id. simpl. omega.
-  - apply to_nat_pos. simpl. unfold Pos.to_nat. simpl. omega.
-  - apply to_nat_pos. rewrite Nat2Z.id. simpl. omega.
+  unfold size. destruct b as [hd bdy ex cor]. simpl.
+  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega).
+  inversion cor; contradict H; simpl; auto.
 (*     rewrite eq. (* inversion COR. *) (* inversion H. *)
   - assert ((length b > 0)%nat). apply length_nonil. auto.
     omega.
@@ -507,10 +506,10 @@ Program Definition bblock_basic_ctl (c: list basic) (i: option control) :=
     | nil => {| header:=nil; body:=Pnop::nil; exit:=None |}
     end
   end.
-(* Next Obligation.
+Next Obligation.
   constructor. subst; discriminate.
 Qed.
- *)
+
 
 (** * Operational semantics *)