From 464da1ee7861e0d51f6c5dc786907a66b0f46e35 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Thu, 31 Jan 2019 15:01:01 +0100
Subject: idee de refactoring

---
 mppa_k1c/PostpassScheduling.v | 78 ++++++++++++++++++++++++++++++-------------
 1 file changed, 54 insertions(+), 24 deletions(-)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 1483a5d7..e8e6fcc5 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -21,30 +21,60 @@ Axiom schedule: bblock -> list bblock.
 
 Extract Constant schedule => "PostpassSchedulingOracle.schedule".
 
-(* TODO - implement the verificator *)
-Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb).
+(* TODO: refactorisation.
 
-Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
-  match lbb with
-  | nil => OK nil
-  | (cons bb lbb) =>
-      do tlbb <- transf_blocks lbb;
-      do tbb <- verified_schedule bb;
-      OK (tbb ++ tlbb)
-  end.
+... concat2 ...
 
-Definition transl_function (f: function) : res function :=
-  do lb <- transf_blocks (fn_blocks f); 
-  OK (mkfunction (fn_sig f) lb).
-
-Definition transf_function (f: function) : res function :=
-  do tf <- transl_function f;
-  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
-  then Error (msg "code size exceeded")
-  else OK tf.
-
-Definition transf_fundef (f: fundef) : res fundef :=
-  transf_partial_fundef transf_function f.
-
-Definition transf_program (p: program) : res program :=
+Fixpoint concat_all (lbb: list bblock) : res bblock :=
+  match lbb with
+  | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list")
+  | bb::nil => OK bb
+  | bb::lbb =>
+      do bb' <- concat_all lbb;
+      concat2 bb bb'
+  end.
+
+Axiom test_equiv_bblock: bblock -> bblock -> bool.
+
+Axiom test_equiv_bblock_correct:
+  forall ge f bb tbb,
+  test_equiv bb tbb = true ->
+  bblock_equiv ge f bb tbb.
+
+Definition verified_schedule (bb : bblock) : res (list bblock) := 
+  DO lbb <- (schedule bb) ;
+  DO tbb <- (concat lbb) ;
+  DO res <- test_equiv_bblock bb tbb ;
+  if res 
+  then OK lbb
+  else Error (msg "blah").
+
+*)
+
+(* TODO - implement the verificator *)
+Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb).
+
+Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
+  match lbb with
+  | nil => OK nil
+  | (cons bb lbb) =>
+      do tlbb <- transf_blocks lbb;
+      do tbb <- verified_schedule bb;
+      OK (tbb ++ tlbb)
+  end.
+
+Definition transl_function (f: function) : res function :=
+  do lb <- transf_blocks (fn_blocks f); 
+  OK (mkfunction (fn_sig f) lb).
+
+Definition transf_function (f: function) : res function :=
+  do tf <- transl_function f;
+  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
+  then Error (msg "code size exceeded")
+  else OK tf.
+
+Definition transf_fundef (f: fundef) : res fundef :=
+  transf_partial_fundef transf_function f.
+
+Definition transf_program (p: program) : res program :=
   transform_partial_program transf_fundef p.
\ No newline at end of file
-- 
cgit