diff options
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 8b7f1190..84f4a426 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -160,6 +160,20 @@ Proof. decide equality. Defined. +Record condition_fact := + mkcondition_fact + { cond_op : condition ; + cond_args : list reg }. + +Definition eq_dec_condition_fact : + forall cf cf' : condition_fact, {cf = cf'} + {cf <> cf'}. +Proof. + generalize peq. + generalize eq_condition. + generalize eq_dec_args. + decide equality. +Defined. + Definition eq_id := node. Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := |