// http://llvm.org/docs/LangRef.html#extractvalue-instr
// keywords: aggregate; instr

.type ExtractValueInstruction <: symbol
.decl extractvalue_instr(instr:ExtractValueInstruction)

instr(v) :- extractvalue_instr(v).

.decl extractvalue_instr_base(instr:ExtractValueInstruction, aggregate:Operand)

//------------------------
// Aggregate Indices
//------------------------

.decl extractvalue_instr_nindices(instr:ExtractValueInstruction, total:number)
.decl extractvalue_instr_index(instr:ExtractValueInstruction, i:number, idx:number)

instr_successor_index(Instr, Index, Index + 1) :-
   extractvalue_instr_index(Instr, Index, _).


//------------------------------------------------
// The resulting type for each dereference.
//------------------------------------------------

.decl extractvalue_instr_base_type(instr:ExtractValueInstruction, type:Type)
.decl extractvalue_instr_value_type(instr:ExtractValueInstruction, type:Type)
.decl extractvalue_instrterm_type(instr:ExtractValueInstruction, i:number, type:Type)

extractvalue_instrterm_type(Instr, 0, Type) :-
   extractvalue_instr_base(Instr, Aggregate),
   operand_has_type(Aggregate, Type).

extractvalue_instrterm_type(Instr, NextIndex, Type) :-
   extractvalue_instrterm_type(Instr, Index, StructType),
   extractvalue_instr_index(Instr, Index, IdxValue),
   struct_type_field(StructType, IdxValue, Type),
   instr_successor_index(Instr, Index, NextIndex).

extractvalue_instrterm_type(Instr, NextIndex, Type) :-
   extractvalue_instrterm_type(Instr, Index, ArrayType),
   array_type_has_component(ArrayType, Type),
   instr_successor_index(Instr, Index, NextIndex).

extractvalue_instr_value_type(Instr, Type) :-
   extractvalue_instr_nindices(Instr, Total),
   extractvalue_instrterm_type(Instr, Total, Type).

extractvalue_instr_base_type(Instr, Type) :-
   extractvalue_instrterm_type(Instr, 0, Type).


//------------------------------------------------------------------------------
// [Constraints]
//
//  (1) The first operand of an ‘extractvalue‘ instr is
//      a value of struct or array type.
//  (2) At least one index must be specified.
//
// The result is the value at the position in the aggregate specified
// by the index operands.
//------------------------------------------------------------------------------

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   extractvalue_instr(Instr),
   !extractvalue_instr_base(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   extractvalue_instr(Instr),
   !extractvalue_instr_nindices(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   extractvalue_instr(Instr),
   !extractvalue_instr_index(Instr, 0, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   extractvalue_instr_base_type(Instr, BaseType),
   !aggregate_type(BaseType).   // c1

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   extractvalue_instr_nindices(Instr, Total),
   Total <= 0.                  // c2

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   extractvalue_instr_value_type(Instr, Type),
   !instr_returns_type(Instr, Type). // creturn
