From 99d5c85e5595799519e6541947f907a892935e4f Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Thu, 7 Feb 2019 17:47:00 +0100
Subject: Un peu de refactorisation

---
 mppa_k1c/PostpassScheduling.v | 87 ++++++++++++++++++++++++++++++++-----------
 1 file changed, 65 insertions(+), 22 deletions(-)

(limited to 'mppa_k1c/PostpassScheduling.v')

diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index e8e6fcc5..11e53a5d 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -21,10 +21,56 @@ Axiom schedule: bblock -> list bblock.
 
 Extract Constant schedule => "PostpassSchedulingOracle.schedule".
 
-(* TODO: refactorisation.
-
-... concat2 ...
-
+(* Lemmas necessary for defining concat_all *)
+Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil.
+Proof.
+  intros. destruct l; simpl.
+  - contradiction.
+  - discriminate.
+Qed.
+
+Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil.
+Proof.
+  destruct l.
+  - intros. simpl; auto.
+  - intros. rewrite <- app_comm_cons. discriminate.
+Qed.
+
+Definition check_size bb :=
+  if zlt Ptrofs.max_unsigned (size bb)
+    then Error (msg "PostpassSchedulingproof.check_size")
+  else OK tt.
+
+Program Definition concat2 (bb bb': bblock) : res bblock :=
+  do ch <- check_size bb;
+  do ch' <- check_size bb';
+  match (exit bb) with
+  | None => 
+      match (header bb') with
+      | nil => 
+          match (exit bb') with 
+          | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone")
+          | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |}
+          end
+      | _ => Error (msg "PostpassSchedulingproof.concat2")
+      end
+  | _ => Error (msg "PostpassSchedulingproof.concat2")
+  end.
+Next Obligation.
+  apply wf_bblock_refl. constructor.
+  - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *.
+    apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF.
+    inversion_clear WF'. inversion_clear WF. clear H1 H3.
+    inversion H2; inversion H0.
+    + left. apply app_nonil. auto.
+    + right. auto.
+    + left. apply app_nonil2. auto.
+    + right. auto.
+  - unfold builtin_alone. intros. rewrite H0 in H.
+    assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))).
+    apply (H ef args res). contradict H1. auto.
+Qed.
+
 Fixpoint concat_all (lbb: list bblock) : res bblock :=
   match lbb with
   | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list")
@@ -34,25 +80,22 @@ Fixpoint concat_all (lbb: list bblock) : res bblock :=
       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").
+Definition verify_schedule (bb bb' : bblock) : res unit := OK tt.
 
-*)
-
-(* TODO - implement the verificator *)
-Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb).
+Program Definition verified_schedule (bb : bblock) : res (list bblock) :=
+  let bb' := {| header := nil; body := body bb; exit := exit bb |} in
+  let lbb := schedule bb' in
+  do tbb <- concat_all lbb;
+  do check <- verify_schedule bb' tbb;
+  match (head lbb) with
+  | None => Error (msg "PostpassScheduling.verified_schedule: empty schedule")
+  | Some fst => OK ({| header := header bb; body := body fst; exit := exit fst |} :: tail lbb)
+  end.
+Next Obligation.
+  destruct bb; simpl. assumption.
+Qed. Next Obligation.
+  destruct fst; simpl. assumption.
+Qed.
 
 Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
   match lbb with
-- 
cgit