diff options
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index ee614253..8101a9b0 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -66,10 +66,11 @@ Section SELECT. Context {hf: helper_functions}. (** Ternary operator *) -(** TODO *) +Definition select0 (ty : typ) (cond0 : condition0) (e1 e2 eC: expr) := + (Eop (Osel cond0 ty) (e1 ::: e2 ::: eC ::: Enil)). + Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr := - Some (Eop (Osel (Ccomp0 Cne) ty) (e1 ::: e2 ::: - (Eop (Ocmp cond) args) ::: Enil)). + Some (select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)). (** ** Constants **) |