// http://llvm.org/docs/LangRef.html#fcmp-instr
// keywords: comparison; binary; instr

.type FCmpInstruction <: symbol
.decl fcmp_instr(instr:FCmpInstruction)

instr(v) :- fcmp_instr(v).

.type FCmpCondition <: symbol

.decl fcmp_instr_condition(instr:FCmpInstruction, cond:FCmpCondition)
.decl fcmp_instr_first_operand(instr:FCmpInstruction, op:Operand)
.decl fcmp_instr_second_operand(instr:FCmpInstruction, op:Operand)


//------------------------------------------------------------------------------
// [Condition Codes]
//
// Condition Code enum representation for the ‘fcmp‘ instr, and
// its selectors.
//------------------------------------------------------------------------------

.decl fcmp_condition(cond:FCmpCondition)
fcmp_condition(Cond) :- fcmp_instr_condition(_, Cond).

.decl fcmp_condition__false(cond:FCmpCondition)
.decl fcmp_condition__true(cond:FCmpCondition)
.decl fcmp_condition__oeq(cond:FCmpCondition)
.decl fcmp_condition__ogt(cond:FCmpCondition)
.decl fcmp_condition__oge(cond:FCmpCondition)
.decl fcmp_condition__olt(cond:FCmpCondition)
.decl fcmp_condition__ole(cond:FCmpCondition)
.decl fcmp_condition__one(cond:FCmpCondition)
.decl fcmp_condition__ord(cond:FCmpCondition)
.decl fcmp_condition__ueq(cond:FCmpCondition)
.decl fcmp_condition__ugt(cond:FCmpCondition)
.decl fcmp_condition__uge(cond:FCmpCondition)
.decl fcmp_condition__ult(cond:FCmpCondition)
.decl fcmp_condition__ule(cond:FCmpCondition)
.decl fcmp_condition__une(cond:FCmpCondition)
.decl fcmp_condition__uno(cond:FCmpCondition)

fcmp_condition__false("false") :- fcmp_condition("false").
fcmp_condition__true("true") :- fcmp_condition("true").
fcmp_condition__oeq("oeq") :- fcmp_condition("oeq").
fcmp_condition__ogt("ogt") :- fcmp_condition("ogt").
fcmp_condition__oge("oge") :- fcmp_condition("oge").
fcmp_condition__olt("olt") :- fcmp_condition("olt").
fcmp_condition__ole("ole") :- fcmp_condition("ole").
fcmp_condition__one("one") :- fcmp_condition("one").
fcmp_condition__ord("ord") :- fcmp_condition("ord").
fcmp_condition__ueq("ueq") :- fcmp_condition("ueq").
fcmp_condition__ugt("ugt") :- fcmp_condition("ugt").
fcmp_condition__uge("uge") :- fcmp_condition("uge").
fcmp_condition__ult("ult") :- fcmp_condition("ult").
fcmp_condition__ule("ule") :- fcmp_condition("ule").
fcmp_condition__une("une") :- fcmp_condition("une").
fcmp_condition__uno("uno") :- fcmp_condition("uno").

// the enum enforcement by constraint
schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(), fcmp_instr_condition(Instr, Cond),
   !fcmp_condition__false(Cond), !fcmp_condition__true(Cond),
   !fcmp_condition__oeq(Cond),   !fcmp_condition__ogt(Cond),
   !fcmp_condition__oge(Cond),   !fcmp_condition__olt(Cond),
   !fcmp_condition__ole(Cond),   !fcmp_condition__one(Cond),
   !fcmp_condition__ord(Cond),   !fcmp_condition__ueq(Cond),
   !fcmp_condition__ugt(Cond),   !fcmp_condition__uge(Cond),
   !fcmp_condition__ult(Cond),   !fcmp_condition__ule(Cond),
   !fcmp_condition__une(Cond),   !fcmp_condition__uno(Cond).


// Helper predicates

.decl fcmp_instr_from_type(instr:FCmpInstruction, type:Type)
.decl fcmp_instr_to_type(instr:FCmpInstruction, type:Type)

fcmp_instr_from_type(Instr, Type) :-
   fcmp_instr_first_operand(Instr, Operand),
   operand_has_type(Operand, Type).

fcmp_instr_to_type(Instr, Type) :-
   fcmp_instr(Instr),
   instr_returns_type(Instr, Type).


//-------------------------------------------------------------------
// [Constraints]
//
// 1) The ‘fcmp‘ instr returns:
//      (i)  a boolean value or
//      (ii) a vector of boolean values
//
//    based on comparison of its two:
//      (i)  floating point or
//      (ii) floating point vector operands.
//
// 2) They must also be identical types.
//
// 3) If the operands are floating point vectors
//      (i)  the result type is a boolean vector
//      (ii) with the same number of elements.
//-------------------------------------------------------------------

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   fcmp_instr(Instr),
   !fcmp_instr_first_operand(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   fcmp_instr(Instr),
   !fcmp_instr_second_operand(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   fcmp_instr(Instr),
   !fcmp_instr_condition(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   fcmp_instr_to_type(Instr, Type),
   !boolean_type(Type),
   !boolean_vector_type(Type).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   fcmp_instr_from_type(Instr, Type),
   !fp_type(Type),
   !fp_vector_type(Type).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   fcmp_instr(Instr),
   fcmp_instr_first_operand(Instr, LeftOp),
   fcmp_instr_second_operand(Instr, RightOp),
   operand_has_type(LeftOp, LeftType),
   operand_has_type(RightOp, RightType),
   LeftType != RightType.

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   fcmp_instr_from_type(Instr, FromType),
   fcmp_instr_to_type(Instr, ToType),
   !vector_compatible_types(FromType, ToType).
