section {* Target Language debug messages *}
theory Print
imports
  "../../Affine_Arithmetic/Executable_Euclidean_Space"
  "Optimize_Integer"
begin

text {* very ad-hoc... *}

subsection {* Printing *}

text {* Just for debugging purposes *}

definition print::"String.literal \<Rightarrow> unit" where "print x = ()"

definition int_to_string::"int \<Rightarrow> String.literal"
  where "int_to_string x = STR ''''"

context includes integer.lifting begin

lift_definition integer_to_string::"integer \<Rightarrow> String.literal"
  is int_to_string .

end

lemma [code]: "integer_to_string x = STR ''''"
  by (simp add: integer_to_string_def int_to_string_def)

lemma [code]: "int_to_string x = integer_to_string (integer_of_int x)"
  by (simp add: integer_to_string_def)

definition "println x = (let _ = print x in print (STR ''\<newline>''))"

code_printing
  constant print \<rightharpoonup> (SML) "TextIO.print"
| constant "integer_to_string :: integer \<Rightarrow> String.literal" \<rightharpoonup> (SML) "IntInf.toString"

lemma prod_case_call_mono[partial_function_mono]:
  "mono_tailrec (\<lambda>f. (let (d, e) = a in (\<lambda>y. f (c d e y))) b)"
  by (simp add: split_beta' call_mono)

partial_function (tailrec) f2f10_frac where
 "f2f10_frac c p r digits cnt e =
    (if r = 0 then (digits, cnt, 0)
    else if p = 0 then (digits, cnt, r)
    else (let
      (d, r) = divmod_int (r * 10) (power_int 2 (-e))
    in f2f10_frac (c \<or> d \<noteq> 0) (if d \<noteq> 0 \<or> c then p - 1 else p) r
      (digits * 10 + d) (cnt + 1)) e)"
declare f2f10_frac.simps[code]

text {* TODO: this is the HOL version of the SML-code in Approximation.thy *}

definition float2_float10::"int \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> int \<Rightarrow> (int * int)" where
  "float2_float10 prec rd m e = (
  let
    (m, e) = (if e < 0 then (m,e) else (m * power_int 2 e, 0));
    sgn = sgn m;
    m = abs m;

    round_down = (sgn = 1 \<and> rd) \<or> (sgn = -1 \<and> \<not> rd);

    (x, r) = divmod_int m ((power_int 2 (-e)));

    p = ((if x = 0 then prec else prec - (log2 x + 1)) * 3) div 10 + 1;

    (digits, e10, r) = if p > 0 then f2f10_frac (x \<noteq> 0) p r 0 0 e else (0,0,0);

    digits = if round_down \<or> r = 0 then digits else digits + 1

  in (sgn * (digits + x * (power_int 10 e10)), -e10))"

definition print_real::"real \<Rightarrow> unit" where "print_real x = ()"

lemma print_Floatreal[code]:
  "print_real (FloatR a b) =
    (let
      (m, e) = float2_float10 25 True a b;
      _ = print (int_to_string m);
      _ = print (STR ''e'');
      _ = print (int_to_string e)
     in
       ())"
  by simp_all

definition print_eucl::"'a::executable_euclidean_space \<Rightarrow> unit"
  where "print_eucl x =
    (let
      _ = print (STR ''('');
      _ = map (\<lambda>i. let _ = print_real (x \<bullet> i); _ = print (STR '', '') in ()) (Basis_list::'a list);
      _ = print (STR '')'')
    in ())"

definition print_eucl'::"'a::executable_euclidean_space \<Rightarrow> unit"
  where "print_eucl' x =
    (let
      _ = map (\<lambda>i. let _ = print_real (x \<bullet> i); _ = print (STR '' '') in ()) (Basis_list::'a list)
    in ())"

definition bind_err:: "String.literal \<Rightarrow> 'c option \<Rightarrow> ('c \<Rightarrow> 'd option) \<Rightarrow> 'd option"
  where [simp]: "bind_err err = Option.bind"

lemma [code]:
  "bind_err err None f = (let _ = println err in None)"
  "bind_err err (Some x) f = f x"
  by auto

fun print_segment
  where "print_segment ((x1, y1), (x2, y2)) =
  (let rs = [x1, y1, x2 - x1, y2 - y1]; _ = map (\<lambda>x. let _ = print_real x in print (STR '' '')) rs in println (STR ''''))"

definition the'::"String.literal \<Rightarrow> 'a option \<Rightarrow> 'a"
  where [simp]: "the' x = the"

lemma [code]:
   "the' err None = (let _ = println err in undefined)"
   "the' err (Some x) = x"
   apply (metis option.simps(4) option.the_def the'_def)
   by (metis option.sel the'_def)

end
