From 51ec982b84851ac3526a0cb3f22e41f974b2d592 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 24 May 2021 22:41:35 +0200
Subject: tiny simplifications in RTLtoBTLproof

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

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 0f9ef44f..97c54021 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -810,94 +810,4 @@ Definition is_goto (ib: iblock): bool :=
   match ib with
   | BF (Bgoto _) _ => true
   | _ => false
-  end.
-
-Definition is_RTLatom (ib: iblock): bool :=
- match ib with
- | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false 
- | _ => true
- end.
-
-Definition Bnop_dec k: { k=Bnop None} + { k<>(Bnop None) }.
-Proof.
-  destruct k; simpl; try destruct oiinfo;
-  intuition congruence.
-Defined.
-
-(** Is expand property to only support atomic instructions on the left part of a Bseq:
-   The tree is right-expanded, and block are normalized to simplify RTL simulation *)
-Inductive is_expand: iblock -> Prop :=
-  | exp_Bseq ib1 ib2:
-     is_RTLatom ib1 = true ->
-     is_expand ib2 -> 
-     is_expand (Bseq ib1 ib2)
-  | exp_Bcond cond args ib1 ib2 i:
-     is_expand ib1 ->
-     is_expand ib2 -> 
-     is_expand (Bcond cond args ib1 ib2 i)
-  | exp_others ib:
-     is_RTLatom ib = true ->
-     is_expand ib
-     .
-Local Hint Constructors is_expand: core.
-
-(** The weak version with more specific hypothesis for conditions *)
-Inductive is_wexpand: iblock -> Prop :=
-  | wexp_Bseq ib1 ib2:
-     is_RTLatom ib1 = true ->
-     is_wexpand ib2 -> 
-     is_wexpand (Bseq ib1 ib2)
-  | wexp_Bcond cond args ib1 ib2 iinfo:
-     (ib1 <> Bnop None -> is_wexpand ib1) ->
-     (ib2 <> Bnop None -> is_wexpand ib2) ->
-     is_wexpand (Bcond cond args ib1 ib2 iinfo)
-  | wexp_others ib:
-     is_RTLatom ib = true ->
-     is_wexpand ib
-     .
-Local Hint Constructors is_wexpand: core.
-
-Fixpoint normRTL (ib: iblock) (k: iblock): iblock :=
-  match ib with
-  | Bseq ib1 ib2 => normRTL ib1 (normRTL ib2 k)
-  | Bcond cond args ib1 ib2 iinfo => 
-     Bcond cond args (normRTL ib1 k) (normRTL ib2 k) iinfo
-  | BF fin iinfo => BF fin iinfo
-  | Bnop None => k
-  | ib =>
-      if Bnop_dec k then ib else Bseq ib k
-  end.
-
-Lemma normRTL_correct ib: forall k,
-  (k <> (Bnop None) -> is_wexpand k) ->
-  (normRTL ib k) <> Bnop None ->
-  is_wexpand (normRTL ib k).
-Proof.
-  induction ib; simpl; intros; try autodestruct; auto.
-  intros; destruct (Bnop_dec k); auto.
-Qed.
-
-Lemma is_join_opt_None {A} (opc1 opc2: option A): 
-  is_join_opt opc1 opc2 None -> opc1 = None /\ opc2 = None.
-Proof.
-  intros X. inv X; auto.
-Qed.
-
-Lemma match_iblock_None_not_Bnop dupmap cfg isfst pc ib: 
-  match_iblock dupmap cfg isfst pc ib None -> ib <> Bnop None.
-Proof.
-  intros X; inv X; try congruence.
-Qed.
-Local Hint Resolve match_iblock_None_not_Bnop: core.
-
-Lemma is_wexpand_expand dupmap cfg ib:
-  is_wexpand ib ->
-  forall isfst pc
-  (MIB: match_iblock dupmap cfg isfst pc ib None),
-  is_expand ib.
-Proof.
-  induction 1; simpl; intros; auto; try (inv MIB); eauto.
-  (* Bcond *)
-  destruct (is_join_opt_None opc1 opc2); subst; eauto.
-  econstructor; eauto.
-Qed.
+  end.
\ No newline at end of file
-- 
cgit