From d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Wed, 26 May 2021 21:42:33 +0200
Subject: end of BTL_SEtheory w.r.t fsem

---
 scheduling/BTL.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 5f75231a..6f699cd0 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -391,10 +391,11 @@ Definition semantics (p: program) :=
 (** The "functional" small-step semantics for a BTL program. 
     at each exit, we only transfer register in "input_regs" (i.e. "alive" registers).
 *)
-
 Definition transfer_regs (inputs: list reg) (rs: regset): regset :=
   init_regs (rs##inputs) inputs.
 
+(* TODO: LEMMA BELOW ON transfer_regs USEFUL ? *)
+
 Lemma transfer_regs_inputs inputs rs r:
   List.In r inputs -> (transfer_regs inputs rs)#r = rs#r.
 Proof.
@@ -456,6 +457,9 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t
 Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset 
   := transfer_regs (Regset.elements (inputs_exit f tbl or)).
 
+(* TODO: BELOW, LEMMA on tr_inputs USEFUL ? *)
+
+
 (* TODO: move this elsewhere *)
 Lemma SetoidList_InA_eq_equiv A (l: list A): forall x,
   SetoidList.InA (fun x y => x = y) x l <-> List.In x l.
@@ -518,6 +522,7 @@ Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: fina
 Definition tr_regs: function -> final -> regset -> regset :=
   poly_tr tr_inputs.
 
+(* TODO: NOT USEFUL ?
 Definition liveout: function -> final -> Regset.t :=
   poly_tr inputs_exit.
 
@@ -533,7 +538,7 @@ Proof.
    Local Opaque inputs_exit.
    destruct fi; simpl; auto.
 Qed.
-
+*)
 
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
 
-- 
cgit