include "arithmetics/nat.ma".

include "cerco/String.ma".
include "cerco/BitVector.ma".
include "cerco-intermediate-languages/utilities/Compare.ma".
include "cerco-intermediate-languages/common/CostLabel.ma".

definition Identifier ≝ Byte.
definition Immediate ≝ nat.

inductive Compare: Type[0] ≝
  Compare_Equal: Compare
| Compare_Less: Compare
| Compare_Greater: Compare
| Compare_LessEqual: Compare
| Compare_GreaterEqual: Compare.

inductive Cast: Type[0] ≝
  Cast_Int: Byte → Cast
| Cast_AddrSymbol: Identifier → Cast
| Cast_StackOffset: Immediate → Cast.

inductive Op1: Type[0] ≝
  Op1_Cast8U: Op1
| Op1_Cast8S: Op1
| Op1_Cast16U: Op1
| Op1_Cast16S: Op1
| Op1_NegInt: Op1
| Op1_NotBool: Op1
| Op1_NotInt: Op1
(*
| Op1_NegFloat: Op1
| Op1_AbsFloat: Op1
| Op1_SingleOfFloat: Op1
| Op1_IntOfFloat: Op1
| Op1_IntUOfFloat: Op1
| Op1_FloatOfInt: Op1
| Op1_FloatOfIntU: Op1
*)
| Op1_Id: Op1
| Op1_PtrOfInt: Op1
| Op1_IntOfPtr: Op1.

inductive Op2: Type[0] ≝
  Op2_Add: Op2
| Op2_Sub: Op2
| Op2_Mul: Op2
| Op2_Div: Op2
| Op2_DivU: Op2
| Op2_Mod: Op2
| Op2_ModU: Op2
| Op2_And: Op2
| Op2_Or: Op2
| Op2_XOr: Op2
| Op2_ShL: Op2
| Op2_ShR: Op2
| Op2_ShRU: Op2
(*
| Op2_AddF: Op2
| Op2_SubF: Op2
| Op2_MulF: Op2
| Op2_DivF: Op2
*)
| Op2_Cmp: Compare → Op2
| Op2_CmpU: Compare → Op2
(*
| Op2_CmpF: Compare → Op2
*)
| Op2_AddP: Op2
| Op2_SubP: Op2
| Op2_CmpP: Compare → Op2.

inductive Data: Type[0] ≝
  Data_Reserve: nat → Data
| Data_Int8: Byte → Data
| Data_Int16: Word → Data.

inductive DataSize: Type[0] ≝
  DataSize_Byte: DataSize
| DataSize_HalfWord: DataSize
| DataSize_Word: DataSize.

inductive SigType: Type[0] ≝
  SigType_Int: SigType
(*
| SigType_Float: SigType
*)
| SigType_Ptr: SigType.

inductive TypeReturn: Type[0] ≝
  TypeReturn_Ret: SigType → TypeReturn
| TypeReturn_Void: TypeReturn.

record Signature: Type[0] ≝
{
  signature_args: list SigType;
  signature_return: TypeReturn
}.

record ExternalFunction: Type[0] ≝
{
  external_function_tag: Identifier;
  external_function_sig: Signature
}.

definition Trace ≝ list CostLabel.