op simplify BTL intro

1 files changed, 7 insertions, 9 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index d6cdff59..3050f2e2 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -2,6 +2,7 @@ Require Import Coqlib AST Maps.
 Require Import Op Registers.
 Require Import RTL BTL Errors.
 Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.
+Require Import BTL_SEsimplify.
 
 Require Import Impure.ImpHCons.
 Import Notations.
@@ -587,14 +588,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
      match is_move_operation op lr with
      | Some arg => hrs_sreg_get hrs arg (* optimization of Omove *)
      | None =>
-         DO lsv <~ hlist_args hrs lr;;
-         hSop op lsv
-        (* TODO gourdinl
        match target_op_simplify op lr hrs with
        | Some fsv => fsval_proj fsv
        | None =>
-         hSop op lhsv
-           end*)
+        DO lhsv <~ hlist_args hrs lr;;
+        hSop op lhsv
+        end
      end
   | Rload _ chunk addr => 
        DO lsv <~ hlist_args hrs lr;;
@@ -665,15 +664,14 @@ Proof.
 Qed.
 
 Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ?? (condition * list_sval) :=
-  (* TODO gourdinl  
   match target_cbranch_expanse prev cond args with
     | Some (cond', vargs) => 
       DO vargs' <~ fsval_list_proj vargs;;
       RET (cond', vargs')
-     | None =>*)
+     | None =>
       DO vargs <~ hlist_args prev args ;;
-      RET (cond, vargs).
-    (*end.*)
+      RET (cond, vargs)
+  end.
 
 Lemma cbranch_expanse_correct hrs c l:
  WHEN cbranch_expanse hrs c l ~> r THEN forall ctx sis