include "ASM/I8051.ma".
include "utilities/BitVectorTrieSet.ma".
include "utilities/IdentifierTools.ma".
include "common/Graphs.ma".

definition Registers ≝ list Register.

definition AbstractRegister ≝ nat.

inductive ERTLStatement: Type[0] ≝
  | ERTL_St_Skip: Identifier → ERTLStatement
  | ERTL_St_Comment: String → Identifier → ERTLStatement
  | ERTL_St_Cost: Identifier → Identifier → ERTLStatement
  | ERTL_St_Get_Hdw: Register → AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_Set_Hdw: AbstractRegister → Register → Identifier → ERTLStatement
  | ERTL_St_Hdw_To_Hdw: Register → Register → Identifier → ERTLStatement
  | ERTL_St_NewFrame: Identifier → ERTLStatement
  | ERTL_St_DelFrame: Identifier → ERTLStatement
  | ERTL_St_FrameSize: AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_Pop: AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_Push: AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_AddrH: AbstractRegister → Identifier → Identifier → ERTLStatement
  | ERTL_St_AddrL: AbstractRegister → Identifier → Identifier → ERTLStatement
  | ERTL_St_Int: AbstractRegister → Byte → Identifier → ERTLStatement
  | ERTL_St_Move: AbstractRegister → AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_Opaccs: OpAccs → AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_Op1: Op1 → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_Op2: Op2 → AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_ClearCarry: Identifier → ERTLStatement
  | ERTL_St_Load: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_Store: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
  | ERTL_St_Call_Id: Identifier → Byte → Identifier → ERTLStatement.

definition ERTLStatementGraph ≝ graph ERTLStatement.

record ERTLInternalFunction: Type[0] ≝
{
  ERTL_IF_LUniverse: Universe;
  ERTL_IF_RUniverse: Universe;
  ERTL_IF_Params: Byte;
  ERTL_IF_Locals: BitVectorTrieSet 16;
  ERTL_IF_Graph: ERTLStatementGraph;
  ERTL_IF_Entry: Identifier;
  ERTL_IF_Exit: Identifier
}.

inductive ERTLFunction: Type[0] ≝
  | ERTL_Fu_Internal: ERTLInternalFunction → ERTLFunction
  | ERTL_Fu_External: ExternalFunction → ERTLFunction.
  
record ERTLProgram: Type[0] ≝
{
  ERTL_Pr_Vars: list (Identifier × nat);
  ERTL_Pr_Funcs: list (Identifier × ERTLFunction);
  ERTL_Pr_Main: option Identifier
}.