diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 15:13:04 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 15:13:04 +0100 |
| commit | 87ccbf33d3c478f9894abcda8bc7c73b9cb7b5b4 (patch) | |
| tree | ccf75c0da126f6428618de3d3f9164e158f2f6f6 /mppa_k1c/SelectOp.vp | |
| parent | 397cefa66b6b56818bd7602e349f98de9a74491b (diff) | |
| download | compcert-kvx-87ccbf33d3c478f9894abcda8bc7c73b9cb7b5b4.tar.gz compcert-kvx-87ccbf33d3c478f9894abcda8bc7c73b9cb7b5b4.zip | |
more on ternary
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 0dad482b..65364579 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -62,11 +62,11 @@ Section SELECT. Context {hf: helper_functions}. (** Stuff for select *) -Definition is_zero_expr (vt : expr) : expr := +Definition is_zero (vt : expr) : expr := Eop (Ocmp (Ccomp Ceq)) (vt:::(Eop (Ointconst Int.zero) Enil):::Enil). -Definition is_nonzero_expr (vt : expr) : expr := +Definition is_nonzero (vt : expr) : expr := Eop (Ocmp (Ccomp Cne)) (vt:::(Eop (Ointconst Int.zero) Enil):::Enil). @@ -76,14 +76,14 @@ Definition bool_to_bitmask (et : expr) : expr := Definition not_bool_to_bitmask (et : expr) : expr := Eop Osub (et:::(Eop (Ointconst Int.one) Enil):::Enil). -Definition ternary_expand (et e0 e1 : expr) : expr := +Definition ternary_expand (e0 e1 et : expr) : expr := Eop Oor ((Eop Oand ((not_bool_to_bitmask et):::e1:::Enil))::: (Eop Oand ((bool_to_bitmask et):::e0:::Enil))::: Enil). -Definition select_or_expand (et e0 e1 : expr) : expr := - ternary_expand (is_nonzero_expr et) e0 e1. +Definition select_or_expand (e0 e1 et: expr) : expr := + ternary_expand e0 e1 (is_zero et). (** ** Constants **) |