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

.type RetInstruction <: symbol
.decl ret_instr(instr:RetInstruction)

instr(v) :- ret_instr(v).
terminator_instr(v) :- ret_instr(v).

// The ‘ret‘ instr optionally accepts a single
// argument, the return value.

.decl ret_instr_operand(instr:RetInstruction, val:Operand)
.decl ret_instr_void_(instr:RetInstruction)

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   ret_instr_void_(Instr),
   ret_instr_operand(Instr, _).


//------------------------------------------------------------------------------
// [Well Formed Functions]
//
// A func is not well formed if:
//  (i)   it it has a non-void return type and contains a ‘ret‘
//        instr with no return value or
//
//  (ii)  a return value with a type that does not match its type, or
//
//  (iii) if it has a void return type and contains a ‘ret‘
//        instr with a return value.
//------------------------------------------------------------------------------

.decl func_is_wellformed(func:Function)
.decl func_is_illformed(func:Function)

func_is_wellformed(Func):-
   func(Func),
   !func_is_illformed(Func).

func_is_illformed(Func) :-
   ret_instr_void_(Instr),
   instr_func(Instr, Func),
   func_ty(Func, FuncType),
   func_type_return(FuncType, RetType),
   !void_type(RetType).

func_is_illformed(Func) :-
   ret_instr_operand(Instr, Value),
   instr_func(Instr, Func),
   func_ty(Func, FuncType),
   func_type_return(FuncType, RetType),
   !void_type(RetType),
   !operand_has_type(Value, RetType).

func_is_illformed(Func) :-
   ret_instr(Instr),
   !ret_instr_void_(Instr),
   instr_func(Instr, Func),
   func_ty(Func, FuncType),
   func_type_return(FuncType, RetType),
   void_type(RetType).


//------------------------------------------------------------------------------
// [Constraints]
//
//  (i) The type of the return value must be a ‘first class‘ type.
//------------------------------------------------------------------------------

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   ret_instr_operand(Instr, Value),
   !operand_is_firstclass(Value).
