diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 21:58:53 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 21:58:53 +0100 |
| commit | fc3c1660ee62b5341ccf75505aa63dca0d2cf16c (patch) | |
| tree | 0ce595db7e1a38db12f17ec25eb4329598f0f2a2 /backend/CSE3analysis.v | |
| parent | ab3f3a52c8737dbad6c599d7afc5720346e00abe (diff) | |
| download | compcert-kvx-fc3c1660ee62b5341ccf75505aa63dca0d2cf16c.tar.gz compcert-kvx-fc3c1660ee62b5341ccf75505aa63dca0d2cf16c.zip | |
get moves
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index f0af0ac7..da527995 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -119,21 +119,12 @@ Proof. - right; congruence. Qed. -Definition get_move (eq : equation) := - if is_smove (eq_op eq) - then match eq_args eq with - | h::nil => Some h - | _ => None - end - else None. - Definition get_moves (eqs : PTree.t equation) : Regmap.t PSet.t := PTree.fold (fun already (eqno : eq_id) (eq : equation) => - match get_move eq with - | Some rhs => add_i_j (eq_lhs eq) rhs already - | None => already - end) eqs (PMap.init PSet.empty). + if is_smove (eq_op eq) + then add_i_j (eq_lhs eq) eqno already + else already) eqs (PMap.init PSet.empty). Record eq_context := mkeqcontext { eq_catalog : node -> option equation; |