1 files changed, 14 insertions, 0 deletions
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 478ce251..b1cac124 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -44,6 +44,7 @@ Require Import Floats.
 Require Import Op.
 Require Import CminorSel.
 Require Import OpHelpers.
+Require Archi.
 
 Local Open Scope cminorsel_scope.
 
@@ -517,6 +518,19 @@ Definition singleofintu (e: expr) :=
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
+(** ** Selection *)
+
+Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
+  if match ty with
+     | Tint => true
+     | Tfloat => true
+     | Tsingle => true
+     | Tlong => Archi.ppc64
+     | _ => false
+     end
+  then Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
+  else None.
+
 (** ** Recognition of addressing modes for load and store operations *)
 
 Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=