// http://llvm.org/docs/LangRef.html#br-instr
// keywords: terminator; instr

.type BrInstruction
  = BrCondInstruction
  | BrUncondInstruction

.type BrCondInstruction <: symbol
.type BrUncondInstruction <: symbol

.decl br_instr(instr:BrInstruction)
.decl br_instr_cond(instr:BrCondInstruction)
.decl br_instr_uncond(instr:BrUncondInstruction)


instr(v) :- br_instr(v).
terminator_instr(v) :- br_instr(v).
br_instr(v) :- br_instr_cond(v).
br_instr(v) :- br_instr_uncond(v).


//-----------------------------
// Conditional branch
//-----------------------------

.decl br_instr_condition(instr:Instruction, cond:Operand)
.decl br_instr_true_label(instr:Instruction, label:Variable)
.decl br_instr_false_label(instr:Instruction, label:Variable)


//-----------------------------
// Unconditional branch
//-----------------------------

.decl br_instr_uncond_label(instr:Instruction, label:Variable)


//------------------------------------------------------------------------------
// [Constraints]
//
//  (1) The conditional branch form of the ‘br‘ instr takes:
//      (i)  a single ‘i1‘ value and
//      (ii) two ‘label‘ values.
//
//  (2) The unconditional form of the ‘br‘ instr takes:
//      (i)  a single ‘label‘ value as a target.
//------------------------------------------------------------------------------

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   br_instr_cond(Instr),
   !br_instr_condition(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   br_instr_cond(Instr),
   br_instr_condition(Instr, Cond),
   operand_has_type(Cond, CondType),
   !int1_type(CondType).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   br_instr_cond(Instr),
   !br_instr_true_label(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   br_instr_cond(Instr),
   !br_instr_false_label(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   br_instr_cond(Instr),
   br_instr_true_label(Instr, Label),
   !variable_is_label(Label).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   br_instr_cond(Instr),
   br_instr_false_label(Instr, Label),
   !variable_is_label(Label).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   br_instr_uncond(Instr),
   !br_instr_uncond_label(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   br_instr_uncond(Instr),
   br_instr_uncond_label(Instr, Label),
   !variable_is_label(Label).
