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.  All initialisation data should only reserve space. *)

definition RTLabs_program ≝ program (fundef internal_function) unit.

(* TO CONSIDER:

   - removing most successor labels from the statements (bit icky, what about
     return and jump tables?)
   - seems like load and store ought to have types that control the size of the
     register list based on the addressing mode; similarly, memory_chunk and
     register are probably related.
   - label and register generation really tell us something about the sets of
     labels and register that may appear, perhaps it should be renamed, or the
     graph made dependent on them to make it obvious, etc.
 *)