From 895470548b89f00111d1f98ae52d217b9fd15643 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 10 May 2021 12:22:34 +0200
Subject: Some more proof cases, comments and cleanup

---
 scheduling/BTL.v | 69 +-------------------------------------------------------
 1 file changed, 1 insertion(+), 68 deletions(-)

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index d7ffa118..a87f674b 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -793,6 +793,7 @@ Definition is_atom (ib: iblock): bool :=
  | _ => true
  end.
 
+(** Is expand property to only support atomic instructions on the left part of a Bseq *)
 Inductive is_expand: iblock -> Prop :=
   | exp_Bseq ib1 ib2:
      is_atom ib1 = true ->
@@ -844,71 +845,3 @@ Proof.
   destruct (cfg!pc); simpl; intros; try_simplify_someHyps.
   apply expand_None_correct; auto.
 Qed.
-
-
-(* TODO: eliminer toute la suite quand "right_assoc" sera remplace par "expand" *)
-
-Definition is_seq (ib: iblock): bool :=
- match ib with
- | Bseq _ _ => true 
- | _ => false
- end.
-
-
-Inductive is_right_assoc: iblock -> Prop :=
-  | ira_Bseq ib1 ib2:
-     is_seq ib1 = false ->
-     is_right_assoc ib1 ->
-     is_right_assoc ib2 -> 
-     is_right_assoc (Bseq ib1 ib2)
- | ira_Bcond cond args ib1 ib2 i:
-     is_right_assoc ib1 ->
-     is_right_assoc ib2 -> 
-     is_right_assoc (Bcond cond args ib1 ib2 i)
- | ira_others ib:
-     is_atom ib = true ->
-     is_right_assoc ib
-     .
-Local Hint Constructors is_right_assoc: core.
-
-Fixpoint right_assoc (ib: iblock): iblock :=
-  match ib with
-  | Bseq ib1 ib2 => rec_rotate ib1 (right_assoc ib2)
-  | Bcond cond args ib1 ib2 i => 
-     Bcond cond args (right_assoc ib1) (right_assoc ib2) i
-  | ib => ib
-  end
-with rec_rotate (ib: iblock) rem: iblock :=
-  match ib with
-  | Bseq ib1 ib2 => 
-     rec_rotate ib1 (rec_rotate ib2 rem)
-  | Bcond cond args ib1 ib2 i => 
-     Bseq (Bcond cond args (right_assoc ib1) (right_assoc ib2) i) rem
-  | ib => Bseq ib rem
-end.
-
-Lemma right_assoc_rec_rotate_correct ib:
-    is_right_assoc (right_assoc ib)
- /\ (forall rem, is_right_assoc rem -> is_right_assoc (rec_rotate ib rem)).
-Proof.
-  induction ib; simpl; intuition.
-Qed.
-
-Lemma right_assoc_correct ib:
-  is_right_assoc (right_assoc ib).
-Proof.
-  destruct (right_assoc_rec_rotate_correct ib); auto.
-Qed.
-
-Definition right_assoc_code (cfg: code): code :=
-  (PTree.map (fun _ ib => {| entry:=right_assoc ib.(entry); input_regs := ib.(input_regs) |}) cfg).
-
-Lemma right_assoc_code_correct cfg pc ib :
-  (right_assoc_code cfg)!pc=Some ib -> is_right_assoc (ib.(entry)).
-Proof.
-  unfold right_assoc_code.
-  rewrite PTree.gmap.
-  destruct (cfg!pc); simpl; intros; try_simplify_someHyps.
-  apply right_assoc_correct; auto.
-Qed.
-
-- 
cgit