1 files changed, 15 insertions, 0 deletions
diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v
new file mode 100644
index 00000000..56e547e5
--- /dev/null
+++ b/mppa_k1c/Peephole.v
@@ -0,0 +1,15 @@
+Require Import Asmvliw.
+
+Definition optimize_body (insns : list basic) := insns.
+
+Program Definition optimize_bblock (bb : bblock) :=
+  let optimized := optimize_body (body bb) in
+  let wf_ok := wf_bblockb optimized (exit bb) in
+  {| header := header bb;
+     body := if wf_ok then optimized else (body bb);
+     exit := exit bb |}.
+Next Obligation.
+  destruct (wf_bblockb (optimize_body (body bb))) eqn:Rwf.
+  - rewrite Rwf. simpl. trivial.
+  - exact (correct bb).
+Qed.