From 98c22a6f37c7230faf80b6366aaa1c2476f9e67c Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Thu, 25 Jul 2019 14:29:28 +0200
Subject: (#139) - Mise à jour du code Coq, oracle
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mppa_k1c/PostpassSchedulingOracle.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'mppa_k1c/PostpassSchedulingOracle.ml')

diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index fd03a80c..40f1d9c7 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -961,10 +961,18 @@ let smart_schedule bb =
       in bundles @ (f lbb)
   in f lbb
 
-(** Called schedule function from Coq *)
-
-let schedule bb = 
+let bblock_to_bundles bb =
   if debug then (eprintf "###############################\n"; Printf.eprintf "SCHEDULING\n"; print_bb stderr bb);
   (* print_problem (build_problem bb); *)
   if Compopts.optim_postpass () then smart_schedule bb else dumb_schedule bb
 
+(** To deal with the Coq Axiom schedule : bblock -> (list (list basic)) * option control *)
+
+let rec bundles_to_coq_schedule = function
+  | [] -> ([], None)
+  | bb :: [] -> ([bb.body], bb.exit)
+  | bb :: lbb -> let (llb, oc) = bundles_to_coq_schedule lbb in (bb.body :: llb, oc)
+
+(** Called schedule function from Coq *)
+
+let schedule bb = let toto = bundles_to_coq_schedule @@ bblock_to_bundles bb in toto
-- 
cgit