//--------------------------------------------------------------------
// [Constant and Constant Expression Hierarchy]
//--------------------------------------------------------------------

.type Constant
  = IntegerConstant
  | FPConstant
  | NullPtrConstant
  | FunctionConstant
  | GlobalVariableConstant
  | ConstantArray
  | ConstantStruct
  | ConstantVector
  | ConstantExpression

.type IntegerConstant <: symbol
.type FPConstant <: symbol
.type NullPtrConstant <: symbol
.type FunctionConstant <: symbol
.type GlobalVariableConstant <: symbol
.type ConstantArray <: symbol
.type ConstantStruct <: symbol
.type ConstantVector <: symbol

.type ConstantExpression
  = BitcastConstantExpression
  | IntToPtrConstantExpression
  | PtrToIntConstantExpression
  | GetElementPtrConstantExpression

.type BitcastConstantExpression <: symbol
.type IntToPtrConstantExpression <: symbol
.type PtrToIntConstantExpression <: symbol
.type GetElementPtrConstantExpression <: symbol

.decl integer_constant(c:IntegerConstant)
.decl fp_constant(c:FPConstant)
.decl nullptr_constant(c:NullPtrConstant)
.decl func_constant(c:FunctionConstant)
.decl global_var_constant(c:GlobalVariableConstant)
.decl constant_array(c:ConstantArray)
.decl constant_struct(c:ConstantStruct)
.decl constant_vector(c:ConstantVector)
.decl constant_expression(c:ConstantExpression)
.decl bitcast_constant_expression(c:BitcastConstantExpression)
.decl inttoptr_constant_expression(c:IntToPtrConstantExpression)
.decl ptrtoint_constant_expression(c:PtrToIntConstantExpression)
.decl getelementptr_constant_expression(c:GetElementPtrConstantExpression)


constant(c) :-
   constant_expression(c)
 ; constant_array(c)
 ; constant_struct(c)
 ; global_var_constant(c)
 ; integer_constant(c)
 ; fp_constant(c)
 ; nullptr_constant(c)
 ; func_constant(c)
 ; undef_constant(c)
 ; poison_constant(c). // technically redundant - poison constants are also undef

constant_expression(c) :-
   bitcast_constant_expression(c)
 ; inttoptr_constant_expression(c)
 ; ptrtoint_constant_expression(c)
 ; getelementptr_constant_expression(c).

constant_in_func(Constant, Function) :-
   constant_in_func_name(Constant, FuncName),
   func_name(Function, FuncName).

//--------------------------------------
// Constant that references func
//--------------------------------------

.decl func_constant_fn_name(fc:FunctionConstant, name:symbol)

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   func_constant(Constant),
   !func_constant_fn_name(Constant, _).


//---------------------------------------------
// Constant that references global variable
//---------------------------------------------

.decl global_var_constant_name(c:GlobalVariableConstant, name:symbol)
.decl global_var_constant_reference(c:GlobalVariableConstant, gv:GlobalVariable)

global_var_constant_reference(C, GVar) :-
   global_var_constant_name(C, Name),
   global_var_name(GVar, Name).

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   global_var_constant(Constant),
   !global_var_constant_name(Constant, _).

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   global_var_constant(Constant),
   !global_var_constant_reference(Constant, _).

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   global_var_constant(Constant),
   global_var_constant_reference(Constant, GVar),
   global_var_type(GVar, Type),
   constant_has_type(Constant, PtrType),
   !pointer_type_has_component(PtrType, Type).


//--------------------------------------
// Array of constants
//--------------------------------------

.decl constant_array_index(c:ConstantArray, i:number, ic:Constant)
.decl constant_array_has_size(c:ConstantArray, size:number)

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   constant_array(Constant),
   !constant_array_has_size(Constant, _).


//--------------------------------------
// Constant Struct
//--------------------------------------

.decl constant_struct_index(c:ConstantStruct, i:number, ic:Constant)
.decl constant_struct_has_size(c:ConstantStruct, size:number)

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   constant_struct(Constant),
   !constant_struct_has_size(Constant, _).


//--------------------------------------
// Constant Vector
//--------------------------------------

.decl constant_vector_index(c:ConstantVector, i:number, ic:Constant)
.decl constant_vector_has_size(c:ConstantVector, size:number)

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   constant_vector(Constant),
   !constant_vector_has_size(Constant, _).

//--------------------------------------
// Undefined Constant
//--------------------------------------

.decl undef_constant(c:Constant)

//--------------------------------------
// Poison Constant
//--------------------------------------

.decl poison_constant(c:Constant)

//--------------------------------------
// Bitcast Constant Expression
//--------------------------------------

.decl bitcast_constant_expression_from(cexpr:BitcastConstantExpression, val:Constant)
.decl bitcast_constant_expression_to_type(cexpr:BitcastConstantExpression, type:Type)

bitcast_constant_expression_to_type(CExpr, Type) :-
   bitcast_constant_expression(CExpr),
   constant_has_type(CExpr, Type).

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   bitcast_constant_expression(Constant),
   !bitcast_constant_expression_from(Constant, _).

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   bitcast_constant_expression(Constant),
   !bitcast_constant_expression_to_type(Constant, _).


//--------------------------------------
// Inttoptr Constant Expression
//--------------------------------------

.decl inttoptr_constant_expression_from(cexpr:IntToPtrConstantExpression, val:Constant)

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   inttoptr_constant_expression(Constant),
   !inttoptr_constant_expression_from(Constant, _).


//--------------------------------------
// Ptrtoint Constant Expression
//--------------------------------------

.decl ptrtoint_constant_expression_from(cexpr:IntToPtrConstantExpression, val:Constant)

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   ptrtoint_constant_expression(Constant),
   !ptrtoint_constant_expression_from(Constant, _).


//--------------------------------------------
// Get Element Pointer  Constant Expression
//--------------------------------------------

.decl getelementptr_constant_expression_base(cexpr:GetElementPtrConstantExpression, base:Constant)
.decl getelementptr_constant_expression_index(cexpr:GetElementPtrConstantExpression, i:GepIndex, c:Constant)
.decl getelementptr_constant_expression_nindices(cexpr:GetElementPtrConstantExpression, size:number)


schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   getelementptr_constant_expression(Constant),
   !getelementptr_constant_expression_nindices(Constant, _).

schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   getelementptr_constant_expression(Constant),
   !getelementptr_constant_expression_base(Constant, _).


// Auxiliary type predicates
.decl _getelementptr_constant_expression_base_type(cexpr:GetElementPtrConstantExpression, type:Type)
.decl _getelementptr_constant_expression_index_type(cexpr:GetElementPtrConstantExpression, type:Type)
.decl _getelementptr_constant_expression_value_type(cexpr:GetElementPtrConstantExpression, type:Type)
.decl _getelementptr_constant_expression_interm_type(cexpr:GetElementPtrConstantExpression, i:number, type:Type)

_getelementptr_constant_expression_base_type(CExpr, PtrType) :-
   getelementptr_constant_expression_base(CExpr, BaseConstant),
   constant_has_type(BaseConstant, PtrType).

_getelementptr_constant_expression_index_type(CExpr, Type) :-
   getelementptr_constant_expression_index(CExpr, _, IdxConstant),
   constant_has_type(IdxConstant, Type).


// Compute next index of each GEP constant expression
.decl _constant_expression_next_index(cexpr:ConstantExpression, i:number, j:number)

_constant_expression_next_index(CExpr, Index, Index + 1) :-
   getelementptr_constant_expression_index(CExpr, Index, _).


// Compute types of GEP constant expression up to some index

_getelementptr_constant_expression_interm_type(CExpr, 1, Type) :-
   getelementptr_constant_expression_base(CExpr, BaseConstant),
   constant_has_type(BaseConstant, PtrType),
   pointer_type_has_component(PtrType, Type).

_getelementptr_constant_expression_interm_type(CExpr, 1, Type) :-
   getelementptr_constant_expression_base(CExpr, BaseConstant),
   constant_has_type(BaseConstant, VectorType),
   vector_type_has_component(VectorType, PtrType),
   pointer_type_has_component(PtrType, Type).

_getelementptr_constant_expression_interm_type(CExpr, NextIndex, Type) :-
   _getelementptr_constant_expression_interm_type(CExpr, Index, ArrayType),
   array_type_has_component(ArrayType, Type),
   _constant_expression_next_index(CExpr, Index, NextIndex).

_getelementptr_constant_expression_interm_type(CExpr, NextIndex, Type) :-
   _getelementptr_constant_expression_interm_type(CExpr, Index, VectorType),
   vector_type_has_component(VectorType, Type),
   _constant_expression_next_index(CExpr, Index, NextIndex).

_getelementptr_constant_expression_interm_type(CExpr, NextIndex, Type) :-
   _getelementptr_constant_expression_interm_type(CExpr, Index, StructType),
   getelementptr_constant_expression_index(CExpr, Index, IdxConstant),
   constant_has_type(IdxConstant, IdxType),
   constant_to_int(IdxConstant, IdxConstantValue),
   int32_type(IdxType),
   struct_type_field(StructType, IdxConstantValue, Type),
   _constant_expression_next_index(CExpr, Index, NextIndex).

_getelementptr_constant_expression_value_type(CExpr, Type) :-
   getelementptr_constant_expression_nindices(CExpr, Total),
   _getelementptr_constant_expression_interm_type(CExpr, Total, Type).


// Additional constraint
schema_invalid_constant(Constant, __FILE__, __LINE__) :-
   schema_sanity(),
   getelementptr_constant_expression(Constant),
   !_getelementptr_constant_expression_value_type(Constant, _).
