include "basics/logic.ma".

include "common/AST.ma".
include "common/CostLabel.ma".
include "common/FrontEndOps.ma".
include "common/Registers.ma".

include "ASM/Vector.ma".
include "common/Graphs.ma".

inductive statement : Type[0] ≝
| St_skip : label → statement
| St_cost : costlabel → label → statement
| St_const : register → constant → label → statement
| St_op1 : unary_operation → register → register → label → statement (* destination source *)
| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
| St_load : memory_chunk → register → register → label → statement
| St_store : memory_chunk → register → register → label → statement
| St_call_id : ident → list register → option register → label → statement
| St_call_ptr : register → list register → option register → label → statement
| St_tailcall_id : ident → list register → statement
| St_tailcall_ptr : register → list register → statement
| St_cond : register → label → label → statement
| St_jumptable : register → list label → statement
| St_return : statement
.

record internal_function : Type[0] ≝
{ f_labgen    : universe LabelTag
; f_reggen    : universe RegisterTag
; f_result    : option (register × typ)
; f_params    : list (register × typ)
; f_locals    : list (register × typ)
; f_stacksize : nat
; f_graph     : graph statement
; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
}.

(* Note that the global variables will be initialised by the code in main
   by this stage, so the only initialisation data is the amount of space to
   allocate. *)

definition RTLabs_program ≝ program (fundef internal_function) nat.