diff options
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/BTL_SEimpl.v | 16 |
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 |