include "ASM/I8051.ma".
include "LIN/JointLTLLIN.ma".
include "utilities/BitVectorTrieSet.ma".
include "utilities/IdentifierTools.ma".
include "common/Graphs.ma".
include "common/CostLabel.ma".
include "common/Registers.ma".

definition registers ≝ list register.

inductive move_registers: Type[0] ≝
  | pseudo: register → move_registers
  | hardware: Register → move_registers.

definition pre_ertl_statement ≝
  joint_statement label register register register register
                  (move_registers × move_registers) register.
                  
inductive ertl_statement (globals: list ident): Type[0] ≝
  | ertl_st_lift_pre: pre_ertl_statement globals → ertl_statement globals
  | ertl_st_new_frame: label → ertl_statement globals
  | ertl_st_del_frame: label → ertl_statement globals
  | ertl_st_frame_size: register → label → ertl_statement globals.

(*
inductive ertl_statement: Type[0] ≝
  | ertl_st_skip: label → ertl_statement
  | ertl_st_comment: String → label → ertl_statement
  | ertl_st_cost: costlabel → label → ertl_statement
  | ertl_st_get_hdw: register → Register → label → ertl_statement
  | ertl_st_set_hdw: Register → register → label → ertl_statement
  | ertl_st_hdw_to_hdw: Register → Register → label → ertl_statement
  | ertl_st_new_frame: label → ertl_statement
  | ertl_st_del_frame: label → ertl_statement
  | ertl_st_frame_size: register → label → ertl_statement
  | ertl_st_pop: register → label → ertl_statement
  | ertl_st_push: register → label → ertl_statement
  | ertl_st_addr: register → register → ident → label → ertl_statement
  | ertl_st_int: register → Byte → label → ertl_statement
  | ertl_st_move: register → register → label → ertl_statement
  | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
  | ertl_st_op1: Op1 → register → register → label → ertl_statement
  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
  | ertl_st_clear_carry: label → ertl_statement
  | ertl_st_set_carry: label → ertl_statement
  | ertl_st_load: register → register → register → label → ertl_statement
  | ertl_st_store: register → register → register → label → ertl_statement
  | ertl_st_call_id: ident → nat → label → ertl_statement
  | ertl_st_cond: register → label → label → ertl_statement
  | ertl_st_return: ertl_statement.
*)

definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).

record ertl_internal_function (globals: list ident): Type[0] ≝
{
  ertl_if_luniverse: universe LabelTag;
  ertl_if_runiverse: universe RegisterTag;
  ertl_if_params: nat;
  ertl_if_locals: registers;
  ertl_if_stacksize: nat;
  ertl_if_graph: ertl_statement_graph globals;
  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
}.

definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
  
record ertl_program (globals: list ident): Type[0] ≝
{
  ertl_pr_vars: list (ident × nat);
  ertl_pr_funcs: list (ident × (ertl_function globals));
  ertl_pr_main: option ident
}.


(* XXX: changed from O'Caml
  | ertl_st_addr_h: register → ident → label → ertl_statement
  | ertl_st_addr_l: register → ident → label → ertl_statement
*)

(* XXX: changed from O'Caml
  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
*)