Added definitions and proof sketch for PostpassScheduling

1 files changed, 19 insertions, 15 deletions

diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 8ec72f90..381e1214 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -10,29 +10,33 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require Import Coqlib Errors AST.
 Require Import Asmblock.
 
+Local Open Scope error_monad_scope.
+
 (** Oracle taking as input a basic block,
-    returns a basic block with its instruction reordered *)
+    returns a basic block with its instructions reordered *)
 Axiom schedule: bblock -> bblock.
 
-(** Oracle taking as input a basic block
-    splits it into several bblocks (representing bundles *)
-Axiom split: bblock -> list bblock.
-
-(* TODO - separate the postpass_schedule in two phases *)
+(* TODO - implement the verificator *)
+Definition transf_block (b : bblock) : res bblock := OK (schedule b).
 
-Definition postpass_schedule (lb : list bblock) : list bblock :=
+Fixpoint transf_blocks (lb : list bblock) : res (list bblock) :=
   match lb with
-  | nil => nil
-  | (cons b lb) => split (schedule b) ++ lb
+  | nil => OK nil
+  | (cons b lb) =>
+      do lb' <- transf_blocks lb;
+      do b' <- transf_block b;
+      OK (b' :: lb')
   end.
 
-Definition transf_function (f: function) : function :=
-  mkfunction (fn_sig f) (postpass_schedule (fn_blocks f)).
+Definition transf_function (f: function) : res function :=
+  do lb <- transf_blocks (fn_blocks f);
+  OK (mkfunction (fn_sig f) lb).
 
-Definition transf_fundef (f: fundef) : fundef :=
-  AST.transf_fundef transf_function f.
+Definition transf_fundef (f: fundef) : res fundef :=
+  transf_partial_fundef transf_function f.
 
-Definition transf_program (p: program) : program :=
-  AST.transform_program transf_fundef p.
\ No newline at end of file
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.
\ No newline at end of file