diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-07-25 14:29:28 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-07-25 14:29:28 +0200 |
| commit | 98c22a6f37c7230faf80b6366aaa1c2476f9e67c (patch) | |
| tree | e18195ce1ee65b69c67f05e8dac87d0250cc94c7 /mppa_k1c/PostpassSchedulingOracle.ml | |
| parent | 4ee5d47c502e05deed69eb8ddf183384a86ffd05 (diff) | |
| download | compcert-kvx-98c22a6f37c7230faf80b6366aaa1c2476f9e67c.tar.gz compcert-kvx-98c22a6f37c7230faf80b6366aaa1c2476f9e67c.zip | |
(#139) - Mise à jour du code Coq, oracle
Diffstat (limited to 'mppa_k1c/PostpassSchedulingOracle.ml')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 14 |
1 files changed, 11 insertions, 3 deletions
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 |