Module DebugAbMachineEnv

Require Import
  Utf8 String ToString
  AdomLib
  AbMachineEnv
  DebugLib DebugCminor.

Section S.

  Local Open Scope string_scope.

  Context {var t iter_t: Type}
          {VS: ToString var}
          {TS: ToString t}
          (verbose: bool)
          `(D: ab_machine_env var t iter_t)
          {TSI: ToString iter_t}.

  Definition string_of_mach_num_ty ty :=
    match ty with
      | MNTint => "%int"
      | MNTint64 => "%int64"
      | MNTfloat => "%float"
      | MNTsingle => "%single"
    end.

  Instance MN_ToString : ToString mach_num := fun itv =>
    match itv with
      | MNint i => to_string i ++ "%int"
      | MNint64 i => to_string i ++ "%int64"
      | MNfloat f => to_string f ++ "%float"
      | MNsingle f => to_string f ++ "%single"
    end.

  Instance MNI_ToString : ToString mach_num_itv := fun itv =>
    match itv with
      | MNIint itv => to_string itv ++ "%int"
      | MNIint64 itv => to_string itv ++ "%int64"
      | MNIfloat itv => to_string itv ++ "%float"
      | MNIsingle itv => to_string itv ++ "%single"
    end.

  Fixpoint string_of_nexpr (e: mexpr var) {struct e} : string :=
    match e with
    | MEvar ty v => to_string v ++ string_of_mach_num_ty ty
    | MEconst c => to_string c
    | MEunop op e' => string_of_unop op ++ string_of_nexpr e'
    | MEbinop op x y => "(" ++ string_of_nexpr x ++ string_of_binop op ++ string_of_nexpr y ++ ")"
    end.

  Global Instance MExprToString : ToString (mexpr var) := string_of_nexpr.

  Definition trace_get_itv e res :=
    "get_itv " ++ e ++ " → " ++ res.

  Definition trace_concretize_int e res :=
    "concretize_int " ++ e ++ " → " ++ res.

  Definition trace_assign x e (r:t+⊥) :=
    "assign " ++ x ++ " := " ++ e ++ if verbose then " → " ++ to_string r else "".

  Definition trace_forget x (r:t+⊥) :=
    "forget " ++ x ++ if verbose then " → " ++ to_string r else "".

  Definition trace_assume e b (r:t+⊥) :=
    "assume " ++ e ++ " " ++ b ++ if verbose then " → " ++ to_string r else "".

  Definition trace_noerror e r :=
    "noerror " ++ e ++ " → " ++ r.

  Program Definition debug_ab_machine_env : ab_machine_env t iter_t :=
    {| mach_leb := leb_print
    ; mach_join := join_print
    ; mach_widen := widen_print
    ; get_itv e ab :=
        let r := get_itv e ab in
        let s := trace_get_itv (to_string e) (to_string r) in
        print s r
    ; concretize_int n e ab :=
        let r := concretize_int n e ab in
        let s := trace_concretize_int (to_string e) (to_string r) in
        print s r
    ; assign x e ab :=
        let r := assign x e ab in
        let s := trace_assign (to_string x) (to_string e) r in
        print s r
    ; assume e b ab :=
        let r := assume e b ab in
        let s := trace_assume (to_string e) (to_string b) r in
        print s r
    ; forget b ab :=
        let r := forget b ab in
        let s := trace_forget (to_string b) r in
        print s r
    ; noerror e ab :=
        let r := noerror e ab in
        let s := trace_noerror (string_of_nexpr e) (to_string r) in
        print s r
    |}.

End S.