Module DebugCshm

Require Import Csharpminorannot DebugLib DebugCminor.
Import String.
Import ToString.

Local Open Scope string_scope.

Definition string_of_const (c: constant) : string :=
  match c with
  | Ointconst i => to_string i
  | Olongconst i => to_string i
  | Ofloatconst f => to_string f
  | Osingleconst f => to_string f
  end.

Instance ConstantToString : ToString constant := string_of_const.

Fixpoint string_of_expr (e: expr) : string :=
  match e with
  | Evar i => "var " ++ string_of_ident i
  | Eaddrof i => "&" ++ string_of_ident i
  | Econst c => to_string c
  | Eunop op e => to_string op ++ string_of_expr e
  | Ebinop op e e' => "(" ++ string_of_expr e ++ to_string op ++ string_of_expr e' ++ ")"
  | Eload _ κ e => to_string κ ++ "[" ++ string_of_expr e ++ "]"
  end.

Instance ExprToString : ToString expr := string_of_expr.