Module DebugCminor

Require Import
  Utf8 String Coqlib ToString
  Integers FloatLib AST Cminor DebugLib.

Local Open Scope string_scope.

Definition string_of_unop (op: unary_operation) : string :=
  match op with
  | Ocast8unsigned => "(uint8)"
  | Ocast8signed => "(int8)"
  | Ocast16unsigned => "(uint16)"
  | Ocast16signed => "(int16)"
  | Onegint | Onegf | Onegfs | Onegl => "-"
  | Onotint | Onotl => "¬"
  | Oabsf | Oabsfs => "absf"
  | Olongofint | Olongofintu
  | Olongofsingle | Olonguofsingle
  | Olongoffloat | Olonguoffloat => "(long)"
  | Ofloatoflong | Ofloatoflongu
  | Ofloatofint | Ofloatofintu | Ofloatofsingle => "(double)"
  | Osingleoffloat | Osingleofint | Osingleofintu
  | Osingleoflong | Osingleoflongu => "(single)"
  | Ointoffloat | Ointofsingle | Ointuofsingle | Ointoflong => "(int)"
  | Ointuoffloat => "(intu)"
  end.

Instance UnopToString : ToString unary_operation := string_of_unop.

Definition string_of_comparison (cmp: comparison) : string :=
  match cmp with
  | Ceq => " = "
  | Cne => " ≠ "
  | Clt => " < "
  | Cle => " ≤ "
  | Cge => " ≥ "
  | Cgt => " > "
  end.

Instance ComparisonToString : ToString comparison := string_of_comparison.

Definition string_of_binop (op: binary_operation) : string :=
  match op with
  | Oadd | Oaddf | Oaddfs | Oaddl => " + "
  | Osub | Osubf | Osubfs | Osubl => " − "
  | Omul | Omulf | Omulfs | Omull=> " × "
  | Odiv | Odivu | Odivl | Odivlu | Odivf | Odivfs => " ÷ "
  | Omod | Omodu | Omodl | Omodlu => " % "
  | Oand | Oandl => " & "
  | Oor | Oorl => " | "
  | Oxor | Oxorl => " ^ "
  | Oshl | Oshll => " << "
  | Oshr | Oshrl => " >> "
  | Oshru | Oshrlu => " >>u "
  | Ocmp c | Ocmpl c | Ocmpf c | Ocmpfs c => string_of_comparison c
  | Ocmpu c | Ocmplu c => string_of_comparison c ++ "ᵤ "
  end.

Instance BinopToString : ToString binary_operation := string_of_binop.

Definition string_of_chunk (κ: memory_chunk) : string :=
  match κ with
  | Mint8signed => "Mint8signed"
  | Mint8unsigned => "Mint8unsigned"
  | Mint16signed => "Mint16signed"
  | Mint16unsigned => "Mint16unsigned"
  | Mint32 => "Mint32"
  | Mint64 => "Mint64"
  | Mfloat32 => "Mfloat32"
  | Mfloat64 => "Mfloat64"
  | Many32 => "Many32"
  | Many64 => "Many64"
  end.

Instance MemChunkToString : ToString memory_chunk := string_of_chunk.

Definition string_of_const (c: constant) : string :=
  match c with
  | Ointconst i => to_string i
  | Olongconst l => to_string l
  | Ofloatconst f => to_string f
  | Osingleconst f => to_string f
  | Oaddrsymbol s o => "&" ++ to_string s ++ " + " ++ to_string o
  | Oaddrstack o => "stk+" ++ to_string o
  end.

Instance ConstantToString : ToString constant := string_of_const.

Fixpoint string_of_expr (e: expr) : string :=
  match e with
  | Evar i => string_of_ident i
  | Econst c => to_string c
  | Eunop op l => string_of_unop op ++ string_of_expr l
  | Ebinop op l r => "(" ++ string_of_expr l ++ string_of_binop op ++ string_of_expr r ++ ")"
  | Eload alpha κ e => "[" ++ string_of_expr e ++ ", " ++ to_string κ ++ "]"
  end.

Instance ExprToString : ToString expr := string_of_expr.