//------------------------------------------------------------------------------
// [Types]
//------------------------------------------------------------------------------

.type Type
  = PrimitiveType
  | IntegerType
  | FPType
  | VoidType
  | LabelType
  | MetadataType
  | DerivedType
.decl type(t:Type)

// Sizes of types in bytes

.decl type_has_size(t:Type, size:Bytes)
.decl type_has_unpadded_size(t:Type, size:Bytes)

// For constraints
.decl schema_invalid_type(type:Type, file:File, line:Line)


//------------------------------------------------------------------------------
// [Primitive Types]
//------------------------------------------------------------------------------

.type PrimitiveType
  = IntegerType
  | FPType
  | VoidType
  | LabelType
  | MetadataType

.type IntegerType <: symbol
.type FPType <: symbol
.type VoidType <: symbol
.type LabelType <: symbol
.type MetadataType <: symbol

.decl primitive_type(type:PrimitiveType)
.decl integer_type(type:IntegerType)
.decl fp_type(type:FPType)
.decl void_type(type:VoidType)
.decl label_type(type:LabelType)
.decl metadata_type(type:MetadataType)
.decl x86mmx_type(type:PrimitiveType)

type(t) :- primitive_type(t).
primitive_type(t) :- integer_type(t).
primitive_type(t) :- fp_type(t).
primitive_type(t) :- void_type(t).
primitive_type(t) :- label_type(t).
primitive_type(t) :- metadata_type(t).
primitive_type(t) :- x86mmx_type(t).


// Standard types as constants

void_type("void").
label_type("label").
metadata_type("metadata").
x86mmx_type("x86mmx").


//------------------------------------------------------------------------------
// [Integer Types] and their selectors
//------------------------------------------------------------------------------

.decl int1_type(type:IntegerType)
.decl int8_type(type:IntegerType)
.decl int32_type(type:IntegerType)
.decl int64_type(type:IntegerType)
.decl boolean_type(type:IntegerType)

integer_type(t) :- int1_type(t).
integer_type(t) :- int8_type(t).
integer_type(t) :- int32_type(t).
integer_type(t) :- int64_type(t).

int1_type("i1").
int8_type("i8").
int32_type("i32").
int64_type("i64").

type_has_size(t, 1) :- int1_type(t).
type_has_size(t, 1) :- int8_type(t).
type_has_size(t, 4) :- int32_type(t).
type_has_size(t, 8) :- int64_type(t).

// Boolean alias
boolean_type(t) :- int1_type(t).

//------------------------------------------------------------------------------
// [Floating Point Types] and their selectors
//------------------------------------------------------------------------------

.decl double_type(type:FPType)
.decl float_type(type:FPType)
.decl half_type(type:FPType)
.decl fp128_type(type:FPType)
.decl x86_fp80_type(type:FPType)
.decl ppc_fp128_type(type:FPType)

fp_type(t) :- double_type(t).
fp_type(t) :- float_type(t).
fp_type(t) :- half_type(t).
fp_type(t) :- fp128_type(t).

double_type("double").
float_type("float").
half_type("half").
fp128_type("fp128").
x86_fp80_type("x86_fp80").
ppc_fp128_type("ppc_fp128").

type_has_size(t, 8) :- double_type(t).
type_has_size(t, 4) :- float_type(t).
type_has_size(t, 2) :- half_type(t).
type_has_size(t, 16) :- fp128_type(t).
type_has_size(t, 10) :- x86_fp80_type(t).
type_has_size(t, 16) :- ppc_fp128_type(t).

//------------------------------------------------------------------------------
// [Derived Types]
//
// keywords: derived; first class; aggregate
// http://llvm.org/docs/LangRef.html#array-type
// http://llvm.org/docs/LangRef.html#func-type
// http://llvm.org/docs/LangRef.html#pointer-type
// http://llvm.org/docs/LangRef.html#structure-type
// http://llvm.org/docs/LangRef.html#vector-type
//------------------------------------------------------------------------------

// Type Hierarchy

.type DerivedType
  = FunctionType
  | PointerType
  | VectorType
  | AggregateType

.type AggregateType
  = ArrayType
  | StructType
  | OpaqueStructType

.type FunctionType <: symbol
.type PointerType <: symbol
.type VectorType <: symbol
.type ArrayType <: symbol

.type StructType
  = TransparentStructType
  | OpaqueStructType

.type TransparentStructType <: symbol
.type OpaqueStructType <: symbol

.decl derived_type(type:DerivedType)
.decl func_type(type:FunctionType)
.decl pointer_type(type:PointerType)
.decl vector_type(type:VectorType)
.decl aggregate_type(type:AggregateType)
.decl array_type(type:ArrayType)
.decl struct_type(type:StructType)
.decl opaque_struct_type(type:OpaqueStructType)

type(t) :- derived_type(t).
derived_type(t) :- func_type(t).
derived_type(t) :- pointer_type(t).
derived_type(t) :- vector_type(t).
derived_type(t) :- aggregate_type(t).
aggregate_type(t) :- array_type(t).
aggregate_type(t) :- struct_type(t).
struct_type(t) :- opaque_struct_type(t).


//----------------------
// First Class Types
//----------------------

.decl type_is_firstclass(type:Type)

type_is_firstclass(Type) :-
   type(Type),
   !func_type(Type),
   !void_type(Type).


//----------------------
// Array type
//----------------------

.decl array_type_has_component(type:ArrayType, comp:Type)
.decl array_type_has_size(type:ArrayType, size:number)

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   array_type(Type),
   !array_type_has_component(Type, _).

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   array_type(Type),
   !array_type_has_size(Type, _).


.decl int8_array_type(type:ArrayType)

int8_array_type(Type) :-
   array_type_has_component(Type, Comp),
   int8_type(Comp).


//----------------------
// Function type
//----------------------

.decl func_type_has_varargs(type:FunctionType)
.decl func_type_return(type:FunctionType, ret:Type)
.decl func_type_param(type:FunctionType, index:ArgumentIndex, param:Type)
.decl func_type_nparams(type:FunctionType, total:number)

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   func_type(Type),
   !func_type_nparams(Type, _).

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   func_type(Type),
   func_type_return(Type, RetType),
   (metadata_type(RetType) ; label_type(RetType)).


//----------------------
// Pointer type
//----------------------

.decl pointer_type_has_component(type:PointerType, comp:Type)
.decl pointer_type_has_addr_space(type:PointerType, addr:number)

.decl integer_pointer_type(type:PointerType)
.decl fp_pointer_type(type:PointerType)
.decl struct_pointer_type(type:PointerType)
.decl array_pointer_type(type:PointerType)
.decl vector_pointer_type(type:PointerType)
.decl pointer_type_to_firstclass(type:PointerType)
.decl pointer_type_base_component(type:PointerType, baseComp:Type)

integer_pointer_type(Type) :-
   pointer_type_has_component(Type, Comp),
   integer_type(Comp).

fp_pointer_type(Type) :-
   pointer_type_has_component(Type, Comp),
   fp_type(Comp).

struct_pointer_type(Type) :-
   pointer_type_has_component(Type, Comp),
   struct_type(Comp).

array_pointer_type(Type) :-
   pointer_type_has_component(Type, Comp),
   array_type(Comp).

vector_pointer_type(Type) :-
   pointer_type_has_component(Type, Comp),
   vector_type(Comp).

pointer_type_to_firstclass(Type) :-
   pointer_type_has_component(Type, Comp),
   type_is_firstclass(Comp).


schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   pointer_type(Type),
   !pointer_type_has_component(Type, _).

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   pointer_type(Type),
   pointer_type_has_component(Type, Comp),
   (void_type(Comp) ; label_type(Comp)).

// Get to the base component
pointer_type_base_component(Type, BaseComp) :-
   pointer_type_has_component(Type, BaseComp),
   !pointer_type(BaseComp).

pointer_type_base_component(Type, BaseComp) :-
   pointer_type_has_component(Type, Comp),
   pointer_type_base_component(Comp,BaseComp).


//----------------------
// Struct type
//----------------------

.decl struct_type_field(type:StructType, index:FieldIndex, field:Type)
.decl struct_type_nfields(type:StructType, total:number)
.decl struct_type_has_name(type:StructType, name:symbol)

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   struct_type(Type),
   !opaque_struct_type(Type),
   !struct_type_nfields(Type, _).

// Byte/bit offset per field
.type SubregionOffset <: number
.decl struct_type_field_offset(type:StructType, index:FieldIndex, offset:SubregionOffset)
.decl struct_type_field_bit_offset(type:StructType, index:FieldIndex, offset:number)

//----------------------
// Vector type
//----------------------

.decl vector_type_has_component(type:VectorType, comp:Type)
.decl vector_type_has_size(type:VectorType, size:number)

.decl integer_vector_type(type:VectorType)
.decl fp_vector_type(type:VectorType)
.decl int32_vector_type(type:VectorType)
.decl boolean_vector_type(type:VectorType)
.decl pointer_vector_type(type:VectorType)

integer_vector_type(Type) :-
   vector_type_has_component(Type, Comp),
   integer_type(Comp).

fp_vector_type(Type) :-
   vector_type_has_component(Type, Comp),
   fp_type(Comp).

int32_vector_type(Type) :-
   vector_type_has_component(Type, Comp),
   int32_type(Comp).

boolean_vector_type(Type) :-
   vector_type_has_component(Type, Comp),
   boolean_type(Comp).

pointer_vector_type(Type) :-
   vector_type_has_component(Type, Comp),
   pointer_type(Comp).


//------------------------------------------------------------------------------
// [Constraints and Vector Compatibiliry]
//
//  (1) A vector type requires a size (number of elements)
//      and a component type.
//  (2) The number of elements is a constant integer value
//      larger than 0.
//  (3) The component type can be any integer or floating point type,
//      or a pointer to these types.
//------------------------------------------------------------------------------

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   vector_type(Type),
   !vector_type_has_component(Type, _).

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   vector_type(Type),
   !vector_type_has_size(Type, _).

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   vector_type(Type),
   vector_type_has_size(Type, Size),
   Size <= 0.

schema_invalid_type(Type, __FILE__, __LINE__) :-
   schema_sanity(),
   vector_type(Type),
   vector_type_has_component(Type, CompType),
   !integer_type(CompType), !fp_type(CompType), !pointer_type(CompType).


//------------------------------------------------------------------------------
// The original version of the constraint contained these two atoms:
//   integer_pointer_type(Comp) ; fp_pointer_type(Comp)
// instead of the single:
//   pointer_type(Comp)
//
// In fact, the LLVM reference manual states that: /elementtype may be
// any integer or floating point type, or a pointer to these types./
//
// However, in practice we have seen that the LLVM IR supports
// pointers to arbitrary types, so we loosened this constaint as
// explained above.
//------------------------------------------------------------------------------


// Helper predicate

.decl eq_size_vector_types(type1:VectorType, type2:VectorType)
.decl eq_size_vector_types_(type1:VectorType, type2:VectorType, type3:VectorType)

eq_size_vector_types(Type1, Type2) :-
   vector_type_has_size(Type1, Size),
   vector_type_has_size(Type2, Size).

eq_size_vector_types_(Type1, Type2, Type3) :-
   vector_type_has_size(Type1, Size),
   vector_type_has_size(Type2, Size),
   vector_type_has_size(Type3, Size).

// Two types are vector-compatible if:
//  (i)  neither is a vector, or
//  (ii) both are vectors of the same size.

.decl vector_compatible_types(type1:Type, type2:Type) inline

vector_compatible_types(Type1, Type2) :-
   type(Type1),
   type(Type2),
   !vector_type(Type1),
   !vector_type(Type2).

vector_compatible_types(Type1, Type2) :-
   eq_size_vector_types(Type1, Type2).
