// http://llvm.org/docs/LangRef.html#shufflevector-instr
// keywords: vector; instr

.type ShuffleVectorInstruction <: symbol
.decl shufflevector_instr(instr:ShuffleVectorInstruction)

instr(v) :- shufflevector_instr(v).

.decl shufflevector_instr_first_vector(instr:ShuffleVectorInstruction, vector:Operand)
.decl shufflevector_instr_second_vector(instr:ShuffleVectorInstruction, vector:Operand)
.decl shufflevector_instr_mask(instr:ShuffleVectorInstruction, mask:Constant)


// Helper Predicates

.decl shufflevector_instrput_type(instr:ShuffleVectorInstruction, type:Type)
.decl shufflevector_instr_element_type(instr:ShuffleVectorInstruction, type:Type)
.decl shufflevector_instr_mask_type(instr:ShuffleVectorInstruction, type:Type)

// The type of the two input vectors.
shufflevector_instrput_type(Instr, Type) :-
   shufflevector_instr_first_vector(Instr, Vector),
   operand_has_type(Vector, Type).

// The element type of the two input vectors
shufflevector_instr_element_type(Instr, ElementType) :-
   shufflevector_instrput_type(Instr, VectorType),
   vector_type_has_component(VectorType, ElementType).

// The type of the shuffle mask.
shufflevector_instr_mask_type(Instr, MaskType) :-
   shufflevector_instr_mask(Instr, Mask),
   constant_has_type(Mask, MaskType).


//------------------------------------------------------------------------------
// [Constraints]
//
// 1. The 'shufflevector' instr takes three arguments:
//  (i)  two vectors of the same type, and
//  (ii) a shuffle mask argument.
//
// 2. The shuffle mask is required to be:
//  (i) a constant vector
//  (ii) with i32-integer component type.
//
// 3. The result is a vector
//  (i)  whose length is the same as the shuffle mask and
//  (ii) whose element type is the same as the element type of the first
//       two operands.
//------------------------------------------------------------------------------


// 1a. Required arguments

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   shufflevector_instr(Instr),
   !shufflevector_instr_first_vector(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   shufflevector_instr(Instr),
   !shufflevector_instr_second_vector(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   shufflevector_instr(Instr),
   !shufflevector_instr_mask(Instr, _).


// 1b. Constraints on the two input vectors

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   shufflevector_instr(Instr),
   shufflevector_instrput_type(Instr, InputType),
   shufflevector_instr_first_vector(Instr, FirstVector),
   operand_has_type(FirstVector, FirstVectorType),
   FirstVectorType != InputType.

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   shufflevector_instr(Instr),
   shufflevector_instrput_type(Instr, InputType),
   shufflevector_instr_second_vector(Instr, SecondVector),
   operand_has_type(SecondVector, SecondVectorType),
   SecondVectorType != InputType.

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   shufflevector_instrput_type(Instr, InputType),
   !vector_type(InputType).


// 2. Constraints on the suffle mask

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   shufflevector_instr_mask_type(Instr, MaskType),
   !int32_vector_type(MaskType).


// 3. Constraints on the result

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   shufflevector_instr_mask_type(Instr, MaskType),
   instr_returns_type(Instr, OutputType),
   !vector_compatible_types(OutputType, MaskType).      // constraint 3.i

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   shufflevector_instr_element_type(Instr, ElementType),
   instr_returns_type(Instr, OutputType),
   !vector_type_has_component(OutputType, ElementType). // constraint 3.ii
