Module DebugAbIdealNonrel


Require Import
  Utf8 String ToString
  AdomLib
  IdealExpr AbIdealNonrel
  DebugLib DebugCminor.

Set Implicit Arguments.
Local Open Scope string_scope.

Definition string_of_i_binary_operation (op: i_binary_operation) : string :=
  match op with
  | IOadd => " + "
  | IOsub => " − "
  | IOmul => " × "
  | IOdiv => " ÷ "
  | IOmod => " % "
  | IOand => " & "
  | IOor => " | "
  | IOxor => " ^ "
  | IOshl => " << "
  | IOshr => " >> "
  | IOaddf => " +. "
  | IOsubf => " −. "
  | IOmulf => " ×. "
  | IOdivf => " ÷. "
  | IOcmp cmp
  | IOcmpf cmp => string_of_comparison cmp
  end.

Definition string_of_i_unary_operation (op: i_unary_operation) : string :=
  match op with
    | IOneg => "-"
    | IOnot => "¬"
    | IOnegf => "-."
    | IOabsf => "absf "
    | IOsingleofz
    | IOsingleoffloat => "(single) "
    | IOfloatofz => "(float) "
    | IOzoffloat => "(Z) "
  end.

Instance i_binary_operation_to_string : ToString i_binary_operation := string_of_i_binary_operation.
Instance i_unary_operation_to_string : ToString i_unary_operation := string_of_i_unary_operation.

Definition print_i_unop (op: i_unary_operation) (x y: string) : string :=
  to_string op ++ x ++ " → " ++ y.

Definition print_i_binop (op: i_binary_operation) (x y z: string) : string :=
  x ++ to_string op ++ y ++ " → " ++ z.

Definition print_backward_i_unop (op: i_unary_operation) (x y x': string) : string :=
  to_string op ++ x ++ " = " ++ y ++ " → " ++ x'.

Definition print_backward_i_binop (op: i_binary_operation) (x y z x'y': string) : string :=
  x ++ to_string op ++ y ++ " = " ++ z ++ " → " ++ x'y'.

Section S.

Context {t: Type} (dom: ab_ideal_nonrel t)
        `(dom_correct: ab_ideal_nonrel_correct t)
        `{ToString t}.

Definition debug_ab_ideal_nonrel : ab_ideal_nonrel t :=
  {| as_leb := leb_print
  ; as_join := join_print
  ; as_meet := meet_print
  ; widen := widen
  ; const := const
  ; z_itv := z_itv
  ; forward_unop op x :=
      let r := forward_unop op x in
      let s := print_i_unop op (to_string x) (to_string r) in
      print s r
  ; forward_binop op x y :=
      let r := forward_binop op x y in
      let s := print_i_binop op (to_string x) (to_string y) (to_string r) in
      print s r
  ; backward_unop op res x :=
      let r := backward_unop op res x in
      let s := print_backward_i_unop op (to_string x) (to_string res) (to_string r) in
      print s r
  ; backward_binop op res x y :=
      let r := backward_binop op res x y in
      let s := print_backward_i_binop op (to_string x) (to_string y) (to_string res) (to_string r) in
      print s r
  ; enrich_query_chan := enrich_query_chan
  ; forward_var := forward_var
  ; backward_var := backward_var
  ; process_msg := process_msg
  ; assign_msgs := assign_msgs
  ; assume_msgs := assume_msgs
  |}.

Instance debug_ab_ideal_nonrel_correct : ab_ideal_nonrel_correct debug_ab_ideal_nonrel _.
Proof.
  destruct dom_correct. split; try assumption.
Qed.

End S.