include "basics/list.ma".
include "common/Registers.ma".
include "common/AST.ma".
include "common/Graphs.ma".
include "common/CostLabel.ma".

definition registers ≝ list register.

inductive rtl_statement: Type[0] ≝
  | rtl_st_skip: label → rtl_statement
  | rtl_st_cost: costlabel → label → rtl_statement
  | rtl_st_addr: register → register → ident → label → rtl_statement
  | rtl_st_stack_addr: register → register → label → rtl_statement
  | rtl_st_int: register → Byte → label → rtl_statement
  | rtl_st_move: register → register → label → rtl_statement
  | rtl_st_clear_carry: label → rtl_statement
  | rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement
  | rtl_st_op1: Op1 → register → register → label → rtl_statement
  | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
  | rtl_st_load: register → register → register → label → rtl_statement
  | rtl_st_store: register → register → register → label → rtl_statement
  | rtl_st_call_id: ident → registers → registers → label → rtl_statement
  | rtl_st_call_ptr: register → register → registers → registers → label → rtl_statement
  | rtl_st_tailcall_id: ident → registers → rtl_statement
  | rtl_st_tailcall_ptr: register → register → registers → rtl_statement
  | rtl_st_cond: register → label → label → rtl_statement
  | rtl_st_set_carry: label → rtl_statement
  | rtl_st_return: label → rtl_statement.
  
definition rtl_statement_graph ≝ graph rtl_statement.

record rtl_internal_function: Type[0] ≝
{
  rtl_if_luniverse: universe LabelTag;
  rtl_if_runiverse: universe RegisterTag;
(*  rtl_if_sig: signature;  -- dropped in front end *)
  rtl_if_result   : registers;
  rtl_if_params   : registers;
  rtl_if_locals   : registers;
  rtl_if_stacksize: nat;
  rtl_if_graph    : rtl_statement_graph;
  rtl_if_entry    : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?;
  rtl_if_exit     : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?
}.

definition rtl_function_definition ≝ fundef rtl_internal_function.
  
record rtl_program: Type[0] ≝
{
  rtl_pr_vars: list (ident × nat);
  rtl_pr_functs: list (ident × rtl_function_definition);
  rtl_pr_main: option ident
}.