Module DebugLib

Require Import
  Utf8 String ToString AdomLib.

Parameter print_string : string → unit.
Parameter string_of_ident: AST.ident → string.

Definition print0 {A} : string → A → A*unit :=
  fun s x =>
  (x, print_string s).

Extraction NoInline print0.

Definition print {A} : string → A → A :=
  fun s x => fst (print0 s x).

Lemma print_id {A} s (x: A) : print s x = x.

Local Open Scope string_scope.

Definition print_leb (x y: string) (r: bool) : string :=
  x ++ " ⊑ " ++ y ++ " → " ++ (if r then "tt" else "ff").

Definition print_join (x y z: string) : string :=
  x ++ " ⊔ " ++ y ++ " → " ++ z.

Definition print_meet (x y z: string) : string :=
  x ++ " ⊔ " ++ y ++ " → " ++ z.

Definition print_widen (x y z: string) : string :=
  x ++ " ∇ " ++ y ++ " → " ++ z.

Definition leb_print {A} {L:leb_op A} {TS:ToString A} : leb_op A := fun x y =>
  let r := x ⊑ y in
  let s := print_leb (to_string x) (to_string y) r in
  print s r.

Definition join_print {A B} {J:join_op A B} {TSA:ToString A} {TSB:ToString B} : join_op A B := fun x y =>
  let r := x ⊔ y in
  let s := print_join (to_string x) (to_string y) (to_string r) in
  print s r.

Definition meet_print {A B} {M:meet_op A B} {TSA:ToString A} {TSB:ToString B} : meet_op A B := fun x y =>
  let r := x ⊓ y in
  let s := print_meet (to_string x) (to_string y) (to_string r) in
  print s r.

Definition widen_print {A B} {W:widen_op A B}
           {TSA:ToString A} {TSB:ToString B} : widen_op A B :=
  {| init_iter := init_iter;
     widen x y :=
       let r := widen x y in
       let s := print_widen (to_string x) (to_string y) (to_string r) in
       print s r |}.

Instance leb_print_correct A B (L:leb_op A) (G:gamma_op A B) (TS:ToString A) :
  leb_op_correct A B -> leb_op_correct A B (L:=leb_print).

Instance join_print_correct A B C (L:join_op A B) (GA:gamma_op A C) (GB:gamma_op B C)
         (TSA:ToString A) (TSB:ToString B):
  join_op_correct A B C -> join_op_correct A B C (J:=join_print).

Instance meet_print_correct A B C (L:meet_op A B) (GA:gamma_op A C) (GB:gamma_op B C)
         (TSA:ToString A) (TSB:ToString B):
  meet_op_correct A B C -> meet_op_correct A B C (J:=meet_print).

Instance widen_print_correct A B C (W:widen_op A B) (GA:gamma_op A C) (GB:gamma_op B C)
         (TSA:ToString A) (TSB:ToString B):
  widen_op_correct A B C -> widen_op_correct A B C (W:=widen_print).