Require Import tactics2.
Require Import Ascii String.


Definition print_endline : string -> unit := fun _ => tt.

Definition CR : string := String (ascii_of_nat 13) "".

Fixpoint str_concat (l : list String.string) : String.string :=
  match l with
  | [] => ""
  | s :: ss => String.append s (str_concat ss)
  end.

Definition bool2string (b : bool) : string :=
  match b with
  | true => "true"
  | false => "false"
  end.

Definition nat2string_aux (n : nat) : string :=
  match n with
  | 0  => "0"
  | 1  => "1"
  | 2  => "2"
  | 3  => "3"
  | 4  => "4"
  | 5  => "5"
  | 6  => "6"
  | 7  => "7"
  | 8  => "8"
  | 9  => "9"
  | _  => "-"
  end.

Lemma nat2string : nat -> string.
Proof.
  apply comp_ind_type; introv ind.
  destruct n.
  { exact "0". }
  remember (Nat.modulo (S n) 10) as md.
  remember (Nat.div (S n) 10) as dv.
  pose proof (Nat.div_lt (S n) 10) as h.
  repeat (autodimp h hyp); auto.
  { apply Nat.lt_0_succ. }
  { repeat apply lt_n_S; apply Nat.lt_0_succ. }
  pose proof (ind (S n / 10) h) as x.
  exact (String.append x (nat2string_aux md)).
Defined.

Definition op2string {T} (f : T -> string) (o : option T) : string :=
  match o with
  | Some t => str_concat ["Some(", f t, ")"]
  | None => "None"
  end.
